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
ι : 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:
exact hV.isOrtho hij.symm hx

Premises used: Ne.symm, OrthogonalFamily.isOrtho
-- 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 : E
zero : Eq.{u_2 + 1} (α := E) (∑ x : ι, 0) 0
⊢ Eq.{u_2 + 1} (α := E) (∑ i : ι, ((V i).starProjection : (a : E) → E) 0) 0

Tactic:
simp_rw [map_zero, Finset.sum_const_zero]

Premises used: map_zero, Finset.sum_const_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 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
add :
  HAdd.hAdd (α := E) (∑ x_2 : ι, ((V x_2).starProjection : (a : E) → E) x)
      (∑ x : ι, ((V x).starProjection : (a : E) → E) y) =
    x + y
⊢ ∑ i : ι, ((V i).starProjection : (a : E) → E) (x + y) = x + y

Tactic:
simp_rw [map_add, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, map_add
-- 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 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
⊢ HAdd.hAdd (α := E) (∑ x_2 : ι, ((V x_2).starProjection : (a : E) → E) x)
      (∑ x : ι, ((V x).starProjection : (a : E) → E) y) =
    x + y

Tactic:
congr_arg₂ (· + ·) hx hy

Premises used: HAdd.hAdd, congr_arg₂
-- 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 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
⊢ HAdd.hAdd (α := E) (∑ x_2 : ι, ((V x_2).starProjection : (a : E) → E) x)
      (∑ x : ι, ((V x).starProjection : (a : E) → E) y) =
    x + y

Tactic:
exact congr_arg₂ (· + ·) hx hy

Premises used: HAdd.hAdd, congr_arg₂
-- 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 : 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
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
⊢ ∑ 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

Premises used: Finset.sum_add_distrib, Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, map_zero, map_add, Submodule.starProjection_apply, Submodule.coe_zero, Finset.sum_const_zero, Submodule.zero, Submodule.add
-- 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ₗᵢ
i : ι
inst_4 : CompleteSpace.{u_2} ↥(V i)
⊢ ((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:
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
ι : 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 :
  ((V i).orthogonalProjection : (a : E) → ↥(V i)) (↑x : E) =
    (DFinsupp.single (β := fun (i : ι) ↦ ↥(V i)) j x : (a : ι) → ↥(V a)) i
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i))
      ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E)
        (((DirectSum.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))) =
    ((((DirectSum.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:
simp_rw [DirectSum.coeAddMonoidHom_of, DirectSum.of,
      -- Need to unfold `DirectSum` to see through the defeq abuse.
      DirectSum, DFinsupp.singleAddHom_apply]

Premises used: DirectSum.coeAddMonoidHom_of, DirectSum.of, DFinsupp.singleAddHom_apply, DirectSum
-- 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ₗᵢ
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
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
⊢ ((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

Premises used: Decidable.eq_or_ne, rfl
-- 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ₗᵢ
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
of₁ of₂ : x = x
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i)) (↑x : E) =
    (DFinsupp.single (β := fun (i : ι) ↦ ↥(V i)) i x : (a : ι) → ↥(V a)) i

Tactic:
rw [orthogonalProjection_mem_subspace_eq_self, DFinsupp.single_eq_same]

Premises used: DFinsupp.single_eq_same, Submodule.orthogonalProjection_mem_subspace_eq_self
-- 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ₗᵢ
i : ι
inst_4 : CompleteSpace.{u_2} ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
of : (↑x : E) ∈ (V i)ᗮ
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i)) (↑x : E) =
    (DFinsupp.single (β := fun (i : ι) ↦ ↥(V i)) j x : (a : ι) → ↥(V a)) i

Tactic:
rw [orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero,
        DFinsupp.single_eq_of_ne hij]

Premises used: Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, DFinsupp.single_eq_of_ne
-- 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ₗᵢ
i : ι
inst_4 : CompleteSpace.{u_2} ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
⊢ (↑x : E) ∈ (V i)ᗮ

Tactic:
hV.isOrtho hij.symm x.prop

Premises used: Ne.symm, OrthogonalFamily.isOrtho, Subtype.prop
-- 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ₗᵢ
i : ι
inst_4 : CompleteSpace.{u_2} ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
⊢ (↑x : E) ∈ (V i)ᗮ

Tactic:
exact hV.isOrtho hij.symm x.prop

Premises used: Ne.symm, OrthogonalFamily.isOrtho, Subtype.prop
-- 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ₗᵢ
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
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
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i))
      ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) (x + y)) =
    (x + y : (a : ι) → ↥(V a)) i

Tactic:
simp_rw [map_add]

Premises used: map_add
-- 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ₗᵢ
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
⊢ 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:
congr_arg₂ (· + ·) hx hy

Premises used: HAdd.hAdd, congr_arg₂
-- 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ₗᵢ
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
⊢ 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:
exact congr_arg₂ (· + ·) hx hy

Premises used: HAdd.hAdd, congr_arg₂
-- 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ₗᵢ
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
of :
  ∀ (j : ι) (x : ↥(V j)),
    ((V i).orthogonalProjection : (a : E) → ↥(V i))
        ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E)
          (((DirectSum.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))) =
      ((((DirectSum.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
add :
  ∀ (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
⊢ ((V i).orthogonalProjection : (a : E) → ↥(V i)) ((DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E) x) =
    (x : (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

Premises used: DFinsupp.single_eq_same, Submodule.orthogonalProjection_mem_subspace_eq_self, Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, map_add, DirectSum.coeAddMonoidHom_of, DirectSum.of, Submodule.zero, DFinsupp.singleAddHom_apply, Submodule.add, DirectSum, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (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ₗᵢ
h : iSup V = ⊤
x : E
dsimp :
  (DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E)
      ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
          (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
        fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x) =
    x
⊢ (DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E)
      ((fun (x : E) ↦
          ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
                (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
              fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x :
            Π₀ (i : ι), ↥(V i)))
        x) =
    x

Tactic:
dsimp only
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (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ₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun (i : ι) ↦ Classical.decEq ↥(V i)
rw :
  (DFinsupp.sumAddHom (β := fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ AddSubmonoidClass.subtype (V i) :
        (a : ⨁ (i : ι), ↥(V i)) → E)
      ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
          (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
        fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x) =
    x
⊢ (DirectSum.coeAddMonoidHom V : (a : ⨁ (i : ι), ↥(V i)) → E)
      ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
          (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
        fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x) =
    x

Tactic:
rw [DirectSum.coeAddMonoidHom, DirectSum.toAddMonoid, DFinsupp.liftAddHom_apply]

Premises used: DFinsupp.liftAddHom_apply, DirectSum.coeAddMonoidHom, DirectSum.toAddMonoid
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (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ₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun (i : ι) ↦ Classical.decEq ↥(V i)
erw :
  (DFinsupp.sum (β := fun (i : ι) ↦ ↥(V i))
      ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
          (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
        fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x)
      fun (x : ι) ↦ (⇑(AddSubmonoidClass.subtype (V x) : ↥(V x) →+ E) : (a : ↥(V x)) → E)) =
    x
⊢ (DFinsupp.sumAddHom (β := fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ AddSubmonoidClass.subtype (V i) :
        (a : ⨁ (i : ι), ↥(V i)) → E)
      ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
          (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
        fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x) =
    x

Tactic:
erw [DFinsupp.sumAddHom_apply]

Premises used: DFinsupp.sumAddHom_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (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ₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun (i : ι) ↦ Classical.decEq ↥(V i)
rw :
  ∑ i : ι,
      ((AddSubmonoidClass.subtype (V i) : ↥(V i) →+ E) : (a : ↥(V i)) → E)
        ((DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i)) : (a : Π₀ (i : ι), ↥(V i)) → (i : ι) → ↥(V i))
            ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
                (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
              fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x)
            i :
          ↥(V i)) =
    x
hf : ∀ (i : ι), Eq (α := E) (((AddSubmonoidClass.subtype (V i) : ↥(V i) →+ E) : (a : ↥(V i)) → E) 0 : E) (0 : E)
⊢ (DFinsupp.sum (β := fun (i : ι) ↦ ↥(V i))
      ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
          (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
        fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x)
      fun (x : ι) ↦ (⇑(AddSubmonoidClass.subtype (V x) : ↥(V x) →+ E) : (a : ↥(V x)) → E)) =
    x

Tactic:
rw [DFinsupp.sum_eq_sum_fintype]

Premises used: DFinsupp.sum_eq_sum_fintype
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
V : ι → Submodule 𝕜 E
inst_7 : ∀ (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ₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun (i : ι) ↦ Classical.decEq ↥(V i)
simp_rw : ∑ x_1 : ι, (↑(((V x_1).orthogonalProjection : (a : E) → ↥(V x_1)) x) : E) = x
⊢ ∑ i : ι,
      ((AddSubmonoidClass.subtype (V i) : ↥(V i) →+ E) : (a : ↥(V i)) → E)
        ((DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i)) : (a : Π₀ (i : ι), ↥(V i)) → (i : ι) → ↥(V i))
            ((Equiv.symm (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦ ↥(V i))) :
                (a : (i : ι) → ↥(V i)) → Π₀ (i : ι), ↥(V i))
              fun (i : ι) ↦ ((V i).orthogonalProjection : (a : E) → ↥(V i)) x)
            i :
          ↥(V i)) =
    x

Tactic:
simp_rw [Equiv.apply_symm_apply, AddSubmonoidClass.coe_subtype]

Premises used: Equiv.apply_symm_apply, AddSubmonoidClass.coe_subtype