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 ι
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
H : gramSchmidtNormed 𝕜 f i = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)
rw : gramSchmidtNormed 𝕜 f i ≠ 0
⊢ (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)

Tactic:
rw [gramSchmidtOrthonormalBasis_apply h, H]

Premises used: InnerProductSpace.gramSchmidtOrthonormalBasis_apply
-- 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
H : gramSchmidtNormed 𝕜 f i = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖f i‖ : 𝕜)⁻¹ (f i)
⊢ gramSchmidtNormed 𝕜 f i ≠ 0

Tactic:
simpa [H] using hi
-- 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
j : ι
rw :
  Membership.mem (γ := Submodule 𝕜 E)
    (span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E)))ᗮ (f j)
⊢ ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) i, f j⟫_𝕜 = 0

Tactic:
rw [← mem_orthogonal_singleton_iff_inner_right]

Premises used: Submodule.mem_orthogonal_singleton_iff_inner_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 ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
this :
  span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂
    span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E))
a : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j)) (f j)
⊢ Membership.mem (γ := Submodule 𝕜 E)
    (span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E)))ᗮ (f j)

Tactic:
apply this
-- 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
j : ι
this :
  span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂
    span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E))
a : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)) (f j)
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j)) (f j)

Tactic:
rw [span_gramSchmidtNormed]

Premises used: InnerProductSpace.span_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
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
this :
  span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂
    span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E))
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)) (f j)

Tactic:
mem_span_gramSchmidt 𝕜 f le_rfl

Premises used: le_rfl, InnerProductSpace.mem_span_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 ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
this :
  span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂
    span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E))
⊢ Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)) (f j)

Tactic:
exact mem_span_gramSchmidt 𝕜 f le_rfl

Premises used: le_rfl, InnerProductSpace.mem_span_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 ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j : ι
suffices :
  span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂
    span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E))
⊢ Membership.mem (γ := Submodule 𝕜 E)
    (span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E)))ᗮ (f j)

Tactic:
suffices span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂ 𝕜 ∙ gramSchmidtOrthonormalBasis h f i by
    apply this
    rw [span_gramSchmidtNormed]
    exact mem_span_gramSchmidt 𝕜 f le_rfl
-- 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
j : ι
rw :
  ∀ ⦃u : E⦄,
    u ∈ gramSchmidtNormed 𝕜 f '' Set.Iic j →
      ∀ ⦃v : E⦄,
        Membership.mem (γ := Set E) (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E)) v →
          ⟪u, v⟫_𝕜 = 0
⊢ span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂
    span 𝕜 (singleton (α := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E))

Tactic:
rw [isOrtho_span]

Premises used: Submodule.isOrtho_span
-- 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
j k : ι
left : k ∈ Set.Iic j
pos :
  ∀ (hk : gramSchmidtNormed 𝕜 f k = 0),
    ⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i⟫_𝕜 = 0
neg :
  ∀ (hk : ¬gramSchmidtNormed 𝕜 f k = 0),
    ⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i⟫_𝕜 = 0
⊢ ⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i⟫_𝕜 = 0

Tactic:
by_cases hk : gramSchmidtNormed 𝕜 f k = 0

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 ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left : k ∈ Set.Iic j
hk : gramSchmidtNormed 𝕜 f k = 0
pos : inner.{u_1, u_2} 𝕜 (E := E) (0 : E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E) = 0
pos₁ pos₂ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i⟫_𝕜 = 0

Tactic:
rw [hk, inner_zero_left]

Premises used: 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 ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
neg :
  inner.{u_1, u_2} 𝕜 (E := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) k : E)
      ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E) =
    0
⊢ ⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f : (a : ι) → E) i⟫_𝕜 = 0

Tactic:
rw [← gramSchmidtOrthonormalBasis_apply h hk]

Premises used: InnerProductSpace.gramSchmidtOrthonormalBasis_apply
-- 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
j k : ι
left : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
hi : gramSchmidtNormed 𝕜 f k = 0
⊢ False

Tactic:
hk hi
-- 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
j k : ι
left : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
hi : gramSchmidtNormed 𝕜 f k = 0
⊢ False

Tactic:
exact hk hi
-- 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
j k : ι
left : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
⊢ k ≠ i

Tactic:
have : k ≠ i := by
    rintro rfl
    exact hk hi
-- 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
j k : ι
left : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
this : k ≠ i
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) k : E)
      ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E) =
    0

Tactic:
(gramSchmidtOrthonormalBasis h f).orthonormal.2 this

Premises used: InnerProductSpace.gramSchmidtOrthonormalBasis, And.right, OrthonormalBasis.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
i : ι
hi : gramSchmidtNormed 𝕜 f i = 0
j k : ι
left : k ∈ Set.Iic j
hk : ¬gramSchmidtNormed 𝕜 f k = 0
this : k ≠ i
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) k : E)
      ((gramSchmidtOrthonormalBasis h f : (a : ι) → E) i : E) =
    0

Tactic:
exact (gramSchmidtOrthonormalBasis h f).orthonormal.2 this

Premises used: InnerProductSpace.gramSchmidtOrthonormalBasis, And.right, OrthonormalBasis.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
i j : ι
hij : i < j
pos : ∀ (hi : gramSchmidtNormed 𝕜 f j = 0), ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) j, f i⟫_𝕜 = 0
neg : ∀ (hi : ¬gramSchmidtNormed 𝕜 f j = 0), ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) j, f i⟫_𝕜 = 0
⊢ ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) j, f i⟫_𝕜 = 0

Tactic:
by_cases hi : gramSchmidtNormed 𝕜 f j = 0

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 ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
hi : gramSchmidtNormed 𝕜 f j = 0
pos pos₁ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) j, f i⟫_𝕜 = 0

Tactic:
rw [inner_gramSchmidtOrthonormalBasis_eq_zero h hi]

Premises used: InnerProductSpace.inner_gramSchmidtOrthonormalBasis_eq_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 ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
hi : ¬gramSchmidtNormed 𝕜 f j = 0
⊢ ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) j, f i⟫_𝕜 = 0

Tactic:
simp [gramSchmidtOrthonormalBasis_apply h hi, gramSchmidtNormed, inner_smul_left,
      gramSchmidt_inv_triangular 𝕜 f hij]

Premises used: InnerProductSpace.gramSchmidtOrthonormalBasis_apply, InnerProductSpace.gramSchmidtNormed, inner_smul_left, InnerProductSpace.gramSchmidt_inv_triangular
-- 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 j : ι
hij : i < j
⊢ Eq.{u_1 + 1} (α := (fun (x : ι) ↦ 𝕜) j)
    (WithLp.ofLp (p := 2) (((gramSchmidtOrthonormalBasis h f).repr : (a : E) → EuclideanSpace 𝕜 ι) (f i)) j) 0

Tactic:
simpa [OrthonormalBasis.repr_apply_apply] using gramSchmidtOrthonormalBasis_inv_triangular h f hij

Premises used: OrthonormalBasis.repr_apply_apply, InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular
-- 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
⊢ ((gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f).BlockTriangular id

Tactic:
fun _ _ =>
  gramSchmidtOrthonormalBasis_inv_triangular' h f

Premises used: Module.Basis.toMatrix, Matrix.BlockTriangular, InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular'
-- 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
inst_8 : DecidableEq ι
⊢ ((gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f).det =
    ∏ i : ι, (gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f i i

Tactic:
Matrix.det_of_upperTriangular (gramSchmidtOrthonormalBasis_inv_blockTriangular h f)

Premises used: InnerProductSpace.gramSchmidtOrthonormalBasis_inv_blockTriangular, Matrix.det_of_upperTriangular
-- 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
inst_8 : DecidableEq ι
h₁ :
  ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x →
      ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) x, f x⟫_𝕜 =
        (gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f x x
⊢ Eq.{u_1 + 1} (α := 𝕜) (((gramSchmidtOrthonormalBasis h f).toBasis.det : (a : ι → E) → 𝕜) f : 𝕜)
    (∏ i : ι, ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) i, f i⟫_𝕜 : 𝕜)

Tactic:
convert! Matrix.det_of_upperTriangular (gramSchmidtOrthonormalBasis_inv_blockTriangular h f)

Premises used: InnerProductSpace.gramSchmidtOrthonormalBasis_inv_blockTriangular, Matrix.det_of_upperTriangular
-- 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
inst_8 : DecidableEq ι
x : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ x
⊢ ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) x, f x⟫_𝕜 = (gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f x x

Tactic:
((gramSchmidtOrthonormalBasis h f).repr_apply_apply (f _) _).symm

Premises used: OrthonormalBasis.repr_apply_apply, Module.Basis.toMatrix, InnerProductSpace.gramSchmidtOrthonormalBasis, 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 ι
inst_6 : Fintype ι
inst_7 : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
inst_8 : DecidableEq ι
x : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ x
⊢ ⟪(gramSchmidtOrthonormalBasis h f : (a : ι) → E) x, f x⟫_𝕜 = (gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f x x

Tactic:
exact ((gramSchmidtOrthonormalBasis h f).repr_apply_apply (f _) _).symm

Premises used: OrthonormalBasis.repr_apply_apply, InnerProductSpace.gramSchmidtOrthonormalBasis, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s : Set E
hf : HarmonicOnNhd f s
⊢ ContDiffOn ℝ 2 f s

Tactic:
fun x hx ↦ (hf x hx).1.contDiffWithinAt

Premises used: ContDiffOn, And.left, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
mp : HarmonicAt f₁ x → HarmonicAt f₂ x
mpr : HarmonicAt f₂ x → HarmonicAt f₁ x
⊢ HarmonicAt f₁ x ↔ HarmonicAt f₂ x

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
hf : HarmonicAt f₁ x
⊢ HarmonicAt f₂ x

Tactic:
⟨hf.1.congr_of_eventuallyEq h.symm, (laplacian_congr_nhds h.symm).trans hf.2⟩

Premises used: Filter.EventuallyEq.trans, InnerProductSpace.HarmonicAt, InnerProductSpace.laplacian_congr_nhds, And.right, And.left, And.intro, ContDiffAt.congr_of_eventuallyEq, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
hf : HarmonicAt f₁ x
⊢ HarmonicAt f₂ x

Tactic:
exact ⟨hf.1.congr_of_eventuallyEq h.symm, (laplacian_congr_nhds h.symm).trans hf.2⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
hf : HarmonicAt f₂ x
⊢ HarmonicAt f₁ x

Tactic:
⟨hf.1.congr_of_eventuallyEq h, (laplacian_congr_nhds h).trans hf.2⟩

Premises used: Filter.EventuallyEq.trans, InnerProductSpace.HarmonicAt, InnerProductSpace.laplacian_congr_nhds, And.right, And.left, And.intro, ContDiffAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
hf : HarmonicAt f₂ x
⊢ HarmonicAt f₁ x

Tactic:
exact ⟨hf.1.congr_of_eventuallyEq h, (laplacian_congr_nhds h).trans hf.2⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicAt f x
⊢ Ne (α := WithTop ℕ∞) 2 (↑⊤ : WithTop ℕ∞)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicAt f x
h₁ : ∀ (a : E) (h₁a : ContDiffAt ℝ 2 f a) (h₂a : ∀ᶠ (x : E) in 𝓝 a, Δ f x = 0 x), HarmonicAt f a
⊢ ∀ᶠ (y : E) in 𝓝 x, HarmonicAt f y

Tactic:
filter_upwards [h.1.eventually (by simp), h.2.eventually_nhds] with a h₁a h₂a

Premises used: Filter.Eventually.eventually_nhds, And.right, And.left, ContDiffAt.eventually
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicAt f x
a : E
h₁a : ContDiffAt ℝ 2 f a
h₂a : ∀ᶠ (x : E) in 𝓝 a, Δ f x = 0 x
⊢ HarmonicAt f a

Tactic:
⟨h₁a, h₂a⟩

Premises used: InnerProductSpace.HarmonicAt, And.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicAt f x
a : E
h₁a : ContDiffAt ℝ 2 f a
h₂a : ∀ᶠ (x : E) in 𝓝 a, Δ f x = 0 x
⊢ HarmonicAt f a

Tactic:
exact ⟨h₁a, h₂a⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
x : E
c : F
⊢ ContDiffAt.{0, u_1, u_2} ℝ (F := F) 2 (fun (x : E) ↦ c) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
x : E
c : F
⊢ (Δ (E := E → F) fun (x : E) ↦ c) =ᶠ[𝓝 x] 0

Tactic:
simp