awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this_1 :
  Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidt 𝕜 (⇑b : (a : ι) → E) '' Set.Iio j))
    (gramSchmidt 𝕜 (⇑b : (a : ι) → E) i)
this_2 :
  Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 ((⇑b : (a : ι) → E) '' Set.Iio j)) (gramSchmidt 𝕜 (⇑b : (a : ι) → E) i)
this :
  (↑(Finsupp.support.{u_3, u_1} (M := 𝕜) ((b.repr : (a : E) → ι →₀ 𝕜) (gramSchmidt 𝕜 (⇑b : (a : ι) → E) i))) : Set ι) ⊆
    Set.Iio j
⊢ Eq.{u_1 + 1} (α := 𝕜) (((b.repr : (a : E) → ι →₀ 𝕜) (gramSchmidt 𝕜 (⇑b : (a : ι) → E) i) : (a : ι) → 𝕜) j : 𝕜) (0 : 𝕜)

Tactic:
(Finsupp.mem_supported' _ _).1 ((Finsupp.mem_supported 𝕜 _).2 this) j Set.self_notMem_Iio

Premises used: Iff.mpr, Set.self_notMem_Iio, Finsupp.mem_supported, Iff.mp, Finsupp.mem_supported'
-- 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 ι
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this_1 :
  Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidt 𝕜 (⇑b : (a : ι) → E) '' Set.Iio j))
    (gramSchmidt 𝕜 (⇑b : (a : ι) → E) i)
this_2 :
  Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 ((⇑b : (a : ι) → E) '' Set.Iio j)) (gramSchmidt 𝕜 (⇑b : (a : ι) → E) i)
this :
  (↑(Finsupp.support.{u_3, u_1} (M := 𝕜) ((b.repr : (a : E) → ι →₀ 𝕜) (gramSchmidt 𝕜 (⇑b : (a : ι) → E) i))) : Set ι) ⊆
    Set.Iio j
⊢ Eq.{u_1 + 1} (α := 𝕜) (((b.repr : (a : E) → ι →₀ 𝕜) (gramSchmidt 𝕜 (⇑b : (a : ι) → E) i) : (a : ι) → 𝕜) j : 𝕜) (0 : 𝕜)

Tactic:
exact (Finsupp.mem_supported' _ _).1 ((Finsupp.mem_supported 𝕜 _).2 this) j Set.self_notMem_Iio

Premises used: Iff.mpr, Set.self_notMem_Iio, Finsupp.mem_supported, Iff.mp, Finsupp.mem_supported'
-- 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
h₀ : LinearIndependent 𝕜 f
⊢ LinearIndependent 𝕜 (gramSchmidt 𝕜 f)

Tactic:
linearIndependent_of_ne_zero_of_inner_eq_zero (fun _ => gramSchmidt_ne_zero _ h₀) fun _ _ =>
    gramSchmidt_orthogonal 𝕜 f

Premises used: InnerProductSpace.gramSchmidt_orthogonal, linearIndependent_of_ne_zero_of_inner_eq_zero, InnerProductSpace.gramSchmidt_ne_zero
-- 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 ι
b : Basis ι 𝕜 E
⊢ Eq (α := (a : ι) → E) (⇑(gramSchmidtBasis b) : (a : ι) → E) (gramSchmidt 𝕜 (⇑b : (a : ι) → E))

Tactic:
Basis.coe_mk _ _

Premises used: Module.Basis.coe_mk
-- 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 : ι
h₀ : LinearIndependent (ι := { x : ι // x ∈ Set.Iic n }) 𝕜 (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ Set.Iic n))
⊢ ‖gramSchmidtNormed 𝕜 f n‖ = 1

Tactic:
simp only [gramSchmidt_ne_zero_coe n h₀, gramSchmidtNormed, norm_smul_inv_norm, Ne,
    not_false_iff]

Premises used: norm_smul_inv_norm, Ne, InnerProductSpace.gramSchmidtNormed, InnerProductSpace.gramSchmidt_ne_zero_coe, not_false_iff
-- 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 : ι
h₀ : LinearIndependent 𝕜 f
⊢ ‖gramSchmidtNormed 𝕜 f n‖ = 1

Tactic:
gramSchmidtNormed_unit_length_coe _ (LinearIndependent.comp h₀ _ Subtype.coe_injective)

Premises used: InnerProductSpace.gramSchmidtNormed_unit_length_coe, Subtype.coe_injective, LinearIndependent.comp
-- 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 : ι
hn : gramSchmidtNormed 𝕜 f n ≠ 0
rw :
  ∀ (hn : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖gramSchmidt 𝕜 f n‖ : 𝕜)⁻¹ (gramSchmidt 𝕜 f n) ≠ 0),
    ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖gramSchmidt 𝕜 f n‖ : 𝕜)⁻¹ (gramSchmidt 𝕜 f n)‖ = 1
⊢ ‖gramSchmidtNormed 𝕜 f n‖ = 1

Tactic:
rw [gramSchmidtNormed] at *

Premises used: InnerProductSpace.gramSchmidtNormed
-- 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 : ι
hn : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖gramSchmidt 𝕜 f n‖ : 𝕜)⁻¹ (gramSchmidt 𝕜 f n) ≠ 0
rw : gramSchmidt 𝕜 f n ≠ 0
⊢ ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖gramSchmidt 𝕜 f n‖ : 𝕜)⁻¹ (gramSchmidt 𝕜 f n)‖ = 1

Tactic:
rw [norm_smul_inv_norm]

Premises used: norm_smul_inv_norm
-- 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 : ι
hn : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖gramSchmidt 𝕜 f n‖ : 𝕜)⁻¹ (gramSchmidt 𝕜 f n) ≠ 0
⊢ gramSchmidt 𝕜 f n ≠ 0

Tactic:
simpa using hn
-- 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
h₀ : LinearIndependent 𝕜 f
left : ∀ (i : ι), ‖gramSchmidtNormed 𝕜 f i‖ = 1
right : Pairwise fun (i j : ι) ↦ ⟪gramSchmidtNormed 𝕜 f i, gramSchmidtNormed 𝕜 f j⟫_𝕜 = 0
⊢ (∀ (i : ι), ‖gramSchmidtNormed 𝕜 f i‖ = 1) ∧
    Pairwise fun (i j : ι) ↦ ⟪gramSchmidtNormed 𝕜 f i, gramSchmidtNormed 𝕜 f j⟫_𝕜 = 0

Tactic:
constructor
-- 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
h₀ : LinearIndependent 𝕜 f
⊢ ∀ (i : ι), ‖gramSchmidtNormed 𝕜 f i‖ = 1

Tactic:
simp only [gramSchmidtNormed_unit_length, h₀, imp_true_iff]

Premises used: imp_true_iff, InnerProductSpace.gramSchmidtNormed_unit_length
-- 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
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
right : gramSchmidt 𝕜 f j = 0 ∨ gramSchmidt 𝕜 f i = 0 ∨ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0
⊢ ⟪gramSchmidtNormed 𝕜 f i, gramSchmidtNormed 𝕜 f j⟫_𝕜 = 0

Tactic:
simp only [gramSchmidtNormed, inner_smul_left, inner_smul_right, RCLike.conj_inv,
      RCLike.conj_ofReal, mul_eq_zero, inv_eq_zero, RCLike.ofReal_eq_zero, norm_eq_zero]

Premises used: norm_eq_zero, inv_eq_zero, RCLike.conj_ofReal, mul_eq_zero, InnerProductSpace.gramSchmidtNormed, RCLike.ofReal_eq_zero, inner_smul_right, RCLike.conj_inv, inner_smul_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
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
right : gramSchmidt 𝕜 f i = 0 ∨ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0
⊢ gramSchmidt 𝕜 f j = 0 ∨ gramSchmidt 𝕜 f i = 0 ∨ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0

Tactic:
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
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
right : ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0
⊢ gramSchmidt 𝕜 f i = 0 ∨ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0

Tactic:
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
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
right : ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0
⊢ gramSchmidt 𝕜 f j = 0 ∨ gramSchmidt 𝕜 f i = 0 ∨ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0

Tactic:
repeat' 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
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0

Tactic:
gramSchmidt_orthogonal 𝕜 f hij

Premises used: InnerProductSpace.gramSchmidt_orthogonal
-- 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
h₀ : LinearIndependent 𝕜 f
i j : ι
hij : i ≠ j
⊢ ⟪gramSchmidt 𝕜 f i, gramSchmidt 𝕜 f j⟫_𝕜 = 0

Tactic:
exact gramSchmidt_orthogonal 𝕜 f hij

Premises used: InnerProductSpace.gramSchmidt_orthogonal
-- 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
⊢ Orthonormal.{u_1, u_2, u_3} 𝕜 (E := E) fun (i : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)) ↦
    gramSchmidtNormed 𝕜 f (↑i : ι)

Tactic:
⟨fun i => gramSchmidtNormed_unit_length' i.prop, ?_⟩

Premises used: Orthonormal, InnerProductSpace.gramSchmidtNormed_unit_length', Subtype.prop, And.intro
-- 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
refine :
  Pairwise fun (i j : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)) ↦
    inner.{u_1, u_2} 𝕜 (E := E)
        ((fun (i : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)) ↦ gramSchmidtNormed 𝕜 f (↑i : ι)) i)
        ((fun (i : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)) ↦ gramSchmidtNormed 𝕜 f (↑i : ι)) j) =
      0
⊢ Orthonormal.{u_1, u_2, u_3} 𝕜 (E := E) fun (i : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)) ↦
    gramSchmidtNormed 𝕜 f (↑i : ι)

Tactic:
refine ⟨fun i => gramSchmidtNormed_unit_length' i.prop, ?_⟩
-- 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
i j : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)
hij : ¬i = j
⊢ ¬(↑i : ι) = (↑j : ι)

Tactic:
rw [Subtype.ext_iff] at hij

Premises used: Subtype.ext_iff
-- 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
i j : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)
hij : ¬(↑i : ι) = (↑j : ι)
⊢ inner.{u_1, u_2} 𝕜 (E := E)
      ((fun (i : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)) ↦ gramSchmidtNormed 𝕜 f (↑i : ι)) i)
      ((fun (i : (↑{i : ι | gramSchmidtNormed 𝕜 f i ≠ 0} : Type u_3)) ↦ gramSchmidtNormed 𝕜 f (↑i : ι)) j) =
    0

Tactic:
simp [gramSchmidtNormed, inner_smul_left, inner_smul_right, gramSchmidt_orthogonal 𝕜 f hij]

Premises used: InnerProductSpace.gramSchmidt_orthogonal, InnerProductSpace.gramSchmidtNormed, inner_smul_right, inner_smul_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
s : Set ι
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 (gramSchmidtNormed 𝕜 f '' s)) (span 𝕜 (gramSchmidt 𝕜 f '' s))

Tactic:
span_eq_span
    (Set.image_subset_iff.2 fun i hi => smul_mem _ _ <| subset_span <| mem_image_of_mem _ hi)
    (Set.image_subset_iff.2 fun i hi =>
      span_mono (image_mono <| singleton_subset_set_iff.2 hi) ?_)

Premises used: Iff.mpr, Norm.norm, Finset.singleton_subset_set_iff, Set.image_mono, RCLike.ofReal, InnerProductSpace.gramSchmidt, Inv.inv, Set.mem_image_of_mem, Submodule.span_mono, Submodule.span, Set.image, Set.image_subset_iff, Submodule.subset_span, Submodule.span_eq_span, Submodule.smul_mem
-- 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
s : Set ι
refine :
  ∀ (i : ι) (hi : i ∈ s),
    Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidtNormed 𝕜 f '' (↑{i} : Set ι))) (gramSchmidt 𝕜 f i)
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 (gramSchmidtNormed 𝕜 f '' s)) (span 𝕜 (gramSchmidt 𝕜 f '' s))

Tactic:
refine span_eq_span
    (Set.image_subset_iff.2 fun i hi => smul_mem _ _ <| subset_span <| mem_image_of_mem _ hi)
    (Set.image_subset_iff.2 fun i hi =>
      span_mono (image_mono <| singleton_subset_set_iff.2 hi) ?_)

Premises used: Iff.mpr, Finset.singleton_subset_set_iff, Set.image_mono, Set.mem_image_of_mem, Submodule.span_mono, Submodule.span, Set.image, Set.image_subset_iff, Submodule.subset_span, Submodule.span_eq_span, Submodule.smul_mem
-- 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
s : Set ι
i : ι
hi : i ∈ s
simp : Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ gramSchmidtNormed 𝕜 f i) (gramSchmidt 𝕜 f i)
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidtNormed 𝕜 f '' (↑{i} : Set ι))) (gramSchmidt 𝕜 f i)

Tactic:
simp only [coe_singleton, Set.image_singleton]

Premises used: Finset.coe_singleton, Set.image_singleton
-- 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
s : Set ι
i : ι
hi : i ∈ s
pos :
  ∀ (h : gramSchmidt 𝕜 f i = 0), Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ gramSchmidtNormed 𝕜 f i) (gramSchmidt 𝕜 f i)
neg :
  ∀ (h : ¬gramSchmidt 𝕜 f i = 0), Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ gramSchmidtNormed 𝕜 f i) (gramSchmidt 𝕜 f i)
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ gramSchmidtNormed 𝕜 f i) (gramSchmidt 𝕜 f i)

Tactic:
by_cases h : gramSchmidt 𝕜 f i = 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
s : Set ι
i : ι
hi : i ∈ s
h : gramSchmidt 𝕜 f i = 0
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ gramSchmidtNormed 𝕜 f i) (gramSchmidt 𝕜 f i)

Tactic:
simp [h]
-- 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
s : Set ι
i : ι
hi : i ∈ s
h : ¬gramSchmidt 𝕜 f i = 0
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ gramSchmidtNormed 𝕜 f i) (gramSchmidt 𝕜 f i)

Tactic:
mem_span_singleton.2 ⟨‖gramSchmidt 𝕜 f i‖, smul_inv_smul₀ ?_ _⟩

Premises used: Iff.mpr, Norm.norm, smul_inv_smul₀, Submodule.mem_span_singleton, RCLike.ofReal, InnerProductSpace.gramSchmidt, Exists.intro
-- 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
s : Set ι
i : ι
hi : i ∈ s
h : ¬gramSchmidt 𝕜 f i = 0
neg : Ne.{u_1 + 1} (α := 𝕜) (↑‖gramSchmidt 𝕜 f i‖ : 𝕜) 0
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ gramSchmidtNormed 𝕜 f i) (gramSchmidt 𝕜 f i)

Tactic:
refine mem_span_singleton.2 ⟨‖gramSchmidt 𝕜 f i‖, smul_inv_smul₀ ?_ _⟩

Premises used: Iff.mpr, Norm.norm, smul_inv_smul₀, Submodule.mem_span_singleton, InnerProductSpace.gramSchmidt, Exists.intro
-- 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
s : Set ι
i : ι
hi : i ∈ s
h : ¬gramSchmidt 𝕜 f i = 0
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑‖gramSchmidt 𝕜 f i‖ : 𝕜) 0

Tactic:
mod_cast norm_ne_zero_iff.2 h

Premises used: Iff.mpr, Norm.norm, Real, congrArg, cast, algebraMap.coe_inj._simp_1, Ne, RCLike.ofReal, InnerProductSpace.gramSchmidt, norm_ne_zero_iff, Nat.cast_zero, algebraMap.coe_zero, Eq.symm, Eq, Not, Eq.trans
-- 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
s : Set ι
i : ι
hi : i ∈ s
h : ¬gramSchmidt 𝕜 f i = 0
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑‖gramSchmidt 𝕜 f i‖ : 𝕜) 0

Tactic:
exact mod_cast norm_ne_zero_iff.2 h

Premises used: Iff.mpr, norm_ne_zero_iff
-- 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
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 (Set.range (gramSchmidtNormed 𝕜 f))) (span 𝕜 (Set.range (gramSchmidt 𝕜 f)))

Tactic:
simpa only [image_univ.symm] using span_gramSchmidtNormed f univ

Premises used: InnerProductSpace.span_gramSchmidtNormed, Set.image_univ, Set.univ, Eq.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
h₀ : LinearIndependent 𝕜 f
unfold :
  LinearIndependent.{u_3, u_1, u_2} 𝕜 (M := E) fun (n : ι) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖gramSchmidt 𝕜 f n‖ : 𝕜)⁻¹ (gramSchmidt 𝕜 f n)
⊢ LinearIndependent 𝕜 (gramSchmidtNormed 𝕜 f)

Tactic:
unfold gramSchmidtNormed

Premises used: InnerProductSpace.gramSchmidtNormed
-- 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
h₀ : LinearIndependent 𝕜 f
i : ι
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑‖gramSchmidt 𝕜 f i‖ : 𝕜)⁻¹ 0

Tactic:
simp [gramSchmidt_ne_zero i h₀]

Premises used: InnerProductSpace.gramSchmidt_ne_zero
-- 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
h₀ : LinearIndependent 𝕜 f
⊢ ∀ (i : ι), IsUnit.{u_1} (M := 𝕜) (↑‖gramSchmidt 𝕜 f i‖ : 𝕜)⁻¹

Tactic:
have (i : ι) : IsUnit (‖gramSchmidt 𝕜 f i‖⁻¹ : 𝕜) :=
    isUnit_iff_ne_zero.mpr (by simp [gramSchmidt_ne_zero i h₀])
-- 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
h₀ : LinearIndependent 𝕜 f
this : ∀ (i : ι), IsUnit.{u_1} (M := 𝕜) (↑‖gramSchmidt 𝕜 f i‖ : 𝕜)⁻¹
w : ι → 𝕜ˣ := fun (i : ι) ↦ ⋯.unit
⊢ LinearIndependent.{u_3, u_1, u_2} 𝕜 (M := E) fun (n : ι) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖gramSchmidt 𝕜 f n‖ : 𝕜)⁻¹ (gramSchmidt 𝕜 f n)

Tactic:
apply (gramSchmidt_linearIndependent h₀).units_smul (w := fun i ↦ (this i).unit)

Premises used: LinearIndependent.units_smul, IsUnit.unit, InnerProductSpace.gramSchmidt_linearIndependent
-- 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 ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i ≠ 0
⊢ (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i = gramSchmidtNormed 𝕜 f i

Tactic:
((gramSchmidtNormed_orthonormal' f).exists_orthonormalBasis_extension_of_card_eq
    (v := gramSchmidtNormed 𝕜 f) h).choose_spec i hi

Premises used: Orthonormal.exists_orthonormalBasis_extension_of_card_eq, Exists.choose_spec, InnerProductSpace.gramSchmidtNormed_orthonormal'
-- 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 ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
hf : Pairwise fun (i j : ι) ↦ ⟪f i, f j⟫_𝕜 = 0
i : ι
hi : f i ≠ 0
rw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖gramSchmidt 𝕜 f i‖ : 𝕜)⁻¹ (gramSchmidt 𝕜 f i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)
rw₁ rw₂ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i) = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)
⊢ gramSchmidtNormed 𝕜 f i = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)

Tactic:
rw [gramSchmidtNormed, gramSchmidt_of_orthogonal 𝕜 hf]

Premises used: InnerProductSpace.gramSchmidt_of_orthogonal, InnerProductSpace.gramSchmidtNormed
-- 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 ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
hf : Pairwise fun (i j : ι) ↦ ⟪f i, f j⟫_𝕜 = 0
i : ι
hi : f i ≠ 0
⊢ gramSchmidtNormed 𝕜 f i = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)

Tactic:
have H : gramSchmidtNormed 𝕜 f i = (‖f i‖⁻¹ : 𝕜) • f i := by
    rw [gramSchmidtNormed, gramSchmidt_of_orthogonal 𝕜 hf]