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
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
⊢ Membership.mem (γ := Submodule ℝ F) (ℝ ∙ x)ᗮ w
have a : ⟪w, x⟫_ℝ = 0
Tactic: rw [mem_orthogonal_singleton_iff_inner_left]
-- 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
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
have H₂V : W ≤ V
Tactic: have H₂V : W ≤ V := by
      intro w hw
      apply hV
      rw [hW w hw]
      refine reflection_mem_subspace_eq_self ?_
      rw [mem_orthogonal_singleton_iff_inner_left]
      exact Submodule.sub_mem _ v.prop hφv _ 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
H₂V : W ≤ V
⊢ (↑v : F) ∈ V
have a : (ρ : (a : F) → F) ((φ : (a : F) → F) (↑v : F) : F) = (↑v : F)
Tactic: apply hV
-- 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
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
H₂V : W ≤ V
⊢ (ρ : (a : F) → F) ((φ : (a : F) → F) (↑v : F) : F) = (↑v : F)
have this₁ : Eq (α := F) ((ρ : (a : F) → F) (↑v : F) : F) ((φ : (a : F) → F) (↑v : F) : F)
Tactic: have : ρ v = φ v := reflection_sub (φ.norm_map v).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
hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n
this_1 : 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
H₂V : W ≤ V
this : Eq (α := F) ((ρ : (a : F) → F) (↑v : F) : F) ((φ : (a : F) → F) (↑v : F) : F)
⊢ (ρ : (a : F) → F) ((φ : (a : F) → F) (↑v : F) : F) = (↑v : F)
have a : (ρ : (a : F) → F) ((ρ : (a : F) → F) (↑v : F) : F) = (↑v : F)
Tactic: rw [← this]
-- 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
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
H₂V : W ≤ V
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
have H₁V : (↑v : F) ∈ V
Tactic: have H₁V : (v : F) ∈ V := by
      apply hV
      have : ρ v = φ v := reflection_sub (φ.norm_map v).symm
      rw [← this]
      exact reflection_reflection _ _
-- 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
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
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
hn : finrank.{0, u_3} ℝ ↥Wᗮ ≤ n + 1
⊢ finrank.{0, u_3} ℝ ↥Vᗮ ≤ n
have this₁ : finrank.{0, u_3} ℝ ↥W + 1 ≤ finrank.{0, u_3} ℝ ↥V
Tactic: have : finrank ℝ W + 1 ≤ finrank ℝ V :=
        finrank_lt_finrank_of_lt ((SetLike.lt_iff_le_and_exists (B := F)).2 ⟨H₂V, v, H₁V, hv'⟩)
-- 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
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_1 : 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
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
hn : finrank.{0, u_3} ℝ ↥Wᗮ ≤ n + 1
this : finrank.{0, u_3} ℝ ↥W + 1 ≤ finrank.{0, u_3} ℝ ↥V
⊢ finrank.{0, u_3} ℝ ↥Vᗮ ≤ n
have this₁ : finrank.{0, u_3} ℝ ↥V + finrank.{0, u_3} ℝ ↥Vᗮ = finrank ℝ F
Tactic: have : finrank ℝ V + finrank ℝ Vᗮ = finrank ℝ F := V.finrank_add_finrank_orthogonal
-- 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
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_1 : 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
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
hn : finrank.{0, u_3} ℝ ↥Wᗮ ≤ n + 1
this_2 : finrank.{0, u_3} ℝ ↥W + 1 ≤ finrank.{0, u_3} ℝ ↥V
this : finrank.{0, u_3} ℝ ↥V + finrank.{0, u_3} ℝ ↥Vᗮ = finrank ℝ F
⊢ finrank.{0, u_3} ℝ ↥Vᗮ ≤ n
have this₁ : finrank.{0, u_3} ℝ ↥W + finrank.{0, u_3} ℝ ↥Wᗮ = finrank ℝ F
Tactic: have : finrank ℝ W + finrank ℝ Wᗮ = finrank ℝ F := W.finrank_add_finrank_orthogonal
-- 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
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
have this₁ : finrank.{0, u_3} ℝ ↥Vᗮ ≤ n
Tactic: have : finrank ℝ Vᗮ ≤ n := by
      change finrank ℝ Wᗮ ≤ n + 1 at hn
      have : finrank ℝ W + 1 ≤ finrank ℝ V :=
        finrank_lt_finrank_of_lt ((SetLike.lt_iff_le_and_exists (B := F)).2 ⟨H₂V, v, H₁V, hv'⟩)
      have : finrank ℝ V + finrank ℝ Vᗮ = finrank ℝ F := V.finrank_add_finrank_orthogonal
      have : finrank ℝ W + finrank ℝ Wᗮ = finrank ℝ F := W.finrank_add_finrank_orthogonal
      lia
-- 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_1 : 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
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
this : finrank.{0, u_3} ℝ ↥Vᗮ ≤ n
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
have neg : ∀ (l : List F) (hl : l.length ≤ n) (hφl : ρ * φ = 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)
Tactic: obtain ⟨l, hl, hφl⟩ := IH (ρ * φ) this
-- 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_1 : 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
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
this : finrank.{0, u_3} ℝ ↥Vᗮ ≤ n
l : List F
hl : l.length ≤ n
hφl : ρ * φ = 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 : φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) (x :: l))
Tactic: refine ⟨x::l, Nat.succ_le_succ hl, ?_⟩
-- 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_1 : 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
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
this : finrank.{0, u_3} ℝ ↥Vᗮ ≤ n
l : List F
hl : l.length ≤ n
hφl : ρ * φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
⊢ φ = HMul.hMul (α := F ≃ₗᵢ[ℝ] F) (reflection (ℝ ∙ x)ᗮ) (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l))
have this₁ : Eq.{u_3 + 1} (α := F ≃ₗᵢ[ℝ] F) ((fun (x : F ≃ₗᵢ[ℝ] F) ↦ ρ * x) (ρ * φ))
  ((fun (x : F ≃ₗᵢ[ℝ] F) ↦ ρ * x) (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)))
Tactic: have := congr_arg (ρ * ·) hφl
-- 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_1 : 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
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
this_2 : finrank.{0, u_3} ℝ ↥Vᗮ ≤ n
l : List F
hl : l.length ≤ n
hφl : ρ * φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
this : ρ * (ρ * φ) = ρ * List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
⊢ φ = HMul.hMul (α := F ≃ₗᵢ[ℝ] F) (reflection (ℝ ∙ x)ᗮ) (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l))
have neg : ∀ (this : ρ * ρ * φ = ρ * List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)),
  φ = HMul.hMul (α := F ≃ₗᵢ[ℝ] F) (reflection (ℝ ∙ x)ᗮ) (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l))
Tactic: rwa [← mul_assoc, reflection_mul_reflection, one_mul] at this
Cleared hypotheses: this
-- 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_1 : 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
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
this_2 : finrank.{0, u_3} ℝ ↥Vᗮ ≤ n
l : List F
hl : l.length ≤ n
hφl : ρ * φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
this : ρ * (ρ * φ) = ρ * List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
neg :
  ∀ (this : ρ * ρ * φ = ρ * List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)),
    φ = HMul.hMul (α := F ≃ₗᵢ[ℝ] F) (reflection (ℝ ∙ x)ᗮ) (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l))
⊢ φ = HMul.hMul (α := F ≃ₗᵢ[ℝ] F) (reflection (ℝ ∙ x)ᗮ) (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l))
have neg₁ : ∀ (this : 1 * φ = ρ * List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)),
  φ = HMul.hMul (α := F ≃ₗᵢ[ℝ] F) (reflection (ℝ ∙ x)ᗮ) (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l))
Tactic: rwa [← mul_assoc, reflection_mul_reflection, one_mul] at this
Cleared hypotheses: this