-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem LinearIsometryEquiv.reflections_generate_dim_aux [FiniteDimensional ℝ F] {n : ℕ}
    (φ : F ≃ₗᵢ[ℝ] F) (hn : finrank ℝ (ker (ContinuousLinearMap.id ℝ F - φ))ᗮ ≤ n) :
    ∃ l : List F, l.length ≤ n ∧ φ = (l.map fun v => reflection (ℝ ∙ v)ᗮ).prod

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ
          ↥(LinearMap.ker
                (ContinuousLinearMap.id ℝ F -
                  ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤
        n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod
φ : F ≃ₗᵢ[ℝ] F
W : Submodule ℝ F :=
  LinearMap.ker
    (ContinuousLinearMap.id ℝ F - ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })
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 := reflection (Submodule.span ℝ {x})ᗮ
V : Submodule ℝ F :=
  LinearMap.ker
    (ContinuousLinearMap.id ℝ F -
      ↑{ toLinearEquiv := (φ.trans ρ).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
H₂V : W ≤ V
H₁V : ↑v ∈ V
hn : finrank ℝ ↥Wᗮ ≤ n + 1
this✝ : finrank ℝ ↥W + 1 ≤ finrank ℝ ↥V
this : finrank ℝ ↥V + finrank ℝ ↥Vᗮ = finrank ℝ F
⊢ finrank ℝ ↥Vᗮ ≤ n

Tactic:
have : finrank ℝ W + finrank ℝ Wᗮ = finrank ℝ F := W.finrank_add_finrank_orthogonal

Result:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ
          ↥(LinearMap.ker
                (ContinuousLinearMap.id ℝ F -
                  ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤
        n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod
φ : F ≃ₗᵢ[ℝ] F
W : Submodule ℝ F :=
  LinearMap.ker
    (ContinuousLinearMap.id ℝ F - ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })
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 := reflection (Submodule.span ℝ {x})ᗮ
V : Submodule ℝ F :=
  LinearMap.ker
    (ContinuousLinearMap.id ℝ F -
      ↑{ toLinearEquiv := (φ.trans ρ).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
H₂V : W ≤ V
H₁V : ↑v ∈ V
hn : finrank ℝ ↥Wᗮ ≤ n + 1
this✝¹ : finrank ℝ ↥W + 1 ≤ finrank ℝ ↥V
this✝ : finrank ℝ ↥V + finrank ℝ ↥Vᗮ = finrank ℝ F
this : finrank ℝ ↥W + finrank ℝ ↥Wᗮ = finrank ℝ F
⊢ finrank ℝ ↥Vᗮ ≤ n

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ
          ↥(LinearMap.ker
                (ContinuousLinearMap.id ℝ F -
                  ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤
        n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn :
  finrank ℝ
      ↥(LinearMap.ker
            (ContinuousLinearMap.id ℝ F -
              ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤
    n + 1
W : Submodule ℝ F :=
  LinearMap.ker
    (ContinuousLinearMap.id ℝ F - ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })
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

Tactic:
exact v.prop w hw

Result:
no goals

Proof state:
case pos.intro.intro
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ
          ↥(LinearMap.ker
                (ContinuousLinearMap.id ℝ F -
                  ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤
        n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn :
  finrank ℝ
      ↥(LinearMap.ker
            (ContinuousLinearMap.id ℝ F -
              ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤
    n + 1
W : Submodule ℝ F :=
  LinearMap.ker
    (ContinuousLinearMap.id ℝ F - ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })
hW : ∀ w ∈ W, φ w = w
hn' : finrank ℝ ↥Wᗮ ≤ n
V : List F
hV₁ : V.length ≤ n
hV₂ : φ = (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) V).prod
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod

Tactic:
exact ⟨V, hV₁.trans n.le_succ, hV₂⟩

Result:
no goals

Proof state:
case a
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ
          ↥(LinearMap.ker
                (ContinuousLinearMap.id ℝ F -
                  ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤
        n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn :
  finrank ℝ
      ↥(LinearMap.ker
            (ContinuousLinearMap.id ℝ F -
              ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤
    n + 1
W : Submodule ℝ F :=
  LinearMap.ker
    (ContinuousLinearMap.id ℝ F - ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })
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 := reflection (Submodule.span ℝ {x})ᗮ
V : Submodule ℝ F :=
  LinearMap.ker
    (ContinuousLinearMap.id ℝ F -
      ↑{ toLinearEquiv := (φ.trans ρ).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
H₂V : W ≤ V
this : ρ ↑v = φ ↑v
⊢ ρ (φ ↑v) = ↑v

Tactic:
rw [← this]

Result:
case a
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
n : ℕ
IH :
  ∀ (φ : F ≃ₗᵢ[ℝ] F),
    finrank ℝ
          ↥(LinearMap.ker
                (ContinuousLinearMap.id ℝ F -
                  ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤
        n →
      ∃ l, l.length ≤ n ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod
φ : F ≃ₗᵢ[ℝ] F
hn :
  finrank ℝ
      ↥(LinearMap.ker
            (ContinuousLinearMap.id ℝ F -
              ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤
    n + 1
W : Submodule ℝ F :=
  LinearMap.ker
    (ContinuousLinearMap.id ℝ F - ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })
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 := reflection (Submodule.span ℝ {x})ᗮ
V : Submodule ℝ F :=
  LinearMap.ker
    (ContinuousLinearMap.id ℝ F -
      ↑{ toLinearEquiv := (φ.trans ρ).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
H₂V : W ≤ V
this : ρ ↑v = φ ↑v
⊢ ρ (ρ ↑v) = ↑v