two more

maXXusXYZ · Sep 25, 2022 · 6e473f1 · 6e473f1
1 parent 3cf06ae
commit 6e473f1
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 6 deletions.
diff --git a/src/Lbar/ses.lean b/src/Lbar/ses.lean
@@ -106,11 +106,11 @@ the corresponding power series `Fₛ : ℤ[[T]][T⁻¹]`. -/
         simpa },
       /- setup equiv with `ℕ` using `k → -k` and use `F.nnreal_summable s` -/ },
     { convert summable_zero, ext ⟨((_|n)|n), hn⟩,
-      { simp only [int.of_nat_eq_coe, int.coe_nat_zero, set.mem_compl_eq, set.mem_set_of_eq,
-         le_refl, not_true] at hn,
+      { simp only [int.of_nat_eq_coe, int.coe_nat_zero, le_refl, not_true, set.mem_compl_iff,
+          set.mem_set_of_eq] at hn,
         exact hn.elim },
       { erw [nnnorm_zero, zero_mul, nnreal.coe_zero], },
-      { simp only [set.mem_compl_eq, set.mem_set_of_eq, not_le, int.neg_succ_not_pos] at hn,
+      { simp only [not_le, int.neg_succ_not_pos, set.mem_compl_iff, set.mem_set_of_eq] at hn,
         exact hn.elim }, },
   end }
 
@@ -490,7 +490,7 @@ begin
   { intro S, ext F s (_|n); refl, },
   { rintro S c F ⟨hF1, hF2⟩,
     simp only [whisker_right_app, laurent_measures.to_Lbar_nat_trans_app, functor.comp_map,
-      set.mem_inter_eq, set.mem_preimage, set.mem_singleton_iff] at hF1 hF2,
+      set.mem_preimage, set.mem_singleton_iff] at hF1 hF2,
     change laurent_measures.to_Lbar r' S F = 0 at hF1,
     change F ∈ pseudo_normed_group.filtration (laurent_measures r' S) c at hF2,
     show F ∈ invpoly.to_laurent_measures r' S ''

diff --git a/src/for_mathlib/single_coproducts.lean b/src/for_mathlib/single_coproducts.lean
@@ -193,8 +193,6 @@ end
 
 variables [enough_projectives A]
 
-instance Ab_op_has_colimits : has_colimits Abᵒᵖ := has_colimits_op_of_has_limits
-
 noncomputable
 instance preserves_coproducts_Ext' {α : Type v} (i : ℤ) (Y : A) [AB4 A] :
   preserves_colimits_of_shape (discrete α)