mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.ClosedSubmodule

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : TopologicalSpace M
inst✝⁷ : Module R M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : Module R N
f : M ≃L[R] N
inst✝³ : ContinuousAdd N
inst✝² : ContinuousConstSMul R N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousConstSMul R M
s : Submodule R M
x : N
⊢ x ∈ ⇑f '' closure ↑s ↔ ∃ x_1 ∈ closure ↑s, f x_1 = x

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : CompleteSpace E
f : (i : ι) → G i
hf : ∀ ε > 0, ∃ N, ∀ (m : Finset ι), N ⊆ m → ∀ (n : Finset ι), N ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε
ε : ℝ
hε : ε > 0
hε' : 0 < ε ^ 2 / 2
a : Finset ι
H : ∀ (m : Finset ι), a ⊆ m → ∀ (n : Finset ι), a ⊆ n → |∑ i ∈ m, ‖f i‖ ^ 2 - ∑ i ∈ n, ‖f i‖ ^ 2| < ε ^ 2 / 2
s₁ : Finset ι
hs₁ : a ⊆ s₁
s₂ : Finset ι
hs₂ : a ⊆ s₂
has : a ⊆ s₁ ⊓ s₂
Hs₁ : ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2
this : s₁ ⊓ s₂ ⊆ s₂
⊢ ∑ x ∈ s₂ \ s₁, ‖f x‖ ^ 2 = ∑ i ∈ s₂ \ (s₁ ⊓ s₂), ‖f i‖ ^ 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.RCLike.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ Module.rank ℝ K = Module.rank ℝ ↥⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.RCLike.Lemmas

Goal state before:
pp: case e'_3
K : Type u_1
inst✝ : RCLike K
⊢ 1 = ‖reCLM 1‖ / ‖1‖

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
hv : ⟪u, v⟫ = 0
w : E
⊢ w ∈ 𝕜 ∙ u → ⟪w, v⟫ = 0

Tactic:
hw

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
hv : ⟪u, v⟫ = 0
w : E
hw : w ∈ 𝕜 ∙ u
⊢ ⟪w, v⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Orthogonal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ ↑(⨅ v, (↑((innerSL 𝕜) ↑v)).ker) = ⋂ i, ↑(↑((innerSL 𝕜) ↑i)).ker

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ∀ u ∈ ⊤, ⟪u, 0⟫ = 0

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
x✝ : E
⊢ x✝ ∈ ↑Kᗮ ↔ x✝ ∈ ⨅ v, (↑((innerSL 𝕜) ↑v)).ker

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ x ∈ (↑⊤ᗮ).carrier ↔ x ∈ (↑⊥).carrier

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ x ∈ (↑⊥ᗮ).carrier ↔ x ∈ (↑⊤).carrier

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
⊢ x ∈ (↑K.closureᗮ).carrier ↔ x ∈ (↑{ toSubmodule := Kᗮ, isClosed' := ⋯ }).carrier

Tactic:
simp

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := (ℝ ∙ (v - w))ᗮ.reflection
this : R v + R v = w + w
⊢ 2 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case e'_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := (ℝ ∙ (v - w))ᗮ.reflection
h₁ : R (v - w) = -(v - w)
h₂ : R (v + w) = v + w
⊢ R v + R v = R (v + w) + R (v - w)

Tactic:
simp

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

Goal state before:
pp: case inl
𝕜 : 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‖
⊢ ∃ x, dist (f x) 0 ≤ 1 / 2 * ‖0‖ ∧ ‖x‖ ≤ (ε / 2)⁻¹ * ‖c‖ * 2 * ↑n * ‖0‖

Tactic:
simp

Goal state after:
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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
⊢ Kᗮ = Kᗮ ⊓ ⊤

Tactic:
simp

Goal state after:
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✝ : K.HasOrthogonalProjection
v : E
hv : v ∈ K
w : E
⊢ w ∈ Kᗮ → ⟪w, v⟫ = 0

Tactic:
hw

Goal state after:
case mpr
𝕜 : 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
w : E
hw : w ∈ Kᗮ
⊢ ⟪w, v⟫ = 0
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
K : ClosedSubmodule 𝕜 E
inst✝ : (↑K).HasOrthogonalProjection
x : E
⊢ x ∈ (↑Kᗮᗮ).carrier ↔ x ∈ (↑K).carrier

Tactic:
simp

Goal state after:
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:
simp

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

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
v : E
⊢ v - v ∈ ⊤ᗮ

Tactic:
simp

Goal state after:
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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v w : E
⊢ w ∈ K → ⟪w, v - K.starProjection v⟫ = 0

Tactic:
hw

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v w : E
hw : w ∈ K
⊢ ⟪w, v - K.starProjection v⟫ = 0
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
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
x✝ : E
⊢ Uᗮ.subtypeL ⟨x✝ - U.subtypeL (U.orthogonalProjectionOnto x✝), ⋯⟩ =
    (ContinuousLinearMap.id 𝕜 E - U.subtypeL ∘SL U.orthogonalProjectionOnto) x✝

Tactic:
simp

Goal state after:
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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : ↥K
⊢ ↑v ∈ K

Tactic:
simp

Goal state after:
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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : ↥K
⊢ ∀ w ∈ K, ⟪↑v - ↑v, w⟫ = 0

Tactic:
simp

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 = v
⊢ K.starProjection v ∈ K

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
⊢ ↑K.starProjection x ∈ K

Tactic:
simp

Goal state after:
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
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
w : F
⊢ w ∈ W → ⟪w, φ ↑v⟫_ℝ = 0

Tactic:
hw

Goal state after:
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
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
w : F
hw : w ∈ W
⊢ ⟪w, φ ↑v⟫_ℝ = 0
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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
⊢ 1 * ‖v‖ = ‖v‖

Tactic:
simp

Goal state after:
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
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
w : F
⊢ ρ (φ w) = w → w ∈ V

Tactic:
hw

Goal state after:
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
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
w : F
hw : ρ (φ w) = w
⊢ w ∈ V
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
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
w : F
hw : ρ (φ w) = w
⊢ w = ρ (φ w)

Tactic:
hw

Goal state after:
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
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
w : F
hw : ρ (φ w) = w
⊢ w = w
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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
⊢ v = ↑(K.orthogonalProjectionOnto v) + (v - ↑(K.orthogonalProjectionOnto v))

Tactic:
simp

Goal state after:
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
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
w : F
⊢ w ∈ W → w ∈ V

Tactic:
hw

Goal state after:
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
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
w : F
hw : w ∈ W
⊢ w ∈ V
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
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
w : E
⊢ K.starProjection w + Kᗮ.starProjection w = w

Tactic:
simp

Goal state after:
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
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
w : F
hw : w ∈ W
⊢ w ∈ (ℝ ∙ x)ᗮ

Tactic:
mem_orthogonal_singleton_iff_inner_left

Goal state after:
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
this : Nontrivial ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : φ ↑v ∈ Wᗮ
hv' : ↑v ∉ W
x : F := ↑v - φ ↑v
ρ : F ≃ₗᵢ[ℝ] F := (ℝ ∙ x)ᗮ.reflection
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - ↑↑(φ.trans ρ))).ker
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
w : F
hw : w ∈ W
⊢ ⟪w, x⟫_ℝ = 0
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
hp : p.IsSymmetricProjection
this : p.range.HasOrthogonalProjection
x : E
⊢ p x ∈ p.range

Tactic:
simp

Goal state after:
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
hp : p.IsSymmetricProjection
this : p.range.HasOrthogonalProjection
x : E
⊢ x - p x ∈ p.ker

Tactic:
simpa using congr($hp.isIdempotentElem.mul_one_sub_self x)

Goal state after:
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:
rintro ⟨_, _, rfl⟩; exact isSymmetricProjection_starProjection _

Goal state after:
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

Tactic:
simp

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

Goal state before:

Tactic:
C * ‖h^[n] y‖ ≤ C * ((1 / 2) ^ n * ‖y‖) := by gcongr; exact hnle n
      _ = (1 / 2) ^ n * (C * ‖y‖) := by ring

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
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‖)
⊢ 0 ≤ 1 / 2

Tactic:
simp

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

Goal state before:
pp: case zero
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
⊢ (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) 0) = 0 i

Tactic:
simp

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
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
⊢ Set.range Subtype.val = v

Tactic:
simp

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‖
⊢ f x + f w = z

Tactic:
wim,

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‖
⊢ f x + (z - y) = z
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
⊢ dist (x + w) x = ‖w‖

Tactic:
simp

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

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
p : ℝ≥0∞
x✝ : WithLp p (n → R)
i✝ : n
⊢ (((toLpLin p p) 1) x✝).ofLp i✝ = (LinearMap.id x✝).ofLp i✝

Tactic:
simp

Goal state after: