awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c_1 : ℝ
c : ℝ := -c_1
hc : 0 < c
x : H
rw : HPow.hPow (β := ℕ) ‖x‖ 2 * c = (re : (a : 𝕜) → ℝ) ⟪(HSMul.hSMul (β := H →L[𝕜] H) c 1 : (a : H) → H) x, x⟫_𝕜
rw₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ)
      ⟪(HSMul.hSMul (α := 𝕜) (β := H →L[𝕜] H) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) 1 : (a : H) → H) x, x⟫_𝕜
rw₂ :
  HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ)
      ⟪HSMul.hSMul (α := 𝕜) (β := (a : H) → H) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) (⇑1 : (a : H) → H) x, x⟫_𝕜
rw₃ :
  HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ)
      ⟪HSMul.hSMul (α := 𝕜) (β := H) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) ((1 : (a : H) → H) x : H), x⟫_𝕜
rw₄ :
  HPow.hPow (β := ℕ) ‖x‖ 2 * c = (re : (a : 𝕜) → ℝ) ⟪HSMul.hSMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) x, x⟫_𝕜
rw₅ :
  HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ)
      (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) c : 𝕜) : 𝕜) ⟪x, x⟫_𝕜)
rw₆ :
  HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ) (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑c : 𝕜) : 𝕜) ⟪x, x⟫_𝕜)
rw₇ : HPow.hPow (β := ℕ) ‖x‖ 2 * c = (re : (a : 𝕜) → ℝ) ((↑c : 𝕜) * ⟪x, x⟫_𝕜)
rw₈ : HPow.hPow (β := ℕ) ‖x‖ 2 * c = HMul.hMul (β := ℝ) c ((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜 : ℝ)
rw₉ : HPow.hPow (β := ℕ) ‖x‖ 2 * c = c * HPow.hPow (β := ℕ) ‖x‖ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * c =
    (re : (a : 𝕜) → ℝ) ⟪(((algebraMap ℝ (H →L[𝕜] H) : (a : ℝ) → H →L[𝕜] H) c : H →L[𝕜] H) : (a : H) → H) x, x⟫_𝕜
have rw₁₀ : c * HPow.hPow (β := ℕ) ‖x‖ 2 = c * HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rw [Algebra.algebraMap_eq_smul_one, ← algebraMap_smul 𝕜 c (1 : (H →L[𝕜] H)), coe_smul',
        Pi.smul_apply, one_apply, inner_smul_left, RCLike.algebraMap_eq_ofReal, conj_ofReal,
        re_ofReal_mul, inner_self_eq_norm_sq, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
⊢ f ≤ g ↔
    ∃ (p : H →L[𝕜] H),
      Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
          p ∧
        g = f + p
have mp : f ≤ g →
  ∃ (p : H →L[𝕜] H),
    Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
        p ∧
      g = f + p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
mp :
  f ≤ g →
    ∃ (p : H →L[𝕜] H),
      Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
          p ∧
        g = f + p
⊢ f ≤ g ↔
    ∃ (p : H →L[𝕜] H),
      Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
          p ∧
        g = f + p
have mpr : (∃ (p : H →L[𝕜] H),
    Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
        p ∧
      g = f + p) →
  f ≤ g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (hypothesis)
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : f ≤ g
⊢ ∃ (p : H →L[𝕜] H),
    Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
        p ∧
      g = f + p
have h₁ : (g - f).IsPositive
Tactic: rw [le_def] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
⊢ ∃ (p : H →L[𝕜] H),
    Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
        p ∧
      g = f + p
have mp : ∀ (p : H →L[𝕜] H) (hp₁ : IsSelfAdjoint p) (hp₃ : p * p = g - f),
  ∃ (p : H →L[𝕜] H),
    Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
        p ∧
      g = f + p
Tactic: obtain ⟨p, hp₁, -, hp₃⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts
        h.isSelfAdjoint h.spectrumRestricts
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p * p = g - f
⊢ g = f + HPow.hPow (β := ℕ) p 2
have symm : f + HPow.hPow (β := ℕ) p 2 = g
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p * p = g - f
⊢ f + HPow.hPow (β := ℕ) p 2 = g
have rwa : HPow.hPow (β := ℕ) p 2 + f = g
Tactic: rwa [add_comm, ← eq_sub_iff_add_eq]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p * p = g - f
rwa : HPow.hPow (β := ℕ) p 2 + f = g
⊢ f + HPow.hPow (β := ℕ) p 2 = g
have rwa₁ : HPow.hPow (β := ℕ) p 2 = g - f
Tactic: rwa [add_comm, ← eq_sub_iff_add_eq]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p * p = g - f
⊢ ∃ (p : H →L[𝕜] H),
    Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
        p ∧
      g = f + p
have mp : Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
  (HPow.hPow (β := ℕ) p 2)
Tactic: refine ⟨p ^ 2, ?_, by symm; rwa [add_comm, ← eq_sub_iff_add_eq]⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f p : H →L[𝕜] H
hp :
  Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s)) p
⊢ f ≤ f + p
have mpr : p.IsPositive
Tactic: rw [le_def, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f p x : H →L[𝕜] H
hf : Membership.mem (γ := Set (H →L[𝕜] H)) (Set.range fun (s : H →L[𝕜] H) ↦ star s * s) x
⊢ x.IsPositive
have mpr : ∀ (f : H →L[𝕜] H), IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := H) ((fun (s : H →L[𝕜] H) ↦ star s * s) f)
Tactic: obtain ⟨f, rfl⟩ := hf
Cleared hypotheses: x, hf
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f p : H →L[𝕜] H
hp :
  Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s)) p
⊢ p.IsPositive
have mpr : ∀ (x : H →L[𝕜] H) (hf : Membership.mem (γ := Set (H →L[𝕜] H)) (Set.range fun (s : H →L[𝕜] H) ↦ star s * s) x),
  x.IsPositive
Tactic: induction hp using AddSubmonoid.closure_induction with
      | mem _ hf =>
        obtain ⟨f, rfl⟩ := hf
        simpa using ContinuousLinearMap.IsPositive.adjoint_conj isPositive_one f
      | zero => exact isPositive_zero
      | add f g _ _ hf hg => exact hf.add hg
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f p : H →L[𝕜] H
hp :
  Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s)) p
mpr :
  ∀ (x : H →L[𝕜] H) (hf : Membership.mem (γ := Set (H →L[𝕜] H)) (Set.range fun (s : H →L[𝕜] H) ↦ star s * s) x),
    x.IsPositive
⊢ p.IsPositive
have mpr₁ : IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := H) 0
Tactic: induction hp using AddSubmonoid.closure_induction with
      | mem _ hf =>
        obtain ⟨f, rfl⟩ := hf
        simpa using ContinuousLinearMap.IsPositive.adjoint_conj isPositive_one f
      | zero => exact isPositive_zero
      | add f g _ _ hf hg => exact hf.add hg
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.StarOrder (goal)
Goal:
𝕜 : Type u_1
H : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
inst_3 : CompleteSpace H
inst_4 : Algebra ℝ (H →L[𝕜] H)
inst_5 : IsScalarTower.{0, u_1, u_2} ℝ 𝕜 (H →L[𝕜] H)
inst_6 : ContinuousFunctionalCalculus.{0, u_2} ℝ (H →L[𝕜] H) IsSelfAdjoint
f p : H →L[𝕜] H
hp :
  Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s)) p
mpr :
  ∀ (x : H →L[𝕜] H) (hf : Membership.mem (γ := Set (H →L[𝕜] H)) (Set.range fun (s : H →L[𝕜] H) ↦ star s * s) x),
    x.IsPositive
mpr₁ : IsPositive.{u_1, u_2} (𝕜 := 𝕜) (E := H) 0
⊢ p.IsPositive
have mpr₂ : ∀ (f g : H →L[𝕜] H),
  Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s)) f →
    Membership.mem (γ := AddSubmonoid (H →L[𝕜] H)) (AddSubmonoid.closure (Set.range fun (s : H →L[𝕜] H) ↦ star s * s))
        g →
      ∀ (hf : f.IsPositive) (hg : g.IsPositive), (f + g).IsPositive
Tactic: induction hp using AddSubmonoid.closure_induction with
      | mem _ hf =>
        obtain ⟨f, rfl⟩ := hf
        simpa using ContinuousLinearMap.IsPositive.adjoint_conj isPositive_one f
      | zero => exact isPositive_zero
      | add f g _ _ hf hg => exact hf.add hg
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : DecidableEq ι
i j : ι
v : G i
w : G j
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) =
    if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) else 0
have pos : ∀ (h : i = j),
  inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) =
    inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : DecidableEq ι
i j : ι
v : G i
w : G j
pos :
  ∀ (h : i = j),
    inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) =
      inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E)
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) =
    if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) else 0
have neg : ∀ (h : ¬i = j), inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst_6 : DecidableEq ι
l : ⨁ (i : ι), G i
i : ι
v : G i
⊢ (DFinsupp.sum (β := fun (i : ι) ↦ G i) l fun (j : ι) (w : G j) ↦
      if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) w : E) else 0) =
    ⟪v, (l : (a : ι) → G a) i⟫
have simp : (if (l : (a : ι) → G a) i ≠ 0 then
    inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V i : (a : G i) → E) ((l : (a : ι) → G a) i) : E)
  else 0) =
  ⟪v, (l : (a : ι) → G a) i⟫
Tactic: simp only [DFinsupp.sum, Finset.sum_ite_eq,
        DFinsupp.mem_support_toFun]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst_6 : DecidableEq ι
l : ⨁ (i : ι), G i
i : ι
v : G i
⊢ (if (l : (a : ι) → G a) i ≠ 0 then
      inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V i : (a : G i) → E) ((l : (a : ι) → G a) i) : E)
    else 0) =
    ⟪v, (l : (a : ι) → G a) i⟫
have pos : ∀ (h : (l : (a : ι) → G a) i ≠ 0),
  inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V i : (a : G i) → E) ((l : (a : ι) → G a) i) : E) =
    ⟪v, (l : (a : ι) → G a) i⟫
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : (i : ι) → (x : G i) → Decidable (x ≠ 0)
inst_6 : DecidableEq ι
l : ⨁ (i : ι), G i
i : ι
v : G i
pos :
  ∀ (h : (l : (a : ι) → G a) i ≠ 0),
    inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V i : (a : G i) → E) ((l : (a : ι) → G a) i) : E) =
      ⟪v, (l : (a : ι) → G a) i⟫
⊢ (if (l : (a : ι) → G a) i ≠ 0 then
      inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V i : (a : G i) → E) ((l : (a : ι) → G a) i) : E)
    else 0) =
    ⟪v, (l : (a : ι) → G a) i⟫
have neg : ∀ (h : ¬(l : (a : ι) → G a) i ≠ 0), 0 = ⟪v, (l : (a : ι) → G a) i⟫
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) (∑ j : ι, (V j : (a : G j) → E) (l j) : E) =
    ∑ j : ι, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E)
have rw : Eq.{u_1 + 1} (α := 𝕜)
  (∑ i_1 : ι, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V i_1 : (a : G i_1) → E) (l i_1) : E))
  (∑ j : ι, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E))
Tactic: rw [inner_sum]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) (∑ j : ι, (V j : (a : G j) → E) (l j) : E) = ⟪v, l i⟫
have i₁ : inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) (∑ j : ι, (V j : (a : G j) → E) (l j) : E) =
  ∑ j : ι, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E)
Tactic: calc
    ⟪V i v, ∑ j : ι, V j (l j)⟫ = ∑ j : ι, ⟪V i v, V j (l j)⟫ := by rw [inner_sum]
    _ = ∑ j, ite (i = j) ⟪V i v, V j (l j)⟫ 0 :=
      (congr_arg (Finset.sum Finset.univ) <| funext fun j => hV.eq_ite v (l j))
    _ = ⟪v, l i⟫ := by
      simp only [Finset.sum_ite_eq, Finset.mem_univ, (V i).inner_map_map, if_true]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
i₁ :
  inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) (∑ j : ι, (V j : (a : G j) → E) (l j) : E) =
    ∑ j : ι, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E)
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) (∑ j : ι, (V j : (a : G j) → E) (l j) : E) = ⟪v, l i⟫
have i₂ : (∑ j : ι,
    if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E) else 0) =
  ⟪v, l i⟫
Tactic: calc
    ⟪V i v, ∑ j : ι, V j (l j)⟫ = ∑ j : ι, ⟪V i v, V j (l j)⟫ := by rw [inner_sum]
    _ = ∑ j, ite (i = j) ⟪V i v, V j (l j)⟫ 0 :=
      (congr_arg (Finset.sum Finset.univ) <| funext fun j => hV.eq_ite v (l j))
    _ = ⟪v, l i⟫ := by
      simp only [Finset.sum_ite_eq, Finset.mem_univ, (V i).inner_map_map, if_true]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) (∑ j : ι, (V j : (a : G j) → E) (l j) : E) = ⟪v, l i⟫
have i₁ : inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) (∑ j : ι, (V j : (a : G j) → E) (l j) : E) =
  ∑ j : ι, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E)
Tactic: classical
  calc
    ⟪V i v, ∑ j : ι, V j (l j)⟫ = ∑ j : ι, ⟪V i v, V j (l j)⟫ := by rw [inner_sum]
    _ = ∑ j, ite (i = j) ⟪V i v, V j (l j)⟫ 0 :=
      (congr_arg (Finset.sum Finset.univ) <| funext fun j => hV.eq_ite v (l j))
    _ = ⟪v, l i⟫ := by
      simp only [Finset.sum_ite_eq, Finset.mem_univ, (V i).inner_map_map, if_true]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Subspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_1, u_5} 𝕜 (G i)
V : (i : ι) → LinearIsometry.{u_1, u_1, u_5, u_2} (RingHom.id 𝕜) (G i) E
hV : OrthogonalFamily 𝕜 G V
inst_5 : Fintype ι
l : (i : ι) → G i
i : ι
v : G i
i₁ :
  inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) (∑ j : ι, (V j : (a : G j) → E) (l j) : E) =
    ∑ j : ι, inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E)
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) (∑ j : ι, (V j : (a : G j) → E) (l j) : E) = ⟪v, l i⟫
have i₂ : (∑ j : ι,
    if i = j then inner.{u_1, u_2} 𝕜 (E := E) ((V i : (a : G i) → E) v : E) ((V j : (a : G j) → E) (l j) : E) else 0) =
  ⟪v, l i⟫
Tactic: classical
  calc
    ⟪V i v, ∑ j : ι, V j (l j)⟫ = ∑ j : ι, ⟪V i v, V j (l j)⟫ := by rw [inner_sum]
    _ = ∑ j, ite (i = j) ⟪V i v, V j (l j)⟫ 0 :=
      (congr_arg (Finset.sum Finset.univ) <| funext fun j => hV.eq_ite v (l j))
    _ = ⟪v, l i⟫ := by
      simp only [Finset.sum_ite_eq, Finset.mem_univ, (V i).inner_map_map, if_true]