mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

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
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ (DFinsupp.sumAddHom fun i ↦ AddSubmonoidClass.subtype (V i))
      (DFinsupp.equivFunOnFintype.symm fun i ↦ (V i).orthogonalProjectionOnto x) =
    x

Tactic:
]

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
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ (DFinsupp.sumAddHom fun i ↦ AddSubmonoidClass.subtype (V i))
      (DFinsupp.equivFunOnFintype.symm fun i ↦ (V i).orthogonalProjectionOnto x) =
    x
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

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
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ ((DFinsupp.equivFunOnFintype.symm fun i ↦ (V i).orthogonalProjectionOnto x).sum fun x ↦
      ⇑(AddSubmonoidClass.subtype (V x))) =
    x

Tactic:
]

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
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ ((DFinsupp.equivFunOnFintype.symm fun i ↦ (V i).orthogonalProjectionOnto x).sum fun x ↦
      ⇑(AddSubmonoidClass.subtype (V x))) =
    x
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

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
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ ∑ i,
      (AddSubmonoidClass.subtype (V i))
        (DFinsupp.equivFunOnFintype (DFinsupp.equivFunOnFintype.symm fun i ↦ (V i).orthogonalProjectionOnto x) i) =
    x

pp: case hf
𝕜 : 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
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ ∀ (i : ι), (AddSubmonoidClass.subtype (V i)) 0 = 0

Tactic:
]

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
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ ∑ i,
      (AddSubmonoidClass.subtype (V i))
        (DFinsupp.equivFunOnFintype (DFinsupp.equivFunOnFintype.symm fun i ↦ (V i).orthogonalProjectionOnto x) i) =
    x

case hf
𝕜 : 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
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ ∀ (i : ι), (AddSubmonoidClass.subtype (V i)) 0 = 0
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n ↦ g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n ↦ ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), f (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n ↦ y - h^[n] y) atTop (𝓝 (f x))
⊢ Tendsto (fun t ↦ (1 / 2) ^ t * ‖y‖) atTop (𝓝 (0 * ‖y‖))

Tactic:
]

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n ↦ g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n ↦ ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), f (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n ↦ y - h^[n] y) atTop (𝓝 (f x))
⊢ Tendsto (fun t ↦ (1 / 2) ^ t * ‖y‖) atTop (𝓝 (0 * ‖y‖))
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ ∀ x ∈ (span 𝕜 v)ᗮ, x = 0

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ ∀ x ∈ (span 𝕜 v)ᗮ, x = 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
⊢ edist x.ofLp.1 y.ofLp.1 ≤ edist x y ∧ edist x.ofLp.2 y.ofLp.2 ≤ edist x y

Tactic:
]

Goal state after:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
⊢ edist x.ofLp.1 y.ofLp.1 ≤ edist x y ∧ edist x.ofLp.2 y.ofLp.2 ≤ edist x y
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
⊢ LipschitzWith 1 ofLp

Tactic:
intro x y
  change max _ _ ≤ _
  rw [ENNReal.coe_one, one_mul, sup_le_iff]
  exact edist_proj_le_edist_aux p x y

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

Goal state before:
pp: case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    ↑(2 ^ (ENNReal.toReal 1 / p.toReal)) * edist x.ofLp y.ofLp

Tactic:
]

Goal state after:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    ↑(2 ^ (ENNReal.toReal 1 / p.toReal)) * edist x.ofLp y.ofLp
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
⊢ comap (fun x ↦ (x.1.ofLp, x.2.ofLp)) (𝓤 (α × β)) = 𝓤 (WithLp p (α × β))

Tactic:
]

Goal state after:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
⊢ comap (fun x ↦ (x.1.ofLp, x.2.ofLp)) (𝓤 (α × β)) = 𝓤 (WithLp p (α × β))
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : e ∉ v
⊢ Pairwise fun i j ↦ ⟪↑i, ↑j⟫_𝕜 = 0

Tactic:
have h_end : ∀ a ∈ v, ⟪a, e⟫ = 0 := by
        intro a ha
        exact he' a (Submodule.subset_span ha)

Goal state after:
case mp.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
⊢ Pairwise fun i j ↦ ⟪↑i, ↑j⟫_𝕜 = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp.refine_2.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
hb : b ∈ v
⊢ ⟪↑⟨b, hb'⟩, ↑⟨a, ha'⟩⟫_𝕜 = 0

Tactic:
]

Goal state after:
case mp.refine_2.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
hb : b ∈ v
⊢ ⟪↑⟨b, hb'⟩, ↑⟨a, ha'⟩⟫_𝕜 = 0
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n ↦ g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n ↦ ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), f (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n ↦ y - h^[n] y) atTop (𝓝 (f x))
L₂ : Tendsto (fun n ↦ y - h^[n] y) atTop (𝓝 (y - 0))
feq : f x = y
⊢ ∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖

Tactic:
]

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
C : ℝ
C0 : C ≥ 0
g : F → E
hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖
h : F → F := fun y ↦ y - f (g y)
hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖
y : F
hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖
u : ℕ → E := fun n ↦ g (h^[n] y)
ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)
sNu : Summable fun n ↦ ‖u n‖
su : Summable u
x : E := tsum u
x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖
fsumeq : ∀ (n : ℕ), f (∑ i ∈ Finset.range n, u i) = y - h^[n] y
this : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)
L₁ : Tendsto (fun n ↦ y - h^[n] y) atTop (𝓝 (f x))
L₂ : Tendsto (fun n ↦ y - h^[n] y) atTop (𝓝 (y - 0))
feq : f x = y
⊢ ∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
f : WithLp ∞ (α × β)
⊢ max ‖f.fst‖₊ ‖f.snd‖₊ = max ‖f.fst‖₊ ‖f.snd‖₊

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ x ∈ (span 𝕜 v)ᗮ, x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : x ∉ v
y : E
hy : y ∈ span 𝕜 v
hxv' : ⟨x, hxu⟩ ∉ Subtype.val ⁻¹' v
⊢ y ∈ span 𝕜 (Subtype.val '' Subtype.val ⁻¹' v)

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ x ∈ (span 𝕜 v)ᗮ, x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : x ∉ v
y : E
hy : y ∈ span 𝕜 v
hxv' : ⟨x, hxu⟩ ∉ Subtype.val ⁻¹' v
⊢ y ∈ span 𝕜 (Subtype.val '' Subtype.val ⁻¹' v)
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ (‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2) ^ (1 / ↑2) = (‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2) ^ (1 / 2)

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ (‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2) ^ (1 / ↑2) = (‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2) ^ (1 / 2)
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
⊢ (span 𝕜 v)ᗮ = ⊥ ↔ ∃ b, ⇑b = Subtype.val

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
⊢ (span 𝕜 v)ᗮ = ⊥ ↔ ∃ b, ⇑b = Subtype.val
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
⊢ span 𝕜 v = ⊤ ↔ ∃ b, ⇑b = Subtype.val

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
⊢ span 𝕜 v = ⊤ ↔ ∃ b, ⇑b = Subtype.val
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ ‖x.fst‖₊ ^ 2 + ‖x.snd‖₊ ^ 2 = ‖x.fst‖₊ ^ 2 + ‖x.snd‖₊ ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
⊢ z = z

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
hv_coe : Set.range Subtype.val = v
h : Basis (↑v) 𝕜 E
coe_h : ⇑h = Subtype.val
⊢ span 𝕜 v = span 𝕜 v

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : f (x + w) = z
⊢ f (x + w) ∈ ⇑f '' s

Tactic:
]

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : f (x + w) = z
⊢ f (x + w) ∈ ⇑f '' s
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x₁ x₂ : α
⊢ ‖x₁ - x₂‖₊ = ‖x₁ - x₂‖₊

Tactic:
]

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

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
y₁ y₂ : β
⊢ ‖y₁ - y₂‖₊ = ‖y₁ - y₂‖₊

Tactic:
]

Goal state after:
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∀ (x : Fin n → α) (x_1 : Matrix (Fin m) (Fin n) α), P (of (vecCons x x_1))) ↔
    ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x

Tactic:
exact Iff.symm Fin.forall_fin_succ_pi

Goal state after:
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: case refine_1
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ A j 0 = A j 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : ‖z - y‖ < ε / C
w : E
wim : f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : f (x + w) = z
⊢ ‖z - y‖ < ε / C

Tactic:
]

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : ‖z - y‖ < ε / C
w : E
wim : f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : f (x + w) = z
⊢ ‖z - y‖ < ε / C
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A * star A = 1
⊢ A * star A = 1

Tactic:
]

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A * star A = 1
⊢ A * star A = 1
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i : ι
a : β i
⊢ a = a

Tactic:
]

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

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i i' : ι
h : i' ≠ i
a : β i
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i i' : ι
h : i ≠ i'
a : β i
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero 𝕜
i : ι
a : 𝕜
j : ι
⊢ Pi.single i a j = Pi.single i a j

Tactic:
]

Goal state after: