awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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)
⊢ l = 0
have h : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) ((l : (a : ι) → 𝕜) i : 𝕜) ((0 : (a : ι) → 𝕜) i : 𝕜)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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⟫
have rw : ⟪v i, 0⟫ = ⟪v i, 0⟫
Tactic: rw [hl]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (hypothesis)
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 : ι
⊢ Eq.{u_1 + 1} (α := 𝕜) ((l : (a : ι) → 𝕜) i : 𝕜) ((0 : (a : ι) → 𝕜) i : 𝕜)
have key : ⟪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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
⊢ Orthonormal 𝕜 (v ∘ f)
have 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
Tactic: rw [orthonormal_iff_ite] at hv ⊢
Cleared hypotheses: hv, f, hf
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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 i = j then 1 else 0
have h : Eq.{u_1 + 1} (α := 𝕜) (if i = j then 1 else 0) (if f i = f j then 1 else 0)
Tactic: convert! hv (f i) (f j) using 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
⊢ Orthonormal 𝕜 (v ∘ f)
have 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
Tactic: classical
  rw [orthonormal_iff_ite] at hv ⊢
  intro i j
  convert! hv (f i) (f j) using 1
  simp [hf.eq_iff]
Cleared hypotheses: hv, f, hf
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
⊢ Orthonormal 𝕜 (v ∘ f)
have 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)
Tactic: classical
  rw [orthonormal_iff_ite] at hv ⊢
  intro i j
  convert! hv (f i) (f j) using 1
  simp [hf.eq_iff]
Cleared hypotheses: hv, f, hf
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
have 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))
Tactic: refine ⟨fun h => h.comp f f.injective, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ Set.range v })
    (Subtype.val (p := fun (x : E) ↦ x ∈ Set.range v))
have rw : Orthonormal 𝕜 (ι := { x : E // x ∈ Set.range v })
  (v ∘ (⇑(Equiv.ofInjective v hv).symm : (a : (↑(Set.range v) : Type u_2)) → ι))
Tactic: rw [← Equiv.self_comp_ofInjective_symm hv]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (hypothesis)
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
⊢ ⟪(linearCombination 𝕜 v : (a : ι →₀ 𝕜) → E) l, v i⟫ = 0
have hl₁ : ∀ x ∉ s, Eq.{u_1 + 1} (α := 𝕜) ((l : (a : ι) → 𝕜) x : 𝕜) (0 : 𝕜)
Tactic: rw [Finsupp.mem_supported'] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
⊢ Orthonormal 𝕜 w
have 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
Tactic: rw [orthonormal_iff_ite] at *
Cleared hypotheses: hv, hw
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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 : ι
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have inl : ∀ (hi : w i = v i), ⟪w i, w j⟫ = if i = j then 1 else 0
Tactic: rcases hw i with hi | hi
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have inr : ∀ (hi : w i = -v i), ⟪w i, w j⟫ = if i = j then 1 else 0
Tactic: rcases hw i with hi | hi
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have inl : ∀ (hj : w j = v j), ⟪w i, w j⟫ = if i = j then 1 else 0
Tactic: rcases hw j with hj | hj
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have inl₁ : ∀ (hj : w j = -v j), ⟪w i, w j⟫ = if i = j then 1 else 0
Tactic: rcases hw j with hj | hj
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have inr : ∀ (hj : w j = v j), ⟪w i, w j⟫ = if i = j then 1 else 0
Tactic: rcases hw j with hj | hj
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have inr₁ : ∀ (hj : w j = -v j), ⟪w i, w j⟫ = if i = j then 1 else 0
Tactic: rcases hw j with hj | hj
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (hypothesis)
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
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have hv₁ : ⟪v i, v j⟫ = if i = j then 1 else 0
Tactic: replace hv := hv i j
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (hypothesis)
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
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have hv₁ : ⟪v i, v j⟫ = if i = j then 1 else 0
Tactic: replace hv := hv i j
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (hypothesis)
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
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have hv₁ : ⟪v i, v j⟫ = if i = j then 1 else 0
Tactic: replace hv := hv i j
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (hypothesis)
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
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have hv₁ : ⟪v i, v j⟫ = if i = j then 1 else 0
Tactic: replace hv := hv i j
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have pos : ∀ (h : i = j) (hv : ⟪v i, v j⟫ = 1), ⟪w i, w j⟫ = 1
Tactic: split_ifs at hv ⊢ with h
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
pos : ∀ (h : i = j) (hv : ⟪v i, v j⟫ = 1), ⟪w i, w j⟫ = 1
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have neg : ∀ (h : ¬i = j) (hv : ⟪v i, v j⟫ = 0), ⟪w i, w j⟫ = 0
Tactic: split_ifs at hv ⊢ with h
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = -v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have pos : ∀ (h : i = j) (hv : ⟪v i, v j⟫ = 1), ⟪w i, w j⟫ = 1
Tactic: split_ifs at hv ⊢ with h
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = -v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
pos : ∀ (h : i = j) (hv : ⟪v i, v j⟫ = 1), ⟪w i, w j⟫ = 1
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have neg : ∀ (h : ¬i = j) (hv : ⟪v i, v j⟫ = 0), ⟪w i, w j⟫ = 0
Tactic: split_ifs at hv ⊢ with h
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have pos : ∀ (h : i = j) (hv : ⟪v i, v j⟫ = 1), ⟪w i, w j⟫ = 1
Tactic: split_ifs at hv ⊢ with h
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
pos : ∀ (h : i = j) (hv : ⟪v i, v j⟫ = 1), ⟪w i, w j⟫ = 1
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have neg : ∀ (h : ¬i = j) (hv : ⟪v i, v j⟫ = 0), ⟪w i, w j⟫ = 0
Tactic: split_ifs at hv ⊢ with h
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have pos : ∀ (h : i = j) (hv : ⟪v i, v j⟫ = 1), ⟪w i, w j⟫ = 1
Tactic: split_ifs at hv ⊢ with h
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
hv : ⟪v i, v j⟫ = if i = j then 1 else 0
pos : ∀ (h : i = j) (hv : ⟪v i, v j⟫ = 1), ⟪w i, w j⟫ = 1
⊢ ⟪w i, w j⟫ = if i = j then 1 else 0
have neg : ∀ (h : ¬i = j) (hv : ⟪v i, v j⟫ = 0), ⟪w i, w j⟫ = 0
Tactic: split_ifs at hv ⊢ with h
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
⊢ Orthonormal 𝕜 w
have 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
Tactic: classical
  rw [orthonormal_iff_ite] at *
  intro i j
  rcases hw i with hi | hi <;> rcases hw j with hj | hj <;>
    replace hv := hv i j <;> split_ifs at hv ⊢ with h <;>
    simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
      neg_eq_zero] using hv
Cleared hypotheses: hv, hw
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
⊢ Orthonormal 𝕜 (E := E) fun (x : (↑(⋃ (i : η), s i) : Type u_2)) ↦ (↑x : E)
have rw : ∀ (v : E),
  Membership.mem (γ := Set E) (⋃ (i : η), s i) v →
    ∀ (w : E), Membership.mem (γ := Set E) (⋃ (i : η), s i) w → ⟪v, w⟫ = if v = w then 1 else 0
Tactic: rw [orthonormal_subtype_iff_ite]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
x : E
i : η
hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x
y : E
j : η
hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y
⊢ ⟪x, y⟫ = if x = y then 1 else 0
have obtain : ∀ (k : η) (hik : s i ⊆ s k) (hjk : s j ⊆ s k), ⟪x, y⟫ = if x = y then 1 else 0
Tactic: obtain ⟨k, hik, hjk⟩ := hs i j
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
x : E
i : η
hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x
y : E
j : η
hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y
k : η
hik : s i ⊆ s k
hjk : s j ⊆ s k
⊢ ⟪x, y⟫ = if x = y then 1 else 0
have h_orth : Orthonormal 𝕜 (E := E) fun (x : (↑(s k) : Type u_2)) ↦ (↑x : E)
Tactic: have h_orth : Orthonormal 𝕜 (fun x => x : s k → E) := h k
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
x : E
i : η
hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x
y : E
j : η
hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y
k : η
hik : s i ⊆ s k
hjk : s j ⊆ s k
h_orth : Orthonormal 𝕜 (E := E) fun (x : (↑(s k) : Type u_2)) ↦ (↑x : E)
⊢ ⟪x, y⟫ = if x = y then 1 else 0
have h_orth₁ : ∀ v ∈ s k, ∀ w ∈ s k, ⟪v, w⟫ = if v = w then 1 else 0
Tactic: rw [orthonormal_subtype_iff_ite] at h_orth
Cleared hypotheses: h_orth
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
⊢ Orthonormal 𝕜 (E := E) fun (x : (↑(⋃ (i : η), s i) : Type u_2)) ↦ (↑x : E)
have rw : ∀ (v : E),
  Membership.mem (γ := Set E) (⋃ (i : η), s i) v →
    ∀ (w : E), Membership.mem (γ := Set E) (⋃ (i : η), s i) w → ⟪v, w⟫ = if v = w then 1 else 0
Tactic: classical
  rw [orthonormal_subtype_iff_ite]
  rintro x ⟨_, ⟨i, rfl⟩, hxi⟩ y ⟨_, ⟨j, rfl⟩, hyj⟩
  obtain ⟨k, hik, hjk⟩ := hs i j
  have h_orth : Orthonormal 𝕜 (fun x => x : s k → E) := h k
  rw [orthonormal_subtype_iff_ite] at h_orth
  exact h_orth x (hik hxi) y (hjk hyj)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
rw rw₁ rw₂ :
  ∀ (v : E),
    Membership.mem (γ := Set E) (⋃ (i : η), s i) v →
      ∀ (w : E), Membership.mem (γ := Set E) (⋃ (i : η), s i) w → ⟪v, w⟫ = if v = w then 1 else 0
⊢ Orthonormal 𝕜 (E := E) fun (x : (↑(⋃ (i : η), s i) : Type u_2)) ↦ (↑x : E)
have rw₃ : ∀ (x : E) (i : η) (hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x) (y : E) (j : η)
  (hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y), ⟪x, y⟫ = if x = y then 1 else 0
Tactic: classical
  rw [orthonormal_subtype_iff_ite]
  rintro x ⟨_, ⟨i, rfl⟩, hxi⟩ y ⟨_, ⟨j, rfl⟩, hyj⟩
  obtain ⟨k, hik, hjk⟩ := hs i j
  have h_orth : Orthonormal 𝕜 (fun x => x : s k → E) := h k
  rw [orthonormal_subtype_iff_ite] at h_orth
  exact h_orth x (hik hxi) y (hjk hyj)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
rw rw₁ rw₂ :
  ∀ (v : E),
    Membership.mem (γ := Set E) (⋃ (i : η), s i) v →
      ∀ (w : E), Membership.mem (γ := Set E) (⋃ (i : η), s i) w → ⟪v, w⟫ = if v = w then 1 else 0
rw₃ :
  ∀ (x : E) (i : η) (hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x) (y : E) (j : η)
    (hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y), ⟪x, y⟫ = if x = y then 1 else 0
⊢ Orthonormal 𝕜 (E := E) fun (x : (↑(⋃ (i : η), s i) : Type u_2)) ↦ (↑x : E)
have rw₄ : ∀ (x : E) (i : η) (hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x) (y : E) (j : η)
  (hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y) (k : η) (hik : s i ⊆ s k) (hjk : s j ⊆ s k),
  ⟪x, y⟫ = if x = y then 1 else 0
Tactic: classical
  rw [orthonormal_subtype_iff_ite]
  rintro x ⟨_, ⟨i, rfl⟩, hxi⟩ y ⟨_, ⟨j, rfl⟩, hyj⟩
  obtain ⟨k, hik, hjk⟩ := hs i j
  have h_orth : Orthonormal 𝕜 (fun x => x : s k → E) := h k
  rw [orthonormal_subtype_iff_ite] at h_orth
  exact h_orth x (hik hxi) y (hjk hyj)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
rw rw₁ rw₂ :
  ∀ (v : E),
    Membership.mem (γ := Set E) (⋃ (i : η), s i) v →
      ∀ (w : E), Membership.mem (γ := Set E) (⋃ (i : η), s i) w → ⟪v, w⟫ = if v = w then 1 else 0
rw₃ :
  ∀ (x : E) (i : η) (hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x) (y : E) (j : η)
    (hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y), ⟪x, y⟫ = if x = y then 1 else 0
rw₄ :
  ∀ (x : E) (i : η) (hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x) (y : E) (j : η)
    (hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y) (k : η) (hik : s i ⊆ s k) (hjk : s j ⊆ s k),
    ⟪x, y⟫ = if x = y then 1 else 0
⊢ Orthonormal 𝕜 (E := E) fun (x : (↑(⋃ (i : η), s i) : Type u_2)) ↦ (↑x : E)
have rw₅ : ∀ (x : E) (i : η) (hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x) (y : E) (j : η)
  (hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y) (k : η) (hik : s i ⊆ s k) (hjk : s j ⊆ s k)
  (h_orth : Orthonormal 𝕜 (E := E) fun (x : (↑(s k) : Type u_2)) ↦ (↑x : E)), ⟪x, y⟫ = if x = y then 1 else 0
Tactic: classical
  rw [orthonormal_subtype_iff_ite]
  rintro x ⟨_, ⟨i, rfl⟩, hxi⟩ y ⟨_, ⟨j, rfl⟩, hyj⟩
  obtain ⟨k, hik, hjk⟩ := hs i j
  have h_orth : Orthonormal 𝕜 (fun x => x : s k → E) := h k
  rw [orthonormal_subtype_iff_ite] at h_orth
  exact h_orth x (hik hxi) y (hjk hyj)