awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
H : LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x - y, x - y⟫ : ℝ) (0 : ℝ)
rwa : ∀ (H : x - y = 0), x = y
⊢ x = y
have rwa₁ : ∀ (H : x = y), x = y
Tactic: rwa [re_inner_self_nonpos, sub_eq_zero] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
⊢ x = y
have suffices : LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x - y, x - y⟫ : ℝ) (0 : ℝ)
Tactic: suffices H : re ⟪x - y, x - y⟫ ≤ 0 by rwa [re_inner_self_nonpos, sub_eq_zero] at H
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖y‖ 2
have ha : 0 ≤ ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
⊢ LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x - y, x - y⟫ : ℝ) (0 : ℝ)
have H₁ : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: have H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2 := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
H₁ : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖y‖ 2
⊢ (re : (a : 𝕜) → ℝ) ⟪y, x⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
have rwa : (re : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, y⟫ : 𝕜) = HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: rwa [← inner_conj_symm, conj_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
H₁ : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖y‖ 2
⊢ LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x - y, x - y⟫ : ℝ) (0 : ℝ)
have H₂ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: have H₂ : re ⟪y, x⟫ = ‖y‖ ^ 2 := by rwa [← inner_conj_symm, conj_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
H₁ : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖y‖ 2
H₂ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
⊢ LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x - y, x - y⟫ : ℝ) (0 : ℝ)
have simp : LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) (⟪x, x⟫ - ⟪y, x⟫ - (⟪x, y⟫ - ⟪y, y⟫)) : ℝ) (0 : ℝ)
Tactic: simp only [inner_sub_left, inner_sub_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
have rw : HPow.hPow (β := ℕ) ‖x + y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔ ‖y‖ • x = ‖x‖ • y
Tactic: rw [← pow_left_inj₀ (norm_nonneg _) (Left.add_nonneg (norm_nonneg _) (norm_nonneg _)) two_ne_zero,
    norm_add_sq (𝕜 := ℝ), add_pow_two, add_left_inj, add_right_inj, re_to_real, mul_assoc,
    mul_right_inj' two_ne_zero, ← inner_eq_norm_mul_iff_real]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : HPow.hPow (β := ℕ) ‖x + y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔ ‖y‖ • x = ‖x‖ • y
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
have rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔
  ‖y‖ • x = ‖x‖ • y
Tactic: rw [← pow_left_inj₀ (norm_nonneg _) (Left.add_nonneg (norm_nonneg _) (norm_nonneg _)) two_ne_zero,
    norm_add_sq (𝕜 := ℝ), add_pow_two, add_left_inj, add_right_inj, re_to_real, mul_assoc,
    mul_right_inj' two_ne_zero, ← inner_eq_norm_mul_iff_real]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : HPow.hPow (β := ℕ) ‖x + y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔ ‖y‖ • x = ‖x‖ • y
rw₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔
    ‖y‖ • x = ‖x‖ • y
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
have rw₂ : HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2 ↔
  ‖y‖ • x = ‖x‖ • y
Tactic: rw [← pow_left_inj₀ (norm_nonneg _) (Left.add_nonneg (norm_nonneg _) (norm_nonneg _)) two_ne_zero,
    norm_add_sq (𝕜 := ℝ), add_pow_two, add_left_inj, add_right_inj, re_to_real, mul_assoc,
    mul_right_inj' two_ne_zero, ← inner_eq_norm_mul_iff_real]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : HPow.hPow (β := ℕ) ‖x + y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔ ‖y‖ • x = ‖x‖ • y
rw₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔
    ‖y‖ • x = ‖x‖ • y
rw₂ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2 ↔
    ‖y‖ • x = ‖x‖ • y
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
have rw₃ : HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) =
    HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ ↔
  ‖y‖ • x = ‖x‖ • y
Tactic: rw [← pow_left_inj₀ (norm_nonneg _) (Left.add_nonneg (norm_nonneg _) (norm_nonneg _)) two_ne_zero,
    norm_add_sq (𝕜 := ℝ), add_pow_two, add_left_inj, add_right_inj, re_to_real, mul_assoc,
    mul_right_inj' two_ne_zero, ← inner_eq_norm_mul_iff_real]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : HPow.hPow (β := ℕ) ‖x + y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔ ‖y‖ • x = ‖x‖ • y
rw₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔
    ‖y‖ • x = ‖x‖ • y
rw₂ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2 ↔
    ‖y‖ • x = ‖x‖ • y
rw₃ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) =
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ ↔
    ‖y‖ • x = ‖x‖ • y
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
have rw₄ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) = 2 * ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
Tactic: rw [← pow_left_inj₀ (norm_nonneg _) (Left.add_nonneg (norm_nonneg _) (norm_nonneg _)) two_ne_zero,
    norm_add_sq (𝕜 := ℝ), add_pow_two, add_left_inj, add_right_inj, re_to_real, mul_assoc,
    mul_right_inj' two_ne_zero, ← inner_eq_norm_mul_iff_real]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : HPow.hPow (β := ℕ) ‖x + y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔ ‖y‖ • x = ‖x‖ • y
rw₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔
    ‖y‖ • x = ‖x‖ • y
rw₂ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2 ↔
    ‖y‖ • x = ‖x‖ • y
rw₃ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) =
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ ↔
    ‖y‖ • x = ‖x‖ • y
rw₄ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) = 2 * ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
have rw₅ : 2 * ⟪x, y⟫_ℝ = 2 * ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
Tactic: rw [← pow_left_inj₀ (norm_nonneg _) (Left.add_nonneg (norm_nonneg _) (norm_nonneg _)) two_ne_zero,
    norm_add_sq (𝕜 := ℝ), add_pow_two, add_left_inj, add_right_inj, re_to_real, mul_assoc,
    mul_right_inj' two_ne_zero, ← inner_eq_norm_mul_iff_real]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : HPow.hPow (β := ℕ) ‖x + y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔ ‖y‖ • x = ‖x‖ • y
rw₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔
    ‖y‖ • x = ‖x‖ • y
rw₂ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2 ↔
    ‖y‖ • x = ‖x‖ • y
rw₃ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) =
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ ↔
    ‖y‖ • x = ‖x‖ • y
rw₄ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) = 2 * ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
rw₅ : 2 * ⟪x, y⟫_ℝ = 2 * ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
have rw₆ : 2 * ⟪x, y⟫_ℝ = 2 * (‖x‖ * ‖y‖) ↔ ‖y‖ • x = ‖x‖ • y
Tactic: rw [← pow_left_inj₀ (norm_nonneg _) (Left.add_nonneg (norm_nonneg _) (norm_nonneg _)) two_ne_zero,
    norm_add_sq (𝕜 := ℝ), add_pow_two, add_left_inj, add_right_inj, re_to_real, mul_assoc,
    mul_right_inj' two_ne_zero, ← inner_eq_norm_mul_iff_real]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : HPow.hPow (β := ℕ) ‖x + y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔ ‖y‖ • x = ‖x‖ • y
rw₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔
    ‖y‖ • x = ‖x‖ • y
rw₂ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2 ↔
    ‖y‖ • x = ‖x‖ • y
rw₃ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) =
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ ↔
    ‖y‖ • x = ‖x‖ • y
rw₄ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) = 2 * ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
rw₅ : 2 * ⟪x, y⟫_ℝ = 2 * ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
rw₆ : 2 * ⟪x, y⟫_ℝ = 2 * (‖x‖ * ‖y‖) ↔ ‖y‖ • x = ‖x‖ • y
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
have rw₇ : ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
Tactic: rw [← pow_left_inj₀ (norm_nonneg _) (Left.add_nonneg (norm_nonneg _) (norm_nonneg _)) two_ne_zero,
    norm_add_sq (𝕜 := ℝ), add_pow_two, add_left_inj, add_right_inj, re_to_real, mul_assoc,
    mul_right_inj' two_ne_zero, ← inner_eq_norm_mul_iff_real]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : HPow.hPow (β := ℕ) ‖x + y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔ ‖y‖ • x = ‖x‖ • y
rw₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔
    ‖y‖ • x = ‖x‖ • y
rw₂ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2 ↔
    ‖y‖ • x = ‖x‖ • y
rw₃ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) =
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ ↔
    ‖y‖ • x = ‖x‖ • y
rw₄ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) = 2 * ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
rw₅ : 2 * ⟪x, y⟫_ℝ = 2 * ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
rw₆ : 2 * ⟪x, y⟫_ℝ = 2 * (‖x‖ * ‖y‖) ↔ ‖y‖ • x = ‖x‖ • y
rw₇ : ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
have rw₈ : ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖
Tactic: rw [← pow_left_inj₀ (norm_nonneg _) (Left.add_nonneg (norm_nonneg _) (norm_nonneg _)) two_ne_zero,
    norm_add_sq (𝕜 := ℝ), add_pow_two, add_left_inj, add_right_inj, re_to_real, mul_assoc,
    mul_right_inj' two_ne_zero, ← inner_eq_norm_mul_iff_real]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F_1 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 G
F : Type u_5
inst_5 : FunLike F G E
inst_6 : LinearMapClass F 𝕜 G E
f : F
this_1 : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G E f
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G E f
x y z : G
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) (x + y) : E) ((f : (a : G) → E) z : E) =
    inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) z : E) +
      inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) y : E) ((f : (a : G) → E) z : E)
have rw : ⟪HAdd.hAdd (α := E) (β := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) y : E), (f : (a : G) → E) z⟫_𝕜 =
  inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) z : E) +
    inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) y : E) ((f : (a : G) → E) z : E)
Tactic: rw [map_add, inner_add_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F_1 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 G
F : Type u_5
inst_5 : FunLike F G E
inst_6 : LinearMapClass F 𝕜 G E
f : F
this_1 : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G E f
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G E f
x y z : G
rw :
  ⟪HAdd.hAdd (α := E) (β := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) y : E), (f : (a : G) → E) z⟫_𝕜 =
    inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) z : E) +
      inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) y : E) ((f : (a : G) → E) z : E)
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) (x + y) : E) ((f : (a : G) → E) z : E) =
    inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) z : E) +
      inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) y : E) ((f : (a : G) → E) z : E)
have rw₁ : inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) z : E) +
    inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) y : E) ((f : (a : G) → E) z : E) =
  inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) z : E) +
    inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) y : E) ((f : (a : G) → E) z : E)
Tactic: rw [map_add, inner_add_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F_1 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 G
F : Type u_5
inst_5 : FunLike F G E
inst_6 : LinearMapClass F 𝕜 G E
f : F
this_1 : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G E f
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G E f
x y : G
r : 𝕜
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) (r • x) : E) ((f : (a : G) → E) y : E) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
      (inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) y : E))
have rw : ⟪HSMul.hSMul (β := E) r ((f : (a : G) → E) x : E), (f : (a : G) → E) y⟫_𝕜 =
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
    (inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) y : E))
Tactic: rw [map_smul, inner_smul_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F_1 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 G
F : Type u_5
inst_5 : FunLike F G E
inst_6 : LinearMapClass F 𝕜 G E
f : F
this_1 : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G E f
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G E f
x y : G
r : 𝕜
rw :
  ⟪HSMul.hSMul (β := E) r ((f : (a : G) → E) x : E), (f : (a : G) → E) y⟫_𝕜 =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
      (inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) y : E))
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) (r • x) : E) ((f : (a : G) → E) y : E) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
      (inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) y : E))
have rw₁ : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
    (inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) y : E)) =
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
    (inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) y : E))
Tactic: rw [map_smul, inner_smul_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x : 𝕜
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (x * star x)
have rw : HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) x ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
Tactic: rw [star_def, mul_conj, ← ofReal_pow, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x : 𝕜
rw : HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) x ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (x * star x)
have rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2)
Tactic: rw [star_def, mul_conj, ← ofReal_pow, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x : 𝕜
rw : HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) x ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (x * star x)
have rw₂ : HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : 𝕜)
Tactic: rw [star_def, mul_conj, ← ofReal_pow, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x : 𝕜
rw : HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) x ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2)
rw₂ : HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : 𝕜)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (x * star x)
have rw₃ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rw [star_def, mul_conj, ← ofReal_pow, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y : 𝕜
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x * star y) = y * star x
have rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HMul.hMul (β := 𝕜) x ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜)) =
  HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
Tactic: rw [star_def, map_mul, starRingEnd_self_apply, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y : 𝕜
rw :
  (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HMul.hMul (β := 𝕜) x ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜)) =
    HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x * star y) = y * star x
have rw₁ : HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) : 𝕜) =
  HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
Tactic: rw [star_def, map_mul, starRingEnd_self_apply, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y : 𝕜
rw :
  (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HMul.hMul (β := 𝕜) x ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜)) =
    HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
rw₁ :
  HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) : 𝕜) =
    HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x * star y) = y * star x
have rw₂ : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) y = HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
Tactic: rw [star_def, map_mul, starRingEnd_self_apply, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y : 𝕜
rw :
  (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HMul.hMul (β := 𝕜) x ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜)) =
    HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
rw₁ :
  HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) : 𝕜) =
    HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
rw₂ :
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) y =
    HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x * star y) = y * star x
have rw₃ : HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) = HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
Tactic: rw [star_def, map_mul, starRingEnd_self_apply, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y z : 𝕜
⊢ z * star (x + y) = z * star x + z * star y
have rw : HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x + y) : 𝕜) =
  HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) +
    HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜)
Tactic: rw [star_def, map_add, mul_add]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y z : 𝕜
rw :
  HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x + y) : 𝕜) =
    HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) +
      HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜)
⊢ z * star (x + y) = z * star x + z * star y
have rw₁ : z * HAdd.hAdd (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) =
  HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) +
    HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜)
Tactic: rw [star_def, map_add, mul_add]