awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
h1 :
  ∑ x ∈ c.support,
      ∑ y ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜)
            (gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v) x y))
          ((c : (a : n) → 𝕜) y : 𝕜) =
    HPow.hPow (α := 𝕜) (β := ℕ)
      (↑(Norm.norm.{u_5} (E := F)
            ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) :
              F)) :
        𝕜)
      2
h2 :
  HPow.hPow (β := ℕ) ‖f‖ 2 •
      HPow.hPow (α := 𝕜) (β := ℕ)
        (↑(Norm.norm.{u_1} (E := E)
              (∑ i ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) i : 𝕜) (v i))) :
          𝕜)
        2 =
    ∑ x ∈ c.support,
      ∑ y ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜) (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v x y))
          ((c : (a : n) → 𝕜) y : 𝕜)
⊢ LE.le.{u_4} (α := 𝕜)
    (∑ x ∈ c.support,
      ∑ x_1 ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜)
            (gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v) x x_1))
          ((c : (a : n) → 𝕜) x_1 : 𝕜))
    (∑ x ∈ c.support,
      ∑ x_1 ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜) (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v x x_1))
          ((c : (a : n) → 𝕜) x_1 : 𝕜))

Tactic:
calc
    ∑ x ∈ c.support, ∑ y ∈ c.support, star (c x) * gram 𝕜 (f ∘ v) x y * c y
    _ = (‖f (∑ x ∈ c.support, c x • v x)‖ : 𝕜) ^ 2 := ?h1
    _ ≤ ‖f‖ ^ 2 • (‖∑ i ∈ c.support, c i • v i‖ : 𝕜) ^ 2 := by
      norm_cast
      grw [f.le_opNorm _, smul_eq_mul, ← mul_pow]
    _ = ∑ x ∈ c.support, ∑ y ∈ c.support, star (c x) * ‖f‖ ^ 2 • gram 𝕜 v x y * c y := ?h2

Premises used: Norm.norm, Finsupp.support, RCLike.ofReal, HSMul.hSMul, DFunLike.coe, Finset.sum
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
h1 :
  ∑ y ∈ c.support,
      ∑ x ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜)
            (gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v) x y))
          ((c : (a : n) → 𝕜) y : 𝕜) =
    HPow.hPow (α := 𝕜) (β := ℕ)
      (↑(Norm.norm.{u_5} (E := F)
            ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) :
              F)) :
        𝕜)
      2
⊢ ∑ x ∈ c.support,
      ∑ y ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜)
            (gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v) x y))
          ((c : (a : n) → 𝕜) y : 𝕜) =
    HPow.hPow (α := 𝕜) (β := ℕ)
      (↑(Norm.norm.{u_5} (E := F)
            ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) :
              F)) :
        𝕜)
      2

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
h1 :
  Eq.{u_4 + 1} (α := 𝕜)
    (∑ x ∈ c.support,
      ∑ x_1 ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((c : (a : n) → 𝕜) x_1 : 𝕜) : 𝕜)
            (inner.{u_4, u_5} 𝕜 (E := F) ((f : (a : E) → F) (v x_1) : F) ((f : (a : E) → F) (v x) : F)))
          ((c : (a : n) → 𝕜) x : 𝕜))
    (∑ x ∈ c.support,
      ∑ i ∈ c.support,
        HMul.hMul (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜)
          (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((c : (a : n) → 𝕜) i : 𝕜) : 𝕜)
            (inner.{u_4, u_5} 𝕜 (E := F) ((f : (a : E) → F) (v i) : F) ((f : (a : E) → F) (v x) : F))))
⊢ ∑ y ∈ c.support,
      ∑ x ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜)
            (gram.{u_5, u_2, u_4} (E := F) 𝕜 ((⇑f : (a : E) → F) ∘ v) x y))
          ((c : (a : n) → 𝕜) y : 𝕜) =
    HPow.hPow (α := 𝕜) (β := ℕ)
      (↑(Norm.norm.{u_5} (E := F)
            ((f : (a : E) → F) (∑ x ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜) (v x)) :
              F)) :
        𝕜)
      2

Tactic:
simp [← inner_self_eq_norm_sq_to_K, inner_sum, sum_inner, inner_smul_left, inner_smul_right,
      Finset.mul_sum, Finset.smul_sum, RCLike.real_smul_eq_coe_mul]

Premises used: Finset.mul_sum, inner_sum, inner_self_eq_norm_sq_to_K, sum_inner, inner_smul_right, Finset.smul_sum, RCLike.real_smul_eq_coe_mul, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ Eq.{u_4 + 1} (α := 𝕜)
    (∑ x ∈ c.support,
      ∑ x_1 ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((c : (a : n) → 𝕜) x_1 : 𝕜) : 𝕜)
            (inner.{u_4, u_5} 𝕜 (E := F) ((f : (a : E) → F) (v x_1) : F) ((f : (a : E) → F) (v x) : F)))
          ((c : (a : n) → 𝕜) x : 𝕜))
    (∑ x ∈ c.support,
      ∑ i ∈ c.support,
        HMul.hMul (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜)
          (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((c : (a : n) → 𝕜) i : 𝕜) : 𝕜)
            (inner.{u_4, u_5} 𝕜 (E := F) ((f : (a : E) → F) (v i) : F) ((f : (a : E) → F) (v x) : F))))

Tactic:
grind
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
h2 :
  HPow.hPow (β := ℕ) ‖f‖ 2 •
      HPow.hPow (α := 𝕜) (β := ℕ)
        (↑(Norm.norm.{u_1} (E := E)
              (∑ i ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) i : 𝕜) (v i))) :
          𝕜)
        2 =
    ∑ y ∈ c.support,
      ∑ x ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜) (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v x y))
          ((c : (a : n) → 𝕜) y : 𝕜)
⊢ HPow.hPow (β := ℕ) ‖f‖ 2 •
      HPow.hPow (α := 𝕜) (β := ℕ)
        (↑(Norm.norm.{u_1} (E := E)
              (∑ i ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) i : 𝕜) (v i))) :
          𝕜)
        2 =
    ∑ x ∈ c.support,
      ∑ y ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜) (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v x y))
          ((c : (a : n) → 𝕜) y : 𝕜)

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
h2 :
  Eq.{u_4 + 1} (α := 𝕜)
    (∑ x ∈ c.support,
      ∑ x_1 ∈ c.support,
        HPow.hPow (α := 𝕜) (β := ℕ) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖f‖ : 𝕜) 2 *
          HMul.hMul (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜)
            (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((c : (a : n) → 𝕜) x_1 : 𝕜) : 𝕜) ⟪v x_1, v x⟫_𝕜))
    (∑ x ∈ c.support,
      ∑ x_1 ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((c : (a : n) → 𝕜) x_1 : 𝕜) : 𝕜)
            (HPow.hPow (α := 𝕜) (β := ℕ) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖f‖ : 𝕜) 2 * ⟪v x_1, v x⟫_𝕜))
          ((c : (a : n) → 𝕜) x : 𝕜))
⊢ HPow.hPow (β := ℕ) ‖f‖ 2 •
      HPow.hPow (α := 𝕜) (β := ℕ)
        (↑(Norm.norm.{u_1} (E := E)
              (∑ i ∈ c.support, HSMul.hSMul.{u_4, u_1, u_1} (α := 𝕜) ((c : (a : n) → 𝕜) i : 𝕜) (v i))) :
          𝕜)
        2 =
    ∑ y ∈ c.support,
      ∑ x ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (star ((c : (a : n) → 𝕜) x) : 𝕜) (HPow.hPow (β := ℕ) ‖f‖ 2 • gram 𝕜 v x y))
          ((c : (a : n) → 𝕜) y : 𝕜)

Tactic:
simp [← inner_self_eq_norm_sq_to_K, inner_sum, sum_inner, inner_smul_left, inner_smul_right,
      Finset.mul_sum, Finset.smul_sum, RCLike.real_smul_eq_coe_mul]

Premises used: Finset.mul_sum, inner_sum, inner_self_eq_norm_sq_to_K, sum_inner, inner_smul_right, Finset.smul_sum, RCLike.real_smul_eq_coe_mul, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ Eq.{u_4 + 1} (α := 𝕜)
    (∑ x ∈ c.support,
      ∑ x_1 ∈ c.support,
        HPow.hPow (α := 𝕜) (β := ℕ) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖f‖ : 𝕜) 2 *
          HMul.hMul (α := 𝕜) ((c : (a : n) → 𝕜) x : 𝕜)
            (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((c : (a : n) → 𝕜) x_1 : 𝕜) : 𝕜) ⟪v x_1, v x⟫_𝕜))
    (∑ x ∈ c.support,
      ∑ x_1 ∈ c.support,
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((c : (a : n) → 𝕜) x_1 : 𝕜) : 𝕜)
            (HPow.hPow (α := 𝕜) (β := ℕ) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) ‖f‖ : 𝕜) 2 * ⟪v x_1, v x⟫_𝕜))
          ((c : (a : n) → 𝕜) x : 𝕜))

Tactic:
grind
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
ι : Type u_3
inst : LinearOrder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : WellFoundedLT ι
n : ι
i : ↥(Iio n)
⊢ (↑i : ι) < n

Tactic:
mem_Iio.1 i.2

Premises used: Iff.mp, Finset.mem_Iio, Subtype.property
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
ι : Type u_3
inst : LinearOrder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : WellFoundedLT ι
n : ι
i : ↥(Iio n)
⊢ (↑i : ι) < n

Tactic:
exact mem_Iio.1 i.2

Premises used: Iff.mp, Finset.mem_Iio, Subtype.property
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
ι : Type u_3
inst : LinearOrder ι
inst_1 : LocallyFiniteOrderBot ι
inst_2 : WellFoundedLT ι
n : ι
i : ↥(Iio n)
⊢ (↑i : ι) < n

Tactic:
decreasing_by exact mem_Iio.1 i.2

Premises used: Iff.mp, Finset.mem_Iio, Subtype.property
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
n : ι
rw : gramSchmidt 𝕜 f n = f n - ∑ x ∈ (Iio n).attach, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f (↑x : ι)) : (a : E) → E) (f n)
rw₁ : gramSchmidt 𝕜 f n = f n - ∑ x : ↥(Iio n), (starProjection (𝕜 ∙ gramSchmidt 𝕜 f (↑x : ι)) : (a : E) → E) (f n)
rw₂ rw₃ :
  f n - ∑ i : ↥(Iio n), (starProjection (𝕜 ∙ gramSchmidt 𝕜 f (↑i : ι)) : (a : E) → E) (f n) =
    f n - ∑ x : ↥(Iio n), (starProjection (𝕜 ∙ gramSchmidt 𝕜 f (↑x : ι)) : (a : E) → E) (f n)
⊢ gramSchmidt 𝕜 f n = f n - ∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f n)

Tactic:
rw [← sum_attach, attach_eq_univ, gramSchmidt]

Premises used: Finset.attach_eq_univ, Finset.sum_attach, InnerProductSpace.gramSchmidt
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
n : ι
rw :
  f n =
    f n - ∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f n) +
      ∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f n)
rw₁ rw₂ : f n = f n
⊢ f n = gramSchmidt 𝕜 f n + ∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f n)

Tactic:
rw [gramSchmidt_def, sub_add_cancel]

Premises used: InnerProductSpace.gramSchmidt_def, sub_add_cancel
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
n : ι
⊢ f n =
    gramSchmidt 𝕜 f n +
      ∑ i ∈ Iio n,
        (⟪gramSchmidt 𝕜 f i, f n⟫_𝕜 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖gramSchmidt 𝕜 f i‖ : 𝕜) 2) • gramSchmidt 𝕜 f i

Tactic:
simp only [← map_pow, ← starProjection_singleton, ← gramSchmidt_def' 𝕜 f n]

Premises used: Submodule.starProjection_singleton, map_pow, InnerProductSpace.gramSchmidt_def'
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrder ι
inst_5 : OrderBot ι
inst_6 : WellFoundedLT ι
f : ι → E
rw : f ⊥ - ∑ i ∈ Iio ⊥, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
rw₁ : f ⊥ - ∑ i ∈ Ico ⊥ ⊥, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
rw₂ : f ⊥ - ∑ i ∈ ∅, (starProjection (𝕜 ∙ gramSchmidt 𝕜 f i) : (a : E) → E) (f ⊥) = f ⊥
rw₃ : f ⊥ - 0 = f ⊥
rw₄ rw₅ : f ⊥ = f ⊥
⊢ gramSchmidt 𝕜 f ⊥ = f ⊥

Tactic:
rw [gramSchmidt_def, Iio_eq_Ico, Finset.Ico_self, Finset.sum_empty, sub_zero]

Premises used: Finset.Ico_self, InnerProductSpace.gramSchmidt_def, Finset.Iio_eq_Ico, sub_zero, Finset.sum_empty
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
n : ι
rw : HSub.hSub (α := E) (0 n) (∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 0 i) : (a : E) → E) (0 n)) = 0
⊢ Eq.{u_2 + 1} (α := E) (gramSchmidt 𝕜 0 n) 0

Tactic:
rw [gramSchmidt_def]

Premises used: InnerProductSpace.gramSchmidt_def
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
n : ι
⊢ HSub.hSub (α := E) (0 n) (∑ i ∈ Iio n, (starProjection (𝕜 ∙ gramSchmidt 𝕜 0 i) : (a : E) → E) (0 n)) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
inl : ∀ (ha : a < b), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
inr : ∀ (hb : b < a), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0

Tactic:
rcases h₀.lt_or_gt with ha | hb

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
ha : a < b
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0

Tactic:
this _ _ ha
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
ha : a < b
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0

Tactic:
exact this _ _ ha
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
hb : b < a
inr : ⟪gramSchmidt 𝕜 f b, gramSchmidt 𝕜 f a⟫_𝕜 = 0
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0

Tactic:
rw [inner_eq_zero_symm]

Premises used: inner_eq_zero_symm
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
hb : b < a
⊢ ⟪gramSchmidt 𝕜 f b, gramSchmidt 𝕜 f a⟫_𝕜 = 0

Tactic:
this _ _ hb
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
a b : ι
h₀ : a ≠ b
this : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
hb : b < a
⊢ ⟪gramSchmidt 𝕜 f b, gramSchmidt 𝕜 f a⟫_𝕜 = 0

Tactic:
exact this _ _ hb
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
a b : ι
h₀ : a ≠ b
suffices : ∀ (a b : ι), a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0

Tactic:
suffices ∀ a b : ι, a < b → ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫ = 0 by
    rcases h₀.lt_or_gt with ha | hb
    · exact this _ _ ha
    · rw [inner_eq_zero_symm]
      exact this _ _ hb
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
a b : ι
h₀ : a < b
revert : ∀ (a : ι) (h₀ : a < b), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0

Tactic:
revert a
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
b : ι
apply :
  ∀ (x : ι),
    (∀ y < x, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0) →
      ∀ (a : ι) (h₀ : a < x), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f x⟫_𝕜 = 0
⊢ ∀ (a : ι) (h₀ : a < b), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0

Tactic:
apply wellFounded_lt.induction b

Premises used: WellFounded.induction, wellFounded_lt
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
simp :
  ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ∑ x ∈ Iio b,
        ⟪gramSchmidt 𝕜 f x, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f x‖ 2) : 𝕜) *
          ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f x⟫_𝕜 =
    0
⊢ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0

Tactic:
simp only [gramSchmidt_def 𝕜 f b, inner_sub_right, inner_sum,
    starProjection_singleton, inner_smul_right]

Premises used: inner_sum, Submodule.starProjection_singleton, InnerProductSpace.gramSchmidt_def, inner_smul_right, inner_sub_right
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
rw :
  ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f a‖ 2) : 𝕜) *
        ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0
rw₁ :
  ∀ b_2 ∈ Iio b,
    b_2 ≠ a →
      ⟪gramSchmidt 𝕜 f b_2, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f b_2‖ 2) : 𝕜) *
          ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b_2⟫_𝕜 =
        0
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ∑ x ∈ Iio b,
        ⟪gramSchmidt 𝕜 f x, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f x‖ 2) : 𝕜) *
          ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f x⟫_𝕜 =
    0

Tactic:
rw [Finset.sum_eq_single_of_mem a (Finset.mem_Iio.mpr h₀)]

Premises used: Iff.mpr, Finset.sum_eq_single_of_mem, Finset.mem_Iio
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
pos :
  ∀ (h : gramSchmidt 𝕜 f a = 0),
    ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
        ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f a‖ 2) : 𝕜) *
          ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
      0
neg :
  ∀ (h : ¬gramSchmidt 𝕜 f a = 0),
    ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
        ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f a‖ 2) : 𝕜) *
          ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
      0
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f a‖ 2) : 𝕜) *
        ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0

Tactic:
by_cases h : gramSchmidt 𝕜 f a = 0

Premises used: InnerProductSpace.gramSchmidt
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
h : gramSchmidt 𝕜 f a = 0
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f a‖ 2) : 𝕜) *
        ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0

Tactic:
simp only [h, inner_zero_left, zero_div, zero_mul, sub_zero]

Premises used: sub_zero, MulZeroClass.zero_mul, zero_div, inner_zero_left
-- Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : LocallyFiniteOrderBot ι
inst_5 : WellFoundedLT ι
f : ι → E
b_1 b : ι
ih : ∀ y < b, ∀ (a : ι) (h₀ : a < y), ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0
a : ι
h₀ : a < b
h : ¬gramSchmidt 𝕜 f a = 0
neg : ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 ≠ 0
⊢ ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 -
      ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / (↑(HPow.hPow (β := ℕ) ‖gramSchmidt 𝕜 f a‖ 2) : 𝕜) *
        ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 =
    0

Tactic:
rw [RCLike.ofReal_pow, ← inner_self_eq_norm_sq_to_K, div_mul_cancel₀, sub_self]

Premises used: div_mul_cancel₀, sub_self, inner_self_eq_norm_sq_to_K, RCLike.ofReal_pow