-- 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:
case neg.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
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
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod

Tactic:
have : finrank ℝ Vᗮ ≤ n := by
  change finrank ℝ Wᗮ ≤ n + 1 at hn
  have : finrank ℝ W + 1 ≤ finrank ℝ V :=
    Submodule.finrank_lt_finrank_of_lt (SetLike.lt_iff_le_and_exists.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
  omega

Result:
case neg.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
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
this : finrank ℝ ↥Vᗮ ≤ n
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod

Proof state:
case neg
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
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).prod

Tactic:
haveI : Nontrivial Wᗮ := nontrivial_of_finrank_pos (by omega : 0 < finrank ℝ Wᗮ)

Result:
case neg
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ᗮ
⊢ ∃ l, l.length ≤ n + 1 ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v})ᗮ) l).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
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 := ⋯ })
w : F
hw : ρ (φ w) = w
⊢ w - ρ (φ w) = 0

Tactic:
rw [sub_eq_zero, hw]

Result:
no goals