chore: bump std4 (#8548)

leanprover-community · Nov 21, 2023 · 366aa49 · 366aa49
1 parent 81e04e3
commit 366aa49
Show file tree

Hide file tree

Showing 5 changed files with 1 addition and 18 deletions.
diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
@@ -642,13 +642,6 @@ theorem isEmpty_iff_eq_nil {l : List α} : l.isEmpty ↔ l = [] := by cases l <;
 
 /-! ### dropLast -/
 
-@[simp]
-theorem length_dropLast : ∀ l : List α, length l.dropLast = length l - 1
-  | [] | [_] => rfl
-  | a::b::l => by
-    rw [dropLast, length_cons, length_cons, length_dropLast (b::l), succ_sub_one, length_cons,
-      succ_sub_one]
-    simp
 #align list.length_init List.length_dropLast
 
 /-! ### getLast -/

diff --git a/Mathlib/Data/Prod/Basic.lean b/Mathlib/Data/Prod/Basic.lean
@@ -125,9 +125,6 @@ theorem ext_iff {p q : α × β} : p = q ↔ p.1 = q.1 ∧ p.2 = q.2 := by
   rw [mk.inj_iff]
 #align prod.ext_iff Prod.ext_iff
 
-@[ext]
-theorem ext {α β} {p q : α × β} (h₁ : p.1 = q.1) (h₂ : p.2 = q.2) : p = q :=
-  ext_iff.2 ⟨h₁, h₂⟩
 #align prod.ext Prod.ext
 
 theorem map_def {f : α → γ} {g : β → δ} : Prod.map f g = fun p : α × β ↦ (f p.1, g p.2) :=

diff --git a/Mathlib/Data/Sigma/Basic.lean b/Mathlib/Data/Sigma/Basic.lean
@@ -64,9 +64,6 @@ theorem eta : ∀ x : Σa, β a, Sigma.mk x.1 x.2 = x
   | ⟨_, _⟩ => rfl
 #align sigma.eta Sigma.eta
 
-@[ext]
-theorem ext {x₀ x₁ : Sigma β} (h₀ : x₀.1 = x₁.1) (h₁ : HEq x₀.2 x₁.2) : x₀ = x₁ := by
-  cases x₀; cases x₁; cases h₀; cases h₁; rfl
 #align sigma.ext Sigma.ext
 
 theorem ext_iff {x₀ x₁ : Sigma β} : x₀ = x₁ ↔ x₀.1 = x₁.1 ∧ HEq x₀.2 x₁.2 := by
@@ -243,9 +240,6 @@ theorem mk.inj_iff {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :
     | _, _, _, _, Eq.refl _, HEq.refl _ => rfl
 #align psigma.mk.inj_iff PSigma.mk.inj_iff
 
-@[ext]
-theorem ext {x₀ x₁ : PSigma β} (h₀ : x₀.1 = x₁.1) (h₁ : HEq x₀.2 x₁.2) : x₀ = x₁ := by
-  cases x₀; cases x₁; cases h₀; cases h₁; rfl
 #align psigma.ext PSigma.ext
 
 theorem ext_iff {x₀ x₁ : PSigma β} : x₀ = x₁ ↔ x₀.1 = x₁.1 ∧ HEq x₀.2 x₁.2 := by

diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean
@@ -682,7 +682,6 @@ theorem exists_swap {p : α → β → Prop} : (∃ x y, p x y) ↔ ∃ y x, p x
 #align forall_exists_index forall_exists_index
 
 #align exists_imp_distrib exists_imp
-alias ⟨_, not_exists_of_forall_not⟩ := exists_imp
 #align not_exists_of_forall_not not_exists_of_forall_not
 
 #align Exists.some Exists.choose

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "a3b80114adc0948ff493f9acb6ee250f76922d80",
+   "rev": "e403f680f0beb8610c29e6f799132e8be880554e",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",