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
r : ℝ
z : K
rw :
  (↑((re : (a : K) → ℝ) (r • z)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)
rw₁ :
  (↑((re : (a : K) → ℝ) (r • z)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
⊢ (starRingEnd K : (a : K) → K) (r • z) = HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)
have rw₂ : (↑(HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
  r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
Tactic: rw [conj_eq_re_sub_im, conj_eq_re_sub_im, smul_re, smul_im, ofReal_mul, ofReal_mul,
    real_smul_eq_coe_mul r (_ - _), mul_sub, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
z : K
rw :
  (↑((re : (a : K) → ℝ) (r • z)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)
rw₁ :
  (↑((re : (a : K) → ℝ) (r • z)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₂ :
  (↑(HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
⊢ (starRingEnd K : (a : K) → K) (r • z) = HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)
have rw₃ : (↑(HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)) : K) -
    HMul.hMul (α := K) (↑(HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)) : K) I =
  r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
Tactic: rw [conj_eq_re_sub_im, conj_eq_re_sub_im, smul_re, smul_im, ofReal_mul, ofReal_mul,
    real_smul_eq_coe_mul r (_ - _), mul_sub, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
z : K
rw :
  (↑((re : (a : K) → ℝ) (r • z)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)
rw₁ :
  (↑((re : (a : K) → ℝ) (r • z)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₂ :
  (↑(HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₃ :
  (↑(HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)) : K) -
      HMul.hMul (α := K) (↑(HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
⊢ (starRingEnd K : (a : K) → K) (r • z) = HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)
have rw₄ : HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
    HMul.hMul (α := K) (↑(HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)) : K) I =
  r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
Tactic: rw [conj_eq_re_sub_im, conj_eq_re_sub_im, smul_re, smul_im, ofReal_mul, ofReal_mul,
    real_smul_eq_coe_mul r (_ - _), mul_sub, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
z : K
rw :
  (↑((re : (a : K) → ℝ) (r • z)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)
rw₁ :
  (↑((re : (a : K) → ℝ) (r • z)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₂ :
  (↑(HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₃ :
  (↑(HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)) : K) -
      HMul.hMul (α := K) (↑(HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₄ :
  HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
      HMul.hMul (α := K) (↑(HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
⊢ (starRingEnd K : (a : K) → K) (r • z) = HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)
have rw₅ : HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
    HMul.hMul (α := K) (↑r : K) (↑((im : (a : K) → ℝ) z) : K) * I =
  r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
Tactic: rw [conj_eq_re_sub_im, conj_eq_re_sub_im, smul_re, smul_im, ofReal_mul, ofReal_mul,
    real_smul_eq_coe_mul r (_ - _), mul_sub, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
z : K
rw :
  (↑((re : (a : K) → ℝ) (r • z)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)
rw₁ :
  (↑((re : (a : K) → ℝ) (r • z)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₂ :
  (↑(HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₃ :
  (↑(HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)) : K) -
      HMul.hMul (α := K) (↑(HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₄ :
  HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
      HMul.hMul (α := K) (↑(HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₅ :
  HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
      HMul.hMul (α := K) (↑r : K) (↑((im : (a : K) → ℝ) z) : K) * I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
⊢ (starRingEnd K : (a : K) → K) (r • z) = HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)
have rw₆ : HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
    HMul.hMul (α := K) (↑r : K) (↑((im : (a : K) → ℝ) z) : K) * I =
  (↑r : K) * ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
Tactic: rw [conj_eq_re_sub_im, conj_eq_re_sub_im, smul_re, smul_im, ofReal_mul, ofReal_mul,
    real_smul_eq_coe_mul r (_ - _), mul_sub, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
z : K
rw :
  (↑((re : (a : K) → ℝ) (r • z)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)
rw₁ :
  (↑((re : (a : K) → ℝ) (r • z)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₂ :
  (↑(HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₃ :
  (↑(HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)) : K) -
      HMul.hMul (α := K) (↑(HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₄ :
  HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
      HMul.hMul (α := K) (↑(HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₅ :
  HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
      HMul.hMul (α := K) (↑r : K) (↑((im : (a : K) → ℝ) z) : K) * I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₆ :
  HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
      HMul.hMul (α := K) (↑r : K) (↑((im : (a : K) → ℝ) z) : K) * I =
    (↑r : K) * ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
⊢ (starRingEnd K : (a : K) → K) (r • z) = HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)
have rw₇ : HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
    HMul.hMul (α := K) (↑r : K) (↑((im : (a : K) → ℝ) z) : K) * I =
  HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
    (↑r : K) * HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I
Tactic: rw [conj_eq_re_sub_im, conj_eq_re_sub_im, smul_re, smul_im, ofReal_mul, ofReal_mul,
    real_smul_eq_coe_mul r (_ - _), mul_sub, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
z : K
rw :
  (↑((re : (a : K) → ℝ) (r • z)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)
rw₁ :
  (↑((re : (a : K) → ℝ) (r • z)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₂ :
  (↑(HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) (r • z)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₃ :
  (↑(HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)) : K) -
      HMul.hMul (α := K) (↑(HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₄ :
  HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
      HMul.hMul (α := K) (↑(HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)) : K) I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₅ :
  HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
      HMul.hMul (α := K) (↑r : K) (↑((im : (a : K) → ℝ) z) : K) * I =
    r • ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₆ :
  HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
      HMul.hMul (α := K) (↑r : K) (↑((im : (a : K) → ℝ) z) : K) * I =
    (↑r : K) * ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₇ :
  HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
      HMul.hMul (α := K) (↑r : K) (↑((im : (a : K) → ℝ) z) : K) * I =
    HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
      (↑r : K) * HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I
⊢ (starRingEnd K : (a : K) → K) (r • z) = HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)
have rw₈ : HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
    (↑r : K) * HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I =
  HMul.hMul (α := K) (↑r : K) (↑((re : (a : K) → ℝ) z) : K) -
    (↑r : K) * HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I
Tactic: rw [conj_eq_re_sub_im, conj_eq_re_sub_im, smul_re, smul_im, ofReal_mul, ofReal_mul,
    real_smul_eq_coe_mul r (_ - _), mul_sub, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ HAdd.hAdd (β := K) z ((starRingEnd K : (a : K) → K) z : K) =
    (↑((re : (a : K) → ℝ) z) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I +
      ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
have rw : HAdd.hAdd (β := K) z ((starRingEnd K : (a : K) → K) z : K) =
  z + ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
Tactic: rw [re_add_im, conj_eq_re_sub_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  HAdd.hAdd (β := K) z ((starRingEnd K : (a : K) → K) z : K) =
    z + ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
⊢ HAdd.hAdd (β := K) z ((starRingEnd K : (a : K) → K) z : K) =
    (↑((re : (a : K) → ℝ) z) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I +
      ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
have rw₁ : z + ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I) =
  z + ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
Tactic: rw [re_add_im, conj_eq_re_sub_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (↑((re : (a : K) → ℝ) z) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I +
      ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I) =
    HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) z) : K)
have rw : HAdd.hAdd (α := K) (↑((re : (a : K) → ℝ) z) : K) (↑((re : (a : K) → ℝ) z) : K) =
  HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) z) : K)
Tactic: rw [add_add_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  HAdd.hAdd (α := K) (↑((re : (a : K) → ℝ) z) : K) (↑((re : (a : K) → ℝ) z) : K) =
    HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) z) : K)
⊢ (↑((re : (a : K) → ℝ) z) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I +
      ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I) =
    HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) z) : K)
have rw₁ : HAdd.hAdd (α := K) (↑((re : (a : K) → ℝ) z) : K) (↑((re : (a : K) → ℝ) z) : K) =
  HAdd.hAdd (α := K) (↑((re : (a : K) → ℝ) z) : K) (↑((re : (a : K) → ℝ) z) : K)
Tactic: rw [add_add_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (↑((re : (a : K) → ℝ) z) : K) = HAdd.hAdd (β := K) z ((starRingEnd K : (a : K) → K) z : K) / 2
have rw : (↑((re : (a : K) → ℝ) z) : K) = HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) z) : K) / 2
Tactic: rw [add_conj, mul_div_cancel_left₀ (re z : K) two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : (↑((re : (a : K) → ℝ) z) : K) = HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) z) : K) / 2
⊢ (↑((re : (a : K) → ℝ) z) : K) = HAdd.hAdd (β := K) z ((starRingEnd K : (a : K) → K) z : K) / 2
have rw₁ : Eq.{u_1 + 1} (α := K) (↑((re : (a : K) → ℝ) z) : K) (↑((re : (a : K) → ℝ) z) : K)
Tactic: rw [add_conj, mul_div_cancel_left₀ (re z : K) two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (↑((im : (a : K) → ℝ) z) : K) = I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
have rw : -(↑((im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
Tactic: rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
    neg_sub, mul_sub, neg_mul, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : -(↑((im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
⊢ (↑((im : (a : K) → ℝ) z) : K) = I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
have rw₁ : (↑(-(im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
Tactic: rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
    neg_sub, mul_sub, neg_mul, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : -(↑((im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₁ : (↑(-(im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
⊢ (↑((im : (a : K) → ℝ) z) : K) = I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
have rw₂ : (↑((re : (a : K) → ℝ) (I * z)) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
Tactic: rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
    neg_sub, mul_sub, neg_mul, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : -(↑((im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₁ : (↑(-(im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₂ : (↑((re : (a : K) → ℝ) (I * z)) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
⊢ (↑((im : (a : K) → ℝ) z) : K) = I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
have rw₃ : HAdd.hAdd (β := K) (I * z) ((starRingEnd K : (a : K) → K) (I * z) : K) / 2 =
  -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
Tactic: rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
    neg_sub, mul_sub, neg_mul, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : -(↑((im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₁ : (↑(-(im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₂ : (↑((re : (a : K) → ℝ) (I * z)) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₃ :
  HAdd.hAdd (β := K) (I * z) ((starRingEnd K : (a : K) → K) (I * z) : K) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
⊢ (↑((im : (a : K) → ℝ) z) : K) = I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
have rw₄ : (I * z + HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
  -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
Tactic: rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
    neg_sub, mul_sub, neg_mul, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : -(↑((im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₁ : (↑(-(im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₂ : (↑((re : (a : K) → ℝ) (I * z)) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₃ :
  HAdd.hAdd (β := K) (I * z) ((starRingEnd K : (a : K) → K) (I * z) : K) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₄ :
  (I * z + HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) I : K) ((starRingEnd K : (a : K) → K) z : K)) /
      2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
⊢ (↑((im : (a : K) → ℝ) z) : K) = I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
have rw₅ : (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
  -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
Tactic: rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
    neg_sub, mul_sub, neg_mul, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : -(↑((im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₁ : (↑(-(im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₂ : (↑((re : (a : K) → ℝ) (I * z)) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₃ :
  HAdd.hAdd (β := K) (I * z) ((starRingEnd K : (a : K) → K) (I * z) : K) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₄ :
  (I * z + HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) I : K) ((starRingEnd K : (a : K) → K) z : K)) /
      2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₅ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
⊢ (↑((im : (a : K) → ℝ) z) : K) = I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
have rw₆ : (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
  -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z) / 2
Tactic: rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
    neg_sub, mul_sub, neg_mul, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : -(↑((im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₁ : (↑(-(im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₂ : (↑((re : (a : K) → ℝ) (I * z)) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₃ :
  HAdd.hAdd (β := K) (I * z) ((starRingEnd K : (a : K) → K) (I * z) : K) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₄ :
  (I * z + HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) I : K) ((starRingEnd K : (a : K) → K) z : K)) /
      2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₅ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₆ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z) / 2
⊢ (↑((im : (a : K) → ℝ) z) : K) = I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
have rw₇ : (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
  I * -HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
Tactic: rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
    neg_sub, mul_sub, neg_mul, sub_eq_add_neg]