merge main

Std/CodeAction/Basic.lean

@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Lean.Elab.BuiltinTerm
 import Lean.Elab.BuiltinNotation
-import Std.Lean.Name
 import Std.Lean.InfoTree
 import Std.CodeAction.Attr
 

Std/CodeAction/Misc.lean

@@ -3,9 +3,11 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Lean.Elab.BuiltinTerm
+import Lean.Elab.BuiltinNotation
 import Std.Lean.Name
 import Std.Lean.Position
-import Std.CodeAction.Basic
+import Std.CodeAction.Attr
 
 /-!
 # Miscellaneous code actions

Std/Control/Nondet/Basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Std.Tactic.Lint
+import Std.Tactic.Lint.Misc
 import Std.Data.MLList.Basic
 
 /-!

Std/Data/Array/Init/Lemmas.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Std.Tactic.NoMatch
 import Std.Tactic.HaveI
 import Std.Classes.LawfulMonad
+import Std.Data.Fin.Init.Lemmas
 import Std.Data.Nat.Init.Lemmas
 import Std.Data.List.Init.Lemmas
 import Std.Data.Array.Init.Basic

Std/Data/Array/Match.lean

@@ -3,8 +3,8 @@ Copyright (c) 2023 F. G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: F. G. Dorais
 -/
-import Std.Data.Array.Basic
-import Std.Data.Array.Lemmas
+import Std.Data.Nat.Lemmas
+import Std.Data.Array.Init.Lemmas
 
 namespace Array
 

Std/Data/Int.lean

@@ -1,3 +1,4 @@
 import Std.Data.Int.Basic
 import Std.Data.Int.DivMod
+import Std.Data.Int.Gcd
 import Std.Data.Int.Lemmas

Std/Data/Int/DivMod.lean

@@ -625,6 +625,8 @@ protected theorem dvd_zero (n : Int) : n ∣ 0 := ⟨0, (Int.mul_zero _).symm⟩
 
 protected theorem dvd_refl (n : Int) : n ∣ n := ⟨1, (Int.mul_one _).symm⟩
 
+protected theorem one_dvd (n : Int) : 1 ∣ n := ⟨n, (Int.one_mul n).symm⟩
+
 protected theorem dvd_trans : ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c
   | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => ⟨d * e, by rw [Int.mul_assoc]⟩
 
@@ -689,6 +691,14 @@ theorem dvd_natAbs {a b : Int} : a ∣ b.natAbs ↔ a ∣ b :=
   | .inl e => by rw [← e]
   | .inr e => by rw [← Int.dvd_neg, ← e]
 
+theorem natAbs_dvd_self {a : Int} : (a.natAbs : Int) ∣ a := by
+  rw [Int.natAbs_dvd]
+  exact Int.dvd_refl a
+
+theorem dvd_natAbs_self {a : Int} : a ∣ (a.natAbs : Int) := by
+  rw [Int.dvd_natAbs]
+  exact Int.dvd_refl a
+
 theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natAbs := by
   rw [← natAbs_dvd_natAbs, natAbs_ofNat]
 

Std/Data/Int/Gcd.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Std.Data.Int.DivMod
+import Std.Data.Nat.Gcd
+import Std.Tactic.Simpa
+
+/-!
+# Results about `Int.gcd`.
+-/
+
+namespace Int
+
+theorem gcd_dvd_left {a b : Int} : (gcd a b : Int) ∣ a := by
+  have := Nat.gcd_dvd_left a.natAbs b.natAbs
+  rw [← Int.ofNat_dvd] at this
+  exact Int.dvd_trans this natAbs_dvd_self
+
+theorem gcd_dvd_right {a b : Int} : (gcd a b : Int) ∣ b := by
+  have := Nat.gcd_dvd_right a.natAbs b.natAbs
+  rw [← Int.ofNat_dvd] at this
+  exact Int.dvd_trans this natAbs_dvd_self
+
+@[simp] theorem one_gcd {a : Int} : gcd 1 a = 1 := by simp [gcd]
+@[simp] theorem gcd_one {a : Int} : gcd a 1 = 1 := by simp [gcd]
+
+@[simp] theorem neg_gcd {a b : Int} : gcd (-a) b = gcd a b := by simp [gcd]
+@[simp] theorem gcd_neg {a b : Int} : gcd a (-b) = gcd a b := by simp [gcd]
+
+/-- Computes the least common multiple of two integers, as a `Nat`. -/
+def lcm (m n : Int) : Nat := m.natAbs.lcm n.natAbs
+
+theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 := by
+  simp only [lcm]
+  apply Nat.lcm_ne_zero <;> simpa
+
+theorem dvd_lcm_left {a b : Int} : a ∣ lcm a b :=
+  Int.dvd_trans dvd_natAbs_self (Int.ofNat_dvd.mpr (Nat.dvd_lcm_left a.natAbs b.natAbs))
+
+theorem dvd_lcm_right {a b : Int} : b ∣ lcm a b :=
+  Int.dvd_trans dvd_natAbs_self (Int.ofNat_dvd.mpr (Nat.dvd_lcm_right a.natAbs b.natAbs))
+
+@[simp] theorem lcm_self {a : Int} : lcm a a = a.natAbs := Nat.lcm_self _

Std/Data/Int/Lemmas.lean

@@ -676,6 +676,14 @@ protected theorem lt_of_lt_of_le {a b c : Int} (h₁ : a < b) (h₂ : b ≤ c) :
 protected theorem lt_trans {a b c : Int} (h₁ : a < b) (h₂ : b < c) : a < c :=
   Int.lt_of_le_of_lt (Int.le_of_lt h₁) h₂
 
+instance : Trans (α := Int) (· ≤ ·) (· ≤ ·) (· ≤ ·) := ⟨Int.le_trans⟩
+
+instance : Trans (α := Int) (· < ·) (· ≤ ·) (· < ·) := ⟨Int.lt_of_lt_of_le⟩
+
+instance : Trans (α := Int) (· ≤ ·) (· < ·) (· < ·) := ⟨Int.lt_of_le_of_lt⟩
+
+instance : Trans (α := Int) (· < ·) (· < ·) (· < ·) := ⟨Int.lt_trans⟩
+
 protected theorem le_of_not_le {a b : Int} : ¬ a ≤ b → b ≤ a := (Int.le_total a b).resolve_left
 
 protected theorem min_def (n m : Int) : min n m = if n ≤ m then n else m := rfl

Std/Data/Json.lean

@@ -3,7 +3,7 @@
  Released under Apache 2.0 license as described in the file LICENSE.
  Authors: E.W.Ayers, Wojciech Nawrocki
 -/
-import Std.Lean.Json
+import Lean.Data.Json.FromToJson
 import Lean.Syntax
 
 /-!

Std/Data/List/Basic.lean

@@ -7,7 +7,6 @@ import Std.Classes.SetNotation
 import Std.Tactic.NoMatch
 import Std.Data.Option.Init.Lemmas
 import Std.Data.Array.Init.Lemmas
-import Std.Data.List.Init.Attach
 
 namespace List
 

Std/Data/List/Init/Lemmas.lean

@@ -3,7 +3,6 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
 -/
-import Std.Data.Fin.Init.Lemmas
 import Std.Classes.SetNotation
 import Std.Logic
 

Std/Data/List/Lemmas.lean

@@ -5,8 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 import Std.Control.ForInStep.Lemmas
 import Std.Data.Bool
-import Std.Data.Fin.Lemmas
-import Std.Data.Nat.Lemmas
+import Std.Data.Fin.Basic
 import Std.Data.List.Basic
 import Std.Data.Option.Lemmas
 import Std.Classes.BEq

Std/Data/List/Perm.lean

@@ -7,6 +7,7 @@ import Std.Tactic.Relation.Rfl
 import Std.Data.List.Lemmas
 import Std.Data.List.Count
 import Std.Data.List.Pairwise
+import Std.Data.List.Init.Attach
 
 /-!
 # List Permutations

Std/Data/Nat/Basic.lean

@@ -107,6 +107,9 @@ there is some `c` such that `b = a * c`.
 -/
 instance : Dvd Nat := ⟨fun a b => ∃ c, b = a * c⟩
 
+/-- The least common multiple of `m` and `n`, defined using `gcd`. -/
+def lcm (m n : Nat) : Nat := m * n / gcd m n
+
 /-- Sum of a list of natural numbers. -/
 protected def sum (l : List Nat) : Nat := l.foldr (·+·) 0
 

Std/Data/Nat/Gcd.lean

@@ -26,9 +26,6 @@ theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
     | _+1, IH => fun _ => H1 _ _ (succ_pos _) (IH _ (mod_lt _ (succ_pos _)) _) )
     n
 
-/-- The least common multiple of `m` and `n`, defined using `gcd`. -/
-def lcm (m n : Nat) : Nat := m * n / gcd m n
-
 /-- `m` and `n` are coprime, or relatively prime, if their `gcd` is 1. -/
 @[reducible] def Coprime (m n : Nat) : Prop := gcd m n = 1
 

Std/Data/Option/Basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Std.Classes.SetNotation
-import Std.Classes.LawfulMonad
 import Std.Tactic.NoMatch
 
 namespace Option

Std/Data/Prod/Lex.lean

@@ -5,7 +5,6 @@ Authors: Jannis Limperg
 -/
 import Std.Tactic.LeftRight
 import Std.Tactic.RCases
-import Std.Logic
 
 namespace Prod
 

Std/Data/Range/Lemmas.lean

@@ -1,5 +1,6 @@
 import Std.Tactic.ByCases
 import Std.Data.List.Lemmas
+import Std.Data.List.Init.Attach
 
 namespace Std.Range
 

Std/Data/String/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg, James Gallicchio, F. G. Dorais
 -/
-
-import Std.Data.Char
 import Std.Data.Nat.Lemmas
 import Std.Data.Array.Match
 

Std/Lean/Json.lean

@@ -3,8 +3,7 @@
  Released under Apache 2.0 license as described in the file LICENSE.
  Authors: E.W.Ayers, Mario Carneiro
 -/
-
-import Lean.Data.Json
+import Lean.Data.Json.FromToJson
 import Std.Lean.Float
 
 open Lean

Std/Lean/Meta/Basic.lean

@@ -3,7 +3,9 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Jannis Limperg
 -/
-import Lean.Meta
+import Lean.Elab.Term
+import Lean.Meta.Tactic.Apply
+import Lean.Meta.Tactic.Replace
 import Std.Lean.LocalContext
 
 open Lean Lean.Meta
@@ -291,7 +293,7 @@ def isIndependentOf (L : List MVarId) (g : MVarId) : MetaM Bool := g.withContext
     -- If the goal is a subsingleton, it is independent of any other goals.
     return true
   -- Finally, we check if the goal `g` appears in the type of any of the goals `L`.
-  L.allM fun g' => do pure !((← getMVars (← g'.getType)).contains g)
+  L.allM fun g' => do pure !((← getMVarDependencies g').contains g)
 
 /-- Solve a goal by synthesizing an instance. -/
 -- FIXME: probably can just be `g.inferInstance` once leanprover/lean4#2054 is fixed

Std/Lean/Meta/Inaccessible.lean

@@ -1,4 +1,9 @@
-import Lean.Meta
+/-
+Copyright (c) 2022 Jannis Limperg. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jannis Limperg
+-/
+import Lean.Meta.InferType
 
 open Lean Lean.Meta
 

Std/Lean/Meta/Simp.lean

@@ -3,8 +3,8 @@ Copyright (c) 2022 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Gabriel Ebner, Floris van Doorn
 -/
+import Lean.Elab.Tactic.Simp
 import Std.Tactic.OpenPrivate
-import Std.Lean.Meta.DiscrTree
 
 /-!
 # Helper functions for using the simplifier.

Std/Lean/Meta/UnusedNames.lean

@@ -3,8 +3,6 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-
-import Lean.Meta
 import Std.Data.String.Basic
 
 open Lean Lean.Meta

Std/Lean/System/IO.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Std.Data.List.Lemmas
-import Std.Data.MLList.Basic
 
 /-!
 # Functions for manipulating a list of tasks

Std/Lean/Util/EnvSearch.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Shing Tak Lam. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shing Tak Lam, Daniel Selsam, Mario Carneiro
 -/
-import Lean.Modifiers
 import Std.Tactic.Lint.Misc
 
 namespace Lean

Std/Tactic/Case.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
-import Lean.Elab.Tactic
+import Lean.Elab.Tactic.Conv.Pattern
 
 /-!
 # Extensions to the `case` tactic

Std/Tactic/FalseOrByContra.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Std.Lean.Expr
+import Lean.Elab.Tactic.Basic
 import Std.Lean.Meta.Basic
 
 /-!

Std/Tactic/LibrarySearch.lean

@@ -7,6 +7,7 @@ import Std.Lean.CoreM
 import Std.Lean.Expr
 import Std.Lean.Meta.DiscrTree
 import Std.Lean.Meta.LazyDiscrTree
+import Std.Data.Option.Basic
 import Std.Tactic.SolveByElim
 import Std.Util.Pickle
 

Std/Tactic/Lint/Basic.lean

@@ -3,9 +3,8 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
 -/
-
 import Std.Util.TermUnsafe
-import Std.Lean.NameMapAttribute
+
 open Lean Meta
 
 namespace Std.Tactic.Lint

Std/Tactic/Omega/Coeffs/IntList.lean

@@ -1,5 +1,4 @@
 import Std.Tactic.Omega.IntList
-import Std.Tactic.Omega.MinNatAbs
 
 /-!
 # `Coeffs` as a wrapper for `IntList`

Std/Tactic/Omega/Constraint.lean

@@ -3,9 +3,10 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+import Std.Classes.Order
 import Std.Tactic.RCases
 import Std.Tactic.NormCast
-import Std.Tactic.Omega.OmegaM
+import Std.Tactic.Omega.Coeffs.IntList
 
 /-!
 A `Constraint` consists of an optional lower and upper bound (inclusive),

Std/Tactic/Omega/Core.lean

@@ -5,7 +5,8 @@ Authors: Scott Morrison
 -/
 import Std.Tactic.Omega.OmegaM
 import Std.Tactic.Omega.Constraint
-import Std.Data.HashMap
+import Std.Tactic.Omega.MinNatAbs
+import Std.Data.HashMap.Basic
 
 open Lean (HashSet)
 

Std/Tactic/Relation/Symm.lean

@@ -3,6 +3,8 @@ Copyright (c) 2022 Siddhartha Gadgil. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddhartha Gadgil, Mario Carneiro, Scott Morrison
 -/
+import Lean.Meta.Reduce
+import Lean.Elab.Tactic.Location
 import Std.Lean.Meta.Basic
 
 /-!

Std/Tactic/SolveByElim.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, David Renshaw
 -/
-import Std.Data.Option.Basic
 import Std.Data.Sum.Basic
 import Std.Tactic.LabelAttr
 import Std.Tactic.Relation.Symm

Std/Util/ProofWanted.lean

@@ -5,7 +5,6 @@ Authors: David Thrane Christiansen
 -/
 import Lean.Elab.Exception
 import Lean.Elab.Command
-import Lean.Parser
 
 
 open Lean Parser Elab Command