-- 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
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
⊢ φ ↑v ∈ Wᗮ

Tactic:
intro w hw

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
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

Proof state:
case zero
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn :
  finrank ℝ
      ↥(LinearMap.ker
            (ContinuousLinearMap.id ℝ F -
              ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤
    0
this :
  LinearMap.ker
      (ContinuousLinearMap.id ℝ F -
        ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) =
    ⊤
⊢ φ = 1

Tactic:
symm

Result:
case zero
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn :
  finrank ℝ
      ↥(LinearMap.ker
            (ContinuousLinearMap.id ℝ F -
              ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }))ᗮ ≤
    0
this :
  LinearMap.ker
      (ContinuousLinearMap.id ℝ F -
        ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) =
    ⊤
⊢ 1 = φ

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

Tactic:
let W := ker (ContinuousLinearMap.id ℝ F - φ)

Result:
case succ
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 := ⋯ })
⊢ ∃ 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 := ⋯ })
hV : ∀ (w : F), ρ (φ w) = w → w ∈ V
w : F
hw : w ∈ W
⊢ w ∈ V

Tactic:
apply hV

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
w : F
hw : w ∈ W
⊢ ρ (φ w) = w