chore: adapt stdlib to new variable behavior

This is a better fix to the problem reported at
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nat.20fighting,
which itself had a problem as reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/omega.20regression/near/456539091.

(cherry picked from commit 215b4a6a8d)

RELEASES.md

@@ -10,7 +10,7 @@ of each version.
 
 v4.11.0
 ----------
-Development in progress.
+Release notes to be written.
 
 v4.10.0
 ----------

src/CMakeLists.txt

@@ -12,7 +12,7 @@ project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
 set(LEAN_VERSION_MINOR 11)
 set(LEAN_VERSION_PATCH 0)
-set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
+set(LEAN_VERSION_IS_RELEASE 1)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
 set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
 if (LEAN_SPECIAL_VERSION_DESC)

src/Init/Data/List/Erase.lean

@@ -354,7 +354,7 @@ theorem erase_eq_iff [LawfulBEq α] {a : α} {l : List α} :
   rw [erase_of_not_mem]
   simp_all
 
-theorem Nodup.erase_eq_filter [BEq α] [LawfulBEq α] {l} (d : Nodup l) (a : α) : l.erase a = l.filter (· != a) := by
+theorem Nodup.erase_eq_filter [LawfulBEq α] {l} (d : Nodup l) (a : α) : l.erase a = l.filter (· != a) := by
   induction d with
   | nil => rfl
   | cons m _n ih =>
@@ -367,13 +367,13 @@ theorem Nodup.erase_eq_filter [BEq α] [LawfulBEq α] {l} (d : Nodup l) (a : α)
       simpa [@eq_comm α] using m
     · simp [beq_false_of_ne h, ih, h]
 
-theorem Nodup.mem_erase_iff [BEq α] [LawfulBEq α] {a : α} (d : Nodup l) : a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l := by
+theorem Nodup.mem_erase_iff [LawfulBEq α] {a : α} (d : Nodup l) : a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l := by
   rw [Nodup.erase_eq_filter d, mem_filter, and_comm, bne_iff_ne]
 
-theorem Nodup.not_mem_erase [BEq α] [LawfulBEq α] {a : α} (h : Nodup l) : a ∉ l.erase a := fun H => by
+theorem Nodup.not_mem_erase [LawfulBEq α] {a : α} (h : Nodup l) : a ∉ l.erase a := fun H => by
   simpa using ((Nodup.mem_erase_iff h).mp H).left
 
-theorem Nodup.erase [BEq α] [LawfulBEq α] (a : α) : Nodup l → Nodup (l.erase a) :=
+theorem Nodup.erase [LawfulBEq α] (a : α) : Nodup l → Nodup (l.erase a) :=
   Nodup.sublist <| erase_sublist _ _
 
 end erase

src/Init/Omega/Int.lean

@@ -83,6 +83,10 @@ theorem neg_congr {a b : Int} (h₁ : a = b) : -a = -b := by
 theorem lt_of_gt {x y : Int} (h : x > y) : y < x := gt_iff_lt.mp h
 theorem le_of_ge {x y : Int} (h : x ≥ y) : y ≤ x := ge_iff_le.mp h
 
+theorem ofNat_mul_nonneg {a b : Nat} : 0 ≤ (a : Int) * b := by
+  rw [← Int.ofNat_mul]
+  exact Int.ofNat_zero_le (a * b)
+
 theorem ofNat_sub_eq_zero {b a : Nat} (h : ¬ b ≤ a) : ((a - b : Nat) : Int) = 0 :=
   Int.ofNat_eq_zero.mpr (Nat.sub_eq_zero_of_le (Nat.le_of_lt (Nat.not_le.mp h)))
 

src/Init/WF.lean

@@ -68,6 +68,7 @@ noncomputable def recursion {C : α → Sort v} (a : α) (h : ∀ x, (∀ y, r y
   induction (apply hwf a) with
   | intro x₁ _ ih => exact h x₁ ih
 
+include hwf in
 theorem induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a :=
   recursion hwf a h
 

src/Lean/Compiler/IR/EmitC.lean

@@ -96,8 +96,13 @@ def shouldExport (n : Name) : Bool :=
   -- libleanshared to avoid Windows symbol limit
   !(`Lean.Compiler.LCNF).isPrefixOf n &&
   !(`Lean.IR).isPrefixOf n &&
-  -- Lean.Server.findModuleRefs is used in Verso
-  (!(`Lean.Server).isPrefixOf n || n == `Lean.Server.findModuleRefs)
+  -- Lean.Server.findModuleRefs is used in SubVerso, and the contents of RequestM are used by the
+  -- full Verso as well as anything else that extends the LSP server.
+  (!(`Lean.Server.Watchdog).isPrefixOf n) &&
+  (!(`Lean.Server.ImportCompletion).isPrefixOf n) &&
+  (!(`Lean.Server.Completion).isPrefixOf n)
+
+
 
 def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M Unit := do
   let ps := decl.params

src/Lean/Elab/BuiltinCommand.lean

@@ -502,6 +502,16 @@ def elabRunMeta : CommandElab := fun stx =>
     addDocString declName (← getDocStringText doc)
   | _ => throwUnsupportedSyntax
 
+@[builtin_command_elab Lean.Parser.Command.include] def elabInclude : CommandElab
+  | `(Lean.Parser.Command.include| include $ids*) => do
+    let vars := (← getScope).varDecls.concatMap getBracketedBinderIds
+    for id in ids do
+      unless vars.contains id.getId do
+        throwError "invalid 'include', variable '{id}' has not been declared in the current scope"
+    modifyScope fun sc =>
+      { sc with includedVars := sc.includedVars ++ ids.toList.map (·.getId) }
+  | _ => throwUnsupportedSyntax
+
 @[builtin_command_elab Parser.Command.exit] def elabExit : CommandElab := fun _ =>
   logWarning "using 'exit' to interrupt Lean"
 

src/Lean/Elab/Command.lean

@@ -51,6 +51,8 @@ structure Scope where
   even if they do not work with binders per se.
   -/
   varDecls      : Array (TSyntax ``Parser.Term.bracketedBinder) := #[]
+  /-- `include`d section variable names -/
+  includedVars  : List Name := []
   /--
   Globally unique internal identifiers for the `varDecls`.
   There is one identifier per variable introduced by the binders

src/Lean/Elab/MutualDef.lean

@@ -323,7 +323,49 @@ private def declValToTerminationHint (declVal : Syntax) : TermElabM TerminationH
   else
     return .none
 
-private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array Expr) :=
+def instantiateMVarsProfiling (e : Expr) : MetaM Expr := do
+  profileitM Exception s!"instantiate metavars" (← getOptions) do
+    instantiateMVars e
+
+/--
+Runs `k` with a restricted local context where only section variables from `vars` are included that
+* are directly referenced in any `headers`,
+* are included in `includedVars` (via the `include` command),
+* are directly referenced in any variable included by these rules, OR
+* are instance-implicit variables that only reference section variables included by these rules.
+-/
+private def withHeaderSecVars {α} (vars : Array Expr) (includedVars : List Name) (headers : Array DefViewElabHeader)
+    (k : Array Expr → TermElabM α) : TermElabM α := do
+  let (_, used) ← collectUsed.run {}
+  let (lctx, localInsts, vars) ← removeUnused vars used
+  withLCtx lctx localInsts <| k vars
+where
+  collectUsed : StateRefT CollectFVars.State MetaM Unit := do
+    -- directly referenced in headers
+    headers.forM (·.type.collectFVars)
+    -- included by `include`
+    vars.forM fun var => do
+      let ldecl ← getFVarLocalDecl var
+      if includedVars.contains ldecl.userName then
+        modify (·.add ldecl.fvarId)
+    -- transitively referenced
+    get >>= (·.addDependencies) >>= set
+    -- instances (`addDependencies` unnecessary as by definition they may only reference variables
+    -- already included)
+    vars.forM fun var => do
+      let ldecl ← getFVarLocalDecl var
+      let st ← get
+      if ldecl.binderInfo.isInstImplicit && (← getFVars ldecl.type).all st.fvarSet.contains then
+        modify (·.add ldecl.fvarId)
+  getFVars (e : Expr) : MetaM (Array FVarId) :=
+    (·.2.fvarIds) <$> e.collectFVars.run {}
+
+register_builtin_option deprecated.oldSectionVars : Bool := {
+  defValue := false
+  descr    := "re-enable deprecated behavior of including exactly the section variables used in a declaration"
+}
+
+private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr) (includedVars : List Name) : TermElabM (Array Expr) :=
   headers.mapM fun header => do
     let mut reusableResult? := none
     if let some snap := header.bodySnap? then
@@ -338,6 +380,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array
       withReuseContext header.value do
       withDeclName header.declName <| withLevelNames header.levelNames do
       let valStx ← liftMacroM <| declValToTerm header.value
+      (if header.kind.isTheorem && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars includedVars #[header] else fun x => x #[]) fun vars => do
       forallBoundedTelescope header.type header.numParams fun xs type => do
         -- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location.
         for i in [0:header.binderIds.size] do
@@ -348,8 +391,21 @@ private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array
           elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
         -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
         -- leads to more section variables being included than necessary
-        let val ← instantiateMVars val
-        mkLambdaFVars xs val
+        let val ← instantiateMVarsProfiling val
+        let val ← mkLambdaFVars xs val
+        unless header.type.hasSorry || val.hasSorry do
+          for var in vars do
+            unless header.type.containsFVar var.fvarId! ||
+                val.containsFVar var.fvarId! ||
+                (← vars.anyM (fun v => return (← v.fvarId!.getType).containsFVar var.fvarId!)) do
+              let varDecl ← var.fvarId!.getDecl
+              let var := if varDecl.userName.hasMacroScopes && varDecl.binderInfo.isInstImplicit then
+                m!"[{varDecl.type}]".group
+              else
+                var
+              logWarningAt header.ref m!"included section variable '{var}' is not used in \
+                '{header.declName}', consider excluding it"
+        return val
     if let some snap := header.bodySnap? then
       snap.new.resolve <| some {
         diagnostics :=
@@ -900,7 +956,7 @@ partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs :
     for preDef in preDefs do
       checkPreDef preDef
 
-def elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit :=
+def elabMutualDef (vars : Array Expr) (includedVars : List Name) (views : Array DefView) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv do
       -- save correct environment in info tree
@@ -921,7 +977,7 @@ where
           addLocalVarInfo view.declId funFVar
         let values ←
           try
-            let values ← elabFunValues headers
+            let values ← elabFunValues headers vars includedVars
             Term.synthesizeSyntheticMVarsNoPostponing
             values.mapM (instantiateMVars ·)
           catch ex =>
@@ -931,7 +987,7 @@ where
         let letRecsToLift ← getLetRecsToLift
         let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
         checkLetRecsToLiftTypes funFVars letRecsToLift
-        withUsed vars headers values letRecsToLift fun vars => do
+        (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars includedVars headers else withUsed vars headers values letRecsToLift) fun vars => do
           let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
           for preDef in preDefs do
             trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
@@ -1002,7 +1058,8 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
     if let some snap := snap? then
       -- no non-fatal diagnostics at this point
       snap.new.resolve <| .ofTyped { defs, diagnostics := .empty : DefsParsedSnapshot }
-    runTermElabM fun vars => Term.elabMutualDef vars views
+    let includedVars := (← getScope).includedVars
+    runTermElabM fun vars => Term.elabMutualDef vars includedVars views
 
 builtin_initialize
   registerTraceClass `Elab.definition.mkClosure

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -101,9 +101,9 @@ partial def asLinearCombo (e : Expr) : OmegaM (LinearCombo × OmegaM Expr × Has
     trace[omega] "Found in cache: {e}"
     return (lc, prf, ∅)
   | none =>
-    let r ← asLinearComboImpl e
-    modifyThe Cache fun cache => (cache.insert e (r.1, r.2.1.run' cache))
-    pure r
+    let (lc, proof, r) ← asLinearComboImpl e
+    modifyThe Cache fun cache => (cache.insert e (lc, proof.run' cache))
+    pure (lc, proof, r)
 
 /--
 Translates an expression into a `LinearCombo`.
@@ -255,16 +255,9 @@ where
     | (``Nat.succ, #[n]) => rewrite e (.app (.const ``Int.ofNat_succ []) n)
     | (``HAdd.hAdd, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_add []) a b)
     | (``HMul.hMul, #[_, _, _, _, a, b]) =>
-      -- Don't push the cast into a multiplication unless it produces a non-trivial linear combination.
-      let r? ← commitWhen do
-        let (lc, prf, r) ← rewrite e (mkApp2 (.const ``Int.ofNat_mul []) a b)
-        if lc.isAtom then
-          pure (none, false)
-        else
-          pure (some (lc, prf, r), true)
-      match r? with
-      | some r => pure r
-      | none => mkAtomLinearCombo e
+      let (lc, prf, r) ← rewrite e (mkApp2 (.const ``Int.ofNat_mul []) a b)
+      -- Add the fact that the multiplication is non-negative.
+      pure (lc, prf, r.insert (mkApp2 (.const ``Int.ofNat_mul_nonneg []) a b))
     | (``HDiv.hDiv, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_ediv []) a b)
     | (``OfNat.ofNat, #[_, n, _]) => rewrite e (.app (.const ``Int.natCast_ofNat []) n)
     | (``HMod.hMod, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_emod []) a b)

src/Lean/Parser/Command.lean

@@ -242,10 +242,10 @@ def «structure»          := leading_parser
 @[builtin_command_parser] def noncomputableSection := leading_parser
   "noncomputable " >> "section" >> optional (ppSpace >> checkColGt >> ident)
 /--
-A `section`/`end` pair delimits the scope of `variable`, `open`, `set_option`, and `local` commands.
-Sections can be nested. `section <id>` provides a label to the section that has to appear with the
-matching `end`. In either case, the `end` can be omitted, in which case the section is closed at the
-end of the file.
+A `section`/`end` pair delimits the scope of `variable`, `include, `open`, `set_option`, and `local`
+commands. Sections can be nested. `section <id>` provides a label to the section that has to appear
+with the matching `end`. In either case, the `end` can be omitted, in which case the section is
+closed at the end of the file.
 -/
 @[builtin_command_parser] def «section»      := leading_parser
   "section" >> optional (ppSpace >> checkColGt >> ident)
@@ -274,12 +274,12 @@ with `end <id>`. The `end` command is optional at the end of a file.
 @[builtin_command_parser] def «end»          := leading_parser
   "end" >> optional (ppSpace >> checkColGt >> ident)
 /-- Declares one or more typed variables, or modifies whether already-declared variables are
-implicit.
+  implicit.
 
 Introduces variables that can be used in definitions within the same `namespace` or `section` block.
-When a definition mentions a variable, Lean will add it as an argument of the definition. The
-`variable` command is also able to add typeclass parameters. This is useful in particular when
-writing many definitions that have parameters in common (see below for an example).
+When a definition mentions a variable, Lean will add it as an argument of the definition. This is
+useful in particular when writing many definitions that have parameters in common (see below for an
+example).
 
 Variable declarations have the same flexibility as regular function paramaters. In particular they
 can be [explicit, implicit][binder docs], or [instance implicit][tpil classes] (in which case they
@@ -287,17 +287,22 @@ can be anonymous). This can be changed, for instance one can turn explicit varia
 implicit one with `variable {x}`. Note that currently, you should avoid changing how variables are
 bound and declare new variables at the same time; see [issue 2789] for more on this topic.
 
+In *theorem bodies* (i.e. proofs), variables are not included based on usage in order to ensure that
+changes to the proof cannot change the statement of the overall theorem. Instead, variables are only
+available to the proof if they have been mentioned in the theorem header or in an `include` command
+or are instance implicit and depend only on such variables.
+
 See [*Variables and Sections* from Theorem Proving in Lean][tpil vars] for a more detailed
 discussion.
 
-[tpil vars]: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#variables-and-sections
-(Variables and Sections on Theorem Proving in Lean)
-[tpil classes]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html
-(Type classes on Theorem Proving in Lean)
-[binder docs]: https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.BinderInfo
-(Documentation for the BinderInfo type)
-[issue 2789]: https://github.com/leanprover/lean4/issues/2789
-(Issue 2789 on github)
+[tpil vars]:
+https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#variables-and-sections
+(Variables and Sections on Theorem Proving in Lean) [tpil classes]:
+https://lean-lang.org/theorem_proving_in_lean4/type_classes.html (Type classes on Theorem Proving in
+Lean) [binder docs]:
+https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.BinderInfo (Documentation
+for the BinderInfo type) [issue 2789]: https://github.com/leanprover/lean4/issues/2789 (Issue 2789
+on github)
 
 ## Examples
 
@@ -368,6 +373,24 @@ namespace Logger
 end Logger
 ```
 
+The following example demonstrates availability of variables in proofs:
+```lean
+variable
+  {α : Type}    -- available in the proof as indirectly mentioned through `a`
+  [ToString α]  -- available in the proof as `α` is included
+  (a : α)       -- available in the proof as mentioned in the header
+  {β : Type}    -- not available in the proof
+  [ToString β]  -- not available in the proof
+
+theorem ex : a = a := rfl
+```
+After elaboration of the proof, the following warning will be generated to highlight the unused
+hypothesis:
+```
+included section variable '[ToString α]' is not used in 'ex', consider excluding it
+```
+In such cases, the offending variable declaration should be moved down or into a section so that
+only theorems that do depend on it follow it until the end of the section.
 -/
 @[builtin_command_parser] def «variable»     := leading_parser
   "variable" >> many1 (ppSpace >> checkColGt >> Term.bracketedBinder)
@@ -703,8 +726,13 @@ list, so it should be brief.
 @[builtin_command_parser] def genInjectiveTheorems := leading_parser
   "gen_injective_theorems% " >> ident
 
-/-- To be implemented. -/
-@[builtin_command_parser] def «include» := leading_parser "include " >> many1 (checkColGt >> ident)
+/--
+`include eeny meeny` instructs Lean to include the section `variable`s `eeny` and `meeny` in all
+declarations in the remainder of the current section, differing from the default behavior of
+conditionally including variables based on use in the declaration header. `include` is usually
+followed by the `in` combinator to limit the inclusion to the subsequent declaration.
+-/
+@[builtin_command_parser] def «include» := leading_parser "include " >> many1 ident
 
 /-- No-op parser used as syntax kind for attaching remaining whitespace at the end of the input. -/
 @[run_builtin_parser_attribute_hooks] def eoi : Parser := leading_parser ""

src/Std/Data/DHashMap/Internal/RawLemmas.lean

@@ -20,7 +20,7 @@ open Std.DHashMap.Internal.List
 
 universe u v
 
-variable {α : Type u} {β : α → Type v} [BEq α] [Hashable α]
+variable {α : Type u} {β : α → Type v}
 
 namespace Std.DHashMap.Internal
 
@@ -41,6 +41,8 @@ theorem Raw.buckets_emptyc {i : Nat} {h} :
     (∅ : Raw α β).buckets[i]'h = AssocList.nil :=
   buckets_empty
 
+variable [BEq α] [Hashable α]
+
 @[simp]
 theorem buckets_empty {c} {i : Nat} {h} :
     (empty c : DHashMap α β).1.buckets[i]'h = AssocList.nil := by
@@ -55,7 +57,9 @@ end empty
 
 namespace Raw₀
 
+variable [BEq α] [Hashable α]
 variable (m : Raw₀ α β) (h : m.1.WF)
+set_option deprecated.oldSectionVars true
 
 /-- Internal implementation detail of the hash map -/
 scoped macro "wf_trivial" : tactic => `(tactic|

src/Std/Data/DHashMap/RawLemmas.lean

@@ -75,6 +75,7 @@ namespace Raw
 open Internal.Raw₀ Internal.Raw
 
 variable {m : Raw α β} (h : m.WF)
+set_option deprecated.oldSectionVars true
 
 @[simp]
 theorem isEmpty_empty {c} : (empty c : Raw α β).isEmpty := by

src/Std/Data/HashMap/RawLemmas.lean

@@ -27,6 +27,7 @@ namespace Std.HashMap
 namespace Raw
 
 variable {m : Raw α β} (h : m.WF)
+set_option deprecated.oldSectionVars true
 
 private theorem ext {m m' : Raw α β} : m.inner = m'.inner → m = m' := by
   cases m; cases m'; rintro rfl; rfl

src/Std/Data/HashSet/Lemmas.lean

@@ -20,7 +20,7 @@ set_option autoImplicit false
 
 universe u v
 
-variable {α : Type u} {_ : BEq α} {_ : Hashable α} [EquivBEq α] [LawfulHashable α]
+variable {α : Type u} {_ : BEq α} {_ : Hashable α}
 
 namespace Std.HashSet
 

src/Std/Data/HashSet/RawLemmas.lean

@@ -27,6 +27,7 @@ namespace Std.HashSet
 namespace Raw
 
 variable {m : Raw α} (h : m.WF)
+set_option deprecated.oldSectionVars true
 
 private theorem ext {m m' : Raw α} : m.inner = m'.inner → m = m' := by
   cases m; cases m'; rintro rfl; rfl

tests/lean/run/3807.lean

@@ -2085,9 +2085,10 @@ variable {R : Type u} {A : Type v} {B : Type w} {C : Type u₁}
 
 section Semiring
 
-variable [Semiring R] [Semiring A] [Semiring B] [Semiring C]
-variable [Algebra R A] [Algebra R B] [Algebra R C]
+variable [Semiring R] [Semiring A] [Semiring B]
+variable [Algebra R A] [Algebra R B]
 
+variable [Semiring C] [Algebra R C] in
 instance funLike : FunLike (A →ₐ[R] B) A B where
   coe f := f.toFun
 
@@ -2101,6 +2102,7 @@ instance algHomClass : AlgHomClass (A →ₐ[R] B) R A B where
 @[ext]
 theorem ext {φ₁ φ₂ : A →ₐ[R] B} (H : ∀ x, φ₁ x = φ₂ x) : φ₁ = φ₂ := sorry
 
+variable [Semiring C] [Algebra R C] in
 def comp (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) : A →ₐ[R] C :=
   { φ₁.toRingHom.comp φ₂ with
     commutes' := sorry }
@@ -2400,7 +2402,7 @@ end Mathlib.FieldTheory.Subfield
 
 section Mathlib.FieldTheory.IntermediateField
 
-variable (K L L' : Type _) [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L']
+variable (K L L' : Type _) [Field K] [Field L] [Field L'] [Algebra K L]
 
 structure IntermediateField extends Subalgebra K L where
   inv_mem' : ∀ x ∈ carrier, x⁻¹ ∈ carrier
@@ -2430,7 +2432,7 @@ end IntermediateField
 
 namespace AlgHom
 
-variable (f : L →ₐ[K] L')
+variable [Algebra K L'] (f : L →ₐ[K] L')
 
 def fieldRange : IntermediateField K L' :=
   { f.range, (f : L →+* L').fieldRange with
@@ -2446,8 +2448,9 @@ def inclusion {E F : IntermediateField K L} (hEF : E ≤ F) : E →ₐ[K] F :=
 section RestrictScalars
 
 variable (K)
-variable [Algebra L' L] [IsScalarTower K L' L]
+variable [Algebra L' L]
 
+variable [Algebra K L'] [IsScalarTower K L' L] in
 def restrictScalars (E : IntermediateField L' L) : IntermediateField K L :=
   { E.toSubfield, E.toSubalgebra.restrictScalars K with
     carrier := E.carrier
@@ -2470,17 +2473,20 @@ namespace IntermediateField
 
 section AdjoinDef
 
-variable (F : Type _) [Field F] {E : Type _} [Field E] [Algebra F E] (S : Set E)
+variable (F : Type _) {E : Type _} [Field E] (S : Set E)
 
+variable [Field F] [Algebra F E] in
 def adjoin : IntermediateField F E :=
   { Subfield.closure (Set.range (algebraMap F E) ∪ S) with
     inv_mem' := sorry }
 
+variable [Field F] [Algebra F E] in
 theorem subset_adjoin : S ⊆ adjoin F S := sorry
 
 theorem subset_adjoin_of_subset_left {F : Subfield E} {T : Set E} (HT : T ⊆ F) : T ⊆ adjoin F S :=
   sorry
 
+variable [Field F] [Algebra F E] in
 theorem adjoin_subset_adjoin_iff {F' : Type _} [Field F'] [Algebra F' E] {S S' : Set E} :
     (adjoin F S : Set E) ⊆ adjoin F' S' ↔
       Set.range (algebraMap F E) ⊆ adjoin F' S' ∧ S ⊆ adjoin F' S' := sorry

tests/lean/run/calc.lean

@@ -1,5 +1,6 @@
 variable (t1 t2 t3 t4 : Nat)
 variable (pf12 : t1 = t2) (pf23 : t2 = t3) (pf34 : t3 = t4)
+include pf12 pf23 pf34
 
 theorem foo : t1 = t4 :=
   calc
@@ -9,6 +10,7 @@ theorem foo : t1 = t4 :=
 
 variable (t5 : Nat)
 variable (pf23' : t2 < t3) (pf45' : t4 < t5)
+include pf23' pf45'
 
 instance [LT α] : Trans (α := α) (· < ·) (· < ·) (· < ·) where
   trans := sorry

tests/lean/run/omega.lean

@@ -398,6 +398,9 @@ example (n : Nat) : 2 * (n * n) = n * n + n * n := by omega
 -- example (n : Nat) : 2 * n * n = n * n + n * n := by omega
 -- example (n : Nat) : n * 2 * n = n * n + n * n := by omega
 
+-- From https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/omega.20regression/near/456539091
+example (a : Nat) : a * 1 = a := by omega
+
 /-! ### Fin -/
 
 -- Test `<`

tests/lean/run/variable.lean

@@ -0,0 +1,62 @@
+/-! # Basic section variable tests -/
+
+/-! Directly referenced variables should be included. -/
+variable {n : Nat} in
+theorem t1 : n = n := by induction n <;> rfl
+
+/-! Variables mentioned only in the body should not be included. -/
+variable {n : Nat} in
+/-- error: unknown identifier 'n' -/
+#guard_msgs in
+theorem t2 : ∃ (n : Nat), n = n := by exists n
+
+/-! Variables transitively mentioned should be included. -/
+variable {n : Nat} (h : n = n) in
+theorem t3 : h = h := rfl
+
+/-! Instance variables mentioning only included variables should be included. -/
+variable {α : Type} [ToString α] in
+theorem t4 (a : α) : a = a := let _ := toString a; rfl
+
+/-! Instance variables not mentioning only included variables should not be included. -/
+variable {α β : Type} [Coe α β] in
+/--
+error: don't know how to synthesize placeholder
+context:
+α : Type
+a : α
+⊢ a = a
+-/
+#guard_msgs in
+theorem t5 (a : α) : a = a := _
+
+/-! Accidentally included variables should be warned for. -/
+variable {α : Type} [ToString α] in
+/-- warning: included section variable '[ToString α]' is not used in 't6', consider excluding it -/
+#guard_msgs in
+theorem t6 (a : α) : a = a := rfl
+
+/-! `include` should always include. -/
+variable {n : Nat} in
+include n in
+theorem t7 : ∃ (n : Nat), n = n := by exists n
+
+/-! traversal order bug broke instance inclusion -/
+variable {M N : Type} (r : N → N → Prop)
+class IsTrans (N : Type) (r : N → N → Prop) : Prop
+variable [IsTrans N r] {a b c d : N}
+/--
+warning: included section variable '[IsTrans N r]' is not used in 'act_rel_of_rel_of_act_rel', consider excluding it
+-/
+#guard_msgs in
+theorem act_rel_of_rel_of_act_rel (ab : r a b) : r a b := ab
+
+/-! More complex include case, instance should be included via `f`. -/
+class EquivLike (F : Type) (α β : Type) : Type
+variable {F : Type} [EquivLike F α β] (f : F) in
+include f in
+theorem MulEquiv.decompositionMonoid (_b : β) : α = α :=
+  let _ : EquivLike F α β := inferInstance; let _ := f; rfl
+/-- info: MulEquiv.decompositionMonoid {α β F : Type} [EquivLike F α β] (f : F) (_b : β) : α = α -/
+#guard_msgs in
+#check MulEquiv.decompositionMonoid