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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : ¬FiniteDimensional 𝕜 ↥Kᗮ
⊢ LinearMap.det ↑K.reflection.toLinearEquiv = (-1) ^ finrank 𝕜 ↥Kᗮ

pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : FiniteDimensional 𝕜 ↥Kᗮ
⊢ LinearMap.det ↑K.reflection.toLinearEquiv = (-1) ^ finrank 𝕜 ↥Kᗮ

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 ↥K
hK : ¬FiniteDimensional 𝕜 ↥Kᗮ
⊢ LinearMap.det ↑K.reflection.toLinearEquiv = (-1) ^ finrank 𝕜 ↥Kᗮ
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : Preorder ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
this : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection
⊢ Tendsto (fun t ↦ (U t).starProjection x) atTop (𝓝 x)

Tactic:
convert! starProjection_tendsto_closure_iSup U hU x

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : Preorder ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : ⊤ ≤ (⨆ t, U t).topologicalClosure
this : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection
⊢ x = (⨆ i, U i).topologicalClosure.starProjection x
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
h : Kᗮᗮ = ⊤
⊢ Kᗮ = ⊥

pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
h : Kᗮ = ⊥
⊢ Kᗮᗮ = ⊤

Tactic:
·

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
h : Kᗮᗮ = ⊤
⊢ Kᗮ = ⊥
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
h : Kᗮ = ⊥
⊢ Kᗮᗮ = ⊤

Tactic:
·

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
h : Kᗮ = ⊥
⊢ Kᗮᗮ = ⊤
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case e'_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 ↥K + finrank 𝕜 ↥Kᗮ = finrank 𝕜 ↥K + finrank 𝕜 ↥(Kᗮ ⊓ ⊤)

pp: case e'_3
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 E = finrank 𝕜 ↥⊤

Tactic:
·

Goal state after:
case e'_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 ↥K + finrank 𝕜 ↥Kᗮ = finrank 𝕜 ↥K + finrank 𝕜 ↥(Kᗮ ⊓ ⊤)
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case e'_3
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 E = finrank 𝕜 ↥⊤

Tactic:
·

Goal state after:
case e'_3
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 E = finrank 𝕜 ↥⊤
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case pos
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker
hW : ∀ w ∈ W, φ w = w
hn' : finrank ℝ ↥Wᗮ ≤ n
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod

pp: case neg
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker
hW : ∀ w ∈ W, φ w = w
hn' : ¬finrank ℝ ↥Wᗮ ≤ n
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod

Tactic:
·

Goal state after:
case pos
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker
hW : ∀ w ∈ W, φ w = w
hn' : finrank ℝ ↥Wᗮ ≤ n
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : K.starProjection v = v
⊢ v ∈ K

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : v ∈ K
⊢ ∀ w ∈ K, ⟪v - v, w⟫ = 0

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : K.starProjection v = v
⊢ v ∈ K
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : v ∈ K
⊢ ∀ w ∈ K, ⟪v - v, w⟫ = 0

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : v ∈ K
⊢ ∀ w ∈ K, ⟪v - v, w⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v ↦ (ℝ ∙ v)ᗮ.reflection) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn : finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).ker
hW : ∀ w ∈ W, φ w = w
hn' : ¬finrank ℝ ↥Wᗮ ≤ n
⊢ 0 < finrank ℝ ↥Wᗮ

Tactic:
by lia

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : K.orthogonalProjectionOnto v = 0
⊢ v ∈ Kᗮ

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : v ∈ Kᗮ
⊢ v - ↑0 ∈ Kᗮ

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : K.orthogonalProjectionOnto v = 0
⊢ v ∈ Kᗮ
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : v ∈ Kᗮ
⊢ v - ↑0 ∈ Kᗮ

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : v ∈ Kᗮ
⊢ v - ↑0 ∈ Kᗮ
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝¹ : p.HasOrthogonalProjection
inst✝ : (map f.toLinearMap p).HasOrthogonalProjection
x : E
⊢ f (p.starProjection x) ∈ map f.toLinearMap p

pp: case refine_2
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝¹ : p.HasOrthogonalProjection
inst✝ : (map f.toLinearMap p).HasOrthogonalProjection
x : E
y : E'
hy : y ∈ map f.toLinearMap p
⊢ ⟪f x - f (p.starProjection x), y⟫ = 0

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝¹ : p.HasOrthogonalProjection
inst✝ : (map f.toLinearMap p).HasOrthogonalProjection
x : E
⊢ f (p.starProjection x) ∈ map f.toLinearMap p
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝¹ : p.HasOrthogonalProjection
inst✝ : (map f.toLinearMap p).HasOrthogonalProjection
x x' : E
hx' : x' ∈ ↑p
⊢ ⟪x - p.starProjection x, x'⟫ = 0

Tactic:
starProjection_inner_eq_zero x x' hx'

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝¹ : p.HasOrthogonalProjection
inst✝ : (map f.toLinearMap p).HasOrthogonalProjection
x x' : E
hx' : x' ∈ ↑p
⊢ 0 = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case hvm
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪v, w⟫ • v ∈ 𝕜 ∙ v

pp: case hvo
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ∀ w_1 ∈ 𝕜 ∙ v, ⟪↑‖v‖ ^ 2 • w - ⟪v, w⟫ • v, w_1⟫ = 0

Tactic:
·

Goal state after:
case hvm
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪v, w⟫ • v ∈ 𝕜 ∙ v
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case hvo
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ∀ w_1 ∈ 𝕜 ∙ v, ⟪↑‖v‖ ^ 2 • w - ⟪v, w⟫ • v, w_1⟫ = 0

Tactic:
·

Goal state after:
case hvo
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ∀ w_1 ∈ 𝕜 ∙ v, ⟪↑‖v‖ ^ 2 • w - ⟪v, w⟫ • v, w_1⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : v = 0
⊢ (𝕜 ∙ v).starProjection w = (⟪v, w⟫ / ↑(‖v‖ ^ 2)) • v

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
⊢ (𝕜 ∙ v).starProjection w = (⟪v, w⟫ / ↑(‖v‖ ^ 2)) • v

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : v = 0
⊢ (𝕜 ∙ v).starProjection w = (⟪v, w⟫ / ↑(‖v‖ ^ 2)) • v
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: case h₂
𝕜 : 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
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < ‖σ c‖
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖σ c‖ * ‖y‖
δ : ℝ := ⋯
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ ⇑f '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ ⇑f '' ball 0 ↑n
x₂ : E
h₂ : dist a (f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : f x₂ = z₂
x : E := ⋯
I : ‖f x - d • y‖ ≤ 2 * δ
J : dist (f (σ' d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ ‖x₁ - x₂‖ ≤ ↑n + ↑n

Tactic:
·

Goal state after:
case h₂
𝕜 : 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
surj : Surjective ⇑f
A : ⋃ n, closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n) = Set.univ
n : ℕ
a : F
ε : ℝ
εpos : ε > 0
H : ball a ε ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f '' ball 0 ↑n)
c : 𝕜
hc : 1 < ‖c‖
y : F
hy : y ≠ 0
hc' : 1 < ‖σ c‖
d : 𝕜'
hd : d ≠ 0
ydlt : ‖d • y‖ < ε / 2
dinv : ‖d‖⁻¹ ≤ (ε / 2)⁻¹ * ‖σ c‖ * ‖y‖
δ : ℝ := ⋯
δpos : 0 < δ
this✝ : a + d • y ∈ ball a ε
z₁ : F
z₁im : z₁ ∈ ⇑f '' ball 0 ↑n
x₁ : E
h₁ : dist (a + d • y) (f x₁) < δ
hx₁ : ‖x₁‖ < ↑n
xz₁ : f x₁ = z₁
this : a ∈ ball a ε
z₂ : F
z₂im : z₂ ∈ ⇑f '' ball 0 ↑n
x₂ : E
h₂ : dist a (f x₂) < δ
hx₂ : ‖x₂‖ < ↑n
xz₂ : f x₂ = z₂
x : E := ⋯
I : ‖f x - d • y‖ ≤ 2 * δ
J : dist (f (σ' d⁻¹ • x)) y ≤ 1 / 2 * ‖y‖
⊢ ‖x₁ - x₂‖ ≤ ↑n + ↑n
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
⊢ (∃ K, ∃ (x : K.HasOrthogonalProjection), p = ↑K.starProjection) → p.IsSymmetricProjection

Tactic:
by rintro ⟨_, _, rfl⟩; exact isSymmetricProjection_starProjection _

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : K.starProjection v = 0
w : E
hw : w ∈ K
⊢ ⟪w, v⟫ = 0

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
hv : v ∈ Kᗮ
⊢ K.starProjection v = 0

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
h : K.starProjection v = 0
w : E
hw : w ∈ K
⊢ ⟪w, v⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
hv : v ∈ Kᗮ
⊢ K.starProjection v = 0

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
hv : v ∈ Kᗮ
⊢ K.starProjection v = 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp 0 (α × β)
⊢ edist f f = 0

pp: case inr.inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp ∞ (α × β)
⊢ edist f f = 0

pp: case inr.inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp p (α × β)
h : 0 < p.toReal
⊢ edist f f = 0

Tactic:
·

Goal state after:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp 0 (α × β)
⊢ edist f f = 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr.inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp ∞ (α × β)
⊢ edist f f = 0

pp: case inr.inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp p (α × β)
h : 0 < p.toReal
⊢ edist f f = 0

Tactic:
·

Goal state after:
case inr.inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp ∞ (α × β)
⊢ edist f f = 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr.inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp p (α × β)
h : 0 < p.toReal
⊢ edist f f = 0

Tactic:
·

Goal state after:
case inr.inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp p (α × β)
h : 0 < p.toReal
⊢ edist f f = 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp 0 (α × β)
⊢ edist f g = edist g f

pp: case inr.inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp ∞ (α × β)
⊢ edist f g = edist g f

pp: case inr.inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp p (α × β)
h : 0 < p.toReal
⊢ edist f g = edist g f

Tactic:
·

Goal state after:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp 0 (α × β)
⊢ edist f g = edist g f
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr.inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp ∞ (α × β)
⊢ edist f g = edist g f

pp: case inr.inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp p (α × β)
h : 0 < p.toReal
⊢ edist f g = edist g f

Tactic:
·

Goal state after:
case inr.inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp ∞ (α × β)
⊢ edist f g = edist g f
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr.inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp p (α × β)
h : 0 < p.toReal
⊢ edist f g = edist g f

Tactic:
·

Goal state after:
case inr.inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp p (α × β)
h : 0 < p.toReal
⊢ edist f g = edist g f
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
hp : Fact (1 ≤ ∞)
f g h : WithLp ∞ (α × β)
⊢ edist f h ≤ edist f g + edist g h

pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ edist f h ≤ edist f g + edist g h

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
hp : Fact (1 ≤ ∞)
f g h : WithLp ∞ (α × β)
⊢ edist f h ≤ edist f g + edist g h
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ edist f h ≤ edist f g + edist g h

Tactic:
·

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ edist f h ≤ edist f g + edist g h
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
hp : Fact (1 ≤ ∞)
f g : WithLp ∞ (α × β)
⊢ 0 ≤ dist f g

pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ 0 ≤ dist f g

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
hp : Fact (1 ≤ ∞)
f g : WithLp ∞ (α × β)
⊢ 0 ≤ dist f g
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ 0 ≤ dist f g

Tactic:
·

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ 0 ≤ dist f g
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
hp : Fact (1 ≤ ∞)
f g : WithLp ∞ (α × β)
⊢ edist f g = ENNReal.ofReal (dist f g)

pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
hp : Fact (1 ≤ ∞)
f g : WithLp ∞ (α × β)
⊢ edist f g = ENNReal.ofReal (dist f g)
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
·

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ edist f g = ENNReal.ofReal (dist f g)