awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
⊢ Eq.{u_1 + 1} (α := K) (↑x : K) 0 ↔ x = 0

Tactic:
algebraMap.coe_eq_zero_iff _ _ _

Premises used: algebraMap.coe_eq_zero_iff
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
⊢ Ne.{u_1 + 1} (α := K) (↑x : K) 0 ↔ x ≠ 0

Tactic:
ofReal_eq_zero.not

Premises used: Iff.not, RCLike.ofReal_eq_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r s : ℝ
⊢ (↑(r + s) : K) = HAdd.hAdd (α := K) (↑r : K) (↑s : K)

Tactic:
algebraMap.coe_add _ _

Premises used: algebraMap.coe_add
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
⊢ Eq.{u_1 + 1} (α := K) (↑(-r) : K) (-(↑r : K))

Tactic:
algebraMap.coe_neg r

Premises used: algebraMap.coe_neg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r s : ℝ
⊢ (↑(r - s) : K) = HSub.hSub (α := K) (↑r : K) (↑s : K)

Tactic:
map_sub (algebraMap ℝ K) r s

Premises used: Real, map_sub, Algebra.algebraMap
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
α : Type u_3
s : Finset α
f : α → ℝ
⊢ Eq.{u_1 + 1} (α := K) (↑(∑ i ∈ s, f i) : K) (∑ i ∈ s, (↑(f i) : K))

Tactic:
map_sum (algebraMap ℝ K) _ _

Premises used: Real, Algebra.algebraMap, map_sum
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
α : Type u_3
M : Type u_4
inst_1 : Zero M
f : α →₀ M
g : α → M → ℝ
⊢ Eq.{u_1 + 1} (α := K) (↑(f.sum fun (a : α) (b : M) ↦ g a b) : K) (f.sum fun (a : α) (b : M) ↦ (↑(g a b) : K))

Tactic:
map_finsuppSum (algebraMap ℝ K) f g

Premises used: Real, Algebra.algebraMap, map_finsuppSum
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r s : ℝ
⊢ (↑(r * s) : K) = HMul.hMul (α := K) (↑r : K) (↑s : K)

Tactic:
algebraMap.coe_mul _ _

Premises used: algebraMap.coe_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
n : ℕ
⊢ (↑(r ^ n) : K) = HPow.hPow (α := K) (↑r : K) n

Tactic:
map_pow (algebraMap ℝ K) r n

Premises used: Real, Algebra.algebraMap, map_pow
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
α : Type u_3
s : Finset α
f : α → ℝ
⊢ Eq.{u_1 + 1} (α := K) (↑(∏ i ∈ s, f i) : K) (∏ i ∈ s, (↑(f i) : K))

Tactic:
map_prod (algebraMap ℝ K) _ _

Premises used: Real, Algebra.algebraMap, map_prod
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
α : Type u_3
M : Type u_4
inst_1 : Zero M
f : α →₀ M
g : α → M → ℝ
⊢ Eq.{u_1 + 1} (α := K) (↑(f.prod fun (a : α) (b : M) ↦ g a b) : K) (f.prod fun (a : α) (b : M) ↦ (↑(g a b) : K))

Tactic:
map_finsuppProd _ f g

Premises used: map_finsuppProd
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r x : ℝ
⊢ HSMul.hSMul (β := K) r (↑x : K) = HMul.hMul (α := K) (↑r : K) (↑x : K)

Tactic:
real_smul_eq_coe_mul _ _

Premises used: RCLike.real_smul_eq_coe_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
z : K
⊢ (re : (a : K) → ℝ) ((↑r : K) * z) = HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)

Tactic:
simp only [mul_re, ofReal_im, zero_mul, ofReal_re, sub_zero]

Premises used: RCLike.ofReal_re, sub_zero, MulZeroClass.zero_mul, RCLike.ofReal_im, RCLike.mul_re
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
r : ℝ
rw : (re : (a : K) → ℝ) ((↑r : K) * z) = HMul.hMul (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r
rw₁ : HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ) = HMul.hMul (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r
rw₂ rw₃ : HMul.hMul (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r = HMul.hMul (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r
⊢ (re : (a : K) → ℝ) (z * (↑r : K)) = HMul.hMul (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r

Tactic:
rw [mul_comm, re_ofReal_mul, mul_comm]

Premises used: mul_comm, RCLike.re_ofReal_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
z : K
⊢ (im : (a : K) → ℝ) ((↑r : K) * z) = HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)

Tactic:
simp only [add_zero, ofReal_im, zero_mul, ofReal_re, mul_im]

Premises used: RCLike.ofReal_re, MulZeroClass.zero_mul, RCLike.ofReal_im, RCLike.mul_im, add_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
r : ℝ
rw : (im : (a : K) → ℝ) ((↑r : K) * z) = HMul.hMul (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) r
rw₁ : HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ) = HMul.hMul (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) r
rw₂ rw₃ : HMul.hMul (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) r = HMul.hMul (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) r
⊢ (im : (a : K) → ℝ) (z * (↑r : K)) = HMul.hMul (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) r

Tactic:
rw [mul_comm, im_ofReal_mul, mul_comm]

Premises used: mul_comm, RCLike.im_ofReal_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
z : K
rw : (re : (a : K) → ℝ) ((↑r : K) * z) = HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)
rw₁ rw₂ : HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ) = HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)
⊢ (re : (a : K) → ℝ) (r • z) = HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ)

Tactic:
rw [real_smul_eq_coe_mul, re_ofReal_mul]

Premises used: RCLike.re_ofReal_mul, RCLike.real_smul_eq_coe_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
z : K
rw : (im : (a : K) → ℝ) ((↑r : K) * z) = HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)
rw₁ rw₂ : HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ) = HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)
⊢ (im : (a : K) → ℝ) (r • z) = HMul.hMul (β := ℝ) r ((im : (a : K) → ℝ) z : ℝ)

Tactic:
rw [real_smul_eq_coe_mul, im_ofReal_mul]

Premises used: RCLike.im_ofReal_mul, RCLike.real_smul_eq_coe_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
⊢ norm.{u_1} (E := K) (↑r : K) = |r|

Tactic:
norm_algebraMap' K r

Premises used: norm_algebraMap'
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : ℝ
n : ℕ
rw : (re : (a : K) → ℝ) (↑(a ^ n) : K) = a ^ n
rw₁ rw₂ : a ^ n = a ^ n
⊢ (re : (a : K) → ℝ) (HPow.hPow (α := K) (↑a : K) n) = a ^ n

Tactic:
rw [← ofReal_pow, @ofReal_re]

Premises used: RCLike.ofReal_re, RCLike.ofReal_pow
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : ℝ
n : ℕ
rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑(a ^ n) : K) : ℝ) (0 : ℝ)
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (HPow.hPow (α := K) (↑a : K) n) : ℝ) (0 : ℝ)

Tactic:
rw [← @ofReal_pow, @ofReal_im_ax]

Premises used: RCLike.ofReal_pow, RCLike.ofReal_im_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
⊢ CharZero K

Tactic:
(RingHom.charZero_iff (algebraMap ℝ K).injective).1 inferInstance

Premises used: Real, Algebra.algebraMap, inferInstance, RingHom.charZero_iff, RingHom.injective, Iff.mp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
α : Type u_3
s : Finset α
f : α → ℝ
⊢ Eq.{u_1 + 1} (α := K) (↑(𝔼 i ∈ s, f i) : K) (𝔼 i ∈ s, (↑(f i) : K))

Tactic:
map_expect (algebraMap ..) ..

Premises used: Algebra.algebraMap, map_expect
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
ι : Type u_3
inst_1 : Fintype ι
f : ι → ℝ
i : ι
⊢ Eq.{u_1 + 1} (α := K) (↑(balance f i) : K) (balance (ofReal ∘ f) i)

Tactic:
map_balance (algebraMap ..) ..

Premises used: Algebra.algebraMap, Fintype.map_balance
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
ι : Type u_3
inst_1 : Fintype ι
f : ι → ℝ
⊢ Eq (α := ι → K) (ofReal ∘ balance f) (balance (ofReal ∘ f))

Tactic:
funext <| ofReal_balance _

Premises used: RCLike.ofReal_balance, funext
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) I : ℝ) (0 : ℝ)

Tactic:
I_re_ax

Premises used: RCLike.I_re_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) I : ℝ) = (im : (a : K) → ℝ) z

Tactic:
mul_im_I_ax z

Premises used: RCLike.mul_im_I_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) I : ℝ) = (im : (a : K) → ℝ) z
rw₁ rw₂ : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) z : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) I : ℝ) ((im : (a : K) → ℝ) z : ℝ) = (im : (a : K) → ℝ) z

Tactic:
rw [mul_comm, I_im]

Premises used: RCLike.I_im, mul_comm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (I * z) : ℝ) (-(im : (a : K) → ℝ) z : ℝ)

Tactic:
simp only [I_re, zero_sub, I_im', zero_mul, mul_re]

Premises used: MulZeroClass.zero_mul, RCLike.mul_re, RCLike.I_re, RCLike.I_im', zero_sub
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := K) I 0 ∨ HMul.hMul (α := K) I I = -1

Tactic:
I_mul_I_ax

Premises used: RCLike.I_mul_I_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
h : HMul.hMul (α := K) I I = -1
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) I : ℝ) (1 : ℝ)

Tactic:
simpa [h] using (I_mul_re (I : K)).symm

Premises used: RCLike.I, RCLike.I_mul_re, Eq.symm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) z : K) : ℝ) ((re : (a : K) → ℝ) z : ℝ)

Tactic:
RCLike.conj_re_ax z

Premises used: RCLike.conj_re_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) z : K) : ℝ) (-(im : (a : K) → ℝ) z : ℝ)

Tactic:
RCLike.conj_im_ax z

Premises used: RCLike.conj_im_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := K) ((starRingEnd K : (a : K) → K) I : K) (-I : K)

Tactic:
RCLike.conj_I_ax

Premises used: RCLike.conj_I_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
rw :
  Eq (α := ℝ) ((re : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) (↑r : K) : K) : ℝ) ((re : (a : K) → ℝ) (↑r : K) : ℝ) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) (↑r : K) : K) : ℝ) ((im : (a : K) → ℝ) (↑r : K) : ℝ)
⊢ Eq (α := K) ((starRingEnd K : (a : K) → K) (↑r : K) : K) ((↑r : K) : K)

Tactic:
rw [ext_iff]

Premises used: RCLike.ext_iff
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) (↑r : K) : K) : ℝ) ((re : (a : K) → ℝ) (↑r : K) : ℝ) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) (↑r : K) : K) : ℝ) ((im : (a : K) → ℝ) (↑r : K) : ℝ)

Tactic:
simp only [ofReal_im, conj_im, conj_re, and_self_iff, neg_zero]

Premises used: RCLike.conj_re, RCLike.ofReal_im, RCLike.conj_im, and_self_iff, neg_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
⊢ Eq (α := K) ((starRingEnd K : (a : K) → K) (↑n : K) : K) ((↑n : K) : K)

Tactic:
map_natCast _ _

Premises used: map_natCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq (α := K) ((starRingEnd K : (a : K) → K) (OfNat.ofNat n) : K) (OfNat.ofNat n : K)

Tactic:
map_ofNat _ _

Premises used: map_ofNat
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
rw : Eq (α := K) (-(starRingEnd K : (a : K) → K) I : K) (I : K)
rw₁ : Eq.{u_1 + 1} (α := K) (- -I) I
rw₂ rw₃ : Eq.{u_1 + 1} (α := K) I I
⊢ Eq (α := K) ((starRingEnd K : (a : K) → K) (-I) : K) (I : K)

Tactic:
rw [map_neg, conj_I, neg_neg]

Premises used: neg_neg, map_neg, RCLike.conj_I
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  HAdd.hAdd (α := K) (β := K) ((starRingEnd K : (a : K) → K) (↑((re : (a : K) → ℝ) z) : K) : K)
      ((starRingEnd K : (a : K) → K) (HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I) : K) =
    (↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I
rw₁ :
  HAdd.hAdd (α := K) ((starRingEnd K : (a : K) → K) (↑((re : (a : K) → ℝ) z) : K) : K)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) (↑((im : (a : K) → ℝ) z) : K) : K)
        ((starRingEnd K : (a : K) → K) I : K)) =
    (↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I
rw₂ :
  HAdd.hAdd (α := K) ((starRingEnd K : (a : K) → K) (↑((re : (a : K) → ℝ) z) : K) : K)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) (↑((im : (a : K) → ℝ) z) : K) : K) (-I : K)) =
    (↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I
rw₃ :
  (↑((re : (a : K) → ℝ) z) : K) +
      HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) (↑((im : (a : K) → ℝ) z) : K) : K) (-I : K) =
    (↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I
rw₄ :
  (↑((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
rw₅ :
  (↑((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
rw₆ rw₇ :
  (↑((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
⊢ (starRingEnd K : (a : K) → 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

Tactic:
rw [map_add, map_mul, conj_I, conj_ofReal, conj_ofReal, mul_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, RCLike.conj_ofReal, map_add, map_mul, RCLike.conj_I, mul_neg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  HSub.hSub (β := K) z ((starRingEnd K : (a : K) → K) z : K) =
    z - ((↑((re : (a : K) → ℝ) z) : K) - HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I)
rw₁ rw₂ :
  HSub.hSub (β := K) z ((starRingEnd K : (a : K) → K) z : K) =
    HSub.hSub (β := K) z ((starRingEnd K : (a : K) → K) z : K)
⊢ HSub.hSub (β := 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)

Tactic:
rw [re_add_im, ← conj_eq_re_sub_im]

Premises used: RCLike.re_add_im, RCLike.conj_eq_re_sub_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I =
    HMul.hMul (α := K) 2 (↑((im : (a : K) → ℝ) z) : K) * I
rw₁ : 2 * HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I = HMul.hMul (α := K) 2 (↑((im : (a : K) → ℝ) z) : K) * I
rw₂ rw₃ :
  2 * HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I = 2 * HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I
⊢ (↑((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 (↑((im : (a : K) → ℝ) z) : K) * I

Tactic:
rw [add_sub_sub_cancel, ← two_mul, mul_assoc]

Premises used: mul_assoc, add_sub_sub_cancel, two_mul
-- Module: Mathlib.Analysis.RCLike.Basic
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
rw₈ 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
⊢ (starRingEnd K : (a : K) → K) (r • z) = HSMul.hSMul (β := K) r ((starRingEnd K : (a : K) → K) z : K)

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]

Premises used: RCLike.smul_re, mul_sub, mul_assoc, HSub.hSub, RCLike.ofReal_mul, RCLike.smul_im, RCLike.conj_eq_re_sub_im, RCLike.real_smul_eq_coe_mul
-- Module: Mathlib.Analysis.RCLike.Basic
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [re_add_im, conj_eq_re_sub_im]

Premises used: RCLike.re_add_im, RCLike.conj_eq_re_sub_im
-- Module: Mathlib.Analysis.RCLike.Basic
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)
rw₁ 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)
⊢ (↑((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)

Tactic:
rw [add_add_sub_cancel, two_mul]

Premises used: two_mul, add_add_sub_cancel
-- Module: Mathlib.Analysis.RCLike.Basic
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := K) (↑((re : (a : K) → ℝ) z) : K) (↑((re : (a : K) → ℝ) z) : K)
⊢ (↑((re : (a : K) → ℝ) z) : K) = HAdd.hAdd (β := K) z ((starRingEnd K : (a : K) → K) z : K) / 2

Tactic:
rw [add_conj, mul_div_cancel_left₀ (re z : K) two_ne_zero]

Premises used: mul_div_cancel_left₀, RCLike.add_conj, RCLike.ofReal, two_ne_zero, RCLike.re, DFunLike.coe
-- Module: Mathlib.Analysis.RCLike.Basic
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
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) z ((starRingEnd K : (a : K) → K) z : K) / 2
rw₉ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    (I * z - HMul.hMul (α := K) (β := K) (I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2
rw₁₀ :
  (I * z + -HMul.hMul (α := K) (β := K) (I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    (I * z - HMul.hMul (α := K) (β := K) (I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2
rw₁₁ rw₁₂ :
  (I * z + -HMul.hMul (α := K) (β := K) (I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    (I * z + -HMul.hMul (α := K) (β := K) (I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2
⊢ (↑((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]

Premises used: neg_sub, neg_div, mul_sub, sub_eq_add_neg, RCLike.ofReal_neg, RCLike.re_eq_add_conj, map_mul, RCLike.conj_I, neg_inj, RCLike.I_mul_re, neg_mul, mul_neg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (starRingEnd K : (a : K) → K) z = z

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ ∀ (a : (starRingEnd K : (a : K) → K) z = z), Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
1 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h_1 : (starRingEnd K : (a : K) → K) z = z
h : (starRingEnd K : (a : K) → K) z = z := h_1
rw : Eq.{u_1 + 1} (α := K) (↑((im : (a : K) → ℝ) z) : K) (↑0 : K)
rw₁ : I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2 = (↑0 : K)
rw₂ : I * (z - z) / 2 = (↑0 : K)
rw₃ : HMul.hMul (α := K) I 0 / 2 = (↑0 : K)
rw₄ : 0 / 2 = (↑0 : K)
rw₅ : Eq.{u_1 + 1} (α := K) 0 (↑0 : K)
rw₆ rw₇ : Eq.{u_1 + 1} (α := K) 0 0
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,
      ofReal_zero]

Premises used: RCLike.ofReal_inj, sub_self, zero_div, RCLike.im_eq_conj_sub, RCLike.ofReal_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ ∀ (a : (starRingEnd K : (a : K) → K) z = z), Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
tfae_have 1 → 4
  | h => by
    rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,
      ofReal_zero]