chore: adaptations for leanprover/lean4#2973 (#9161)

This is a PR to Mathlib's `bump/v4.5.0` branch, containing adaptations required for leanprover/lean4#2973, which landed in `leanprover/lean4:nightly-2023-12-19` and will become part of `v4.5.0-rc1` soon. Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Dec 21, 2023 · 5e6437b · 5e6437b
1 parent 043df18
commit 5e6437b
Show file tree

Hide file tree

Showing 11 changed files with 14 additions and 19 deletions.
diff --git a/Mathlib/Data/List/Func.lean b/Mathlib/Data/List/Func.lean
@@ -106,7 +106,6 @@ theorem length_set : ∀ {m : ℕ} {as : List α}, as {m ↦ a}.length = max as.
     · simp [Nat.le_add_right]
       exact Nat.succ_le_succ (Nat.zero_le _)
   | m + 1, [] => by
-    have := @length_set m []
     simp [set, length, @length_set m, Nat.zero_max]
   | m + 1, _ :: as => by
     simp [set, length, @length_set m, Nat.succ_max_succ]

diff --git a/Mathlib/Data/List/Join.lean b/Mathlib/Data/List/Join.lean
@@ -52,8 +52,7 @@ theorem join_filter_isEmpty_eq_false [DecidablePred fun l : List α => l.isEmpty
   | [] :: L => by
       simp [join_filter_isEmpty_eq_false (L := L), isEmpty_iff_eq_nil]
   | (a :: l) :: L => by
-      have cons_not_empty : isEmpty (a :: l) = false := rfl
-      simp [join_filter_isEmpty_eq_false (L := L), cons_not_empty]
+      simp [join_filter_isEmpty_eq_false (L := L), isEmpty_cons]
 #align list.join_filter_empty_eq_ff List.join_filter_isEmpty_eq_false
 
 @[simp]

diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean
@@ -174,9 +174,7 @@ theorem binaryRec_eq' {C : ℕ → Sort*} {z : C 0} {f : ∀ b n, C n → C (bit
     simp only [imp_false, or_false_iff, eq_self_iff_true, not_true] at h
     exact h.symm
   · dsimp only []
-    -- Porting note: this line was `generalize_proofs e`:
-    generalize @id (C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
-      (Eq.symm (bit_decomp (bit b n)) ▸ Eq.refl (C (bit b n))) = e
+    generalize_proofs e
     revert e
     rw [bodd_bit, div2_bit]
     intros

diff --git a/Mathlib/Data/PFun.lean b/Mathlib/Data/PFun.lean
@@ -342,7 +342,7 @@ theorem fixInduction_spec {C : α → Sort*} {f : α →. Sum β α} {b : β} {a
     @fixInduction _ _ C _ _ _ h H = H a h fun a' h' => fixInduction (fix_fwd h h') H := by
   unfold fixInduction
   -- Porting note: `generalize` required to address `generalize_proofs` bug
-  generalize (Part.mem_assert_iff.1 h).fst = ha
+  generalize @fixInduction.proof_1 α β f b a h = ha
   induction ha
   rfl
 #align pfun.fix_induction_spec PFun.fixInduction_spec

diff --git a/Mathlib/Data/Stream/Init.lean b/Mathlib/Data/Stream/Init.lean
@@ -432,7 +432,6 @@ theorem get_interleave_left : ∀ (n : Nat) (s₁ s₂ : Stream' α),
   | n + 1, s₁, s₂ => by
     change get (s₁ ⋈ s₂) (succ (succ (2 * n))) = get s₁ (succ n)
     rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons]
-    have : n < succ n := Nat.lt_succ_self n
     rw [get_interleave_left n (tail s₁) (tail s₂)]
     rfl
 #align stream.nth_interleave_left Stream'.get_interleave_left

diff --git a/Mathlib/Init/Data/Nat/Bitwise.lean b/Mathlib/Init/Data/Nat/Bitwise.lean
@@ -10,6 +10,7 @@ import Mathlib.Init.Data.Bool.Lemmas
 import Mathlib.Init.ZeroOne
 import Mathlib.Tactic.Cases
 import Mathlib.Tactic.Says
+import Mathlib.Tactic.GeneralizeProofs
 
 #align_import init.data.nat.bitwise from "leanprover-community/lean"@"53e8520d8964c7632989880372d91ba0cecbaf00"
 
@@ -341,9 +342,8 @@ theorem binaryRec_eq {C : Nat → Sort u} {z : C 0} {f : ∀ b n, C n → C (bit
     rfl
   case neg h' =>
     simp only [dif_neg h]
-    generalize @id (C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
-      (Eq.symm (bit_decomp (bit b n)) ▸ Eq.refl (C (bit b n))) = e
-    revert e
+    generalize_proofs h
+    revert h
     rw [bodd_bit, div2_bit]
     intros; rfl
 #align nat.binary_rec_eq Nat.binaryRec_eq

diff --git a/Mathlib/RingTheory/Localization/Basic.lean b/Mathlib/RingTheory/Localization/Basic.lean
@@ -811,7 +811,7 @@ theorem isLocalization_iff_of_algEquiv [Algebra R P] (h : S ≃ₐ[R] P) :
 #align is_localization.is_localization_iff_of_alg_equiv IsLocalization.isLocalization_iff_of_algEquiv
 
 theorem isLocalization_iff_of_ringEquiv (h : S ≃+* P) :
-    IsLocalization M S ↔ have := (h.toRingHom.comp <| algebraMap R S).toAlgebra;
+    IsLocalization M S ↔ haveI := (h.toRingHom.comp <| algebraMap R S).toAlgebra;
       IsLocalization M P :=
   letI := (h.toRingHom.comp <| algebraMap R S).toAlgebra
   isLocalization_iff_of_algEquiv M { h with commutes' := fun _ => rfl }
@@ -820,7 +820,7 @@ theorem isLocalization_iff_of_ringEquiv (h : S ≃+* P) :
 variable (S)
 
 theorem isLocalization_of_base_ringEquiv [IsLocalization M S] (h : R ≃+* P) :
-    have := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra;
+    haveI := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra;
       IsLocalization (M.map h.toMonoidHom) S := by
   letI : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
   constructor

diff --git a/Mathlib/Tactic/Clean.lean b/Mathlib/Tactic/Clean.lean
@@ -29,8 +29,8 @@ def clean (e : Expr) : Expr :=
     | .app (.app (.const n _) _) e' => if n ∈ cleanConsts then some e' else none
     | .app (.lam _ _ (.bvar 0) _) e' => some e'
     | e =>
-      match letFunAnnotation? e with
-      | some (.app (.lam _ _ (.bvar 0) _) e') => some e'
+      match e.letFun? with
+      | some (_n, _t, v, .bvar 0) => some v
       | _ => none
 
 end Lean.Expr

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "71e11a6be0e43dabcba416e1af15b5bbbbfc9dde",
+   "rev": "a17925cb39040c461c92ce63cd152f1767b02832",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "bump/v4.5.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",

diff --git a/lakefile.lean b/lakefile.lean
@@ -26,7 +26,7 @@ package mathlib where
 meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 
-require std from git "https://github.com/leanprover/std4" @ "main"
+require std from git "https://github.com/leanprover/std4" @ "bump/v4.5.0"
 require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
 require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
 require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.23"

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-12-16
+leanprover/lean4:nightly-2023-12-19