awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) *
        HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) +
      HAdd.hAdd (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ) *
        HAdd.hAdd (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ) =
    HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) z : ℝ) +
          HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) z : ℝ) +
        (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) w : ℝ) ((re : (a : K) → ℝ) w : ℝ) +
          HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) w : ℝ) ((im : (a : K) → ℝ) w : ℝ)) +
      2 *
        (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) -
          HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) (-(im : (a : K) → ℝ) w : ℝ))

Tactic:
ring
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) z : ℝ) ≤ (normSq : (a : K) → ℝ) z

Tactic:
le_add_of_nonneg_right (mul_self_nonneg _)

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

Tactic:
le_add_of_nonneg_left (mul_self_nonneg _)

Premises used: mul_self_nonneg, le_add_of_nonneg_left
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
hre :
  Eq (α := ℝ) ((re : (a : K) → ℝ) (HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) z : K)) : ℝ)
    ((re : (a : K) → ℝ) (HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2) : ℝ)
him :
  Eq (α := ℝ) ((im : (a : K) → ℝ) (HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) z : K)) : ℝ)
    ((im : (a : K) → ℝ) (HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2) : ℝ)
⊢ HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) z : K) = HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2

Tactic:
apply ext

Premises used: RCLike.ext
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) z : K)) : ℝ)
    ((re : (a : K) → ℝ) (HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2) : ℝ)

Tactic:
simp [← ofReal_pow, norm_sq_eq_def, mul_comm]

Premises used: RCLike.ofReal_pow, RCLike.norm_sq_eq_def, mul_comm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) z : K)) : ℝ)
    ((im : (a : K) → ℝ) (HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2) : ℝ)

Tactic:
simp [← ofReal_pow, norm_sq_eq_def, mul_comm]

Premises used: RCLike.ofReal_pow, RCLike.norm_sq_eq_def, mul_comm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) z : K) = HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2
rw₁ rw₂ : HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2 = HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2
⊢ HMul.hMul (α := K) ((starRingEnd K : (a : K) → K) z : K) z = HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2

Tactic:
rw [mul_comm, mul_conj]

Premises used: RCLike.mul_conj, mul_comm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
hz : ‖z‖ = 1
simp_rw : HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2 = 1
simp_rw₁ : HPow.hPow (α := K) (β := ℕ) (↑1 : K) 2 = 1
simp_rw₂ : HPow.hPow (α := K) (β := ℕ) 1 2 = 1
⊢ HMul.hMul (α := K) ((starRingEnd K : (a : K) → K) z : K) z = 1

Tactic:
simp_rw [conj_mul, hz, algebraMap.coe_one, one_pow]

Premises used: one_pow, algebraMap.coe_one, RCLike.conj_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
⊢ (normSq : (a : K) → ℝ) (z - w) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) w : ℝ) -
      HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
        ((re : (a : K) → ℝ) (HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) w : K)) : ℝ)

Tactic:
simp only [normSq_add, sub_eq_add_neg, map_neg, mul_neg, normSq_neg, map_neg]

Premises used: RCLike.normSq_neg, sub_eq_add_neg, map_neg, RCLike.normSq_add, mul_neg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : √(HPow.hPow (β := ℕ) ‖z‖ 2) = ‖z‖
rw₁ rw₂ : ‖z‖ = ‖z‖
⊢ √((normSq : (a : K) → ℝ) z) = ‖z‖

Tactic:
rw [normSq_eq_def', Real.sqrt_sq (norm_nonneg _)]

Premises used: RCLike.normSq_eq_def', Real.sqrt_sq, norm_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
⊢ Eq.{u_1 + 1} (α := K) (↑r⁻¹ : K) (↑r : K)⁻¹

Tactic:
map_inv₀ _ r

Premises used: map_inv₀
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
inl :
  0⁻¹ =
    HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) 0 : K)
      ((↑(HPow.hPow (β := ℕ) (norm.{u_1} (E := K) 0) 2)⁻¹ : K) : K)
inr :
  ∀ (h₀ : z ≠ 0),
    z⁻¹ = HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)
⊢ z⁻¹ = HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)

Tactic:
rcases eq_or_ne z 0 with (rfl | h₀)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ 0⁻¹ =
    HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) 0 : K)
      ((↑(HPow.hPow (β := ℕ) (norm.{u_1} (E := K) 0) 2)⁻¹ : K) : K)

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h₀ : z ≠ 0
inr :
  z * HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K) = 1
⊢ z⁻¹ = HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)

Tactic:
apply inv_eq_of_mul_eq_one_right

Premises used: inv_eq_of_mul_eq_one_right
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h₀ : z ≠ 0
inr : HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2 ≠ 0
⊢ z * HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K) = 1

Tactic:
rw [← mul_assoc, mul_conj, ofReal_inv, ofReal_pow, mul_inv_cancel₀]

Premises used: RCLike.mul_conj, mul_inv_cancel₀, mul_assoc, RCLike.ofReal_pow, RCLike.ofReal_inv
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h₀ : z ≠ 0
⊢ HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2 ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
rw₁ :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₂ :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K) ((starRingEnd K : (a : K) → K) z : K)) =
    HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₃ :
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((re : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) z : K) : ℝ) =
    HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₄ :
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((re : (a : K) → ℝ) z : ℝ) =
    HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₅ rw₆ :
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((re : (a : K) → ℝ) z : ℝ) =
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((re : (a : K) → ℝ) z : ℝ)
⊢ (re : (a : K) → ℝ) z⁻¹ = HDiv.hDiv (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)

Tactic:
rw [inv_def, normSq_eq_def', mul_comm, re_ofReal_mul, conj_re, div_eq_inv_mul]

Premises used: RCLike.conj_re, RCLike.normSq_eq_def', RCLike.inv_def, mul_comm, RCLike.re_ofReal_mul, div_eq_inv_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (β := ℝ) (-(im : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
rw₁ :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₂ :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K) ((starRingEnd K : (a : K) → K) z : K)) =
    HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₃ :
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((im : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) z : K) : ℝ) =
    HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₄ :
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ (-(im : (a : K) → ℝ) z : ℝ) =
    HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₅ rw₆ :
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ (-(im : (a : K) → ℝ) z : ℝ) =
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ (-(im : (a : K) → ℝ) z : ℝ)
⊢ (im : (a : K) → ℝ) z⁻¹ = HDiv.hDiv (α := ℝ) (β := ℝ) (-(im : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)

Tactic:
rw [inv_def, normSq_eq_def', mul_comm, im_ofReal_mul, conj_im, div_eq_inv_mul]

Premises used: RCLike.normSq_eq_def', RCLike.conj_im, RCLike.inv_def, mul_comm, RCLike.im_ofReal_mul, div_eq_inv_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
⊢ (re : (a : K) → ℝ) (z / w) =
    HDiv.hDiv (β := ℝ) (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ))
        ((normSq : (a : K) → ℝ) w : ℝ) +
      HDiv.hDiv (β := ℝ) (HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ))
        ((normSq : (a : K) → ℝ) w : ℝ)

Tactic:
simp only [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, neg_mul, mul_neg, neg_neg,
    rclike_simps]

Premises used: mul_assoc, sub_eq_add_neg, neg_neg, div_eq_mul_inv, neg_mul, mul_neg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
⊢ (im : (a : K) → ℝ) (z / w) =
    HDiv.hDiv (β := ℝ) (HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ))
        ((normSq : (a : K) → ℝ) w : ℝ) -
      HDiv.hDiv (β := ℝ) (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ))
        ((normSq : (a : K) → ℝ) w : ℝ)

Tactic:
simp only [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, add_comm, neg_mul, mul_neg,
    rclike_simps]

Premises used: mul_assoc, sub_eq_add_neg, div_eq_mul_inv, add_comm, neg_mul, mul_neg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
⊢ Eq (α := K) ((starRingEnd K : (a : K) → K) x⁻¹ : K) (((starRingEnd K : (a : K) → K) x)⁻¹ : K)

Tactic:
star_inv₀ _

Premises used: star_inv₀
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
⊢ (starRingEnd K : (a : K) → K) (x / y) =
    HDiv.hDiv (α := K) (β := K) ((starRingEnd K : (a : K) → K) x : K) ((starRingEnd K : (a : K) → K) y : K)

Tactic:
map_div' conj conj_inv _ _

Premises used: map_div', RCLike.conj_inv, starRingEnd
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
inl : ∃ (c : K), ‖c‖ = 1 ∧ (↑(norm.{u_1} (E := K) 0) : K) = c * 0
inr : ∀ (hx : x ≠ 0), ∃ (c : K), ‖c‖ = 1 ∧ (↑‖x‖ : K) = c * x
⊢ ∃ (c : K), ‖c‖ = 1 ∧ (↑‖x‖ : K) = c * x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ norm.{u_1} (E := K) 1 = 1 ∧ (↑(norm.{u_1} (E := K) 0) : K) = HMul.hMul (α := K) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ ∃ (c : K), ‖c‖ = 1 ∧ (↑(norm.{u_1} (E := K) 0) : K) = c * 0

Tactic:
exact ⟨1, by simp⟩
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
hx : x ≠ 0
⊢ ‖(↑‖x‖ : K) / x‖ = 1 ∧ (↑‖x‖ : K) = (↑‖x‖ : K) / x * x

Tactic:
simp [norm_ne_zero_iff.2, hx]

Premises used: Iff.mpr, norm_ne_zero_iff
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ (c : K), ‖c‖ = 1 ∧ (↑‖x‖ : K) = c * x

Tactic:
exact ⟨‖x‖ / x, by simp [norm_ne_zero_iff.2, hx]⟩
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
inl : ∃ (c : K), ‖c‖ = 1 ∧ c * (↑(norm.{u_1} (E := K) 0) : K) = 0
inr : ∀ (hx : x ≠ 0), ∃ (c : K), ‖c‖ = 1 ∧ c * (↑‖x‖ : K) = x
⊢ ∃ (c : K), ‖c‖ = 1 ∧ c * (↑‖x‖ : K) = x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ norm.{u_1} (E := K) 1 = 1 ∧ HMul.hMul (α := K) 1 (↑(norm.{u_1} (E := K) 0) : K) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ ∃ (c : K), ‖c‖ = 1 ∧ c * (↑(norm.{u_1} (E := K) 0) : K) = 0

Tactic:
exact ⟨1, by simp⟩
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
hx : x ≠ 0
⊢ ‖x / (↑‖x‖ : K)‖ = 1 ∧ x / (↑‖x‖ : K) * (↑‖x‖ : K) = x

Tactic:
simp [norm_ne_zero_iff.2, hx]

Premises used: Iff.mpr, norm_ne_zero_iff
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ (c : K), ‖c‖ = 1 ∧ c * (↑‖x‖ : K) = x

Tactic:
exact ⟨x / ‖x‖, by simp [norm_ne_zero_iff.2, hx]⟩
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r s : ℝ
⊢ (↑(r / s) : K) = HDiv.hDiv (α := K) (↑r : K) (↑s : K)

Tactic:
map_div₀ (algebraMap ℝ K) r s

Premises used: Real, Algebra.algebraMap, map_div₀
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
r : ℝ
rw : (re : (a : K) → ℝ) ((↑r : K)⁻¹ * z) = HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r
rw₁ : (re : (a : K) → ℝ) ((↑r : K)⁻¹ * z) = HMul.hMul (β := ℝ) r⁻¹ ((re : (a : K) → ℝ) z : ℝ)
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) → ℝ) (z / (↑r : K)) = HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r

Tactic:
rw [div_eq_inv_mul, div_eq_inv_mul, ← ofReal_inv, re_ofReal_mul]

Premises used: RCLike.re_ofReal_mul, div_eq_inv_mul, RCLike.ofReal_inv
-- 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_zpow₀ (algebraMap ℝ K) r n

Premises used: Real, Algebra.algebraMap, map_zpow₀
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Ne.{u_1 + 1} (α := K) I 0 → HMul.hMul (α := K) I I = -1

Tactic:
I_mul_I_ax.resolve_left

Premises used: Or.resolve_left, RCLike.I_mul_I_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
pos : ∀ (h : Eq.{u_1 + 1} (α := K) I 0), Eq.{u_1 + 1} (α := K) I⁻¹ (-I)
neg : ∀ (h : ¬Eq.{u_1 + 1} (α := K) I 0), Eq.{u_1 + 1} (α := K) I⁻¹ (-I)
⊢ Eq.{u_1 + 1} (α := K) I⁻¹ (-I)

Tactic:
by_cases h : (I : K) = 0

Premises used: RCLike.I
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
h : Eq.{u_1 + 1} (α := K) I 0
⊢ Eq.{u_1 + 1} (α := K) I⁻¹ (-I)

Tactic:
simp [h]
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
h : ¬Eq.{u_1 + 1} (α := K) I 0
neg : 1 = -HPow.hPow (α := K) (β := ℕ) I 2
⊢ Eq.{u_1 + 1} (α := K) I⁻¹ (-I)

Tactic:
field_simp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
h : ¬Eq.{u_1 + 1} (α := K) I 0
⊢ 1 = -HPow.hPow (α := K) (β := ℕ) I 2

Tactic:
linear_combination I_mul_I_of_nonzero h

Premises used: RCLike.I_mul_I_of_nonzero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : z * I⁻¹ = -(z * I)
rw₁ : z * -I = -(z * I)
rw₂ rw₃ : -(z * I) = -(z * I)
⊢ z / I = -(z * I)

Tactic:
rw [div_eq_mul_inv, inv_I, mul_neg]

Premises used: div_eq_mul_inv, mul_neg, RCLike.inv_I
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ Eq (α := ℝ) ((normSq : (a : K) → ℝ) z⁻¹ : ℝ) (((normSq : (a : K) → ℝ) z)⁻¹ : ℝ)

Tactic:
map_inv₀ normSq z

Premises used: map_inv₀, RCLike.normSq
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
⊢ (normSq : (a : K) → ℝ) (z / w) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((normSq : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) w : ℝ)

Tactic:
map_div₀ normSq z w

Premises used: map_div₀, RCLike.normSq
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ norm (E := K) ((starRingEnd K : (a : K) → K) z : K) = ‖z‖

Tactic:
simp only [← sqrt_normSq_eq_norm, normSq_conj]

Premises used: RCLike.sqrt_normSq_eq_norm, RCLike.normSq_conj
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ nnnorm (E := K) ((starRingEnd K : (a : K) → K) z : K) = ‖z‖₊

Tactic:
simp [nnnorm]

Premises used: NNNorm.nnnorm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ enorm (E := K) ((starRingEnd K : (a : K) → K) z : K) = ‖z‖ₑ

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : K
r : ℝ
a : K
hre : Eq (α := ℝ) ((re : (a : K) → ℝ) (star (r • a)) : ℝ) ((re : (a : K) → ℝ) (star r • star a) : ℝ)
him : Eq (α := ℝ) ((im : (a : K) → ℝ) (star (r • a)) : ℝ) ((im : (a : K) → ℝ) (star r • star a) : ℝ)
⊢ star (r • a) = star r • star a

Tactic:
apply RCLike.ext

Premises used: RCLike.ext
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : K
r : ℝ
a : K
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (star (r • a)) : ℝ) ((re : (a : K) → ℝ) (star r • star a) : ℝ)

Tactic:
simp [RCLike.smul_re, RCLike.smul_im]

Premises used: RCLike.smul_re, RCLike.smul_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : K
r : ℝ
a : K
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (star (r • a)) : ℝ) ((im : (a : K) → ℝ) (star r • star a) : ℝ)

Tactic:
simp [RCLike.smul_re, RCLike.smul_im]

Premises used: RCLike.smul_re, RCLike.smul_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
⊢ Eq.{u_1 + 1} (α := K) (↑(↑n : ℝ) : K) (↑n : K)

Tactic:
map_natCast (algebraMap ℝ K) n

Premises used: Real, Algebra.algebraMap, map_natCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(↑n : ℝ) : K) : ℝ) ((↑n : ℝ) : ℝ)
rw₁ rw₂ : Eq (α := ℝ) (↑n : ℝ) (↑n : ℝ)
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (↑n : K) : ℝ) ((↑n : ℝ) : ℝ)

Tactic:
rw [← ofReal_natCast, ofReal_re]

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

Tactic:
rw [← ofReal_natCast, ofReal_im]

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

Tactic:
natCast_re n

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

Tactic:
natCast_im n

Premises used: RCLike.natCast_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := K) (↑(OfNat.ofNat n) : K) (OfNat.ofNat n)

Tactic:
ofReal_natCast n

Premises used: RCLike.ofReal_natCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
inst_1 : n.AtLeastTwo
z : K
rw :
  (re : (a : K) → ℝ) ((↑(OfNat.ofNat n) : K) * z) =
    HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((re : (a : K) → ℝ) z : ℝ)
rw₁ rw₂ :
  HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((re : (a : K) → ℝ) z : ℝ) =
    HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((re : (a : K) → ℝ) z : ℝ)
⊢ (re : (a : K) → ℝ) (OfNat.ofNat n * z) = HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((re : (a : K) → ℝ) z : ℝ)

Tactic:
rw [← ofReal_ofNat, re_ofReal_mul]

Premises used: RCLike.ofReal_ofNat, RCLike.re_ofReal_mul
-- Module: Mathlib.Analysis.RCLike.Basic
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 : ℝ)
rw₁ rw₂ :
  HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((im : (a : 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 : ℝ)

Tactic:
rw [← ofReal_ofNat, im_ofReal_mul]

Premises used: RCLike.im_ofReal_mul, RCLike.ofReal_ofNat
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℤ
⊢ Eq.{u_1 + 1} (α := K) (↑(↑n : ℝ) : K) (↑n : K)

Tactic:
map_intCast _ n

Premises used: map_intCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℤ
rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(↑n : ℝ) : K) : ℝ) ((↑n : ℝ) : ℝ)
rw₁ rw₂ : Eq (α := ℝ) (↑n : ℝ) (↑n : ℝ)
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (↑n : K) : ℝ) ((↑n : ℝ) : ℝ)

Tactic:
rw [← ofReal_intCast, ofReal_re]

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

Tactic:
rw [← ofReal_intCast, ofReal_im]

Premises used: RCLike.ofReal_im, RCLike.ofReal_intCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℚ≥0
⊢ Eq.{u_1 + 1} (α := K) (↑(↑n : ℝ) : K) (↑n : K)

Tactic:
map_nnratCast _ n

Premises used: map_nnratCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
q : ℚ≥0
rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(↑q : ℝ) : K) : ℝ) ((↑q : ℝ) : ℝ)
rw₁ rw₂ : Eq (α := ℝ) (↑q : ℝ) (↑q : ℝ)
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (↑q : K) : ℝ) ((↑q : ℝ) : ℝ)

Tactic:
rw [← ofReal_nnratCast, ofReal_re]

Premises used: RCLike.ofReal_re, RCLike.ofReal_nnratCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
q : ℚ≥0
rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑(↑q : ℝ) : K) : ℝ) (0 : ℝ)
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑q : K) : ℝ) (0 : ℝ)

Tactic:
rw [← ofReal_nnratCast, ofReal_im]

Premises used: RCLike.ofReal_im, RCLike.ofReal_nnratCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℚ
⊢ Eq.{u_1 + 1} (α := K) (↑(↑n : ℝ) : K) (↑n : K)

Tactic:
map_ratCast _ n

Premises used: map_ratCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
q : ℚ
rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(↑q : ℝ) : K) : ℝ) ((↑q : ℝ) : ℝ)
rw₁ rw₂ : Eq (α := ℝ) (↑q : ℝ) (↑q : ℝ)
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (↑q : K) : ℝ) ((↑q : ℝ) : ℝ)

Tactic:
rw [← ofReal_ratCast, ofReal_re]

Premises used: RCLike.ofReal_re, RCLike.ofReal_ratCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
q : ℚ
rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑(↑q : ℝ) : K) : ℝ) (0 : ℝ)
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑q : K) : ℝ) (0 : ℝ)

Tactic:
rw [← ofReal_ratCast, ofReal_im]

Premises used: RCLike.ofReal_im, RCLike.ofReal_ratCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
m : ℕ
s : Bool
e : ℕ
⊢ Eq.{u_1 + 1} (α := K) (↑(ofScientific m s e) : K) (ofScientific m s e)

Tactic:
ofReal_nnratCast _

Premises used: RCLike.ofReal_nnratCast