awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
classical
  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]
-- 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 : (i : ι) → G i
s : Finset ι
⊢ HPow.hPow (α := 𝕜) (β := ℕ) (↑(Norm.norm.{u_2} (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l i))) : 𝕜) 2 =
    ∑ i ∈ s, HPow.hPow (α := 𝕜) (β := ℕ) (↑‖l i‖ : 𝕜) 2

Tactic:
simp only [← inner_self_eq_norm_sq_to_K, hV.inner_sum]

Premises used: inner_self_eq_norm_sq_to_K, OrthogonalFamily.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
l : (i : ι) → G i
s : Finset ι
⊢ HPow.hPow (α := 𝕜) (β := ℕ) (↑(Norm.norm.{u_2} (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l i))) : 𝕜) 2 =
    ∑ i ∈ s, HPow.hPow (α := 𝕜) (β := ℕ) (↑‖l i‖ : 𝕜) 2

Tactic:
have : ((‖∑ i ∈ s, V i (l i)‖ : ℝ) : 𝕜) ^ 2 = ∑ i ∈ s, ((‖l i‖ : ℝ) : 𝕜) ^ 2 := by
    simp only [← inner_self_eq_norm_sq_to_K, hV.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
l : (i : ι) → G i
s : Finset ι
this :
  HPow.hPow (α := 𝕜) (β := ℕ) (↑(Norm.norm.{u_2} (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l i))) : 𝕜) 2 =
    ∑ i ∈ s, HPow.hPow (α := 𝕜) (β := ℕ) (↑‖l i‖ : 𝕜) 2
⊢ HPow.hPow (β := ℕ) (Norm.norm.{u_2} (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l i))) 2 =
    ∑ i ∈ s, HPow.hPow (β := ℕ) ‖l i‖ 2

Tactic:
mod_cast this

Premises used: algebraMap.coe_sum._simp_1, Norm.norm, algebraMap.coe_pow._simp_1, Real, congrArg, cast, algebraMap.coe_inj._simp_1, HPow.hPow, congr, Eq.refl, OfNat.ofNat, Eq, DFunLike.coe, Finset.sum_congr, Finset.sum, Eq.trans
-- 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 : (i : ι) → G i
s : Finset ι
this :
  HPow.hPow (α := 𝕜) (β := ℕ) (↑(Norm.norm.{u_2} (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l i))) : 𝕜) 2 =
    ∑ i ∈ s, HPow.hPow (α := 𝕜) (β := ℕ) (↑‖l i‖ : 𝕜) 2
⊢ HPow.hPow (β := ℕ) (Norm.norm.{u_2} (E := E) (∑ i ∈ s, (V i : (a : G i) → E) (l i))) 2 =
    ∑ i ∈ s, HPow.hPow (β := ℕ) ‖l i‖ 2

Tactic:
exact mod_cast this
-- 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
γ : Type u_6
f : γ → ι
hf : Function.Injective f
⊢ OrthogonalFamily.{u_1, u_2, u_6, u_5} 𝕜 (E := E) (fun (g : γ) ↦ G (f g)) fun (g : γ) ↦ V (f g)

Tactic:
fun _i _j hij v w => hV (hf.ne hij) v w

Premises used: Function.Injective.ne, OrthogonalFamily, Pairwise
-- 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
left :
  ∀ (i : (i : ι) × α i),
    Norm.norm.{u_2} (E := E)
        ((fun (a : (i : ι) × α i) ↦
            ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
                (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
              E))
          i) =
      1
right :
  Pairwise fun (i j : (i : ι) × α i) ↦
    inner.{u_1, u_2} 𝕜 (E := E)
        ((fun (a : (i : ι) × α i) ↦
            ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
                (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
              E))
          i)
        ((fun (a : (i : ι) × α i) ↦
            ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
                (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
              E))
          j) =
      0
⊢ Orthonormal 𝕜 (E := E) fun (a : (i : ι) × α i) ↦
    (V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
      (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i)))

Tactic:
constructor
-- 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
⊢ Norm.norm.{u_2} (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i v)) =
    1

Tactic:
simpa only [LinearIsometry.norm_map] using (hv_family i).left v

Premises used: LinearIsometry.norm_map, And.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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
j : ι
w : α j
hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) j w
pos :
  ∀ (hij : i = j),
    inner.{u_1, u_2} 𝕜 (E := E)
        ((fun (a : (i : ι) × α i) ↦
            ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
                (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
              E))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
        ((fun (a : (i : ι) × α i) ↦
            ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
                (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
              E))
          (Sigma.mk (β := fun (i : ι) ↦ α i) j w)) =
      0
neg :
  ∀ (hij : ¬i = j),
    inner.{u_1, u_2} 𝕜 (E := E)
        ((fun (a : (i : ι) × α i) ↦
            ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
                (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
              E))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
        ((fun (a : (i : ι) × α i) ↦
            ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
                (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
              E))
          (Sigma.mk (β := fun (i : ι) ↦ α i) j w)) =
      0
⊢ inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) j w)) =
    0

Tactic:
by_cases hij : i = 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
j : ι
w : α j
hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) j w
hij : i = j
pos :
  ∀ (w : α i) (hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) i w),
    inner.{u_1, u_2} 𝕜 (E := E)
        ((fun (a : (i : ι) × α i) ↦
            ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
                (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
              E))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
        ((fun (a : (i : ι) × α i) ↦
            ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
                (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
              E))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i w)) =
      0
⊢ inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) j w)) =
    0

Tactic:
subst hij
-- 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v w : α i
hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) i w
h : v = w
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) i v

Tactic:
subst 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) i v
⊢ False

Tactic:
hvw 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
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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) i v
⊢ False

Tactic:
exact hvw 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
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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v w : α i
hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) i w
⊢ v ≠ w

Tactic:
have : v ≠ w := fun h => by
      subst h
      exact hvw 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v w : α i
hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) i w
this : v ≠ w
⊢ inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i w)) =
    0

Tactic:
simpa only [LinearIsometry.inner_map_map] using (hv_family i).2 this

Premises used: LinearIsometry.inner_map_map, And.right
-- 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
j : ι
w : α j
hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) j w
hij : ¬i = j
⊢ inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) j w)) =
    0

Tactic:
hV hij (v_family i v) (v_family j 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
α : ι → Type u_6
v_family : (i : ι) → α i → G i
hv_family : ∀ (i : ι), Orthonormal 𝕜 (v_family i)
i : ι
v : α i
j : ι
w : α j
hvw : Sigma.mk (β := fun (i : ι) ↦ α i) i v ≠ Sigma.mk (β := fun (i : ι) ↦ α i) j w
hij : ¬i = j
⊢ inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i v))
      ((fun (a : (i : ι) × α i) ↦
          ((V (a.fst (β := fun (i : ι) ↦ α i)) : (a : G a.fst) → E)
              (v_family (a.fst (β := fun (i : ι) ↦ α i)) (a.snd (β := fun (i : ι) ↦ α i))) :
            E))
        (Sigma.mk (β := fun (i : ι) ↦ α i) j w)) =
    0

Tactic:
exact hV hij (v_family i v) (v_family j 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 ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
rw :
  HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (∑ x ∈ s₁ \ s₂, (V x : (a : G x) → E) (f x)) (∑ x ∈ s₂ \ s₁, -(V x : (a : G x) → E) (f x))‖
      2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2)
⊢ HPow.hPow (β := ℕ)
      ‖HSub.hSub (α := E) (∑ i ∈ s₁, (V i : (a : G i) → E) (f i)) (∑ i ∈ s₂, (V i : (a : G i) → E) (f i))‖ 2 =
    HAdd.hAdd (α := ℝ) (∑ i ∈ s₁ \ s₂, HPow.hPow (β := ℕ) ‖f i‖ 2) (∑ i ∈ s₂ \ s₁, HPow.hPow (β := ℕ) ‖f i‖ 2)

Tactic:
rw [← Finset.sum_sdiff_sub_sum_sdiff, sub_eq_add_neg, ← Finset.sum_neg_distrib]

Premises used: sub_eq_add_neg, Finset.sum_sdiff_sub_sum_sdiff, Finset.sum_neg_distrib
-- 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 ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
⊢ ∀ i ∈ s₁ \ s₂, F i = f i

Tactic:
have hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i := fun i hi => if_pos (Finset.sdiff_subset hi)
-- 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 ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
⊢ ∀ i ∈ s₂ \ s₁, F i = -f i

Tactic:
have hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i := fun i hi => if_neg (Finset.mem_sdiff.mp hi).2
-- 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 ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
i : ι
dsimp : ‖if i ∈ s₁ then f i else -f i‖ = ‖f i‖
⊢ ‖F i‖ = ‖f i‖

Tactic:
dsimp only [F]
-- 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 ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
i : ι
pos : i ∈ s₁ → ‖f i‖ = ‖f i‖
neg : i ∉ s₁ → ‖-f i‖ = ‖f i‖
⊢ ‖if i ∈ s₁ then f i else -f i‖ = ‖f i‖

Tactic:
split_ifs
-- 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 ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
i : ι
h : i ∈ s₁
⊢ ‖f i‖ = ‖f i‖

Tactic:
simp only [norm_neg]

Premises used: norm_neg
-- 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 ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun (i : ι) ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
i : ι
h : i ∉ s₁
⊢ ‖-f i‖ = ‖f i‖

Tactic:
simp only [norm_neg]

Premises used: norm_neg