chore: golf proofs (leanprover-community#33549)

euprunin · euprunin · commit 9afc927ed5e6 · 2026-01-06T12:33:41.000Z
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean
@@ -234,7 +234,6 @@ lemma face_eq_ofSimplex {n : ℕ} (S : Finset (Fin (n + 1))) (m : ℕ) (e : Fin
         monotone' := (objEquiv x).toOrderHom.monotone }
     refine ⟨Quiver.Hom.op
       (SimplexCategory.Hom.mk ((e.symm.toOrderEmbedding.toOrderHom.comp φ))), ?_⟩
-    obtain ⟨f, rfl⟩ := objEquiv.symm.surjective x
     ext j : 1
     simpa only [Subtype.ext_iff] using e.apply_symm_apply ⟨_, hx j⟩
   · simp
diff --git a/Mathlib/CategoryTheory/Generator/Presheaf.lean b/Mathlib/CategoryTheory/Generator/Presheaf.lean
@@ -60,9 +60,8 @@ lemma freeYonedaHomEquiv_comp {X : C} {M : A} {F G : Cᵒᵖ ⥤ A}
 lemma freeYonedaHomEquiv_symm_comp {X : C} {M : A} {F G : Cᵒᵖ ⥤ A} (α : M ⟶ F.obj (op X))
     (f : F ⟶ G) :
     freeYonedaHomEquiv.symm α ≫ f = freeYonedaHomEquiv.symm (α ≫ f.app (op X)) := by
-  obtain ⟨β, rfl⟩ := freeYonedaHomEquiv.surjective α
   apply freeYonedaHomEquiv.injective
-  simp only [Equiv.symm_apply_apply, freeYonedaHomEquiv_comp, Equiv.apply_symm_apply]
+  simp only [freeYonedaHomEquiv_comp, Equiv.apply_symm_apply]
 
 variable (C)
 
diff --git a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
@@ -257,17 +257,13 @@ noncomputable def add (f₁ f₂ : X' ⟶ Y') : X' ⟶ Y' :=
 @[reassoc]
 lemma add_comp (f₁ f₂ : X' ⟶ Y') (g : Y' ⟶ Z') :
     add W eX eY f₁ f₂ ≫ g = add W eX eZ (f₁ ≫ g) (f₂ ≫ g) := by
-  obtain ⟨f₁, rfl⟩ := (homEquiv eX eY).symm.surjective f₁
-  obtain ⟨f₂, rfl⟩ := (homEquiv eX eY).symm.surjective f₂
   obtain ⟨g, rfl⟩ := (homEquiv eY eZ).symm.surjective g
   simp [add]
 
 @[reassoc]
 lemma comp_add (f : X' ⟶ Y') (g₁ g₂ : Y' ⟶ Z') :
     f ≫ add W eY eZ g₁ g₂ = add W eX eZ (f ≫ g₁) (f ≫ g₂) := by
   obtain ⟨f, rfl⟩ := (homEquiv eX eY).symm.surjective f
-  obtain ⟨g₁, rfl⟩ := (homEquiv eY eZ).symm.surjective g₁
-  obtain ⟨g₂, rfl⟩ := (homEquiv eY eZ).symm.surjective g₂
   simp [add]
 
 lemma add_eq_add {X'' Y'' : C} (eX' : L.obj X'' ≅ X') (eY' : L.obj Y'' ≅ Y')
diff --git a/Mathlib/Data/QPF/Univariate/Basic.lean b/Mathlib/Data/QPF/Univariate/Basic.lean
@@ -78,7 +78,6 @@ theorem id_map {α : Type _} (x : F α) : id <$> x = x := by
 theorem comp_map {α β γ : Type _} (f : α → β) (g : β → γ) (x : F α) :
     (g ∘ f) <$> x = g <$> f <$> x := by
   rw [← abs_repr x]
-  obtain ⟨a, f⟩ := repr x
   rw [← abs_map, ← abs_map, ← abs_map]
   rfl
 
diff --git a/Mathlib/Data/Seq/Computation.lean b/Mathlib/Data/Seq/Computation.lean
@@ -409,7 +409,6 @@ theorem get_thinkN (n) : get (thinkN s n) = get s :=
 theorem get_promises : s ~> get s := fun _ => get_eq_of_mem _
 
 theorem mem_of_promises {a} (p : s ~> a) : a ∈ s := by
-  obtain ⟨h⟩ := h
   obtain ⟨a', h⟩ := h
   rw [p h]
   exact h
diff --git a/Mathlib/Data/Sigma/Lex.lean b/Mathlib/Data/Sigma/Lex.lean
@@ -51,7 +51,6 @@ theorem lex_iff : Lex r s a b ↔ r a.1 b.1 ∨ ∃ h : a.1 = b.1, s b.1 (h.rec
     · exact Or.inl hij
     · exact Or.inr ⟨rfl, hab⟩
   · obtain ⟨i, a⟩ := a
-    obtain ⟨j, b⟩ := b
     dsimp only
     rintro (h | ⟨rfl, h⟩)
     · exact Lex.left _ _ h
@@ -153,7 +152,6 @@ theorem lex_iff {a b : Σ' i, α i} :
     · exact Or.inl hij
     · exact Or.inr ⟨rfl, hab⟩
   · obtain ⟨i, a⟩ := a
-    obtain ⟨j, b⟩ := b
     dsimp only
     rintro (h | ⟨rfl, h⟩)
     · exact Lex.left _ _ h
diff --git a/Mathlib/Data/WSeq/Basic.lean b/Mathlib/Data/WSeq/Basic.lean
@@ -433,7 +433,6 @@ theorem eq_or_mem_iff_mem {s : WSeq α} {a a' s'} :
     simp at this
   · obtain ⟨i1, i2⟩ := this
     rw [i1, i2]
-    obtain ⟨f, al⟩ := s'
     dsimp only [cons, Membership.mem, WSeq.Mem, Seq.Mem, Seq.cons]
     have h_a_eq_a' : a = a' ↔ some (some a) = some (some a') := by simp
     rw [h_a_eq_a']
diff --git a/Mathlib/LinearAlgebra/Basis/Submodule.lean b/Mathlib/LinearAlgebra/Basis/Submodule.lean
@@ -64,7 +64,6 @@ theorem Basis.eq_bot_of_rank_eq_zero [NoZeroDivisors R] (b : Basis ι R M) (N :
   refine ⟨1, fun _ => ⟨x, hx⟩, ?_, one_ne_zero⟩
   rw [Fintype.linearIndependent_iff]
   rintro g sum_eq i
-  obtain ⟨_, hi⟩ := i
   simp only [Fin.default_eq_zero, Finset.univ_unique,
     Finset.sum_singleton] at sum_eq
   convert (b.smul_eq_zero.mp sum_eq).resolve_right x_ne
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean
@@ -179,7 +179,6 @@ theorem foldr'Aux_apply_apply (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R]
 theorem foldr'Aux_foldr'Aux (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N)
     (hf : ∀ m x fx, f m (ι Q m * x, f m (x, fx)) = Q m • fx) (v : M) (x_fx) :
     foldr'Aux Q f v (foldr'Aux Q f v x_fx) = Q v • x_fx := by
-  obtain ⟨x, fx⟩ := x_fx
   simp only [foldr'Aux_apply_apply]
   rw [← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, hf, Prod.smul_mk]
 
diff --git a/Mathlib/Logic/Equiv/Fin/Rotate.lean b/Mathlib/Logic/Equiv/Fin/Rotate.lean
@@ -102,7 +102,6 @@ theorem lt_finRotate_iff_ne_neg_one [NeZero n] (i : Fin n) :
 
 lemma coe_finRotate_symm_of_ne_zero [NeZero n] {i : Fin n} (hi : i ≠ 0) :
     ((finRotate _).symm i : ℕ) = i - 1 := by
-  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
   rwa [finRotate_succ_symm_apply, Fin.val_sub_one_of_ne_zero]
 
 theorem finRotate_symm_lt_iff_ne_zero [NeZero n] (i : Fin n) :
diff --git a/Mathlib/ModelTheory/DirectLimit.lean b/Mathlib/ModelTheory/DirectLimit.lean
@@ -241,8 +241,6 @@ theorem funMap_quotient_mk'_sigma_mk' {n : ℕ} {F : L.Functions n} {i : ι} {x
 theorem relMap_quotient_mk'_sigma_mk' {n : ℕ} {R : L.Relations n} {i : ι} {x : Fin n → G i} :
     RelMap R (fun a => (⟦.mk f i (x a)⟧ : DirectLimit G f)) = RelMap R x := by
   rw [relMap_quotient_mk']
-  obtain ⟨k, _, _⟩ :=
-    directed_of (· ≤ ·) i (Classical.choose (Finite.bddAbove_range fun _ : Fin n => i))
   rw [relMap_equiv_unify G f R (fun a => .mk f i (x a)) i (fun _ ⟨_, hj⟩ => le_of_eq hj.symm)]
   rw [unify_sigma_mk_self]
 
diff --git a/Mathlib/NumberTheory/ModularForms/Basic.lean b/Mathlib/NumberTheory/ModularForms/Basic.lean
@@ -546,7 +546,6 @@ def mcast {a b : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} (h : a = b) (f : ModularF
 theorem gradedMonoid_eq_of_cast {Γ : Subgroup (GL (Fin 2) ℝ)} {a b : GradedMonoid (ModularForm Γ)}
     (h : a.fst = b.fst) (h2 : mcast h a.snd = b.snd) : a = b := by
   obtain ⟨i, a⟩ := a
-  obtain ⟨j, b⟩ := b
   cases h
   exact congr_arg _ h2
 
diff --git a/Mathlib/Topology/Sheaves/Stalks.lean b/Mathlib/Topology/Sheaves/Stalks.lean
@@ -247,7 +247,6 @@ lemma pullback_obj_obj_ext {Z : C} {f : X ⟶ Y} {F : Y.Presheaf C} (U : (Opens
         ((pullback C f).obj F).map (homOfLE hV).op ≫ φ =
       ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫
         ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ) : φ = ψ := by
-  obtain ⟨U⟩ := U
   apply ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit F _).hom_ext
   rintro ⟨⟨V⟩, ⟨⟩, ⟨b⟩⟩
   simpa [pushforwardPullbackAdjunction, Functor.lanAdjunction_unit]
