awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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_1 : 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
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
hn : finrank.{0, u_3} ℝ ↥Wᗮ ≤ n + 1
this : finrank.{0, u_3} ℝ ↥W + 1 ≤ finrank.{0, u_3} ℝ ↥V
⊢ finrank.{0, u_3} ℝ ↥V + finrank.{0, u_3} ℝ ↥Vᗮ = finrank ℝ F

Tactic:
have : finrank ℝ V + finrank ℝ Vᗮ = finrank ℝ F := V.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
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
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_1 : 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
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
hn : finrank.{0, u_3} ℝ ↥Wᗮ ≤ n + 1
this_2 : finrank.{0, u_3} ℝ ↥W + 1 ≤ finrank.{0, u_3} ℝ ↥V
this : finrank.{0, u_3} ℝ ↥V + finrank.{0, u_3} ℝ ↥Vᗮ = finrank ℝ F
⊢ finrank.{0, u_3} ℝ ↥W + finrank.{0, u_3} ℝ ↥Wᗮ = finrank ℝ F

Tactic:
have : finrank ℝ W + finrank ℝ Wᗮ = finrank ℝ F := W.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
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
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_1 : 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
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
hn : finrank.{0, u_3} ℝ ↥Wᗮ ≤ n + 1
this_2 : finrank.{0, u_3} ℝ ↥W + 1 ≤ finrank.{0, u_3} ℝ ↥V
this_3 : finrank.{0, u_3} ℝ ↥V + finrank.{0, u_3} ℝ ↥Vᗮ = finrank ℝ F
this : finrank.{0, u_3} ℝ ↥W + finrank.{0, u_3} ℝ ↥Wᗮ = finrank ℝ F
⊢ finrank.{0, u_3} ℝ ↥Vᗮ ≤ n

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
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
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
⊢ finrank.{0, u_3} ℝ ↥Vᗮ ≤ n

Tactic:
have : finrank ℝ Vᗮ ≤ n := by
      change finrank ℝ Wᗮ ≤ n + 1 at hn
      have : finrank ℝ W + 1 ≤ finrank ℝ V :=
        finrank_lt_finrank_of_lt ((SetLike.lt_iff_le_and_exists (B := F)).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
      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
this_1 : 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
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
this : finrank.{0, u_3} ℝ ↥Vᗮ ≤ n
neg :
  ∀ (l : List F) (hl : l.length ≤ n) (hφl : ρ * φ = 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)
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)

Tactic:
obtain ⟨l, hl, hφl⟩ := IH (ρ * φ) this

Premises used: HMul.hMul
-- 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_1 : 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
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
this : finrank.{0, u_3} ℝ ↥Vᗮ ≤ n
l : List F
hl : l.length ≤ n
hφl : ρ * φ = 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:
⟨x::l, Nat.succ_le_succ hl, ?_⟩

Premises used: List.cons, And.intro, Exists.intro, Nat.succ_le_succ
-- 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_1 : 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
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
this : finrank.{0, u_3} ℝ ↥Vᗮ ≤ n
l : List F
hl : l.length ≤ n
hφl : ρ * φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
neg : φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) (x :: l))
⊢ ∃ (l : List F), l.length ≤ n + 1 ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)

Tactic:
refine ⟨x::l, Nat.succ_le_succ hl, ?_⟩
-- 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_1 : 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
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
this : finrank.{0, u_3} ℝ ↥Vᗮ ≤ n
l : List F
hl : l.length ≤ n
hφl : ρ * φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
⊢ Eq.{u_3 + 1} (α := F ≃ₗᵢ[ℝ] F) ((fun (x : F ≃ₗᵢ[ℝ] F) ↦ ρ * x) (ρ * φ))
    ((fun (x : F ≃ₗᵢ[ℝ] F) ↦ ρ * x) (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)))

Tactic:
have := congr_arg (ρ * ·) hφl
-- 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_1 : 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
hV : ∀ (w : F), (ρ : (a : F) → F) ((φ : (a : F) → F) w : F) = w → w ∈ V
H₂V : W ≤ V
H₁V : (↑v : F) ∈ V
this_2 : finrank.{0, u_3} ℝ ↥Vᗮ ≤ n
l : List F
hl : l.length ≤ n
hφl : ρ * φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
this : ρ * (ρ * φ) = ρ * List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)
neg :
  ∀ (this : ρ * ρ * φ = ρ * List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)),
    φ = HMul.hMul (α := F ≃ₗᵢ[ℝ] F) (reflection (ℝ ∙ x)ᗮ) (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l))
neg₁ :
  ∀ (this : 1 * φ = ρ * List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)),
    φ = HMul.hMul (α := F ≃ₗᵢ[ℝ] F) (reflection (ℝ ∙ x)ᗮ) (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l))
neg₂ neg₃ neg₄ neg₅ :
  ∀ (this : φ = ρ * List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)),
    φ = HMul.hMul (α := F ≃ₗᵢ[ℝ] F) (reflection (ℝ ∙ x)ᗮ) (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l))
⊢ φ = HMul.hMul (α := F ≃ₗᵢ[ℝ] F) (reflection (ℝ ∙ x)ᗮ) (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l))

Tactic:
rwa [← mul_assoc, reflection_mul_reflection, one_mul] at this

Premises used: mul_assoc, Submodule.reflection_mul_reflection, one_mul
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
⊢ ∃ (l : List F), l.length ≤ finrank ℝ F ∧ φ = List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l)

Tactic:
let ⟨l, hl₁, hl₂⟩ := φ.reflections_generate_dim_aux le_rfl
  ⟨l, hl₁.trans (finrank_le _), hl₂⟩

Premises used: Real, le_rfl, List.map, LinearMap.ker, HSub.hSub, LinearIsometryEquiv.reflections_generate_dim_aux, Exists, ContinuousLinearMap.toLinearMap, _private.0.LinearIsometryEquiv.reflections_generate_dim.match_1, ContinuousLinearMap.id, LE.le, Submodule.orthogonal, And, And.intro, Exists.intro, Submodule.span, Submodule.reflection, Submodule.finrank_le, LinearIsometryEquiv.toContinuousLinearEquiv, LE.le.trans, Singleton.singleton, Eq, List.length, Module.finrank, ContinuousLinearEquiv.toContinuousLinearMap, List.prod
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
rw :
  ∀ (x : F ≃ₗᵢ[ℝ] F),
    Membership.mem (γ := Subgroup (F ≃ₗᵢ[ℝ] F)) (Subgroup.closure (Set.range fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ)) x
⊢ Eq.{u_3 + 1} (α := Subgroup (F ≃ₗᵢ[ℝ] F)) (Subgroup.closure (Set.range fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ)) ⊤

Tactic:
rw [Subgroup.eq_top_iff']

Premises used: Subgroup.eq_top_iff'
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
rcases :
  ∀ (l : List F),
    l.length ≤ finrank ℝ F →
      Membership.mem (γ := Subgroup (F ≃ₗᵢ[ℝ] F)) (Subgroup.closure (Set.range fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ))
        (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l))
⊢ Membership.mem (γ := Subgroup (F ≃ₗᵢ[ℝ] F)) (Subgroup.closure (Set.range fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ)) φ

Tactic:
rcases φ.reflections_generate_dim with ⟨l, _, rfl⟩

Premises used: LinearIsometryEquiv.reflections_generate_dim, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
l : List F
left : l.length ≤ finrank ℝ F
apply :
  ∀ (x : F ≃ₗᵢ[ℝ] F),
    Membership.mem (γ := List (F ≃ₗᵢ[ℝ] F)) (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l) x →
      Membership.mem (γ := Subgroup (F ≃ₗᵢ[ℝ] F)) (Subgroup.closure (Set.range fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ)) x
⊢ Membership.mem (γ := Subgroup (F ≃ₗᵢ[ℝ] F)) (Subgroup.closure (Set.range fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ))
    (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l))

Tactic:
apply (Subgroup.closure _).list_prod_mem

Premises used: Subgroup.closure, Subgroup.list_prod_mem
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
l : List F
left : l.length ≤ finrank ℝ F
x : F ≃ₗᵢ[ℝ] F
hx : Membership.mem (γ := List (F ≃ₗᵢ[ℝ] F)) (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l) x
rcases :
  ∀ a ∈ l,
    ∀ (hax : reflection (ℝ ∙ a)ᗮ = x),
      Membership.mem (γ := Subgroup (F ≃ₗᵢ[ℝ] F)) (Subgroup.closure (Set.range fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ)) x
⊢ Membership.mem (γ := Subgroup (F ≃ₗᵢ[ℝ] F)) (Subgroup.closure (Set.range fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ)) x

Tactic:
rcases List.mem_map.mp hx with ⟨a, _, hax⟩

Premises used: Iff.mp, List.mem_map
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
l : List F
left : l.length ≤ finrank ℝ F
x : F ≃ₗᵢ[ℝ] F
hx : Membership.mem (γ := List (F ≃ₗᵢ[ℝ] F)) (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l) x
a : F
left_1 : a ∈ l
hax : reflection (ℝ ∙ a)ᗮ = x
⊢ Membership.mem (γ := Subgroup (F ≃ₗᵢ[ℝ] F)) (Subgroup.closure (Set.range fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ)) x

Tactic:
Subgroup.subset_closure ⟨a, hax⟩

Premises used: Subgroup.subset_closure, Exists.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
l : List F
left : l.length ≤ finrank ℝ F
x : F ≃ₗᵢ[ℝ] F
hx : Membership.mem (γ := List (F ≃ₗᵢ[ℝ] F)) (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l) x
a : F
left_1 : a ∈ l
hax : reflection (ℝ ∙ a)ᗮ = x
⊢ Membership.mem (γ := Subgroup (F ≃ₗᵢ[ℝ] F)) (Subgroup.closure (Set.range fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ)) x

Tactic:
exact Subgroup.subset_closure ⟨a, hax⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
hc : IsComplete (↑(iSup V) : Set E)
⊢ CompleteSpace.{u_2} ↥(iSup V)

Tactic:
haveI : CompleteSpace (↥(iSup V)) := hc.completeSpace_coe
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
hc : IsComplete (↑(iSup V) : Set E)
this : CompleteSpace.{u_2} ↥(iSup V)
⊢ DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥

Tactic:
simp only [DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, hV.independent,
    true_and, orthogonal_eq_bot_iff]

Premises used: DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, Submodule.orthogonal_eq_bot_iff, OrthogonalFamily.independent, true_and
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : FiniteDimensional 𝕜 E
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
⊢ DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥

Tactic:
haveI := FiniteDimensional.proper_rclike 𝕜 (↥(iSup V))
  hV.isInternal_iff_of_isComplete (completeSpace_coe_iff_isComplete.mp inferInstance)

Premises used: OrthogonalFamily.isInternal_iff_of_isComplete, inferInstance, Iff.mp, completeSpace_coe_iff_isComplete
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
V : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
x_1 : E
i : ι
x : E
hx : x ∈ V i
⊢ ∑ i : ι, ((V i).starProjection : (a : E) → E) x = x

Tactic:
(Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hij => ?_).trans
        (starProjection_eq_self_iff.mpr hx)

Premises used: Iff.mpr, Finset.mem_univ, Finset.sum_eq_single_of_mem, Eq.trans, Submodule.starProjection_eq_self_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
V : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
x_1 : E
i : ι
x : E
hx : x ∈ V i
mem :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι) Finset.univ j →
      ∀ (hij : j ≠ i), Eq (α := E) (((V j).starProjection : (a : E) → E) x : E) (0 : E)
⊢ ∑ i : ι, ((V i).starProjection : (a : E) → E) x = x

Tactic:
refine
      (Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hij => ?_).trans
        (starProjection_eq_self_iff.mpr hx)

Premises used: Iff.mpr, Finset.mem_univ, Finset.sum_eq_single_of_mem, Eq.trans, Submodule.starProjection_eq_self_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
V : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
x_1 : E
i : ι
x : E
hx : x ∈ V i
j : ι
h : Membership.mem (γ := Finset ι) Finset.univ j
hij : j ≠ i
mem : x ∈ (V j)ᗮ
⊢ Eq (α := E) (((V j).starProjection : (a : E) → E) x : E) (0 : E)

Tactic:
rw [starProjection_apply, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero,
      Submodule.coe_zero]

Premises used: Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, Submodule.starProjection_apply, Submodule.coe_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
V : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), CompleteSpace.{u_2} ↥(V i)
hV : OrthogonalFamily.{u_1, u_2, u_4, u_2} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
x_1 : E
i : ι
x : E
hx : x ∈ V i
j : ι
h : Membership.mem (γ := Finset ι) Finset.univ j
hij : j ≠ i
⊢ x ∈ (V j)ᗮ

Tactic:
hV.isOrtho hij.symm hx

Premises used: Ne.symm, OrthogonalFamily.isOrtho