awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
inst_1 : n.AtLeastTwo
z : K
rw :
  (im : (a : K) → ℝ) ((↑(OfNat.ofNat n) : K) * z) =
    HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((im : (a : K) → ℝ) z : ℝ)
⊢ (im : (a : K) → ℝ) (OfNat.ofNat n * z) = HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((im : (a : K) → ℝ) z : ℝ)
have rw₁ : HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((im : (a : K) → ℝ) z : ℝ) =
  HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((im : (a : K) → ℝ) z : ℝ)
Tactic: rw [← ofReal_ofNat, im_ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
n : ℤ
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (↑n : K) : ℝ) ((↑n : ℝ) : ℝ)
have rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(↑n : ℝ) : K) : ℝ) ((↑n : ℝ) : ℝ)
Tactic: rw [← ofReal_intCast, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
n : ℤ
rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(↑n : ℝ) : K) : ℝ) ((↑n : ℝ) : ℝ)
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (↑n : K) : ℝ) ((↑n : ℝ) : ℝ)
have rw₁ : Eq (α := ℝ) (↑n : ℝ) (↑n : ℝ)
Tactic: rw [← ofReal_intCast, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
n : ℤ
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑n : K) : ℝ) (0 : ℝ)
have rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑(↑n : ℝ) : K) : ℝ) (0 : ℝ)
Tactic: rw [← ofReal_intCast, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
n : ℤ
rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑(↑n : ℝ) : K) : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑n : K) : ℝ) (0 : ℝ)
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← ofReal_intCast, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
q : ℚ≥0
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (↑q : K) : ℝ) ((↑q : ℝ) : ℝ)
have rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(↑q : ℝ) : K) : ℝ) ((↑q : ℝ) : ℝ)
Tactic: rw [← ofReal_nnratCast, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
q : ℚ≥0
rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(↑q : ℝ) : K) : ℝ) ((↑q : ℝ) : ℝ)
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (↑q : K) : ℝ) ((↑q : ℝ) : ℝ)
have rw₁ : Eq (α := ℝ) (↑q : ℝ) (↑q : ℝ)
Tactic: rw [← ofReal_nnratCast, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
q : ℚ≥0
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑q : K) : ℝ) (0 : ℝ)
have rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑(↑q : ℝ) : K) : ℝ) (0 : ℝ)
Tactic: rw [← ofReal_nnratCast, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
q : ℚ≥0
rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑(↑q : ℝ) : K) : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑q : K) : ℝ) (0 : ℝ)
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← ofReal_nnratCast, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
q : ℚ
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (↑q : K) : ℝ) ((↑q : ℝ) : ℝ)
have rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(↑q : ℝ) : K) : ℝ) ((↑q : ℝ) : ℝ)
Tactic: rw [← ofReal_ratCast, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
q : ℚ
rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(↑q : ℝ) : K) : ℝ) ((↑q : ℝ) : ℝ)
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (↑q : K) : ℝ) ((↑q : ℝ) : ℝ)
have rw₁ : Eq (α := ℝ) (↑q : ℝ) (↑q : ℝ)
Tactic: rw [← ofReal_ratCast, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
q : ℚ
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑q : K) : ℝ) (0 : ℝ)
have rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑(↑q : ℝ) : K) : ℝ) (0 : ℝ)
Tactic: rw [← ofReal_ratCast, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
q : ℚ
rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑(↑q : ℝ) : K) : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑q : K) : ℝ) (0 : ℝ)
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← ofReal_ratCast, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
m : ℕ
s : Bool
e : ℕ
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (ofScientific m s e) : ℝ) (ofScientific m s e : ℝ)
have rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(ofScientific m s e) : K) : ℝ) (ofScientific m s e : ℝ)
Tactic: rw [← ofReal_ofScientific, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
m : ℕ
s : Bool
e : ℕ
rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(ofScientific m s e) : K) : ℝ) (ofScientific m s e : ℝ)
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (ofScientific m s e) : ℝ) (ofScientific m s e : ℝ)
have rw₁ : Eq (α := ℝ) (ofScientific m s e) (ofScientific m s e)
Tactic: rw [← ofReal_ofScientific, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
m : ℕ
s : Bool
e : ℕ
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (ofScientific m s e) : ℝ) (0 : ℝ)
have rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑(ofScientific m s e) : K) : ℝ) (0 : ℝ)
Tactic: rw [← ofReal_ofScientific, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
m : ℕ
s : Bool
e : ℕ
rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑(ofScientific m s e) : K) : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (ofScientific m s e) : ℝ) (0 : ℝ)
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← ofReal_ofScientific, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
⊢ norm.{u_1} (E := K) (↑n : K) = (↑n : ℝ)
have rw : norm.{u_1} (E := K) (↑(↑n : ℝ) : K) = (↑n : ℝ)
Tactic: rw [← ofReal_natCast]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
q : ℚ≥0
⊢ norm.{u_1} (E := K) (↑q : K) = (↑q : ℝ)
have rw : norm.{u_1} (E := K) (↑(↑q : ℝ) : K) = (↑q : ℝ)
Tactic: rw [← ofReal_nnratCast]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
q : ℚ≥0
⊢ nnnorm.{u_1} (E := K) (↑q : K) = (↑q : NNReal)
have simp : NNReal.mk (↑q : ℝ) sorry = (↑q : NNReal)
Tactic: simp [nnnorm]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ ‖z‖ * ‖z‖ = (normSq : (a : K) → ℝ) z
have rw : ‖z‖ * ‖z‖ = HPow.hPow (β := ℕ) ‖z‖ 2
Tactic: rw [normSq_eq_def', sq]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : ‖z‖ * ‖z‖ = HPow.hPow (β := ℕ) ‖z‖ 2
⊢ ‖z‖ * ‖z‖ = (normSq : (a : K) → ℝ) z
have rw₁ : ‖z‖ * ‖z‖ = ‖z‖ * ‖z‖
Tactic: rw [normSq_eq_def', sq]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ |(re : (a : K) → ℝ) z| ≤ ‖z‖
have rw : HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) z : ℝ) ≤ (normSq : (a : K) → ℝ) z
Tactic: rw [mul_self_le_mul_self_iff (abs_nonneg _) (norm_nonneg _), abs_mul_abs_self, mul_self_norm]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ |(im : (a : K) → ℝ) z| ≤ ‖z‖
have rw : HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) z : ℝ) ≤ (normSq : (a : K) → ℝ) z
Tactic: rw [mul_self_le_mul_self_iff (abs_nonneg _) (norm_nonneg _), abs_mul_abs_self, mul_self_norm]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
a : K
h : ‖a‖ ≤ (re : (a : K) → ℝ) a
⊢ (↑((re : (a : K) → ℝ) a) : K) = a
have rw : (starRingEnd K : (a : K) → K) a = a
Tactic: rw [← conj_eq_iff_re, conj_eq_iff_im, im_eq_zero_of_le h]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
a : K
h : ‖a‖ ≤ (re : (a : K) → ℝ) a
rw : (starRingEnd K : (a : K) → K) a = a
⊢ (↑((re : (a : K) → ℝ) a) : K) = a
have rw₁ : Eq (α := ℝ) ((im : (a : K) → ℝ) a : ℝ) (0 : ℝ)
Tactic: rw [← conj_eq_iff_re, conj_eq_iff_im, im_eq_zero_of_le h]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
a : K
h : ‖a‖ ≤ (re : (a : K) → ℝ) a
rw : (starRingEnd K : (a : K) → K) a = a
rw₁ : Eq (α := ℝ) ((im : (a : K) → ℝ) a : ℝ) (0 : ℝ)
⊢ (↑((re : (a : K) → ℝ) a) : K) = a
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [← conj_eq_iff_re, conj_eq_iff_im, im_eq_zero_of_le h]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ |HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ‖z‖| ≤ 1
have rw : HDiv.hDiv (α := ℝ) (|(re : (a : K) → ℝ) z| : ℝ) ‖z‖ ≤ 1
Tactic: rw [abs_div, abs_norm]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ |HDiv.hDiv (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ‖z‖| ≤ 1
have rw : HDiv.hDiv (α := ℝ) (|(im : (a : K) → ℝ) z| : ℝ) ‖z‖ ≤ 1
Tactic: rw [abs_div, abs_norm]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
hI : Ne.{u_1 + 1} (α := K) I 0
⊢ norm.{u_1} (E := K) I = 1
have rw : norm.{u_1} (E := K) I * norm.{u_1} (E := K) I = HMul.hMul (α := ℝ) 1 1
Tactic: rw [← mul_self_inj_of_nonneg (norm_nonneg I) zero_le_one, one_mul, ← norm_mul,
    I_mul_I_of_nonzero hI, norm_neg, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
hI : Ne.{u_1 + 1} (α := K) I 0
rw : norm.{u_1} (E := K) I * norm.{u_1} (E := K) I = HMul.hMul (α := ℝ) 1 1
⊢ norm.{u_1} (E := K) I = 1
have rw₁ : norm.{u_1} (E := K) I * norm.{u_1} (E := K) I = 1
Tactic: rw [← mul_self_inj_of_nonneg (norm_nonneg I) zero_le_one, one_mul, ← norm_mul,
    I_mul_I_of_nonzero hI, norm_neg, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
hI : Ne.{u_1 + 1} (α := K) I 0
rw : norm.{u_1} (E := K) I * norm.{u_1} (E := K) I = HMul.hMul (α := ℝ) 1 1
rw₁ : norm.{u_1} (E := K) I * norm.{u_1} (E := K) I = 1
⊢ norm.{u_1} (E := K) I = 1
have rw₂ : ‖HMul.hMul (α := K) I I‖ = 1
Tactic: rw [← mul_self_inj_of_nonneg (norm_nonneg I) zero_le_one, one_mul, ← norm_mul,
    I_mul_I_of_nonzero hI, norm_neg, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
hI : Ne.{u_1 + 1} (α := K) I 0
rw : norm.{u_1} (E := K) I * norm.{u_1} (E := K) I = HMul.hMul (α := ℝ) 1 1
rw₁ : norm.{u_1} (E := K) I * norm.{u_1} (E := K) I = 1
rw₂ : ‖HMul.hMul (α := K) I I‖ = 1
⊢ norm.{u_1} (E := K) I = 1
have rw₃ : norm.{u_1} (E := K) (-1) = 1
Tactic: rw [← mul_self_inj_of_nonneg (norm_nonneg I) zero_le_one, one_mul, ← norm_mul,
    I_mul_I_of_nonzero hI, norm_neg, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
hI : Ne.{u_1 + 1} (α := K) I 0
rw : norm.{u_1} (E := K) I * norm.{u_1} (E := K) I = HMul.hMul (α := ℝ) 1 1
rw₁ : norm.{u_1} (E := K) I * norm.{u_1} (E := K) I = 1
rw₂ : ‖HMul.hMul (α := K) I I‖ = 1
rw₃ : norm.{u_1} (E := K) (-1) = 1
⊢ norm.{u_1} (E := K) I = 1
have rw₄ : norm.{u_1} (E := K) 1 = 1
Tactic: rw [← mul_self_inj_of_nonneg (norm_nonneg I) zero_le_one, one_mul, ← norm_mul,
    I_mul_I_of_nonzero hI, norm_neg, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
hI : Ne.{u_1 + 1} (α := K) I 0
rw : norm.{u_1} (E := K) I * norm.{u_1} (E := K) I = HMul.hMul (α := ℝ) 1 1
rw₁ : norm.{u_1} (E := K) I * norm.{u_1} (E := K) I = 1
rw₂ : ‖HMul.hMul (α := K) I I‖ = 1
rw₃ : norm.{u_1} (E := K) (-1) = 1
rw₄ : norm.{u_1} (E := K) 1 = 1
⊢ norm.{u_1} (E := K) I = 1
have rw₅ : Eq (α := ℝ) 1 1
Tactic: rw [← mul_self_inj_of_nonneg (norm_nonneg I) zero_le_one, one_mul, ← norm_mul,
    I_mul_I_of_nonzero hI, norm_neg, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
⊢ (re : (a : K) → ℝ) (HMul.hMul (β := K) x ((starRingEnd K : (a : K) → K) x : K)) =
    ‖HMul.hMul (β := K) x ((starRingEnd K : (a : K) → K) x : K)‖
have rw : (re : (a : K) → ℝ) (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : K) = norm.{u_1} (E := K) (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : K)
Tactic: rw [mul_conj, ← ofReal_pow]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
⊢ HPow.hPow (β := ℕ) ‖HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)) : ℝ) 2
have rw : HPow.hPow (β := ℕ) ‖HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) x) : K)‖ 2 =
  HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) x) : K)) : ℝ) 2
Tactic: rw [add_conj, ← ofReal_ofNat, ← ofReal_mul, norm_ofReal, sq_abs, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
rw :
  HPow.hPow (β := ℕ) ‖HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) x) : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) x) : K)) : ℝ) 2
⊢ HPow.hPow (β := ℕ) ‖HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)) : ℝ) 2
have rw₁ : HPow.hPow (β := ℕ) ‖HMul.hMul (α := K) (↑2 : K) (↑((re : (a : K) → ℝ) x) : K)‖ 2 =
  HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HMul.hMul (α := K) (↑2 : K) (↑((re : (a : K) → ℝ) x) : K)) : ℝ) 2
Tactic: rw [add_conj, ← ofReal_ofNat, ← ofReal_mul, norm_ofReal, sq_abs, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
rw :
  HPow.hPow (β := ℕ) ‖HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) x) : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) x) : K)) : ℝ) 2
rw₁ :
  HPow.hPow (β := ℕ) ‖HMul.hMul (α := K) (↑2 : K) (↑((re : (a : K) → ℝ) x) : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HMul.hMul (α := K) (↑2 : K) (↑((re : (a : K) → ℝ) x) : K)) : ℝ) 2
⊢ HPow.hPow (β := ℕ) ‖HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)) : ℝ) 2
have rw₂ : HPow.hPow (β := ℕ) (norm.{u_1} (E := K) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K)) 2 =
  HPow.hPow (α := ℝ) (β := ℕ)
    ((re : (a : K) → ℝ) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K) : ℝ) 2
Tactic: rw [add_conj, ← ofReal_ofNat, ← ofReal_mul, norm_ofReal, sq_abs, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
rw :
  HPow.hPow (β := ℕ) ‖HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) x) : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) x) : K)) : ℝ) 2
rw₁ :
  HPow.hPow (β := ℕ) ‖HMul.hMul (α := K) (↑2 : K) (↑((re : (a : K) → ℝ) x) : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HMul.hMul (α := K) (↑2 : K) (↑((re : (a : K) → ℝ) x) : K)) : ℝ) 2
rw₂ :
  HPow.hPow (β := ℕ) (norm.{u_1} (E := K) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K)) 2 =
    HPow.hPow (α := ℝ) (β := ℕ)
      ((re : (a : K) → ℝ) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K) : ℝ) 2
⊢ HPow.hPow (β := ℕ) ‖HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)) : ℝ) 2
have rw₃ : HPow.hPow (β := ℕ) |HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)| 2 =
  HPow.hPow (α := ℝ) (β := ℕ)
    ((re : (a : K) → ℝ) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K) : ℝ) 2
Tactic: rw [add_conj, ← ofReal_ofNat, ← ofReal_mul, norm_ofReal, sq_abs, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
rw :
  HPow.hPow (β := ℕ) ‖HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) x) : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) x) : K)) : ℝ) 2
rw₁ :
  HPow.hPow (β := ℕ) ‖HMul.hMul (α := K) (↑2 : K) (↑((re : (a : K) → ℝ) x) : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HMul.hMul (α := K) (↑2 : K) (↑((re : (a : K) → ℝ) x) : K)) : ℝ) 2
rw₂ :
  HPow.hPow (β := ℕ) (norm.{u_1} (E := K) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K)) 2 =
    HPow.hPow (α := ℝ) (β := ℕ)
      ((re : (a : K) → ℝ) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K) : ℝ) 2
rw₃ :
  HPow.hPow (β := ℕ) |HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)| 2 =
    HPow.hPow (α := ℝ) (β := ℕ)
      ((re : (a : K) → ℝ) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K) : ℝ) 2
⊢ HPow.hPow (β := ℕ) ‖HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)) : ℝ) 2
have rw₄ : HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) 2 =
  HPow.hPow (α := ℝ) (β := ℕ)
    ((re : (a : K) → ℝ) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K) : ℝ) 2
Tactic: rw [add_conj, ← ofReal_ofNat, ← ofReal_mul, norm_ofReal, sq_abs, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
rw :
  HPow.hPow (β := ℕ) ‖HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) x) : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) x) : K)) : ℝ) 2
rw₁ :
  HPow.hPow (β := ℕ) ‖HMul.hMul (α := K) (↑2 : K) (↑((re : (a : K) → ℝ) x) : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HMul.hMul (α := K) (↑2 : K) (↑((re : (a : K) → ℝ) x) : K)) : ℝ) 2
rw₂ :
  HPow.hPow (β := ℕ) (norm.{u_1} (E := K) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K)) 2 =
    HPow.hPow (α := ℝ) (β := ℕ)
      ((re : (a : K) → ℝ) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K) : ℝ) 2
rw₃ :
  HPow.hPow (β := ℕ) |HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)| 2 =
    HPow.hPow (α := ℝ) (β := ℕ)
      ((re : (a : K) → ℝ) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K) : ℝ) 2
rw₄ :
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) 2 =
    HPow.hPow (α := ℝ) (β := ℕ)
      ((re : (a : K) → ℝ) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K) : ℝ) 2
⊢ HPow.hPow (β := ℕ) ‖HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)) : ℝ) 2
have rw₅ : HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) 2 =
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) 2
Tactic: rw [add_conj, ← ofReal_ofNat, ← ofReal_mul, norm_ofReal, sq_abs, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
⊢ HPow.hPow (β := ℕ) ‖HAdd.hAdd (α := K) ((starRingEnd K : (a : K) → K) x : K) x‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (α := K) ((starRingEnd K : (a : K) → K) x : K) x) : ℝ) 2
have rw : HPow.hPow (β := ℕ) ‖HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)‖ 2 =
  HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)) : ℝ) 2
Tactic: rw [add_comm, norm_sq_re_add_conj]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
rw :
  HPow.hPow (β := ℕ) ‖HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)) : ℝ) 2
⊢ HPow.hPow (β := ℕ) ‖HAdd.hAdd (α := K) ((starRingEnd K : (a : K) → K) x : K) x‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (α := K) ((starRingEnd K : (a : K) → K) x : K) x) : ℝ) 2
have rw₁ : HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)) : ℝ) 2 =
  HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)) : ℝ) 2
Tactic: rw [add_comm, norm_sq_re_add_conj]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : K
r : ℤ
x : K
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
have rw : ‖(↑r : K) * x‖ = ‖r‖ * ‖x‖
Tactic: rw [zsmul_eq_mul, norm_mul, ← ofReal_intCast, norm_ofReal, Int.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : K
r : ℤ
x : K
rw : ‖(↑r : K) * x‖ = ‖r‖ * ‖x‖
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
have rw₁ : norm.{u_1} (E := K) (↑r : K) * ‖x‖ = ‖r‖ * ‖x‖
Tactic: rw [zsmul_eq_mul, norm_mul, ← ofReal_intCast, norm_ofReal, Int.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : K
r : ℤ
x : K
rw : ‖(↑r : K) * x‖ = ‖r‖ * ‖x‖
rw₁ : norm.{u_1} (E := K) (↑r : K) * ‖x‖ = ‖r‖ * ‖x‖
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
have rw₂ : norm.{u_1} (E := K) (↑(↑r : ℝ) : K) * ‖x‖ = ‖r‖ * ‖x‖
Tactic: rw [zsmul_eq_mul, norm_mul, ← ofReal_intCast, norm_ofReal, Int.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : K
r : ℤ
x : K
rw : ‖(↑r : K) * x‖ = ‖r‖ * ‖x‖
rw₁ : norm.{u_1} (E := K) (↑r : K) * ‖x‖ = ‖r‖ * ‖x‖
rw₂ : norm.{u_1} (E := K) (↑(↑r : ℝ) : K) * ‖x‖ = ‖r‖ * ‖x‖
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
have rw₃ : |(↑r : ℝ)| * ‖x‖ = ‖r‖ * ‖x‖
Tactic: rw [zsmul_eq_mul, norm_mul, ← ofReal_intCast, norm_ofReal, Int.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : K
r : ℤ
x : K
rw : ‖(↑r : K) * x‖ = ‖r‖ * ‖x‖
rw₁ : norm.{u_1} (E := K) (↑r : K) * ‖x‖ = ‖r‖ * ‖x‖
rw₂ : norm.{u_1} (E := K) (↑(↑r : ℝ) : K) * ‖x‖ = ‖r‖ * ‖x‖
rw₃ : |(↑r : ℝ)| * ‖x‖ = ‖r‖ * ‖x‖
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
have rw₄ : |(↑r : ℝ)| * ‖x‖ = |(↑r : ℝ)| * ‖x‖
Tactic: rw [zsmul_eq_mul, norm_mul, ← ofReal_intCast, norm_ofReal, Int.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
inst_1 : NormedField E
inst_2 : CharZero E
inst_3 : NormedSpace K E
ι : Type u_3
s : Finset ι
f : ι → E
x : ℕ
x_1 : E
⊢ ‖HSMul.hSMul (α := ℚ≥0) (↑x : ℚ≥0)⁻¹ x_1‖ = HSMul.hSMul (α := ℚ≥0) (↑x : ℚ≥0)⁻¹ ‖x_1‖
have rw : HSMul.hSMul (α := ℚ≥0) (↑x : ℚ≥0)⁻¹ ‖x_1‖ = HSMul.hSMul (α := ℚ≥0) (↑x : ℚ≥0)⁻¹ ‖x_1‖
Tactic: rw [norm_nnqsmul K]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z w : K
⊢ z < w ↔
    LT.lt (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)
have simp_rw : (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)) ∧
    z ≠ w ↔
  (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
      Ne (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)
Tactic: simp_rw [lt_iff_le_and_ne, @RCLike.le_iff_re_im K]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z w : K
⊢ (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)) ∧
      z ≠ w ↔
    (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Ne (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)
have mp : (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)) ∧
    z ≠ w →
  (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
      Ne (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)
Tactic: constructor