awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
h h₁ : finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥Kᗮ = finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥Kᗮ
⊢ finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥Kᗮ = finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥(Kᗮ ⊓ ⊤)

Tactic:
rw [inf_top_eq]

Premises used: inf_top_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank 𝕜 E = finrank.{u_1, u_2} 𝕜 ↥⊤

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
n : ℕ
h_dim : finrank.{u_1, u_2} 𝕜 ↥K + n = finrank 𝕜 E
rw : finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥Kᗮ = finrank.{u_1, u_2} 𝕜 ↥K + n
⊢ finrank.{u_1, u_2} 𝕜 ↥Kᗮ = n

Tactic:
rw [← add_right_inj (finrank 𝕜 K)]

Premises used: Membership.mem, Subtype, add_right_inj, Module.finrank
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
n : ℕ
h_dim : finrank.{u_1, u_2} 𝕜 ↥K + n = finrank 𝕜 E
⊢ finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥Kᗮ = finrank.{u_1, u_2} 𝕜 ↥K + n

Tactic:
simp [Submodule.finrank_add_finrank_orthogonal, h_dim]

Premises used: Submodule.finrank_add_finrank_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
_i : Fact (finrank 𝕜 E = n + 1)
v : E
hv : v ≠ 0
⊢ FiniteDimensional 𝕜 E

Tactic:
haveI : FiniteDimensional 𝕜 E := .of_fact_finrank_eq_succ n
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
_i : Fact (finrank 𝕜 E = n + 1)
v : E
hv : v ≠ 0
this : FiniteDimensional 𝕜 E
⊢ finrank.{u_1, u_2} 𝕜 ↥(𝕜 ∙ v) + n = finrank 𝕜 E

Tactic:
simp [finrank_span_singleton hv, _i.elim, add_comm]

Premises used: add_comm, Fact.elim, finrank_span_singleton
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
_i : Fact (finrank 𝕜 E = n + 1)
v : E
hv : v ≠ 0
this : FiniteDimensional 𝕜 E
⊢ finrank.{u_1, u_2} 𝕜 ↥(𝕜 ∙ v)ᗮ = n

Tactic:
exact finrank_add_finrank_orthogonal' <| by
    simp [finrank_span_singleton hv, _i.elim, add_comm]

Premises used: Submodule.finrank_add_finrank_orthogonal'
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
⊢ ∃ (l : List F), l.length ≤ 0 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)

Tactic:
⟨[], rfl.le, show φ = 1 from ?_⟩

Premises used: Eq.le, And.intro, Exists.intro, rfl, List.nil
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
zero : φ = 1
⊢ ∃ (l : List F), l.length ≤ 0 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)

Tactic:
refine ⟨[], rfl.le, show φ = 1 from ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
rwa :
  ∀ (hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ = 0),
    (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
rwa₁ :
  ∀ (hn : (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ = ⊥),
    (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (hn : (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤),
    (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
⊢ (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤

Tactic:
rwa [le_zero_iff, finrank_eq_zero, orthogonal_eq_bot_iff] at hn

Premises used: le_zero_iff, Submodule.orthogonal_eq_bot_iff, Submodule.finrank_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
⊢ (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤

Tactic:
have : (ContinuousLinearMap.id ℝ F - φ).ker = ⊤ := by
      rwa [le_zero_iff, finrank_eq_zero, orthogonal_eq_bot_iff] at hn
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
this : (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
zero : 1 = φ
⊢ φ = 1

Tactic:
symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
this : (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
zero : ∀ (x : F), Eq (α := F) ((1 : (a : F) → F) x : F) ((φ : (a : F) → F) x : F)
⊢ 1 = φ

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
this : (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
x : F
⊢ Eq (α := F) (((↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F) : (a : F) → F) x : F)
    ((0 : (a : F) → F) x : F)

Tactic:
have := LinearMap.congr_fun (LinearMap.ker_eq_top.mp this) x
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
hn : finrank.{0, u_3} ℝ ↥(↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).kerᗮ ≤ 0
this_1 : (↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F).ker = ⊤
x : F
this :
  Eq (α := F) (((↑(ContinuousLinearMap.id ℝ F - (↑(↑φ : F ≃L[ℝ] F) : F →L[ℝ] F)) : F →ₗ[ℝ] F) : (a : F) → F) x : F)
    ((0 : (a : F) → F) x : F)
⊢ Eq (α := F) ((1 : (a : F) → F) x : F) ((φ : (a : F) → F) x : F)

Tactic:
simpa only [sub_eq_zero, ContinuousLinearMap.coe_sub, LinearMap.sub_apply,
      LinearMap.zero_apply] using this

Premises used: LinearMap.zero_apply, sub_eq_zero, ContinuousLinearMap.coe_sub, LinearMap.sub_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
⊢ ∀ w ∈ W, (φ : (a : F) → F) w = w

Tactic:
have hW : ∀ w ∈ W, φ w = w := fun w hw => (sub_eq_zero.mp hw).symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
pos :
  ∀ (hn' : finrank.{0, u_3} ℝ ↥Wᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
neg :
  ∀ (hn' : ¬finrank.{0, u_3} ℝ ↥Wᗮ ≤ n),
    ∃ (l : List F), l.length ≤ n + 1 ∧ φ = 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:
by_cases hn' : finrank ℝ Wᗮ ≤ n

Premises used: Real, Membership.mem, Subtype, Submodule.orthogonal, Module.finrank
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
pos :
  ∀ (V : List F) (hV₁ : V.length ≤ n) (hV₂ : φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) V)),
    ∃ (l : List F), l.length ≤ n + 1 ∧ φ = 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 ⟨V, hV₁, hV₂⟩ := IH φ hn'
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
V : List F
hV₁ : V.length ≤ n
hV₂ : φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) V)
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)

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

Premises used: Nat.le_succ, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
V : List F
hV₁ : V.length ≤ n
hV₂ : φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) V)
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)

Tactic:
exact ⟨V, hV₁.trans n.le_succ, hV₂⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
⊢ 0 < finrank.{0, u_3} ℝ ↥Wᗮ

Tactic:
lia
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
⊢ Nontrivial.{u_3} ↥Wᗮ

Tactic:
haveI : Nontrivial Wᗮ := nontrivial_of_finrank_pos (by lia : 0 < finrank ℝ Wᗮ)
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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ᗮ
neg :
  ∀ (v : ↥Wᗮ) (hv : v ≠ 0),
    ∃ (l : List F), l.length ≤ n + 1 ∧ φ = 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 ⟨v, hv⟩ := exists_ne (0 : Wᗮ)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
w : F
hw : w ∈ W
rw : ⟪w, (↑v : F)⟫_ℝ = 0
⊢ ⟪w, (φ : (a : F) → F) (↑v : F)⟫_ℝ = 0

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

Premises used: LinearIsometryEquiv.inner_map_map
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
w : F
hw : w ∈ W
⊢ ⟪w, (↑v : F)⟫_ℝ = 0

Tactic:
v.prop w hw

Premises used: Subtype.prop
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
w : F
hw : w ∈ W
⊢ ⟪w, (↑v : F)⟫_ℝ = 0

Tactic:
exact v.prop w hw

Premises used: Subtype.prop
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
⊢ Membership.mem (α := F) Wᗮ ((φ : (a : F) → F) (↑v : F) : F)

Tactic:
have hφv : φ v ∈ Wᗮ := by
      intro w hw
      rw [← hW w hw, LinearIsometryEquiv.inner_map_map]
      exact v.prop w hw
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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)
h : (↑v : F) ∈ W
⊢ False

Tactic:
hv ((mem_left_iff_eq_zero_of_disjoint W.orthogonal_disjoint).mp h)

Premises used: Submodule.orthogonal_disjoint, Submodule.mem_left_iff_eq_zero_of_disjoint, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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)
h : (↑v : F) ∈ W
⊢ False

Tactic:
exact hv ((mem_left_iff_eq_zero_of_disjoint W.orthogonal_disjoint).mp h)

Premises used: Submodule.orthogonal_disjoint, Submodule.mem_left_iff_eq_zero_of_disjoint, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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)
⊢ (↑v : F) ∉ W

Tactic:
have hv' : (v : F) ∉ W := by
      intro h
      exact hv ((mem_left_iff_eq_zero_of_disjoint W.orthogonal_disjoint).mp h)
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
w : F
hw : (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w
change : HSub.hSub (β := F) w ((ρ : (a : F) → F) ((φ : (a : F) → F) w : F) : F) = 0
⊢ w ∈ V

Tactic:
change w - ρ (φ w) = 0

Premises used: DFunLike.coe