chore: backports for leanprover/lean4#4814 (part 1) (#15245)

The new variables inclusion mechanism leanprover/lean4#4814 is going to require many changes to Mathlib.

Some of these changes are to make sure typeclass hypotheses are not unnecessarily included. This is achieved either by using `section` to bound `variable [...]`, using `variable ... in`, or reordering theorems. (I think you can see all three being using here.)

Other changes require adding `include ...` to include variables that the new mechanism won't automatically include. These changes can't be backported to master, and instead are accumulating on the `lean-pr-testing-4814` branch.

Author: kim-em

Mathlib/Control/Lawful.lean

@@ -55,12 +55,10 @@ variable {α β ε : Type u} {m : Type u → Type v} (x : ExceptT ε m α)
 theorem run_mk (x : m (Except ε α)) : ExceptT.run (ExceptT.mk x) = x :=
   rfl
 
-variable [Monad m]
-
 attribute [simp] run_bind
 
 @[simp]
-theorem run_monadLift {n} [MonadLiftT n m] (x : n α) :
+theorem run_monadLift {n} [Monad m] [MonadLiftT n m] (x : n α) :
     (monadLift x : ExceptT ε m α).run = Except.ok <$> (monadLift x : m α) :=
   rfl
 
@@ -115,6 +113,7 @@ variable {α β : Type u} {m : Type u → Type v} (x : OptionT m α)
 theorem run_mk (x : m (Option α)) : OptionT.run (OptionT.mk x) = x :=
   rfl
 
+section Monad
 variable [Monad m]
 
 @[simp]
@@ -142,6 +141,8 @@ theorem run_monadLift {n} [MonadLiftT n m] (x : n α) :
     (monadLift x : OptionT m α).run = (monadLift x : m α) >>= fun a => pure (some a) :=
   rfl
 
+end Monad
+
 @[simp]
 theorem run_monadMap {n} [MonadFunctorT n m] (f : ∀ {α}, n α → n α) :
     (monadMap (@f) x : OptionT m α).run = monadMap (@f) x.run :=

Mathlib/Control/Traversable/Basic.lean

@@ -79,8 +79,8 @@ end ApplicativeTransformation
 
 namespace ApplicativeTransformation
 
-variable (F : Type u → Type v) [Applicative F] [LawfulApplicative F]
-variable (G : Type u → Type w) [Applicative G] [LawfulApplicative G]
+variable (F : Type u → Type v) [Applicative F]
+variable (G : Type u → Type w) [Applicative G]
 
 instance : CoeFun (ApplicativeTransformation F G) fun _ => ∀ {α}, F α → G α :=
   ⟨fun η ↦ η.app _⟩
@@ -133,6 +133,8 @@ theorem preserves_pure {α} : ∀ x : α, η (pure x) = pure x :=
 theorem preserves_seq {α β : Type u} : ∀ (x : F (α → β)) (y : F α), η (x <*> y) = η x <*> η y :=
   η.preserves_seq'
 
+variable [LawfulApplicative F] [LawfulApplicative G]
+
 @[functor_norm]
 theorem preserves_map {α β} (x : α → β) (y : F α) : η (x <$> y) = x <$> η y := by
   rw [← pure_seq, η.preserves_seq, preserves_pure, pure_seq]
@@ -154,7 +156,7 @@ instance : Inhabited (ApplicativeTransformation F F) :=
 
 universe s t
 
-variable {H : Type u → Type s} [Applicative H] [LawfulApplicative H]
+variable {H : Type u → Type s} [Applicative H]
 
 /-- The composition of applicative transformations. -/
 def comp (η' : ApplicativeTransformation G H) (η : ApplicativeTransformation F G) :

Mathlib/Init/Algebra/Classes.lean

@@ -333,22 +333,22 @@ local infixl:50 " ≺ " => r
 def Equiv (a b : α) : Prop :=
   ¬a ≺ b ∧ ¬b ≺ a
 
-variable [IsStrictWeakOrder α r]
-
 local infixl:50 " ≈ " => @Equiv _ r
 
-theorem erefl (a : α) : a ≈ a :=
-  ⟨irrefl a, irrefl a⟩
-
 theorem esymm {a b : α} : a ≈ b → b ≈ a := fun ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩
 
-theorem etrans {a b c : α} : a ≈ b → b ≈ c → a ≈ c :=
-  incomp_trans
-
 theorem not_lt_of_equiv {a b : α} : a ≈ b → ¬a ≺ b := fun h => h.1
 
 theorem not_lt_of_equiv' {a b : α} : a ≈ b → ¬b ≺ a := fun h => h.2
 
+variable [IsStrictWeakOrder α r]
+
+theorem erefl (a : α) : a ≈ a :=
+  ⟨irrefl a, irrefl a⟩
+
+theorem etrans {a b c : α} : a ≈ b → b ≈ c → a ≈ c :=
+  incomp_trans
+
 instance isEquiv : IsEquiv α (@Equiv _ r) where
   refl := erefl
   trans _ _ _ := etrans

Mathlib/Logic/Basic.lean

@@ -951,6 +951,9 @@ either branch to `a`. -/
 theorem ite_apply (f g : ∀ a, σ a) (a : α) : (ite P f g) a = ite P (f a) (g a) :=
   dite_apply P (fun _ ↦ f) (fun _ ↦ g) a
 
+section
+variable [Decidable Q]
+
 theorem ite_and : ite (P ∧ Q) a b = ite P (ite Q a b) b := by
   by_cases hp : P <;> by_cases hq : Q <;> simp [hp, hq]
 
@@ -966,6 +969,8 @@ theorem ite_ite_comm (h : P → ¬Q) :
      if Q then b else if P then a else c :=
   dite_dite_comm P Q h
 
+end
+
 variable {P Q}
 
 theorem ite_prop_iff_or : (if P then Q else R) ↔ (P ∧ Q ∨ ¬ P ∧ R) := by

Mathlib/Logic/Function/Basic.lean

@@ -454,7 +454,7 @@ end SurjInv
 
 section Update
 
-variable {α : Sort u} {β : α → Sort v} {α' : Sort w} [DecidableEq α] [DecidableEq α']
+variable {α : Sort u} {β : α → Sort v} {α' : Sort w} [DecidableEq α]
   {f g : (a : α) → β a} {a : α} {b : β a}
 
 
@@ -523,6 +523,8 @@ theorem update_comp_eq_of_forall_ne' {α'} (g : ∀ a, β a) {f : α' → α} {i
     (h : ∀ x, f x ≠ i) : (fun j ↦ (update g i a) (f j)) = fun j ↦ g (f j) :=
   funext fun _ ↦ update_noteq (h _) _ _
 
+variable [DecidableEq α']
+
 /-- Non-dependent version of `Function.update_comp_eq_of_forall_ne'` -/
 theorem update_comp_eq_of_forall_ne {α β : Sort*} (g : α' → β) {f : α → α'} {i : α'} (a : β)
     (h : ∀ x, f x ≠ i) : update g i a ∘ f = g ∘ f :=

Mathlib/Order/Defs.lean

@@ -346,7 +346,7 @@ def ltByCases (x y : α) {P : Sort*} (h₁ : x < y → P) (h₂ : x = y → P) (
   if h : x < y then h₁ h
   else if h' : y < x then h₃ h' else h₂ (le_antisymm (le_of_not_gt h') (le_of_not_gt h))
 
-theorem le_imp_le_of_lt_imp_lt {β} [Preorder α] [LinearOrder β] {a b : α} {c d : β}
+theorem le_imp_le_of_lt_imp_lt {α β} [Preorder α] [LinearOrder β] {a b : α} {c d : β}
     (H : d < c → b < a) (h : a ≤ b) : c ≤ d :=
   le_of_not_lt fun h' => not_le_of_gt (H h') h
 

Mathlib/Tactic/PushNeg.lean

@@ -22,7 +22,7 @@ namespace Mathlib.Tactic.PushNeg
 
 open Lean Meta Elab.Tactic Parser.Tactic
 
-variable (p q : Prop) {α : Sort*} (s : α → Prop)
+variable (p q : Prop) {α : Sort*} {β : Type*} (s : α → Prop)
 
 theorem not_not_eq : (¬ ¬ p) = p := propext not_not
 theorem not_and_eq : (¬ (p ∧ q)) = (p → ¬ q) := propext not_and
@@ -35,12 +35,16 @@ theorem not_ne_eq (x y : α) : (¬ (x ≠ y)) = (x = y) := ne_eq x y ▸ not_not
 theorem not_iff : (¬ (p ↔ q)) = ((p ∧ ¬ q) ∨ (¬ p ∧ q)) := propext <|
   _root_.not_iff.trans <| iff_iff_and_or_not_and_not.trans <| by rw [not_not, or_comm]
 
-variable {β : Type*} [LinearOrder β]
+section LinearOrder
+variable [LinearOrder β]
+
 theorem not_le_eq (a b : β) : (¬ (a ≤ b)) = (b < a) := propext not_le
 theorem not_lt_eq (a b : β) : (¬ (a < b)) = (b ≤ a) := propext not_lt
 theorem not_ge_eq (a b : β) : (¬ (a ≥ b)) = (a < b) := propext not_le
 theorem not_gt_eq (a b : β) : (¬ (a > b)) = (a ≤ b) := propext not_lt
 
+end LinearOrder
+
 theorem not_nonempty_eq (s : Set β) : (¬ s.Nonempty) = (s = ∅) := by
   have A : ∀ (x : β), ¬(x ∈ (∅ : Set β)) := fun x ↦ id
   simp only [Set.Nonempty, not_exists, eq_iff_iff]