awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
⊢ normSq.{u_1, u_3} (𝕜 := 𝕜) x * HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 =
    HPow.hPow (β := ℕ) t 2 * normSq.{u_1, u_3} (𝕜 := 𝕜) (⟪x, y⟫ • x)
have h : HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (HPow.hPow (β := ℕ) t 2) * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 =
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) t 2)
    ((re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 * ⟪x, x⟫) : ℝ)
Tactic: rw [normSq, normSq, inner_smul_right, inner_smul_left, ← mul_assoc _ _ ⟪x, x⟫,
        mul_conj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
⊢ HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (HPow.hPow (β := ℕ) t 2) * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 =
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) t 2)
      ((re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 * ⟪x, x⟫) : ℝ)
have h : HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (HPow.hPow (β := ℕ) t 2) * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 =
  HPow.hPow (β := ℕ) t 2 * HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
Tactic: rw [← ofReal_pow, re_ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
⊢ 2 * ‖⟪x, y⟫‖ * t = HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪⟪x, y⟫ • x, y⟫ : ℝ) * (t / ‖⟪x, y⟫‖)
have h : HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 * t = HMul.hMul (β := ℝ) t ((re : (a : 𝕜) → ℝ) ⟪⟪x, y⟫ • x, y⟫ : ℝ)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
⊢ HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 * t = HMul.hMul (β := ℝ) t ((re : (a : 𝕜) → ℝ) ⟪⟪x, y⟫ • x, y⟫ : ℝ)
have h : HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 * t = t * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2
Tactic: rw [inner_smul_left, mul_comm _ ⟪x, y⟫_𝕜, mul_conj, ← ofReal_pow, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = ‖x‖ * ‖x‖
have rw : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) * √((re : (a : 𝕜) → ℝ) ⟪x, x⟫)
Tactic: rw [norm_eq_sqrt_re_inner, ← sqrt_mul inner_self_nonneg, sqrt_mul_self inner_self_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
rw : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) * √((re : (a : 𝕜) → ℝ) ⟪x, x⟫)
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = ‖x‖ * ‖x‖
have rw₁ : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ =
  √(HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ))
Tactic: rw [norm_eq_sqrt_re_inner, ← sqrt_mul inner_self_nonneg, sqrt_mul_self inner_self_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
rw : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) * √((re : (a : 𝕜) → ℝ) ⟪x, x⟫)
rw₁ :
  (re : (a : 𝕜) → ℝ) ⟪x, x⟫ =
    √(HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ))
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = ‖x‖ * ‖x‖
have rw₂ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
Tactic: rw [norm_eq_sqrt_re_inner, ← sqrt_mul inner_self_nonneg, sqrt_mul_self inner_self_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖ = ‖⟪x, y⟫‖ * ‖⟪y, x⟫‖
have rw : ‖⟪y, x⟫‖ * ‖⟪y, x⟫‖ = ‖⟪y, x⟫‖ * ‖⟪y, x⟫‖
Tactic: rw [norm_inner_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)
have simp : ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)
Tactic: simp only [inner_self_eq_norm_mul_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ √((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫) ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) + √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)
have h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
Tactic: have h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖ := norm_inner_le_norm _ _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
⊢ √((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫) ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) + √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)
have h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
Tactic: have h₂ : re ⟪x, y⟫ ≤ ‖⟪x, y⟫‖ := re_le_norm _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
⊢ √((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫) ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) + √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)
have h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
Tactic: have h₃ : re ⟪x, y⟫ ≤ ‖x‖ * ‖y‖ := h₂.trans h₁
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
⊢ (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
have rwa : (re : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, y⟫ : 𝕜) ≤ ‖x‖ * ‖y‖
Tactic: rwa [← inner_conj_symm, conj_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
⊢ √((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫) ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) + √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)
have h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
Tactic: have h₄ : re ⟪y, x⟫ ≤ ‖x‖ * ‖y‖ := by rwa [← inner_conj_symm, conj_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
⊢ ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖)
have simp : HAdd.hAdd (β := ℝ)
    (HAdd.hAdd (β := ℝ) (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
    ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) ≤
  HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
    HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
Tactic: simp only [← inner_self_eq_norm_mul_norm, inner_add_add_self, mul_add, mul_comm, map_add]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
⊢ HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ) (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) ≤
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
      HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
have linarith : HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
      HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) <
    HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ) (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) →
  ‖⟪x, y⟫‖ - ‖x‖ * ‖y‖ + HSub.hSub (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) ‖⟪x, y⟫‖ +
        HSub.hSub (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) (‖x‖ * ‖y‖) +
      (HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
          HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) -
        HAdd.hAdd (β := ℝ)
          (HAdd.hAdd (β := ℝ)
            (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
            ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
          ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
⊢ √((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫) ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) + √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)
have this : ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖)
Tactic: have : ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖) := by
          simp only [← inner_self_eq_norm_mul_norm, inner_add_add_self, mul_add, mul_comm, map_add]
          linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
r : 𝕜
x : F
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
have rw : √((re : (a : 𝕜) → ℝ) (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) r * ⟪x, x⟫)) ≤ ‖r‖ * ‖x‖
Tactic: rw [norm_eq_sqrt_re_inner, inner_smul_left, inner_smul_right, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
r : 𝕜
x : F
⊢ √((re : (a : 𝕜) → ℝ) (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) r * ⟪x, x⟫)) ≤ ‖r‖ * ‖x‖
have rw : √(HPow.hPow (β := ℕ) ‖r‖ 2) * √(normSq.{u_1, u_3} (𝕜 := 𝕜) x) ≤ ‖r‖ * ‖x‖
Tactic: rw [RCLike.conj_mul, ← ofReal_pow, re_ofReal_mul, sqrt_mul, ← ofReal_normSq_eq_inner_self,
      ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
r : 𝕜
x : F
rw : √(HPow.hPow (β := ℕ) ‖r‖ 2) * √(normSq.{u_1, u_3} (𝕜 := 𝕜) x) ≤ ‖r‖ * ‖x‖
⊢ √((re : (a : 𝕜) → ℝ) (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) r * ⟪x, x⟫)) ≤ ‖r‖ * ‖x‖
have hx : 0 ≤ HPow.hPow (β := ℕ) ‖r‖ 2
Tactic: rw [RCLike.conj_mul, ← ofReal_pow, re_ofReal_mul, sqrt_mul, ← ofReal_normSq_eq_inner_self,
      ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
x y : F
⊢ √((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫) ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) + √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)
have h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
Tactic: have h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖ := norm_inner_le_norm _ _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
⊢ √((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫) ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) + √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)
have h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
Tactic: have h₂ : re ⟪x, y⟫ ≤ ‖⟪x, y⟫‖ := re_le_norm _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
⊢ √((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫) ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) + √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)
have h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
Tactic: have h₃ : re ⟪x, y⟫ ≤ ‖x‖ * ‖y‖ := h₂.trans h₁
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
⊢ (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
have rwa : (re : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, y⟫ : 𝕜) ≤ ‖x‖ * ‖y‖
Tactic: rwa [← inner_conj_symm, conj_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
⊢ √((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫) ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) + √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)
have h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
Tactic: have h₄ : re ⟪y, x⟫ ≤ ‖x‖ * ‖y‖ := by rwa [← inner_conj_symm, conj_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
⊢ ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖)
have simp : HAdd.hAdd (β := ℝ)
    (HAdd.hAdd (β := ℝ) (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
    ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) ≤
  HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
    HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
Tactic: simp only [← inner_self_eq_norm_mul_norm, inner_add_add_self, mul_add, mul_comm, map_add]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
⊢ HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ) (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) ≤
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
      HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
have linarith : HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
      HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) <
    HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ) (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) →
  ‖⟪x, y⟫‖ - ‖x‖ * ‖y‖ + HSub.hSub (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) ‖⟪x, y⟫‖ +
        HSub.hSub (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) (‖x‖ * ‖y‖) +
      (HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
          HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) -
        HAdd.hAdd (β := ℝ)
          (HAdd.hAdd (β := ℝ)
            (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
            ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
          ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
⊢ √((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫) ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) + √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)
have this : ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖)
Tactic: have : ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖) := by
          simp only [← inner_self_eq_norm_mul_norm, inner_add_add_self, mul_add, mul_comm, map_add]
          linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : WithSeminorms.{u_1, u_3, 0} (𝕜 := 𝕜) (E := F) (ι := Fin 1) fun (i : Fin 1) ↦ p
⊢ tF = UniformSpace.toTopologicalSpace
have rw : Eq.{u_3 + 1} (α := TopologicalSpace F) (⨅ (i : Fin 1), UniformSpace.toTopologicalSpace) UniformSpace.toTopologicalSpace
Tactic: rw [(SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _).1 this]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
⊢ tF = UniformSpace.toTopologicalSpace
have suffices : WithSeminorms.{u_1, u_3, 0} (𝕜 := 𝕜) (E := F) (ι := Fin 1) fun (i : Fin 1) ↦ p
Tactic: suffices WithSeminorms (fun (i : Fin 1) ↦ p) by
    rw [(SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _).1 this]
    simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
⊢ p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
have h₁ : ∀ (v : F),
  v ∈ p.ball 0 1 ↔ Membership.mem (γ := Set F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)} v
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
⊢ v ∈ p.ball 0 1 ↔ Membership.mem (γ := Set F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)} v
have h₁ : ‖v‖ < 1 ↔ LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)
Tactic: simp only [ball_normSeminorm, Metric.mem_ball, dist_eq_norm, sub_zero, Set.mem_setOf_eq, p]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
⊢ ‖v‖ < 1 ↔ LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)
have h₁ : √((re : (a : 𝕜) → ℝ) ⟪v, v⟫) < 1 ↔ LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)
Tactic: change √(re (cd.inner v v)) < 1 ↔ re (cd.inner v v) < 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
| √((re : (a : 𝕜) → ℝ) ⟪v, v⟫) < 1
have rw : √((re : (a : 𝕜) → ℝ) ⟪v, v⟫) < √1
Tactic: rw [show (1 : ℝ) = √1 by simp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
⊢ √((re : (a : 𝕜) → ℝ) ⟪v, v⟫) < 1 ↔ LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)
have h₁ : √((re : (a : 𝕜) → ℝ) ⟪v, v⟫) < √1 ↔ LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)
Tactic: conv_lhs => rw [show (1 : ℝ) = √1 by simp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
⊢ √((re : (a : 𝕜) → ℝ) ⟪v, v⟫) < √1 ↔ LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)
have h₁ : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ)
Tactic: rw [sqrt_lt_sqrt_iff]