awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i j : ι
hij : i ≠ j
⊢ ⟪v i, v j⟫ = 0

Tactic:
simpa [hij] using h i j
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Subsingleton ι
v : ι → E
⊢ Orthonormal 𝕜 v ↔ ∀ (i : ι), ‖v i‖ = 1

Tactic:
simp [orthonormal_iff_ite, ← map_pow, pow_eq_one_iff_of_nonneg]

Premises used: map_pow, orthonormal_iff_ite, pow_eq_one_iff_of_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq E
s : Set E
rw :
  (∀ (i j : { x : E // x ∈ s }), ⟪(↑i : E), (↑j : E)⟫ = if i = j then 1 else 0) ↔
    ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫ = if v = w then 1 else 0
⊢ Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) ↔
    ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫ = if v = w then 1 else 0

Tactic:
rw [orthonormal_iff_ite]

Premises used: orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq E
s : Set E
⊢ (∀ (i j : { x : E // x ∈ s }), ⟪(↑i : E), (↑j : E)⟫ = if i = j then 1 else 0) ↔
    ∀ v ∈ s, ∀ w ∈ s, ⟪v, w⟫ = if v = w then 1 else 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
i : ι
⊢ ⟪v i, (linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l⟫ = (l : (a : ι) → 𝕜) i

Tactic:
simp [linearCombination_apply, Finsupp.inner_sum, orthonormal_iff_ite.mp hv, inner_smul_right,
    eq_comm]

Premises used: Finsupp.inner_sum, Finsupp.linearCombination_apply, eq_comm, inner_smul_right, Iff.mp, orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
i : ι
⊢ ⟪v i, (linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l⟫ = (l : (a : ι) → 𝕜) i

Tactic:
classical
  simp [linearCombination_apply, Finsupp.inner_sum, orthonormal_iff_ite.mp hv, inner_smul_right,
    eq_comm]

Premises used: Finsupp.inner_sum, Finsupp.linearCombination_apply, eq_comm, inner_smul_right, Iff.mp, orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι → 𝕜
s : Finset ι
i : ι
hi : i ∈ s
⊢ ⟪v i, ∑ i ∈ s, l i • v i⟫ = l i

Tactic:
simp [inner_sum, inner_smul_right, orthonormal_iff_ite.mp hv, hi]

Premises used: inner_sum, inner_smul_right, Iff.mp, orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι → 𝕜
s : Finset ι
i : ι
hi : i ∈ s
⊢ ⟪v i, ∑ i ∈ s, l i • v i⟫ = l i

Tactic:
classical
  simp [inner_sum, inner_smul_right, orthonormal_iff_ite.mp hv, hi]

Premises used: inner_sum, inner_smul_right, Iff.mp, orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
v : ι → E
hv : Orthonormal 𝕜 v
l : ι → 𝕜
i : ι
⊢ ⟪v i, ∑ i : ι, l i • v i⟫ = l i

Tactic:
hv.inner_right_sum l (Finset.mem_univ _)

Premises used: Finset.mem_univ, Orthonormal.inner_right_sum
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
i : ι
rw :
  Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪v i, (linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l⟫ : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((l : (a : ι) → 𝕜) i : 𝕜) : 𝕜)
rw₁ rw₂ :
  Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((l : (a : ι) → 𝕜) i : 𝕜) : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((l : (a : ι) → 𝕜) i : 𝕜) : 𝕜)
⊢ ⟪(linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l, v i⟫ = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((l : (a : ι) → 𝕜) i : 𝕜)

Tactic:
rw [← inner_conj_symm, hv.inner_right_finsupp]

Premises used: Orthonormal.inner_right_finsupp, inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι → 𝕜
s : Finset ι
i : ι
hi : i ∈ s
⊢ ⟪∑ i ∈ s, l i • v i, v i⟫ = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l i)

Tactic:
simp only [sum_inner, inner_smul_left, orthonormal_iff_ite.mp hv, hi, mul_boole,
    Finset.sum_ite_eq', if_true]

Premises used: if_true, Finset.sum_ite_eq', sum_inner, mul_boole, Iff.mp, orthonormal_iff_ite, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι → 𝕜
s : Finset ι
i : ι
hi : i ∈ s
⊢ ⟪∑ i ∈ s, l i • v i, v i⟫ = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l i)

Tactic:
classical
  simp only [sum_inner, inner_smul_left, orthonormal_iff_ite.mp hv, hi, mul_boole,
    Finset.sum_ite_eq', if_true]

Premises used: if_true, Finset.sum_ite_eq', sum_inner, mul_boole, Iff.mp, orthonormal_iff_ite, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
v : ι → E
hv : Orthonormal 𝕜 v
l : ι → 𝕜
i : ι
⊢ ⟪∑ i : ι, l i • v i, v i⟫ = (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l i)

Tactic:
hv.inner_left_sum l (Finset.mem_univ _)

Premises used: Finset.mem_univ, Orthonormal.inner_left_sum
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι →₀ 𝕜
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l₁ : E)
      ((linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l₂ : E) =
    l₁.sum fun (i : ι) (y : 𝕜) ↦
      HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) ((l₂ : (a : ι) → 𝕜) i : 𝕜)

Tactic:
simp [l₁.linearCombination_apply, Finsupp.sum_inner, hv.inner_right_finsupp, inner_smul_left]

Premises used: Finsupp.sum_inner, Finsupp.linearCombination_apply, Orthonormal.inner_right_finsupp, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι →₀ 𝕜
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l₁ : E)
      ((linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l₂ : E) =
    l₂.sum fun (i : ι) (y : 𝕜) ↦ HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((l₁ : (a : ι) → 𝕜) i : 𝕜) : 𝕜) y

Tactic:
simp [l₂.linearCombination_apply, Finsupp.inner_sum, hv.inner_left_finsupp, mul_comm,
    inner_smul_right]

Premises used: Orthonormal.inner_left_finsupp, Finsupp.inner_sum, Finsupp.linearCombination_apply, inner_smul_right, mul_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι → 𝕜
s : Finset ι
simp_rw :
  Eq.{u_1 + 1} (α := 𝕜)
    (∑ x ∈ s, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ x) : 𝕜) ⟪v x, ∑ i ∈ s, l₂ i • v i⟫)
    (∑ i ∈ s, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i))
⊢ inner.{u_1, u_2} 𝕜 (E := E) (∑ i ∈ s, l₁ i • v i) (∑ i ∈ s, l₂ i • v i) =
    ∑ i ∈ s, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i)

Tactic:
simp_rw [sum_inner, inner_smul_left]

Premises used: sum_inner, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι → 𝕜
s : Finset ι
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (∑ x ∈ s, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ x) : 𝕜) ⟪v x, ∑ i ∈ s, l₂ i • v i⟫)
    (∑ i ∈ s, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i))

Tactic:
Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι → 𝕜
s : Finset ι
refine :
  ∀ (i : ι) (hi : i ∈ s),
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) ⟪v i, ∑ i ∈ s, l₂ i • v i⟫ =
      HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (∑ x ∈ s, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ x) : 𝕜) ⟪v x, ∑ i ∈ s, l₂ i • v i⟫)
    (∑ i ∈ s, HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i))

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι → 𝕜
s : Finset ι
i : ι
hi : i ∈ s
rw rw₁ :
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i)
⊢ HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) ⟪v i, ∑ i ∈ s, l₂ i • v i⟫ =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (l₁ i) : 𝕜) (l₂ i)

Tactic:
rw [hv.inner_right_sum l₂ hi]

Premises used: Orthonormal.inner_right_sum
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
s : Finset ι
v : ι → E
hv : Orthonormal 𝕜 v
a : ι → ι → 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ s, ∑ j ∈ s, a i j • ⟪v j, v i⟫) (∑ k ∈ s, a k k)

Tactic:
simp [orthonormal_iff_ite.mp hv]

Premises used: Iff.mp, orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
s : Finset ι
v : ι → E
hv : Orthonormal 𝕜 v
a : ι → ι → 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ s, ∑ j ∈ s, a i j • ⟪v j, v i⟫) (∑ k ∈ s, a k k)

Tactic:
classical
  simp [orthonormal_iff_ite.mp hv]

Premises used: Iff.mp, orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
rw : ∀ (l : ι →₀ 𝕜), Eq.{u_2 + 1} (α := E) ((linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l : E) (0 : E) → l = 0
⊢ LinearIndependent 𝕜 v

Tactic:
rw [linearIndependent_iff]

Premises used: linearIndependent_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : Eq.{u_2 + 1} (α := E) ((linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l : E) (0 : E)
h : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) ((l : (a : ι) → 𝕜) i : 𝕜) ((0 : (a : ι) → 𝕜) i : 𝕜)
⊢ l = 0

Tactic:
ext i
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : Eq.{u_2 + 1} (α := E) ((linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l : E) (0 : E)
i : ι
rw rw₁ : ⟪v i, 0⟫ = ⟪v i, 0⟫
⊢ ⟪v i, (linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l⟫ = ⟪v i, 0⟫

Tactic:
rw [hl]
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : Eq.{u_2 + 1} (α := E) ((linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l : E) (0 : E)
i : ι
⊢ ⟪v i, (linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l⟫ = ⟪v i, 0⟫

Tactic:
have key : ⟪v i, Finsupp.linearCombination 𝕜 v l⟫ = ⟪v i, 0⟫ := by rw [hl]
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : Eq.{u_2 + 1} (α := E) ((linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l : E) (0 : E)
i : ι
key : ⟪v i, (linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l⟫ = ⟪v i, 0⟫
⊢ Eq.{u_1 + 1} (α := 𝕜) ((l : (a : ι) → 𝕜) i : 𝕜) ((0 : (a : ι) → 𝕜) i : 𝕜)

Tactic:
simpa only [hv.inner_right_finsupp, inner_zero_right] using key

Premises used: inner_zero_right, Orthonormal.inner_right_finsupp
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : Orthonormal 𝕜 v
f : ι' → ι
hf : Function.Injective f
rw :
  ∀ (hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0) (f : ι' → ι) (hf : Function.Injective f) (i j : ι'),
    ⟪(v ∘ f) i, (v ∘ f) j⟫ = if i = j then 1 else 0
⊢ Orthonormal 𝕜 (v ∘ f)

Tactic:
rw [orthonormal_iff_ite] at hv ⊢

Premises used: orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
f : ι' → ι
hf : Function.Injective f
i j : ι'
⊢ ⟪v (f i), v (f j)⟫ = if f i = f j then 1 else 0

Tactic:
hv (f i) (f j)
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
f : ι' → ι
hf : Function.Injective f
i j : ι'
h : Eq.{u_1 + 1} (α := 𝕜) (if i = j then 1 else 0) (if f i = f j then 1 else 0)
⊢ ⟪(v ∘ f) i, (v ∘ f) j⟫ = if i = j then 1 else 0

Tactic:
convert! hv (f i) (f j) using 1
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
f : ι' → ι
hf : Function.Injective f
i j : ι'
⊢ Eq.{u_1 + 1} (α := 𝕜) (if i = j then 1 else 0) (if f i = f j then 1 else 0)

Tactic:
simp [hf.eq_iff]

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : Orthonormal 𝕜 v
f : ι' → ι
hf : Function.Injective f
rw rw₁ rw₂ rw₃ :
  ∀ (hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0) (f : ι' → ι) (hf : Function.Injective f) (i j : ι'),
    ⟪(v ∘ f) i, (v ∘ f) j⟫ = if i = j then 1 else 0
h :
  ∀ (hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0) (f : ι' → ι) (hf : Function.Injective f) (i j : ι'),
    Eq.{u_1 + 1} (α := 𝕜) (if i = j then 1 else 0) (if f i = f j then 1 else 0)
⊢ Orthonormal 𝕜 (v ∘ f)

Tactic:
classical
  rw [orthonormal_iff_ite] at hv ⊢
  intro i j
  convert! hv (f i) (f j) using 1
  simp [hf.eq_iff]

Premises used: Function.Injective.eq_iff, orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Function.Injective v
f : Equiv.{u_4 + 1, u_2 + 1} ι (↑(Set.range v) : Type u_2) := Equiv.ofInjective v hv
⊢ Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ Set.range v })
      (Subtype.val (p := fun (x : E) ↦ x ∈ Set.range v)) ↔
    Orthonormal 𝕜 v

Tactic:
⟨fun h => h.comp f f.injective, fun h => ?_⟩

Premises used: Orthonormal.comp, Iff.intro, Equiv.injective, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Function.Injective v
f : Equiv.{u_4 + 1, u_2 + 1} ι (↑(Set.range v) : Type u_2) := Equiv.ofInjective v hv
refine :
  ∀ (h : Orthonormal 𝕜 v),
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ Set.range v })
      (Subtype.val (p := fun (x : E) ↦ x ∈ Set.range v))
⊢ Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ Set.range v })
      (Subtype.val (p := fun (x : E) ↦ x ∈ Set.range v)) ↔
    Orthonormal 𝕜 v

Tactic:
refine ⟨fun h => h.comp f f.injective, fun h => ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Function.Injective v
f : Equiv.{u_4 + 1, u_2 + 1} ι (↑(Set.range v) : Type u_2) := Equiv.ofInjective v hv
h : Orthonormal 𝕜 v
rw :
  Orthonormal 𝕜 (ι := { x : E // x ∈ Set.range v })
    (v ∘ (⇑(Equiv.ofInjective v hv).symm : (a : (↑(Set.range v) : Type u_2)) → ι))
⊢ Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ Set.range v })
    (Subtype.val (p := fun (x : E) ↦ x ∈ Set.range v))

Tactic:
rw [← Equiv.self_comp_ofInjective_symm hv]

Premises used: Equiv.self_comp_ofInjective_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Function.Injective v
f : Equiv.{u_4 + 1, u_2 + 1} ι (↑(Set.range v) : Type u_2) := Equiv.ofInjective v hv
h : Orthonormal 𝕜 v
⊢ Orthonormal 𝕜 (ι := { x : E // x ∈ Set.range v })
    (v ∘ (⇑(Equiv.ofInjective v hv).symm : (a : (↑(Set.range v) : Type u_2)) → ι))

Tactic:
h.comp f.symm f.symm.injective

Premises used: Orthonormal.comp, Equiv.injective, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Function.Injective v
f : Equiv.{u_4 + 1, u_2 + 1} ι (↑(Set.range v) : Type u_2) := Equiv.ofInjective v hv
h : Orthonormal 𝕜 v
⊢ Orthonormal 𝕜 (ι := { x : E // x ∈ Set.range v })
    (v ∘ (⇑(Equiv.ofInjective v hv).symm : (a : (↑(Set.range v) : Type u_2)) → ι))

Tactic:
exact h.comp f.symm f.symm.injective

Premises used: Orthonormal.comp, Equiv.injective, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
⊢ Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ Set.range v })
    (Subtype.val (p := fun (x : E) ↦ x ∈ Set.range v))

Tactic:
(orthonormal_subtype_range hv.linearIndependent.injective).2 hv

Premises used: Orthonormal.linearIndependent, Iff.mpr, orthonormal_subtype_range, LinearIndependent.injective
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
s : Set ι
i : ι
hi : i ∉ s
l : ι →₀ 𝕜
hl : Membership.mem (γ := Submodule 𝕜 (ι →₀ 𝕜)) (supported 𝕜 𝕜 s) l
⊢ ∀ x ∉ s, Eq.{u_1 + 1} (α := 𝕜) ((l : (a : ι) → 𝕜) x : 𝕜) (0 : 𝕜)

Tactic:
rw [Finsupp.mem_supported'] at hl

Premises used: Finsupp.mem_supported'
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
s : Set ι
i : ι
hi : i ∉ s
l : ι →₀ 𝕜
hl : ∀ x ∉ s, Eq.{u_1 + 1} (α := 𝕜) ((l : (a : ι) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ ⟪(linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l, v i⟫ = 0

Tactic:
simp only [hv.inner_left_finsupp, hl i hi, map_zero]

Premises used: Orthonormal.inner_left_finsupp, map_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : Orthonormal 𝕜 v
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
rw :
  ∀ (hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0) (hw : ∀ (i : ι), w i = v i ∨ w i = -v i) (i j : ι),
    ⟪w i, w j⟫ = if i = j then 1 else 0
⊢ Orthonormal 𝕜 w

Tactic:
rw [orthonormal_iff_ite] at *

Premises used: orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
inl : ∀ (hi : w i = v i), ⟪w i, w j⟫ = if i = j then 1 else 0
inr : ∀ (hi : w i = -v i), ⟪w i, w j⟫ = if i = j then 1 else 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0

Tactic:
rcases hw i with hi | hi
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
inl : ∀ (hj : w j = v j), ⟪w i, w j⟫ = if i = j then 1 else 0
inl₁ : ∀ (hj : w j = -v j), ⟪w i, w j⟫ = if i = j then 1 else 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0

Tactic:
rcases hw j with hj | hj
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
inr : ∀ (hj : w j = v j), ⟪w i, w j⟫ = if i = j then 1 else 0
inr₁ : ∀ (hj : w j = -v j), ⟪w i, w j⟫ = if i = j then 1 else 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0

Tactic:
rcases hw j with hj | hj
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = v j
⊢ ⟪v i, v j⟫ = if i = j then 1 else 0

Tactic:
replace hv := hv i j
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = -v j
⊢ ⟪v i, v j⟫ = if i = j then 1 else 0

Tactic:
replace hv := hv i j
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hv : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = v j
⊢ ⟪v i, v j⟫ = if i = j then 1 else 0

Tactic:
replace hv := hv i j