awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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))
⊢ φ = HMul.hMul (α := F ≃ₗᵢ[ℝ] F) (reflection (ℝ ∙ x)ᗮ) (List.prod (List.map (fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ) l))
have 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))
Tactic: rwa [← mul_assoc, reflection_mul_reflection, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
⊢ Eq.{u_3 + 1} (α := Subgroup (F ≃ₗᵢ[ℝ] F)) (Subgroup.closure (Set.range fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ)) ⊤
have rw : ∀ (x : F ≃ₗᵢ[ℝ] F),
  Membership.mem (γ := Subgroup (F ≃ₗᵢ[ℝ] F)) (Subgroup.closure (Set.range fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ)) x
Tactic: rw [Subgroup.eq_top_iff']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
φ : F ≃ₗᵢ[ℝ] F
⊢ Membership.mem (γ := Subgroup (F ≃ₗᵢ[ℝ] F)) (Subgroup.closure (Set.range fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ)) φ
have 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))
Tactic: rcases φ.reflections_generate_dim with ⟨l, _, rfl⟩
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : FiniteDimensional ℝ F
l : List F
left : 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))
have 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
Tactic: apply (Subgroup.closure _).list_prod_mem
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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
⊢ Membership.mem (γ := Subgroup (F ≃ₗᵢ[ℝ] F)) (Subgroup.closure (Set.range fun (v : F) ↦ reflection (ℝ ∙ v)ᗮ)) x
have rcases : ∀ a ∈ l,
  ∀ (hax : reflection (ℝ ∙ a)ᗮ = 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⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
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)
⊢ DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥
have this : CompleteSpace.{u_2} ↥(iSup V)
Tactic: haveI : CompleteSpace (↥(iSup V)) := hc.completeSpace_coe
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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
have mem : ∀ (j : ι),
  Membership.mem (γ := Finset ι) Finset.univ j →
    ∀ (hij : j ≠ i), Eq (α := E) (((V j).starProjection : (a : E) → E) x : E) (0 : E)
Tactic: refine
      (Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hij => ?_).trans
        (starProjection_eq_self_iff.mpr hx)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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
⊢ Eq (α := E) (((V j).starProjection : (a : E) → E) x : E) (0 : E)
have mem : x ∈ (V j)ᗮ
Tactic: rw [starProjection_apply, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero,
      Submodule.coe_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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 : E
⊢ Eq.{u_2 + 1} (α := E) (∑ i : ι, ((V i).starProjection : (a : E) → E) 0) 0
have zero : Eq.{u_2 + 1} (α := E) (∑ x : ι, 0) 0
Tactic: simp_rw [map_zero, Finset.sum_const_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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 x y : E
hx_1 : Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), V i) x
hy_1 : Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), V i) y
hx : ∑ i : ι, ((V i).starProjection : (a : E) → E) x = x
hy : ∑ i : ι, ((V i).starProjection : (a : E) → E) y = y
⊢ ∑ i : ι, ((V i).starProjection : (a : E) → E) (x + y) = x + y
have add : HAdd.hAdd (α := E) (∑ x_2 : ι, ((V x_2).starProjection : (a : E) → E) x)
    (∑ x : ι, ((V x).starProjection : (a : E) → E) y) =
  x + y
Tactic: simp_rw [map_add, Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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 : E
hx : x ∈ iSup V
⊢ ∑ i : ι, ((V i).starProjection : (a : E) → E) x = x
have mem : ∀ (i : ι) (x : E) (hx : x ∈ V i), ∑ i : ι, ((V i).starProjection : (a : E) → E) x = x
Tactic: induction hx using iSup_induction' with
  | mem i x hx =>
    refine
      (Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hij => ?_).trans
        (starProjection_eq_self_iff.mpr hx)
    rw [starProjection_apply, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero,
      Submodule.coe_zero]
    exact hV.isOrtho hij.symm hx
  | zero =>
    simp_rw [map_zero, Finset.sum_const_zero]
  | add x y _ _ hx hy =>
    simp_rw [map_add, Finset.sum_add_distrib]
    exact congr_arg₂ (· + ·) hx hy
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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 : E
hx : x ∈ iSup V
mem : ∀ (i : ι) (x : E) (hx : x ∈ V i), ∑ i : ι, ((V i).starProjection : (a : E) → E) x = x
⊢ ∑ i : ι, ((V i).starProjection : (a : E) → E) x = x
have zero : Eq.{u_2 + 1} (α := E) (∑ i : ι, ((V i).starProjection : (a : E) → E) 0) 0
Tactic: induction hx using iSup_induction' with
  | mem i x hx =>
    refine
      (Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hij => ?_).trans
        (starProjection_eq_self_iff.mpr hx)
    rw [starProjection_apply, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero,
      Submodule.coe_zero]
    exact hV.isOrtho hij.symm hx
  | zero =>
    simp_rw [map_zero, Finset.sum_const_zero]
  | add x y _ _ hx hy =>
    simp_rw [map_add, Finset.sum_add_distrib]
    exact congr_arg₂ (· + ·) hx hy
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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 : E
hx : x ∈ iSup V
mem : ∀ (i : ι) (x : E) (hx : x ∈ V i), ∑ i : ι, ((V i).starProjection : (a : E) → E) x = x
zero : Eq.{u_2 + 1} (α := E) (∑ i : ι, ((V i).starProjection : (a : E) → E) 0) 0
⊢ ∑ i : ι, ((V i).starProjection : (a : E) → E) x = x
have add : ∀ (x y : E),
  Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), V i) x →
    Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), V i) y →
      ∀ (hx : ∑ i : ι, ((V i).starProjection : (a : E) → E) x = x)
        (hy : ∑ i : ι, ((V i).starProjection : (a : E) → E) y = y),
        ∑ i : ι, ((V i).starProjection : (a : E) → E) (x + y) = x + y
Tactic: induction hx using iSup_induction' with
  | mem i x hx =>
    refine
      (Finset.sum_eq_single_of_mem i (Finset.mem_univ _) fun j _ hij => ?_).trans
        (starProjection_eq_self_iff.mpr hx)
    rw [starProjection_apply, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero,
      Submodule.coe_zero]
    exact hV.isOrtho hij.symm hx
  | zero =>
    simp_rw [map_zero, Finset.sum_const_zero]
  | add x y _ _ hx hy =>
    simp_rw [map_add, Finset.sum_add_distrib]
    exact congr_arg₂ (· + ·) hx hy
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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ₗᵢ
i : ι
inst_4 : CompleteSpace.{u_2} ↥(V i)
j : ι
x : ↥(V j)
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i))
      ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E)
        (((of.{u_4, u_2} (fun (i : ι) ↦ ↥(V i)) j : ↥(V j) →+ ⨁ (i : ι), ↥(V i)) : (a : ↥(V j)) → ⨁ (i : ι), ↥(V i)) x :
          ⨁ (i : ι), ↥(V i))) =
    ((((of.{u_4, u_2} (fun (i : ι) ↦ ↥(V i)) j : ↥(V j) →+ ⨁ (i : ι), ↥(V i)) : (a : ↥(V j)) → ⨁ (i : ι), ↥(V i)) x :
          ⨁ (i : ι), ↥(V i)) :
        (a : ι) → ↥(V a))
      i
have of : ((V i).orthogonalProjection : (a : E) → ↥(V i)) (↑x : E) =
  (DFinsupp.single (β := fun (i : ι) ↦ ↥(V i)) j x : (a : ι) → ↥(V a)) i
Tactic: simp_rw [DirectSum.coeAddMonoidHom_of, DirectSum.of,
      -- Need to unfold `DirectSum` to see through the defeq abuse.
      DirectSum, DFinsupp.singleAddHom_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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ₗᵢ
i : ι
inst_4 : CompleteSpace.{u_2} ↥(V i)
j : ι
x : ↥(V j)
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i)) (↑x : E) =
    (DFinsupp.single (β := fun (i : ι) ↦ ↥(V i)) j x : (a : ι) → ↥(V a)) i
have of : ∀ (x : ↥(V i)),
  ((V i).orthogonalProjection : (a : E) → ↥(V i)) (↑x : E) =
    (DFinsupp.single (β := fun (i : ι) ↦ ↥(V i)) i x : (a : ι) → ↥(V a)) i
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
Cleared hypotheses: j, x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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ₗᵢ
i : ι
inst_4 : CompleteSpace.{u_2} ↥(V i)
j : ι
x : ↥(V j)
of :
  ∀ (x : ↥(V i)),
    ((V i).orthogonalProjection : (a : E) → ↥(V i)) (↑x : E) =
      (DFinsupp.single (β := fun (i : ι) ↦ ↥(V i)) i x : (a : ι) → ↥(V a)) i
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i)) (↑x : E) =
    (DFinsupp.single (β := fun (i : ι) ↦ ↥(V i)) j x : (a : ι) → ↥(V a)) i
have of₁ : ∀ (hij : i ≠ j),
  ((V i).orthogonalProjection : (a : E) → ↥(V i)) (↑x : E) =
    (DFinsupp.single (β := fun (i : ι) ↦ ↥(V i)) j x : (a : ι) → ↥(V a)) i
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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ₗᵢ
i : ι
inst_4 : CompleteSpace.{u_2} ↥(V i)
x : ↥(V i)
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i)) (↑x : E) =
    (DFinsupp.single (β := fun (i : ι) ↦ ↥(V i)) i x : (a : ι) → ↥(V a)) i
have of : x = (DFinsupp.single (β := fun (i : ι) ↦ ↥(V i)) i x : (a : ι) → ↥(V a)) i
Tactic: rw [orthogonalProjection_mem_subspace_eq_self, DFinsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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ₗᵢ
i : ι
inst_4 : CompleteSpace.{u_2} ↥(V i)
x : ↥(V i)
of : x = (DFinsupp.single (β := fun (i : ι) ↦ ↥(V i)) i x : (a : ι) → ↥(V a)) i
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i)) (↑x : E) =
    (DFinsupp.single (β := fun (i : ι) ↦ ↥(V i)) i x : (a : ι) → ↥(V a)) i
have of₁ : x = x
Tactic: rw [orthogonalProjection_mem_subspace_eq_self, DFinsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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ₗᵢ
i : ι
inst_4 : CompleteSpace.{u_2} ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i)) (↑x : E) =
    (DFinsupp.single (β := fun (i : ι) ↦ ↥(V i)) j x : (a : ι) → ↥(V a)) i
have of : (↑x : E) ∈ (V i)ᗮ
Tactic: rw [orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero,
        DFinsupp.single_eq_of_ne hij]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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ₗᵢ
i : ι
inst_4 : CompleteSpace.{u_2} ↥(V i)
x y : ⨁ (i : ι), ↥(V i)
hx :
  ((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) x) =
    (x : (a : ι) → ↥(V a)) i
hy :
  ((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) y) =
    (y : (a : ι) → ↥(V a)) i
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i))
      ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) (x + y)) =
    (x + y : (a : ι) → ↥(V a)) i
have add : HAdd.hAdd (α := ↥(V i)) (β := ↥(V i))
    (((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) x) :
      ↥(V i))
    (((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) y) :
      ↥(V i)) =
  (x + y : (a : ι) → ↥(V a)) i
Tactic: simp_rw [map_add]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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ₗᵢ
x : ⨁ (i : ι), ↥(V i)
i : ι
inst_4 : CompleteSpace.{u_2} ↥(V i)
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) x) =
    (x : (a : ι) → ↥(V a)) i
have zero : ((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) 0) =
  ((0 : ⨁ (i : ι), ↥(V i)) : (a : ι) → ↥(V a)) i
Tactic: induction x using DirectSum.induction_on with
  | zero => simp
  | of j x =>
    simp_rw [DirectSum.coeAddMonoidHom_of, DirectSum.of,
      -- Need to unfold `DirectSum` to see through the defeq abuse.
      DirectSum, DFinsupp.singleAddHom_apply]
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [orthogonalProjection_mem_subspace_eq_self, DFinsupp.single_eq_same]
    · rw [orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero,
        DFinsupp.single_eq_of_ne hij]
      exact hV.isOrtho hij.symm x.prop
  | add x y hx hy =>
    simp_rw [map_add]
    exact congr_arg₂ (· + ·) hx hy
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
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ₗᵢ
x : ⨁ (i : ι), ↥(V i)
i : ι
inst_4 : CompleteSpace.{u_2} ↥(V i)
zero :
  ((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) 0) =
    ((0 : ⨁ (i : ι), ↥(V i)) : (a : ι) → ↥(V a)) i
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) x) =
    (x : (a : ι) → ↥(V a)) i
have of : ∀ (j : ι) (x : ↥(V j)),
  ((V i).orthogonalProjection : (a : E) → ↥(V i))
      ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E)
        (((of.{u_4, u_2} (fun (i : ι) ↦ ↥(V i)) j : ↥(V j) →+ ⨁ (i : ι), ↥(V i)) : (a : ↥(V j)) → ⨁ (i : ι), ↥(V i)) x :
          ⨁ (i : ι), ↥(V i))) =
    ((((of.{u_4, u_2} (fun (i : ι) ↦ ↥(V i)) j : ↥(V j) →+ ⨁ (i : ι), ↥(V i)) : (a : ↥(V j)) → ⨁ (i : ι), ↥(V i)) x :
          ⨁ (i : ι), ↥(V i)) :
        (a : ι) → ↥(V a))
      i
Tactic: induction x using DirectSum.induction_on with
  | zero => simp
  | of j x =>
    simp_rw [DirectSum.coeAddMonoidHom_of, DirectSum.of,
      -- Need to unfold `DirectSum` to see through the defeq abuse.
      DirectSum, DFinsupp.singleAddHom_apply]
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [orthogonalProjection_mem_subspace_eq_self, DFinsupp.single_eq_same]
    · rw [orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero,
        DFinsupp.single_eq_of_ne hij]
      exact hV.isOrtho hij.symm x.prop
  | add x y hx hy =>
    simp_rw [map_add]
    exact congr_arg₂ (· + ·) hx hy
Cleared hypotheses: x