Merge remote-tracking branch 'origin/master' into nightly-testing

Mathlib/Algebra/Group/Submonoid/Basic.lean

@@ -65,14 +65,14 @@ variable [MulOneClass M] {s : Set M}
 variable [AddZeroClass A] {t : Set A}
 
 /-- `OneMemClass S M` says `S` is a type of subsets `s ≤ M`, such that `1 ∈ s` for all `s`. -/
-class OneMemClass (S : Type*) (M : Type*) [One M] [SetLike S M] : Prop where
+class OneMemClass (S : Type*) (M : outParam Type*) [One M] [SetLike S M] : Prop where
   /-- By definition, if we have `OneMemClass S M`, we have `1 ∈ s` for all `s : S`. -/
   one_mem : ∀ s : S, (1 : M) ∈ s
 
 export OneMemClass (one_mem)
 
 /-- `ZeroMemClass S M` says `S` is a type of subsets `s ≤ M`, such that `0 ∈ s` for all `s`. -/
-class ZeroMemClass (S : Type*) (M : Type*) [Zero M] [SetLike S M] : Prop where
+class ZeroMemClass (S : Type*) (M : outParam Type*) [Zero M] [SetLike S M] : Prop where
   /-- By definition, if we have `ZeroMemClass S M`, we have `0 ∈ s` for all `s : S`. -/
   zero_mem : ∀ s : S, (0 : M) ∈ s
 
@@ -96,7 +96,7 @@ add_decl_doc Submonoid.toSubsemigroup
 
 /-- `SubmonoidClass S M` says `S` is a type of subsets `s ≤ M` that contain `1`
 and are closed under `(*)` -/
-class SubmonoidClass (S : Type*) (M : Type*) [MulOneClass M] [SetLike S M] extends
+class SubmonoidClass (S : Type*) (M : outParam Type*) [MulOneClass M] [SetLike S M] extends
   MulMemClass S M, OneMemClass S M : Prop
 
 section
@@ -115,7 +115,7 @@ add_decl_doc AddSubmonoid.toAddSubsemigroup
 
 /-- `AddSubmonoidClass S M` says `S` is a type of subsets `s ≤ M` that contain `0`
 and are closed under `(+)` -/
-class AddSubmonoidClass (S : Type*) (M : Type*) [AddZeroClass M] [SetLike S M] extends
+class AddSubmonoidClass (S : Type*) (M : outParam Type*) [AddZeroClass M] [SetLike S M] extends
   AddMemClass S M, ZeroMemClass S M : Prop
 
 attribute [to_additive] Submonoid SubmonoidClass

Mathlib/Algebra/Group/Subsemigroup/Basic.lean

@@ -57,14 +57,14 @@ variable [Mul M] {s : Set M}
 variable [Add A] {t : Set A}
 
 /-- `MulMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(*)` -/
-class MulMemClass (S : Type*) (M : Type*) [Mul M] [SetLike S M] : Prop where
+class MulMemClass (S : Type*) (M : outParam Type*) [Mul M] [SetLike S M] : Prop where
   /-- A substructure satisfying `MulMemClass` is closed under multiplication. -/
   mul_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
 
 export MulMemClass (mul_mem)
 
 /-- `AddMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(+)` -/
-class AddMemClass (S : Type*) (M : Type*) [Add M] [SetLike S M] : Prop where
+class AddMemClass (S : Type*) (M : outParam Type*) [Add M] [SetLike S M] : Prop where
   /-- A substructure satisfying `AddMemClass` is closed under addition. -/
   add_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a + b ∈ s
 

Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean

@@ -61,7 +61,7 @@ noncomputable def hom :
     (descCochain _ 0 (Cochain.ofHom (inr (f ≫ g))) (neg_add_cancel 1)) (by
       ext p _ rfl
       simp [mappingConeCompTriangle, map, ext_from_iff _ _ _ rfl,
-        inl_v_d_assoc _ (p+1) p (p+2) (by linarith) (by linarith)])
+        inl_v_d_assoc _ (p+1) p (p+2) (by omega) (by omega)])
 
 /-- Given two composable morphisms `f` and `g` in the category of cochain complexes, this
 is the canonical morphism (which is an homotopy equivalence) from the mapping cone of
@@ -72,7 +72,7 @@ noncomputable def inv : mappingCone (mappingConeCompTriangle f g).mor₁ ⟶ map
       ext p
       rw [ext_from_iff _ (p + 1) _ rfl, ext_to_iff _ _ (p + 1) rfl]
       simp [map, δ_zero_cochain_comp,
-        Cochain.comp_v _ _ (add_neg_cancel 1) p (p+1) p (by linarith) (by linarith)])
+        Cochain.comp_v _ _ (add_neg_cancel 1) p (p+1) p (by omega) (by omega)])
 
 @[reassoc (attr := simp)]
 lemma hom_inv_id : hom f g ≫ inv f g = 𝟙 _ := by
@@ -86,44 +86,25 @@ this is the `homotopyInvHomId` field of the homotopy equivalence
 the morphism `mappingCone f ⟶ mappingCone (f ≫ g)`. -/
 noncomputable def homotopyInvHomId : Homotopy (inv f g ≫ hom f g) (𝟙 _) :=
   (Cochain.equivHomotopy _ _).symm ⟨-((snd _).comp ((fst (f ≫ g)).1.comp
-    ((inl f).comp (inl _) (by linarith)) (show 1 + (-2) = -1 by linarith)) (zero_add (-1))), by
+    ((inl f).comp (inl _) (by omega)) (show 1 + (-2) = -1 by omega)) (zero_add (-1))), by
       rw [δ_neg, δ_zero_cochain_comp _ _ _ (neg_add_cancel 1),
         Int.negOnePow_neg, Int.negOnePow_one, Units.neg_smul, one_smul,
-        δ_comp _ _ (show 1 + (-2) = -1 by linarith) 2 (-1) 0 (by linarith)
-          (by linarith) (by linarith),
-        δ_comp _ _ (show (-1) + (-1) = -2 by linarith) 0 0 (-1) (by linarith)
-          (by linarith) (by linarith), Int.negOnePow_neg, Int.negOnePow_neg,
-        Int.negOnePow_even 2 ⟨1, by linarith⟩, Int.negOnePow_one, Units.neg_smul,
+        δ_comp _ _ (show 1 + (-2) = -1 by omega) 2 (-1) 0 (by omega)
+          (by omega) (by omega),
+        δ_comp _ _ (show (-1) + (-1) = -2 by omega) 0 0 (-1) (by omega)
+          (by omega) (by omega), Int.negOnePow_neg, Int.negOnePow_neg,
+        Int.negOnePow_even 2 ⟨1, by omega⟩, Int.negOnePow_one, Units.neg_smul,
         one_smul, one_smul, δ_inl, δ_inl, δ_snd, Cocycle.δ_eq_zero, Cochain.zero_comp, add_zero,
         Cochain.neg_comp, neg_neg]
       ext n
       rw [ext_from_iff _ (n + 1) n rfl, ext_from_iff _ (n + 1) n rfl,
-        ext_from_iff _ (n + 2) (n + 1) (by linarith)]
-      simp? [hom, inv, ext_to_iff _ n (n + 1) rfl, map, Cochain.comp_v _ _
-          (add_neg_cancel 1) n (n + 1) n (by linarith) (by linarith),
-        Cochain.comp_v _ _ (show 1 + -2 = -1 by linarith) (n + 1) (n + 2) n
-          (by linarith) (by linarith),
-        Cochain.comp_v _ _ (show (-1) + -1 = -2 by linarith) (n + 2) (n + 1) n
-          (by linarith) (by linarith)] says
-        simp only [mappingConeCompTriangle_obj₁, mappingConeCompTriangle_obj₂,
-          mappingConeCompTriangle_mor₁, map, Int.reduceNeg, inv, hom, Cochain.ofHom_comp,
-          ofHom_desc, ofHom_lift, descCocycle_coe, AddSubmonoid.coe_zero,
-          Cochain.comp_zero_cochain_v, inl_v_descCochain_v_assoc, Cochain.zero_cochain_comp_v,
-          assoc, inl_v_snd_v_assoc, zero_comp, Cochain.id_comp,
-          Cochain.comp_assoc_of_first_is_zero_cochain, Cochain.comp_add, Cochain.comp_neg,
-          Cochain.comp_assoc_of_second_is_zero_cochain, neg_add_rev, neg_neg, Cochain.add_v,
-          Cochain.neg_v,
-          Cochain.comp_v _ _ (add_neg_cancel 1) n (n + 1) n (by linarith) (by linarith),
-          Cochain.comp_v _ _ (show 1 + -2 = -1 by linarith) (n + 1) (n + 2) n (by linarith)
-            (by linarith),
-          Cochain.comp_v _ _ (show (-1) + -1 = -2 by linarith) (n + 2) (n + 1) n (by linarith)
-            (by linarith),
-          Cochain.ofHom_v, HomologicalComplex.id_f, Preadditive.comp_add, Preadditive.comp_neg,
-          inl_v_fst_v_assoc, neg_zero, add_zero, comp_id, neg_add_cancel, inr_f_snd_v_assoc,
-          inr_f_descCochain_v_assoc, inr_f_fst_v_assoc, comp_zero, zero_add,
-          ext_to_iff _ n (n + 1) rfl, liftCochain_v_fst_v, inl_v_descCochain_v, inl_v_fst_v,
-          liftCochain_v_snd_v, Cochain.zero_v, inl_v_snd_v, and_self, neg_add_cancel_right,
-          inr_f_descCochain_v, inr_f_fst_v, inr_f_snd_v]⟩
+        ext_from_iff _ (n + 2) (n + 1) (by omega)]
+      simp [hom, inv, ext_to_iff _ n (n + 1) rfl, map, Cochain.comp_v _ _
+          (add_neg_cancel 1) n (n + 1) n (by omega) (by omega),
+        Cochain.comp_v _ _ (show 1 + -2 = -1 by omega) (n + 1) (n + 2) n
+          (by omega) (by omega),
+        Cochain.comp_v _ _ (show (-1) + -1 = -2 by omega) (n + 2) (n + 1) n
+          (by omega) (by omega)]⟩
 
 end MappingConeCompHomotopyEquiv
 

Mathlib/Algebra/Order/Group/Cone.lean

@@ -24,7 +24,7 @@ class AddGroupConeClass (S : Type*) (G : outParam Type*) [AddCommGroup G] [SetLi
 
 /-- `GroupConeClass S G` says that `S` is a type of cones in `G`. -/
 @[to_additive]
-class GroupConeClass (S G : Type*) [CommGroup G] [SetLike S G] extends
+class GroupConeClass (S : Type*) (G : outParam Type*) [CommGroup G] [SetLike S G] extends
     SubmonoidClass S G : Prop where
   eq_one_of_mem_of_inv_mem {C : S} {a : G} : a ∈ C → a⁻¹ ∈ C → a = 1
 

Mathlib/Algebra/Ring/Subsemiring/Basic.lean

@@ -27,7 +27,7 @@ section AddSubmonoidWithOneClass
 
 /-- `AddSubmonoidWithOneClass S R` says `S` is a type of subsets `s ≤ R` that contain `0`, `1`,
 and are closed under `(+)` -/
-class AddSubmonoidWithOneClass (S R : Type*) [AddMonoidWithOne R]
+class AddSubmonoidWithOneClass (S : Type*) (R : outParam Type*) [AddMonoidWithOne R]
   [SetLike S R] extends AddSubmonoidClass S R, OneMemClass S R : Prop
 
 variable {S R : Type*} [AddMonoidWithOne R] [SetLike S R] (s : S)

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -294,12 +294,7 @@ theorem mem_carrier_iff_of_mem (hm : 0 < m) (q : Spec.T A⁰_ f) (a : A) {n} (hn
   trans (HomogeneousLocalization.mk ⟨m * n, ⟨proj 𝒜 n a ^ m, by rw [← smul_eq_mul]; mem_tac⟩,
     ⟨f ^ n, by rw [mul_comm]; mem_tac⟩, ⟨_, rfl⟩⟩ : A⁰_ f) ∈ q.asIdeal
   · refine ⟨fun h ↦ h n, fun h i ↦ if hi : i = n then hi ▸ h else ?_⟩
-    #adaptation_note
-    /--
-    After https://github.com/leanprover/lean4/pull/5376
-    we need to specify the implicit arguments by `inferInstance`.
-    -/
-    convert @zero_mem _ _ inferInstance inferInstance _ q.asIdeal
+    convert zero_mem q.asIdeal
     apply HomogeneousLocalization.val_injective
     simp only [proj_apply, decompose_of_mem_ne _ hn (Ne.symm hi), zero_pow hm.ne',
       HomogeneousLocalization.val_mk, Localization.mk_zero, HomogeneousLocalization.val_zero]

Mathlib/GroupTheory/GroupAction/Quotient.lean

@@ -404,12 +404,6 @@ noncomputable def equivSubgroupOrbitsQuotientGroup [IsPretransitive α β]
     convert one_mem H
     · rw [inv_mul_eq_one, eq_comm, ← inv_mul_eq_one, ← Subgroup.mem_bot, ← free (g⁻¹ • x),
         mem_stabilizer_iff, mul_smul, (exists_smul_eq α (g⁻¹ • x) x).choose_spec]
-    #adaptation_note
-    /--
-    After https://github.com/leanprover/lean4/pull/5376 we need to search for this instance explicitly.
-    TODO: change `convert` to more agressively solve such goals with `infer_instance` itself.
-    -/
-    infer_instance
 
 end MulAction
 

Mathlib/Order/SuccPred/LinearLocallyFinite.lean

@@ -185,7 +185,7 @@ end LinearLocallyFiniteOrder
 section toZ
 
 -- Requiring either of `IsSuccArchimedean` or `IsPredArchimedean` is equivalent.
-variable [SuccOrder ι] [IsSuccArchimedean ι] [P : PredOrder ι] {i0 i : ι}
+variable [SuccOrder ι] [IsSuccArchimedean ι] [PredOrder ι] {i0 i : ι}
 
 -- For "to_Z"
 
@@ -200,7 +200,7 @@ theorem toZ_of_ge (hi : i0 ≤ i) : toZ i0 i = Nat.find (exists_succ_iterate_of_
   dif_pos hi
 
 theorem toZ_of_lt (hi : i < i0) :
-    toZ i0 i = -Nat.find (@exists_pred_iterate_of_le _ _ P _ _ _ hi.le) :=
+    toZ i0 i = -Nat.find (exists_pred_iterate_of_le (α := ι) hi.le) :=
   dif_neg (not_le.mpr hi)
 
 @[simp]
@@ -311,8 +311,8 @@ theorem toZ_mono {i j : ι} (h_le : i ≤ j) : toZ i0 i ≤ toZ i0 j := by
     · exact le_of_not_le h
   · exact absurd h_le (not_le.mpr (hj.trans_le hi))
   · exact (toZ_neg hi).le.trans (toZ_nonneg hj)
-  · let m := Nat.find (@exists_pred_iterate_of_le _ _ P _ _ _ h_le)
-    have hm : pred^[m] j = i := Nat.find_spec (exists_pred_iterate_of_le h_le)
+  · let m := Nat.find (exists_pred_iterate_of_le (α := ι) h_le)
+    have hm : pred^[m] j = i := Nat.find_spec (exists_pred_iterate_of_le (α := ι) h_le)
     have hj_eq : i = pred^[(-toZ i0 j).toNat + m] i0 := by
       rw [← hm, add_comm]
       nth_rw 1 [← iterate_pred_toZ j hj]