awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
⊢ ∃ (l : List F), l.length ≤ 0 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
have zero : φ = 1
Tactic: refine ⟨[], rfl.le, show φ = 1 from ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
⊢ (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
have rwa : ∀ (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ = 0),
  (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
Tactic: rwa [le_zero_iff, finrank_eq_zero, orthogonal_eq_bot_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
rwa :
  ∀ (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ = 0),
    (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
⊢ (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
have rwa₁ : ∀ (hn : (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ = ⊥),
  (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
Tactic: rwa [le_zero_iff, finrank_eq_zero, orthogonal_eq_bot_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
rwa :
  ∀ (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ = 0),
    (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
rwa₁ :
  ∀ (hn : (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ = ⊥),
    (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
⊢ (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
have rwa₂ : ∀ (hn : (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤),
  (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
Tactic: rwa [le_zero_iff, finrank_eq_zero, orthogonal_eq_bot_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
⊢ φ = 1
have this : (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
Tactic: have : (ContinuousLinearMap.id ℝ F - φ).ker = ⊤ := by
      rwa [le_zero_iff, finrank_eq_zero, orthogonal_eq_bot_iff] at hn
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
this : (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
⊢ φ = 1
have zero : 1 = φ
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
this : (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
⊢ 1 = φ
have zero : ∀ (x : F), Eq (α := F) ((1 : (a : F) → F) x : F) ((φ : (a : F) → F) x : F)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
this : (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
x : F
⊢ Eq (α := F) ((1 : (a : F) → F) x : F) ((φ : (a : F) → F) x : F)
have this₁ : Eq (α := F) (((↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F) : (a : F) → F) x : F)
  ((0 : (a : F) → F) x : F)
Tactic: have := LinearMap.congr_fun (LinearMap.ker_eq_top.mp this) x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
have hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
Tactic: have hW : ∀ w ∈ W, φ w = w := fun w hw => (sub_eq_zero.mp hw).symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
have pos : ∀ (hn' : finrank.{0, u_3} ℝ ↥Wᗮ ≤ n),
  ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
Tactic: by_cases hn' : finrank ℝ Wᗮ ≤ n
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
pos :
  ∀ (hn' : finrank.{0, u_3} ℝ ↥Wᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
have neg : ∀ (hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n),
  ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
Tactic: by_cases hn' : finrank ℝ Wᗮ ≤ n
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
hn' : finrank.{0, u_3} ℝ ↥Wᗮ ≤ n
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
have pos : ∀ (V : List F) (hV₁ : V.length ≤ n) (hV₂ : φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) V)),
  ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
Tactic: obtain ⟨V, hV₁, hV₂⟩ := IH φ hn'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
have this : Nontrivial.{u_3} ↥Wᗮ
Tactic: haveI : Nontrivial Wᗮ := nontrivial_of_finrank_pos (by lia : 0 < finrank ℝ Wᗮ)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n
this : Nontrivial.{u_3} ↥Wᗮ
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
have neg : ∀ (v : ↥Wᗮ) (hv : v ≠ 0),
  ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
Tactic: obtain ⟨v, hv⟩ := exists_ne (0 : Wᗮ)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n
this : Nontrivial.{u_3} ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
w : F
hw : w ∈ W
⊢ ⟪w, (φ : (a : F) → F) (↑v : F)⟫_ℝ = 0
have rw : ⟪w, (↑v : F)⟫_ℝ = 0
Tactic: rw [← hW w hw, LinearIsometryEquiv.inner_map_map]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n
this : Nontrivial.{u_3} ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
have hφv : Membership.mem (α := F) Wᗮ ((φ : (a : F) → F) (↑v : F) : F)
Tactic: have hφv : φ v ∈ Wᗮ := by
      intro w hw
      rw [← hW w hw, LinearIsometryEquiv.inner_map_map]
      exact v.prop w hw
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n
this : Nontrivial.{u_3} ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : Membership.mem (α := F) Wᗮ ((φ : (a : F) → F) (↑v : F) : F)
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
have hv' : (↑v : F) ∉ W
Tactic: have hv' : (v : F) ∉ W := by
      intro h
      exact hv ((mem_left_iff_eq_zero_of_disjoint W.orthogonal_disjoint).mp h)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n
this : Nontrivial.{u_3} ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : Membership.mem (α := F) Wᗮ ((φ : (a : F) → F) (↑v : F) : F)
hv' : (↑v : F) ∉ W
x : F := HSub.hSub (β := F) (↑v : F) ((φ : (a : F) → F) (↑v : F) : F)
ρ : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ x)ᗮ
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑(φ.trans ρ) : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
w : F
hw : (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w
⊢ w ∈ V
have change : HSub.hSub (β := F) w ((ρ : (a : F) → F) ((φ : (a : F) → F) w : F) : F) = 0
Tactic: change w - ρ (φ w) = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n
this : Nontrivial.{u_3} ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : Membership.mem (α := F) Wᗮ ((φ : (a : F) → F) (↑v : F) : F)
hv' : (↑v : F) ∉ W
x : F := HSub.hSub (β := F) (↑v : F) ((φ : (a : F) → F) (↑v : F) : F)
ρ : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ x)ᗮ
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑(φ.trans ρ) : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
w : F
hw : (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w
⊢ HSub.hSub (β := F) w ((ρ : (a : F) → F) ((φ : (a : F) → F) w : F) : F) = 0
have rw : w = (ρ : (a : F) → F) ((φ : (a : F) → F) w : F)
Tactic: rw [sub_eq_zero, hw]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n
this : Nontrivial.{u_3} ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : Membership.mem (α := F) Wᗮ ((φ : (a : F) → F) (↑v : F) : F)
hv' : (↑v : F) ∉ W
x : F := HSub.hSub (β := F) (↑v : F) ((φ : (a : F) → F) (↑v : F) : F)
ρ : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ x)ᗮ
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑(φ.trans ρ) : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
w : F
hw : (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w
rw : w = (ρ : (a : F) → F) ((φ : (a : F) → F) w : F)
⊢ HSub.hSub (β := F) w ((ρ : (a : F) → F) ((φ : (a : F) → F) w : F) : F) = 0
have rw₁ : w = w
Tactic: rw [sub_eq_zero, hw]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n
this : Nontrivial.{u_3} ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : Membership.mem (α := F) Wᗮ ((φ : (a : F) → F) (↑v : F) : F)
hv' : (↑v : F) ∉ W
x : F := HSub.hSub (β := F) (↑v : F) ((φ : (a : F) → F) (↑v : F) : F)
ρ : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ x)ᗮ
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑(φ.trans ρ) : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
have hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
Tactic: have hV : ∀ w, ρ (φ w) = w → w ∈ V := by
      intro w hw
      change w - ρ (φ w) = 0
      rw [sub_eq_zero, hw]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n
this : Nontrivial.{u_3} ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : Membership.mem (α := F) Wᗮ ((φ : (a : F) → F) (↑v : F) : F)
hv' : (↑v : F) ∉ W
x : F := HSub.hSub (β := F) (↑v : F) ((φ : (a : F) → F) (↑v : F) : F)
ρ : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ x)ᗮ
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑(φ.trans ρ) : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
w : F
hw : w ∈ W
⊢ w ∈ V
have a : (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w
Tactic: apply hV
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n
this : Nontrivial.{u_3} ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : Membership.mem (α := F) Wᗮ ((φ : (a : F) → F) (↑v : F) : F)
hv' : (↑v : F) ∉ W
x : F := HSub.hSub (β := F) (↑v : F) ((φ : (a : F) → F) (↑v : F) : F)
ρ : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ x)ᗮ
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑(φ.trans ρ) : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
w : F
hw : w ∈ W
⊢ (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w
have a : (ρ : (a : F) → F) w = w
Tactic: rw [hW w hw]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F)
    (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ n + 1
W : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hW : ∀ w ∈ W, (φ : (a : F) → F) w = w
hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n
this : Nontrivial.{u_3} ↥Wᗮ
v : ↥Wᗮ
hv : v ≠ 0
hφv : Membership.mem (α := F) Wᗮ ((φ : (a : F) → F) (↑v : F) : F)
hv' : (↑v : F) ∉ W
x : F := HSub.hSub (β := F) (↑v : F) ((φ : (a : F) → F) (↑v : F) : F)
ρ : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ x)ᗮ
V : Submodule ℝ F := (↑(ContinuousLinearMap.id ℝ F - (↑(↑(φ.trans ρ) : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
w : F
hw : w ∈ W
⊢ (ρ : (a : F) → F) w = w
have a : Membership.mem (γ := Submodule ℝ F) (ℝ ∙ x)ᗮ w
Tactic: refine reflection_mem_subspace_eq_self ?_