-- 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
w : F
hw : w ∈ W
⊢ ⟪w, φ ↑v⟫_ℝ = 0

Tactic:
rw [← hW w hw, LinearIsometryEquiv.inner_map_map]

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

Tactic:
obtain ⟨v, hv⟩ := exists_ne (0 : Wᗮ)

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