awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f_1 p f g : H →L[𝕜] H
hx :
  Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s)) f
hy :
  Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s)) g
hf : f.IsPositive
hg : g.IsPositive
⊢ (f + g).IsPositive

Tactic:
hf.add hg

Premises used: ContinuousLinearMap.IsPositive.add
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f_1 p f g : H →L[𝕜] H
hx :
  Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s)) f
hy :
  Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s)) g
hf : f.IsPositive
hg : g.IsPositive
⊢ (f + g).IsPositive

Tactic:
exact hf.add hg

Premises used: ContinuousLinearMap.IsPositive.add
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f p : H →L[𝕜] H
hp :
  Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s)) p
mpr :
  ∀ (x : H →L[𝕜] H) (hf : Membership.mem (γ := Set (H →L[𝕜] H)) (Set.range fun (s : H →L[𝕜] H) ↦ star s * s) x),
    x.IsPositive
mpr₁ : IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := H) 0
mpr₂ :
  ∀ (f g : H →L[𝕜] H),
    Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
        f →
      Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
          g →
        ∀ (hf : f.IsPositive) (hg : g.IsPositive), (f + g).IsPositive
⊢ p.IsPositive

Tactic:
induction hp using AddSubmonoid.closure_induction with
      | mem _ hf =>
        obtain ⟨f, rfl⟩ := hf
        simpa using ContinuousLinearMap.IsPositive.adjoint_conj isPositive_one f
      | zero => exact isPositive_zero
      | add f g _ _ hf hg => exact hf.add hg

Premises used: ContinuousLinearMap.zero, ContinuousLinearMap.add, ContinuousLinearMap.IsPositive.adjoint_conj, ContinuousLinearMap.isPositive_zero, ContinuousLinearMap.isPositive_one, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.StarOrder
Goal:
𝕜 : Type u_1
H_1 : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H_1
inst_2 : InnerProductSpace 𝕜 H_1
inst_3 : CompleteSpace H_1
inst_4 : Algebra ℝ (H_1 →L[𝕜] H_1)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H_1 →L[𝕜] H_1)
H : Type u_3
inst_6 : NormedAddCommGroup H
inst_7 : InnerProductSpace ℂ H
inst_8 : CompleteSpace H
⊢ StarOrderedRing.{u_3} (H →L[ℂ] H)

Tactic:
instStarOrderedRingRCLike

Premises used: ContinuousLinearMap.instStarOrderedRingRCLike
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
W : Submodule 𝕜 E
x y : ↥W
⊢ ⟪x, y⟫ = ⟪(↑x : E), (↑y : E)⟫

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
s : Submodule 𝕜 E
hvs : ∀ (i : ι), v i ∈ s
⊢ Orthonormal 𝕜 (Set.codRestrict v (↑s : Set E) hvs)

Tactic:
s.subtypeₗᵢ.orthonormal_comp_iff.mp hv

Premises used: Set.Mem, LinearIsometry.orthonormal_comp_iff, Iff.mp, Submodule.subtypeₗᵢ
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
⊢ Orthonormal.{u_1, u_2, u_4} 𝕜 (E := ↥(Submodule.span 𝕜 (Set.range v))) fun (i : ι) ↦
    Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Submodule 𝕜 E) (Submodule.span 𝕜 (Set.range v)) x) (v i) ⋯

Tactic:
hv.codRestrict (Submodule.span 𝕜 (Set.range v)) fun i =>
    Submodule.subset_span (Set.mem_range_self i)

Premises used: Set.mem_range_self, Orthonormal.codRestrict, Submodule.span, Set.codRestrict, Submodule.subset_span, Set.range
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
hij : i ≠ j
a : (fun (_i : ι) ↦ 𝕜) i
b : (fun (_i : ι) ↦ 𝕜) j
⊢ inner.{u_1, u_2} 𝕜 (E := E)
      (((fun (i : ι) ↦ (LinearIsometry.toSpanSingleton 𝕜 E ⋯ : 𝕜 →ₗᵢ[𝕜] E)) i : (a : (fun (_i : ι) ↦ 𝕜) i) → E) a : E)
      (((fun (i : ι) ↦ (LinearIsometry.toSpanSingleton 𝕜 E ⋯ : 𝕜 →ₗᵢ[𝕜] E)) j : (a : (fun (_i : ι) ↦ 𝕜) j) → E) b : E) =
    0

Tactic:
simp [inner_smul_left, inner_smul_right, hv.2 hij]

Premises used: inner_smul_right, And.right, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : DecidableEq ι
i j : ι
v : G i
w : G j
pos :
  ∀ (h : i = j),
    inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) =
      inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E)
neg : ∀ (h : ¬i = j), inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) = 0
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) =
    if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : DecidableEq ι
i j : ι
v : G i
w : G j
h : i = j
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) =
    inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E)

Tactic:
rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : DecidableEq ι
i j : ι
v : G i
w : G j
h : ¬i = j
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) = 0

Tactic:
hV h v w
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : DecidableEq ι
i j : ι
v : G i
w : G j
h : ¬i = j
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) = 0

Tactic:
exact hV h v w
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst_6 : DecidableEq ι
l : ⨁ (i : ι), G i
i : ι
v : G i
simp :
  (if (l : (a : ι) → G a) i ≠ 0 then
      inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V i : (a : G i) → E) ((l : (a : ι) → G a) i) : E)
    else 0) =
    ⟪v, (l : (a : ι) → G a) i⟫
⊢ (DFinsupp.sum (β := fun (i : ι) ↦ G i) l fun (j : ι) (w : G j) ↦
      if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) else 0) =
    ⟪v, (l : (a : ι) → G a) i⟫

Tactic:
simp only [DFinsupp.sum, Finset.sum_ite_eq,
        DFinsupp.mem_support_toFun]

Premises used: DFinsupp.mem_support_toFun, DFinsupp.sum, Finset.sum_ite_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst_6 : DecidableEq ι
l : ⨁ (i : ι), G i
i : ι
v : G i
pos :
  ∀ (h : (l : (a : ι) → G a) i ≠ 0),
    inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V i : (a : G i) → E) ((l : (a : ι) → G a) i) : E) =
      ⟪v, (l : (a : ι) → G a) i⟫
neg : ∀ (h : ¬(l : (a : ι) → G a) i ≠ 0), 0 = ⟪v, (l : (a : ι) → G a) i⟫
⊢ (if (l : (a : ι) → G a) i ≠ 0 then
      inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V i : (a : G i) → E) ((l : (a : ι) → G a) i) : E)
    else 0) =
    ⟪v, (l : (a : ι) → G a) i⟫

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst_6 : DecidableEq ι
l : ⨁ (i : ι), G i
i : ι
v : G i
h : (l : (a : ι) → G a) i ≠ 0
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V i : (a : G i) → E) ((l : (a : ι) → G a) i) : E) =
    ⟪v, (l : (a : ι) → G a) i⟫

Tactic:
simp only [LinearIsometry.inner_map_map]

Premises used: LinearIsometry.inner_map_map
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst_6 : DecidableEq ι
l : ⨁ (i : ι), G i
i : ι
v : G i
h : ¬(l : (a : ι) → G a) i ≠ 0
⊢ 0 = ⟪v, (l : (a : ι) → G a) i⟫

Tactic:
simp only [of_not_not h, inner_zero_right]

Premises used: inner_zero_right, of_not_not
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
rw rw₁ :
  Eq.{u_1 + 1} (α := 𝕜)
    (∑ i_1 : ι, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V i_1 : (a : G i_1) → E) (l i_1) : E))
    (∑ j : ι, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E))
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) (∑ j : ι, (V j : (a : G j) → E) (l j) : E) =
    ∑ j : ι, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E)

Tactic:
rw [inner_sum]

Premises used: inner_sum
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (∑ j : ι, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E))
    (∑ j : ι,
      if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E) else 0)

Tactic:
(congr_arg (Finset.sum Finset.univ) <| funext fun j => hV.eq_ite v (l j))

Premises used: Finset.univ, congr_arg, funext, OrthogonalFamily.eq_ite, Finset.sum
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
⊢ (∑ j : ι,
      if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E)
      else 0) =
    ⟪v, l i⟫

Tactic:
simp only [Finset.sum_ite_eq, Finset.mem_univ, (V i).inner_map_map, if_true]

Premises used: Finset.mem_univ, if_true, LinearIsometry.inner_map_map, Finset.sum_ite_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
i₁ :
  inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) (∑ j : ι, (V j : (a : G j) → E) (l j) : E) =
    ∑ j : ι, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E)
i₂ :
  (∑ j : ι,
      if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E)
      else 0) =
    ⟪v, l i⟫
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) (∑ j : ι, (V j : (a : G j) → E) (l j) : E) = ⟪v, l i⟫

Tactic:
calc
    ⟪V i v, ∑ j : ι, V j (l j)⟫ = ∑ j : ι, ⟪V i v, V j (l j)⟫ := by rw [inner_sum]
    _ = ∑ j, ite (i = j) ⟪V i v, V j (l j)⟫ 0 :=
      (congr_arg (Finset.sum Finset.univ) <| funext fun j => hV.eq_ite v (l j))
    _ = ⟪v, l i⟫ := by
      simp only [Finset.sum_ite_eq, Finset.mem_univ, (V i).inner_map_map, if_true]

Premises used: Finset.univ, congr_arg, funext, OrthogonalFamily.eq_ite, DFunLike.coe, Finset.sum
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
i₁ :
  inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) (∑ j : ι, (V j : (a : G j) → E) (l j) : E) =
    ∑ j : ι, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E)
i₂ :
  (∑ j : ι,
      if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E)
      else 0) =
    ⟪v, l i⟫
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) (∑ j : ι, (V j : (a : G j) → E) (l j) : E) = ⟪v, l i⟫

Tactic:
classical
  calc
    ⟪V i v, ∑ j : ι, V j (l j)⟫ = ∑ j : ι, ⟪V i v, V j (l j)⟫ := by rw [inner_sum]
    _ = ∑ j, ite (i = j) ⟪V i v, V j (l j)⟫ 0 :=
      (congr_arg (Finset.sum Finset.univ) <| funext fun j => hV.eq_ite v (l j))
    _ = ⟪v, l i⟫ := by
      simp only [Finset.sum_ite_eq, Finset.mem_univ, (V i).inner_map_map, if_true]

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
⊢ inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
    ∑ j ∈ s, ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)

Tactic:
simp only [sum_inner, inner_sum]

Premises used: inner_sum, sum_inner
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
e_f :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := 𝕜)
      (∑ i_1 ∈ s,
        inner.{u_1, u_2} 𝕜 (E := E) ((V i_1 : (a : G i_1) → E) (l₁ i_1) : E) ((V i : (a : G i) → E) (l₂ i) : E))
      (∑ i_1 ∈ s,
        if i_1 = i then
          inner.{u_1, u_2} 𝕜 (E := E) ((V i_1 : (a : G i_1) → E) (l₁ i_1) : E) ((V i : (a : G i) → E) (l₂ i) : E)
        else 0)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (∑ j ∈ s,
      ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E))
    (∑ j ∈ s,
      ∑ i ∈ s,
        if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
        else 0)

Tactic:
congr with i
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
i : ι
e_f :
  ∀ (j : ι),
    inner.{u_1, u_2} 𝕜 (E := E) ((V j : (a : G j) → E) (l₁ j) : E) ((V i : (a : G i) → E) (l₂ i) : E) =
      if j = i then inner.{u_1, u_2} 𝕜 (E := E) ((V j : (a : G j) → E) (l₁ j) : E) ((V i : (a : G i) → E) (l₂ i) : E)
      else 0
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (∑ i_1 ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i_1 : (a : G i_1) → E) (l₁ i_1) : E) ((V i : (a : G i) → E) (l₂ i) : E))
    (∑ i_1 ∈ s,
      if i_1 = i then
        inner.{u_1, u_2} 𝕜 (E := E) ((V i_1 : (a : G i_1) → E) (l₁ i_1) : E) ((V i : (a : G i) → E) (l₂ i) : E)
      else 0)

Tactic:
congr with j
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
i j : ι
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V j : (a : G j) → E) (l₁ j) : E) ((V i : (a : G i) → E) (l₂ i) : E) =
    if j = i then inner.{u_1, u_2} 𝕜 (E := E) ((V j : (a : G j) → E) (l₁ j) : E) ((V i : (a : G i) → E) (l₂ i) : E)
    else 0

Tactic:
apply hV.eq_ite

Premises used: OrthogonalFamily.eq_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (∑ j ∈ s,
      ∑ i ∈ s,
        if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
        else 0)
    (∑ i ∈ s, ⟪l₁ i, l₂ i⟫)

Tactic:
simp only [Finset.sum_ite_of_true, Finset.sum_ite_eq', LinearIsometry.inner_map_map,
        imp_self, imp_true_iff]

Premises used: Finset.sum_ite_eq', LinearIsometry.inner_map_map, imp_true_iff, imp_self, Finset.sum_ite_of_true
-- Module: Mathlib.Analysis.InnerProductSpace.Subspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
i :
  inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
    ∑ j ∈ s, ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
i₁ :
  Eq.{u_1 + 1} (α := 𝕜)
    (∑ j ∈ s,
      ∑ i ∈ s, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E))
    (∑ j ∈ s,
      ∑ i ∈ s,
        if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
        else 0)
i₂ :
  Eq.{u_1 + 1} (α := 𝕜)
    (∑ j ∈ s,
      ∑ i ∈ s,
        if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) (l₁ i) : E) ((V j : (a : G j) → E) (l₂ j) : E)
        else 0)
    (∑ i ∈ s, ⟪l₁ i, l₂ i⟫)
⊢ inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l₁ i)) (∑ j ∈ s, (V j : (a : G j) → E) (l₂ j)) =
    ∑ i ∈ s, ⟪l₁ i, l₂ i⟫

Tactic:
calc
    ⟪∑ i ∈ s, V i (l₁ i), ∑ j ∈ s, V j (l₂ j)⟫ = ∑ j ∈ s, ∑ i ∈ s, ⟪V i (l₁ i), V j (l₂ j)⟫ := by
      simp only [sum_inner, inner_sum]
    _ = ∑ j ∈ s, ∑ i ∈ s, ite (i = j) ⟪V i (l₁ i), V j (l₂ j)⟫ 0 := by
      congr with i
      congr with j
      apply hV.eq_ite
    _ = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫ := by
      simp only [Finset.sum_ite_of_true, Finset.sum_ite_eq', LinearIsometry.inner_map_map,
        imp_self, imp_true_iff]