[Merged by Bors] - chore: backports for leanprover/lean4#4814 (part 3)

Mathlib/Algebra/GroupWithZero/Divisibility.lean

@@ -129,7 +129,10 @@ end MonoidWithZero
 
 section CancelCommMonoidWithZero
 
-variable [CancelCommMonoidWithZero α] [Subsingleton αˣ] {a b : α} {m n : ℕ}
+variable [CancelCommMonoidWithZero α] {a b : α} {m n : ℕ}
+
+section Subsingleton
+variable [Subsingleton αˣ]
 
 theorem dvd_antisymm : a ∣ b → b ∣ a → a = b := by
   rintro ⟨c, rfl⟩ ⟨d, hcd⟩
@@ -152,6 +155,8 @@ theorem eq_of_forall_dvd (h : ∀ c, a ∣ c ↔ b ∣ c) : a = b :=
 theorem eq_of_forall_dvd' (h : ∀ c, c ∣ a ↔ c ∣ b) : a = b :=
   ((h _).1 dvd_rfl).antisymm <| (h _).2 dvd_rfl
 
+end Subsingleton
+
 lemma pow_dvd_pow_iff (ha₀ : a ≠ 0) (ha : ¬IsUnit a) : a ^ n ∣ a ^ m ↔ n ≤ m := by
   constructor
   · intro h

Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean

@@ -30,7 +30,7 @@ end Commute
 section MonoidWithZero
 
 variable [GroupWithZero G₀] [Nontrivial M₀] [MonoidWithZero M₀'] [FunLike F G₀ M₀]
-  [MonoidWithZeroHomClass F G₀ M₀] [FunLike F' G₀ M₀'] [MonoidWithZeroHomClass F' G₀ M₀']
+  [MonoidWithZeroHomClass F G₀ M₀] [FunLike F' G₀ M₀']
   (f : F) {a : G₀}
 
 
@@ -41,8 +41,8 @@ theorem map_ne_zero : f a ≠ 0 ↔ a ≠ 0 :=
 theorem map_eq_zero : f a = 0 ↔ a = 0 :=
   not_iff_not.1 (map_ne_zero f)
 
-
-theorem eq_on_inv₀ (f g : F') (h : f a = g a) : f a⁻¹ = g a⁻¹ := by
+theorem eq_on_inv₀ [MonoidWithZeroHomClass F' G₀ M₀'] (f g : F') (h : f a = g a) :
+    f a⁻¹ = g a⁻¹ := by
   rcases eq_or_ne a 0 with (rfl | ha)
   · rw [inv_zero, map_zero, map_zero]
   · exact (IsUnit.mk0 a ha).eq_on_inv f g h

Mathlib/CategoryTheory/Functor/FullyFaithful.lean

@@ -32,7 +32,7 @@ universe v₁ v₂ v₃ u₁ u₂ u₃
 
 namespace CategoryTheory
 
-variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] {E : Type*} [Category E]
 
 namespace Functor
 
@@ -79,7 +79,10 @@ theorem map_preimage (F : C ⥤ D) [Full F] {X Y : C} (f : F.obj X ⟶ F.obj Y)
     F.map (preimage F f) = f :=
   (F.map_surjective f).choose_spec
 
-variable {F : C ⥤ D} [Full F] [F.Faithful] {X Y Z : C}
+variable {F : C ⥤ D} {X Y Z : C}
+
+section
+variable [Full F] [F.Faithful]
 
 @[simp]
 theorem preimage_id : F.preimage (𝟙 (F.obj X)) = 𝟙 X :=
@@ -110,6 +113,9 @@ theorem preimageIso_mapIso (f : X ≅ Y) : F.preimageIso (F.mapIso f) = f := by
   ext
   simp
 
+end
+
+variable (F) in
 /-- Structure containing the data of inverse map `(F.obj X ⟶ F.obj Y) ⟶ (X ⟶ Y)` of `F.map`
 in order to express that `F` is a fully faithful functor. -/
 structure FullyFaithful where
@@ -122,13 +128,20 @@ namespace FullyFaithful
 
 attribute [simp] map_preimage preimage_map
 
+variable (F) in
 /-- A `FullyFaithful` structure can be obtained from the assumption the `F` is both
 full and faithful. -/
 noncomputable def ofFullyFaithful [F.Full] [F.Faithful] :
     F.FullyFaithful where
   preimage := F.preimage
 
-variable {F}
+variable (C) in
+/-- The identity functor is fully faithful. -/
+@[simps]
+def id : (𝟭 C).FullyFaithful where
+  preimage f := f
+
+section
 variable (hF : F.FullyFaithful)
 
 /-- The equivalence `(X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y)` given by `h : F.FullyFaithful`. -/
@@ -177,19 +190,13 @@ def isoEquiv {X Y : C} : (X ≅ Y) ≃ (F.obj X ≅ F.obj Y) where
   left_inv := by aesop_cat
   right_inv := by aesop_cat
 
-variable (C) in
-/-- The identity functor is fully faithful. -/
-@[simps]
-def id : (𝟭 C).FullyFaithful where
-  preimage f := f
-
-variable {E : Type*} [Category E]
-
 /-- Fully faithful functors are stable by composition. -/
 @[simps]
 def comp {G : D ⥤ E} (hG : G.FullyFaithful) : (F ⋙ G).FullyFaithful where
   preimage f := hF.preimage (hG.preimage f)
 
+end
+
 /-- If `F ⋙ G` is fully faithful and `G` is faithful, then `F` is fully faithful. -/
 def ofCompFaithful {G : D ⥤ E} [G.Faithful] (hFG : (F ⋙ G).FullyFaithful) :
     F.FullyFaithful where

Mathlib/Combinatorics/Quiver/Covering.lean

@@ -250,7 +250,7 @@ end Prefunctor.IsCovering
 
 section HasInvolutiveReverse
 
-variable [HasInvolutiveReverse U] [HasInvolutiveReverse V] [Prefunctor.MapReverse φ]
+variable [HasInvolutiveReverse U] [HasInvolutiveReverse V]
 
 /-- In a quiver with involutive inverses, the star and costar at every vertex are equivalent.
 This map is induced by `Quiver.reverse`. -/
@@ -271,13 +271,15 @@ theorem Quiver.starEquivCostar_symm_apply {u v : U} (e : u ⟶ v) :
     (Quiver.starEquivCostar v).symm (Quiver.Costar.mk e) = Quiver.Star.mk (reverse e) :=
   rfl
 
+variable [Prefunctor.MapReverse φ]
+
 theorem Prefunctor.costar_conj_star (u : U) :
     φ.costar u = Quiver.starEquivCostar (φ.obj u) ∘ φ.star u ∘ (Quiver.starEquivCostar u).symm := by
   ext ⟨v, f⟩ <;> simp
 
 theorem Prefunctor.bijective_costar_iff_bijective_star (u : U) :
     Bijective (φ.costar u) ↔ Bijective (φ.star u) := by
-  rw [Prefunctor.costar_conj_star, EquivLike.comp_bijective, EquivLike.bijective_comp]
+  rw [Prefunctor.costar_conj_star φ, EquivLike.comp_bijective, EquivLike.bijective_comp]
 
 theorem Prefunctor.isCovering_of_bijective_star (h : ∀ u, Bijective (φ.star u)) : φ.IsCovering :=
   ⟨h, fun u => (φ.bijective_costar_iff_bijective_star u).2 (h u)⟩

Mathlib/Control/Monad/Cont.lean

@@ -104,7 +104,10 @@ instance (ε) [MonadExcept ε m] : MonadExcept ε (ContT r m) where
 
 end ContT
 
-variable {m : Type u → Type v} [Monad m]
+variable {m : Type u → Type v}
+
+section
+variable [Monad m]
 
 def ExceptT.mkLabel {α β ε} : Label (Except.{u, u} ε α) m β → Label α (ExceptT ε m) β
   | ⟨f⟩ => ⟨fun a => monadLift <| f (Except.ok a)⟩
@@ -183,6 +186,8 @@ def WriterT.callCC' [MonadCont m] {α β ω : Type _} [Monoid ω]
   WriterT.mk <|
     MonadCont.callCC (WriterT.run ∘ f ∘ WriterT.mkLabel' : Label (α × ω) m β → m (α × ω))
 
+end
+
 instance (ω) [Monad m] [EmptyCollection ω] [MonadCont m] : MonadCont (WriterT ω m) where
   callCC := WriterT.callCC
 
@@ -202,7 +207,7 @@ nonrec def StateT.callCC {σ} [MonadCont m] {α β : Type _}
 instance {σ} [MonadCont m] : MonadCont (StateT σ m) where
   callCC := StateT.callCC
 
-instance {σ} [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (StateT σ m) where
+instance {σ} [Monad m] [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (StateT σ m) where
   callCC_bind_right := by
     intros
     simp only [callCC, StateT.callCC, StateT.run_bind, callCC_bind_right]; ext; rfl
@@ -228,7 +233,7 @@ nonrec def ReaderT.callCC {ε} [MonadCont m] {α β : Type _}
 instance {ρ} [MonadCont m] : MonadCont (ReaderT ρ m) where
   callCC := ReaderT.callCC
 
-instance {ρ} [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (ReaderT ρ m) where
+instance {ρ} [Monad m] [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (ReaderT ρ m) where
   callCC_bind_right := by intros; simp only [callCC, ReaderT.callCC, ReaderT.run_bind,
                                     callCC_bind_right]; ext; rfl
   callCC_bind_left := by

Mathlib/Control/Monad/Writer.lean

@@ -33,14 +33,14 @@ class MonadWriter (ω : outParam (Type u)) (M : Type u → Type v) where
 
 export MonadWriter (tell listen pass)
 
-variable {M : Type u → Type v} [Monad M] {α ω ρ σ : Type u}
+variable {M : Type u → Type v} {α ω ρ σ : Type u}
 
 instance [MonadWriter ω M] : MonadWriter ω (ReaderT ρ M) where
   tell w := (tell w : M _)
   listen x r := listen <| x r
   pass x r := pass <| x r
 
-instance [MonadWriter ω M] : MonadWriter ω (StateT σ M) where
+instance [Monad M] [MonadWriter ω M] : MonadWriter ω (StateT σ M) where
   tell w := (tell w : M _)
   listen x s := (fun ((a,w), s) ↦ ((a,s), w)) <$> listen (x s)
   pass x s := pass <| (fun ((a, f), s) ↦ ((a, s), f)) <$> (x s)
@@ -57,7 +57,7 @@ protected def runThe (ω : Type u) (cmd : WriterT ω M α) : M (α × ω) := cmd
 @[ext]
 protected theorem ext {ω : Type u} (x x' : WriterT ω M α) (h : x.run = x'.run) : x = x' := h
 
-variable {ω : Type u} {α β : Type u}
+variable {ω : Type u} {α β : Type u} [Monad M]
 
 /-- Creates an instance of Monad, with an explicitly given empty and append operation.
 

Mathlib/Data/List/Count.lean

@@ -42,6 +42,11 @@ end CountP
 
 section Count
 
+@[simp]
+theorem count_map_of_injective {β} [DecidableEq α] [DecidableEq β] (l : List α) (f : α → β)
+    (hf : Function.Injective f) (x : α) : count (f x) (map f l) = count x l := by
+  simp only [count, countP_map, (· ∘ ·), hf.beq_eq]
+
 variable [DecidableEq α]
 
 @[deprecated (since := "2023-08-23")]
@@ -54,11 +59,6 @@ theorem count_cons' (a b : α) (l : List α) :
 lemma count_attach (a : {x // x ∈ l}) : l.attach.count a = l.count ↑a :=
   Eq.trans (countP_congr fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _
 
-@[simp]
-theorem count_map_of_injective {β} [DecidableEq α] [DecidableEq β] (l : List α) (f : α → β)
-    (hf : Function.Injective f) (x : α) : count (f x) (map f l) = count x l := by
-  simp only [count, countP_map, (· ∘ ·), hf.beq_eq]
-
 end Count
 
 end List

Mathlib/Order/Hom/Basic.lean

@@ -557,25 +557,25 @@ protected theorem strictMono : StrictMono f := fun _ _ => f.lt_iff_lt.2
 protected theorem acc (a : α) : Acc (· < ·) (f a) → Acc (· < ·) a :=
   f.ltEmbedding.acc a
 
-protected theorem wellFounded :
+protected theorem wellFounded (f : α ↪o β) :
     WellFounded ((· < ·) : β → β → Prop) → WellFounded ((· < ·) : α → α → Prop) :=
   f.ltEmbedding.wellFounded
 
-protected theorem isWellOrder [IsWellOrder β (· < ·)] : IsWellOrder α (· < ·) :=
+protected theorem isWellOrder [IsWellOrder β (· < ·)] (f : α ↪o β) : IsWellOrder α (· < ·) :=
   f.ltEmbedding.isWellOrder
 
 /-- An order embedding is also an order embedding between dual orders. -/
 protected def dual : αᵒᵈ ↪o βᵒᵈ :=
   ⟨f.toEmbedding, f.map_rel_iff⟩
 
 /-- A preorder which embeds into a well-founded preorder is itself well-founded. -/
-protected theorem wellFoundedLT [WellFoundedLT β] : WellFoundedLT α where
+protected theorem wellFoundedLT [WellFoundedLT β] (f : α ↪o β) : WellFoundedLT α where
   wf := f.wellFounded IsWellFounded.wf
 
 /-- A preorder which embeds into a preorder in which `(· > ·)` is well-founded
 also has `(· > ·)` well-founded. -/
-protected theorem wellFoundedGT [WellFoundedGT β] : WellFoundedGT α :=
-  @OrderEmbedding.wellFoundedLT αᵒᵈ _ _ _ f.dual _
+protected theorem wellFoundedGT [WellFoundedGT β] (f : α ↪o β) : WellFoundedGT α :=
+  @OrderEmbedding.wellFoundedLT αᵒᵈ _ _ _ _ f.dual
 
 /-- A version of `WithBot.map` for order embeddings. -/
 @[simps (config := .asFn)]
@@ -1225,13 +1225,14 @@ theorem OrderIso.isCompl {x y : α} (h : IsCompl x y) : IsCompl (f x) (f y) :=
 theorem OrderIso.isCompl_iff {x y : α} : IsCompl x y ↔ IsCompl (f x) (f y) :=
   ⟨f.isCompl, fun h => f.symm_apply_apply x ▸ f.symm_apply_apply y ▸ f.symm.isCompl h⟩
 
-theorem OrderIso.complementedLattice [ComplementedLattice α] : ComplementedLattice β :=
+theorem OrderIso.complementedLattice [ComplementedLattice α] (f : α ≃o β) : ComplementedLattice β :=
   ⟨fun x => by
     obtain ⟨y, hy⟩ := exists_isCompl (f.symm x)
     rw [← f.symm_apply_apply y] at hy
     exact ⟨f y, f.symm.isCompl_iff.2 hy⟩⟩
 
-theorem OrderIso.complementedLattice_iff : ComplementedLattice α ↔ ComplementedLattice β :=
+theorem OrderIso.complementedLattice_iff (f : α ≃o β) :
+    ComplementedLattice α ↔ ComplementedLattice β :=
   ⟨by intro; exact f.complementedLattice,
    by intro; exact f.symm.complementedLattice⟩
 

Mathlib/Order/WithBot.lean

@@ -174,6 +174,13 @@ theorem unbot_coe (x : α) (h : (x : WithBot α) ≠ ⊥ := coe_ne_bot) : (x : W
 instance canLift : CanLift (WithBot α) α (↑) fun r => r ≠ ⊥ where
   prf x h := ⟨x.unbot h, coe_unbot _ _⟩
 
+instance instTop [Top α] : Top (WithBot α) where
+  top := (⊤ : α)
+
+@[simp, norm_cast] lemma coe_top [Top α] : ((⊤ : α) : WithBot α) = ⊤ := rfl
+@[simp, norm_cast] lemma coe_eq_top [Top α] {a : α} : (a : WithBot α) = ⊤ ↔ a = ⊤ := coe_eq_coe
+@[simp, norm_cast] lemma top_eq_coe [Top α] {a : α} : ⊤ = (a : WithBot α) ↔ ⊤ = a := coe_eq_coe
+
 section LE
 
 variable [LE α]
@@ -195,13 +202,6 @@ theorem some_le_some : @LE.le (WithBot α) _ (Option.some a) (Option.some b) ↔
 @[simp, deprecated bot_le "Don't mix Option and WithBot" (since := "2024-05-27")]
 theorem none_le {a : WithBot α} : @LE.le (WithBot α) _ none a := bot_le
 
-instance instTop [Top α] : Top (WithBot α) where
-  top := (⊤ : α)
-
-@[simp, norm_cast] lemma coe_top [Top α] : ((⊤ : α) : WithBot α) = ⊤ := rfl
-@[simp, norm_cast] lemma coe_eq_top [Top α] {a : α} : (a : WithBot α) = ⊤ ↔ a = ⊤ := coe_eq_coe
-@[simp, norm_cast] lemma top_eq_coe [Top α] {a : α} : ⊤ = (a : WithBot α) ↔ ⊤ = a := coe_eq_coe
-
 instance orderTop [OrderTop α] : OrderTop (WithBot α) where
   le_top o a ha := by cases ha; exact ⟨_, rfl, le_top⟩
 
@@ -752,6 +752,13 @@ theorem untop_coe (x : α) (h : (x : WithTop α) ≠ ⊤ := coe_ne_top) : (x : W
 instance canLift : CanLift (WithTop α) α (↑) fun r => r ≠ ⊤ where
   prf x h := ⟨x.untop h, coe_untop _ _⟩
 
+instance instBot [Bot α] : Bot (WithTop α) where
+  bot := (⊥ : α)
+
+@[simp, norm_cast] lemma coe_bot [Bot α] : ((⊥ : α) : WithTop α) = ⊥ := rfl
+@[simp, norm_cast] lemma coe_eq_bot [Bot α] {a : α} : (a : WithTop α) = ⊥ ↔ a = ⊥ := coe_eq_coe
+@[simp, norm_cast] lemma bot_eq_coe [Bot α] {a : α} : (⊥ : WithTop α) = a ↔ ⊥ = a := coe_eq_coe
+
 section LE
 
 variable [LE α]
@@ -797,13 +804,6 @@ instance orderTop : OrderTop (WithTop α) where
 @[simp, deprecated le_top "Don't mix Option and WithTop" (since := "2024-05-27")]
 theorem le_none {a : WithTop α} : @LE.le (WithTop α) _ a none := le_top
 
-instance instBot [Bot α] : Bot (WithTop α) where
-  bot := (⊥ : α)
-
-@[simp, norm_cast] lemma coe_bot [Bot α] : ((⊥ : α) : WithTop α) = ⊥ := rfl
-@[simp, norm_cast] lemma coe_eq_bot [Bot α] {a : α} : (a : WithTop α) = ⊥ ↔ a = ⊥ := coe_eq_coe
-@[simp, norm_cast] lemma bot_eq_coe [Bot α] {a : α} : (⊥ : WithTop α) = a ↔ ⊥ = a := coe_eq_coe
-
 instance orderBot [OrderBot α] : OrderBot (WithTop α) where
   bot_le o a ha := by cases ha; exact ⟨_, rfl, bot_le⟩