mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ ContinuousAt
    (↑(Z.localTrivAt x).toOpenPartialHomeomorph ∘
      have this := fun x ↦ { proj := x, snd := v };
      this)
    x

Tactic:
apply continuousAt_id.prodMk

Goal state after:
case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ ContinuousAt
    (fun x_1 ↦
      Z.coordChange
        (Z.indexAt
          ((have this := fun x ↦ { proj := x, snd := v };
              this)
              x_1).proj)
        (Z.indexAt x)
        ((have this := fun x ↦ { proj := x, snd := v };
            this)
            x_1).proj
        ((have this := fun x ↦ { proj := x, snd := v };
            this)
            x_1).snd)
    x
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsSeparatedMap f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂

Tactic:
by
  simp_rw [isSeparatedMap_iff_disjoint_nhds, Filter.disjoint_iff]

Goal state after:
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
⊢ IsOpen[inst✝⁶] (⋃ g, (fun x ↦ g • x) ⁻¹' U)

Tactic:
exact isOpen_iUnion fun g ↦ open_U.preimage (continuous_const_smul g)

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
Y : Type u_4
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered (⇑g ∘ f) (g x) I
⊢ IsEvenlyCovered f x I

Tactic:
convert! h.homeomorph_comp g.symm <;> ((try ext); simp)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
r : ℝ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
hr : r ≠ 0
ha₁ : IsSelfAdjoint a
⊢ cfc Real.log (cfc (fun x ↦ r • x) a) = (algebraMap ℝ A) (Real.log r) + log a

Tactic:
← cfc_comp Real.log (r • ·) a,

Goal state after:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
r : ℝ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
hr : r ≠ 0
ha₁ : IsSelfAdjoint a
⊢ cfc (Real.log ∘ fun x ↦ r • x) a = (algebraMap ℝ A) (Real.log r) + log a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
ha₂'' : ContinuousOn Real.log ((fun x ↦ x ^ n) '' spectrum ℝ a)
⊢ log (a ^ n) = n • log a

Tactic:
rw [log, ← cfc_pow_id (R := ℝ) a n ha₁, ← cfc_comp' Real.log (· ^ n) a ha₂'', log]

Goal state after:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
ha₂'' : ContinuousOn Real.log ((fun x ↦ x ^ n) '' spectrum ℝ a)
⊢ cfc (fun x ↦ Real.log (x ^ n)) a = n • cfc Real.log a
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
⊢ InjOn (⇑exp) s

Tactic:
intro t₁

Goal state after:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
⊢ t₁ ∈ s → ∀ ⦃x₂ : ℝ⦄, x₂ ∈ s → exp t₁ = exp x₂ → t₁ = x₂
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})

Tactic:
have : DiscreteTopology (f ⁻¹' {x}) :=
    (IsDiscrete.of_openPartialHomeomorph f subset_rfl h).1

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this : DiscreteTopology ↑(f ⁻¹' {x})
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case inr.refine_2
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h✝¹ : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝² : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝¹ : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this✝ : Finite ↑(f ⁻¹' {x})
hU' : IsOpen[inst✝¹] U'
hUV : ∀ (e : ↑(f ⁻¹' {x})), U' ⊆ f '' V' e
this : Nonempty E
e : ↑(f ⁻¹' {x})
s : Set X
hs : s ⊆ U'
h : IsOpen[inst✝²] (f ⁻¹' s ∩ V' e)
⊢ IsOpen[inst✝¹] s

Tactic:
have : s ⊆ (φ e).target := hs.trans <| (hUV e).trans <| by
      rw [← (φ e).image_source_eq_target, (hφ e).2]; exact image_mono inter_subset_right

Goal state after:
case inr.refine_2
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h✝¹ : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝³ : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝² : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this✝¹ : Finite ↑(f ⁻¹' {x})
hU' : IsOpen[inst✝¹] U'
hUV : ∀ (e : ↑(f ⁻¹' {x})), U' ⊆ f '' V' e
this✝ : Nonempty E
e : ↑(f ⁻¹' {x})
s : Set X
hs : s ⊆ U'
h : IsOpen[inst✝²] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
⊢ IsOpen[inst✝¹] s
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
u : ↥(unitary A)
⊢ ((mulLeft R A) u).symm = (mulLeft R A) (star u)

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : F
⊢ ‖(toSesqForm A) x‖ ≤ ‖A‖ * ‖x‖

Tactic:
exact toSesqForm_apply_norm_le

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ‖(toSesqForm (adjointAux A)) x‖ ≤ ‖adjointAux A‖ * ‖x‖

Tactic:
exact toSesqForm_apply_norm_le

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
⊢ ∀ (x : ↥(unitary A)) (i : ℝ), 0 < i ∧ i < 2 → IsPathConnected {y | (y, x) ∈ {p | dist p.1 p.2 < i}}

Tactic:
simpa using! isPathConnected_ball

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] F
⊢ (↑T).rangeᗮ = (↑(adjoint T)).ker

Tactic:
rw [← T†.ker.orthogonal_orthogonal, T†.orthogonal_ker]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] F
⊢ (↑T).rangeᗮ = (↑(adjoint (adjoint T))).range.topologicalClosureᗮ
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
f : E →L[𝕜] E
hf : (↑f).IsSymmetric
⊢ (innerSL 𝕜) x ∘SL f = (innerSL 𝕜) (f x)

Tactic:
ext; simp [hf]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsIdempotentElem T
⊢ IsSelfAdjoint T ↔ IsStarNormal T

Tactic:
refine ⟨fun h => by rw [isStarNormal_iff, h], fun h => ?_⟩
  suffices T = star T * T from this ▸ IsSelfAdjoint.star_mul_self _
  rw [← sub_eq_zero, ContinuousLinearMap.ext_iff]
  simp_rw [zero_apply, ← norm_eq_zero (E := E)]
  have :=
    calc (∀ x : E, ‖(T - star T * T) x‖ = 0) ↔ ∀ x, ‖(adjoint (1 - T)) (T x)‖ = 0 := by
          simp [star_eq_adjoint, one_def]
      _ ↔ ∀ x, ‖(1 - T) (T x)‖ = 0 := by
          simp only [isStarNormal_iff_norm_eq_adjoint.mp h.one_sub]
      _ ↔ ∀ x, ‖(T - T * T) x‖ = 0 := by simp
      _ ↔ T - T * T = 0 := by simp only [norm_eq_zero, ContinuousLinearMap.ext_iff, zero_apply]
      _ ↔ IsIdempotentElem T := by simp only [sub_eq_zero, IsIdempotentElem, eq_comm]
  exact this.mpr hT

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
⊢ A = adjoint B ↔ ∀ (i : ι) (y : F), ⟪A (b i), y⟫_𝕜 = ⟪b i, B y⟫_𝕜

Tactic:
refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => Basis.ext b fun i => ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i : ι) (y : F), ⟪A (b i), y⟫_𝕜 = ⟪b i, B y⟫_𝕜
i : ι
⊢ A (b i) = (adjoint B) (b i)
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ι → P
hi : AffineIndependent k p
⊢ 1 ≤ Fintype.card ι

Tactic:
exact Fintype.card_pos

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace 𝕜 H
inst✝ : CompleteSpace H
u v : ↥(unitary (H →L[𝕜] H))
⊢ (let __src := ↑(u * v);
    { toLinearMap := ↑__src, invFun := ⇑↑↑(star (u * v)), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }) =
    (let __src := ↑u;
      { toLinearMap := ↑__src, invFun := ⇑↑↑(star u), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }) *
      let __src := ↑v;
      { toLinearMap := ↑__src, invFun := ⇑↑↑(star v), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : InnerProductSpace 𝕜 F
m : Type u_5
n : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
v₁ : OrthonormalBasis n 𝕜 E
v₂ : OrthonormalBasis m 𝕜 F
A : Matrix m n 𝕜
⊢ (toLin v₂.toBasis v₁.toBasis) Aᴴ = adjoint ((toLin v₁.toBasis v₂.toBasis) A)

Tactic:
refine eq_adjoint_iff_basis v₂.toBasis v₁.toBasis _ _ |>.mpr fun i j ↦ ?_
  simp_rw [toLin_self]
  simp [sum_inner, inner_smul_left, inner_sum, inner_smul_right,
    orthonormal_iff_ite.mp v₁.orthonormal, orthonormal_iff_ite.mp v₂.orthonormal]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k (Set.range p) ≤ sp
hc : Fintype.card ι = finrank k ↥sp.direction + 1
⊢ affineSpan k (Set.range p) = sp

Tactic:
rw [← Finset.card_univ] at hc
  rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image] at hle ⊢
  exact hi.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hle hc

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p ↦ if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) ⋯
p : P
hp : p ∈ t
⊢ (fun p ↦ (lineMap q ↑p) ↑(w p)) ⟨p, hp⟩ ∈ u

Tactic:
by_cases hps : p ∈ s <;>
    simp only [w, hps, lineMap_apply_one, Units.val_mk0, dif_neg, dif_pos, not_false_iff,
      Units.val_one] <;>
    [exact hsu hps; exact hf p]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ p₃ ∈ line[k, p₁, p₂]

Tactic:
rw [collinear_iff_of_mem hp₁] at h

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
h : ∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁
p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ p₃ ∈ line[k, p₁, p₂]
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

Tactic:
have hf' : ¬FiniteDimensional k (vectorSpan k (insert p (s : Set P))) := by
      intro h
      have h' : s.direction ≤ vectorSpan k (insert p (s : Set P)) := by
        conv_lhs => rw [← affineSpan_coe s, direction_affineSpan]
        exact vectorSpan_mono k (Set.subset_insert _ _)
      exact hf (Submodule.finiteDimensional_of_le h')
    rw [finrank_of_infinite_dimensional hf, finrank_of_infinite_dimensional hf', zero_add]
    exact zero_le_one

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case pos.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
hs : s = ⊥
⊢ finrank k ↥(vectorSpan k (insert p ∅)) ≤ finrank k ↥⊥ + 1

Tactic:
finrank_bot,

Goal state after:
case pos.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
hs : s = ⊥
⊢ finrank k ↥(vectorSpan k (insert p ∅)) ≤ 0 + 1
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f 0
i : α
⊢ ¬c • f i = 0 → ¬f i = 0

Tactic:
exact not_imp_not.mpr fun hf' => hf'.symm ▸ smul_zero c

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
i : α
hp : ∞ ≠ 0
f : ↥(lp E ∞)
⊢ ‖↑f i‖ ≤ ‖f‖

Tactic:
have : Nonempty α := ⟨i⟩

Goal state after:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
i : α
hp : ∞ ≠ 0
f : ↥(lp E ∞)
this : Nonempty α
⊢ ‖↑f i‖ ≤ ‖f‖
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p
i : α
x : E i
⊢ ‖lp.single p i x‖ = ‖x‖

Tactic:
have : Nonempty α := ⟨i⟩

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p
i : α
x : E i
this : Nonempty α
⊢ ‖lp.single p i x‖ = ‖x‖
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
this : 0 < 1 + ‖x‖ ^ 2
⊢ ‖x‖ ^ 2 < √(1 + ‖x‖ ^ 2) ^ 2

Tactic:
Real.sq_sqrt this.le

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
this : 0 < 1 + ‖x‖ ^ 2
⊢ ‖x‖ ^ 2 < 1 + ‖x‖ ^ 2
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p✝ q✝ : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
p q r : ℝ≥0∞
h : p ≤ q
x✝¹ x✝ : ↥(lp E p)
⊢ ⟨↑(x✝¹ + x✝), ⋯⟩ = ⟨↑x✝¹, ⋯⟩ + ⟨↑x✝, ⋯⟩

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p✝ q✝ : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
p q r : ℝ≥0∞
h : p ≤ q
x✝¹ : 𝕜
x✝ : ↥(lp E p)
⊢ ⟨↑(x✝¹ • x✝), ⋯⟩ = (RingHom.id 𝕜) x✝¹ • ⟨↑x✝, ⋯⟩

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case pos
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddGroup G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
H : ∀ p ∈ s, ∀ (x : G), g p x = 0
⊢ EqOn (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (fun x ↦ 0) (s ×ˢ univ)

Tactic:
rintro ⟨p, x⟩ ⟨hp, -⟩

Goal state after:
case pos
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddGroup G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
H : ∀ p ∈ s, ∀ (x : G), g p x = 0
p : P
x : G
hp : (p, x).1 ∈ s
⊢ (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (p, x) = (fun x ↦ 0) (p, x)