awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ 0 ≤ z ↔ LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
simpa only [map_zero, eq_comm] using le_iff_re_im (z := 0) (w := z)

Premises used: RCLike.le_iff_re_im, map_zero, eq_comm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ 0 < z ↔ LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
simpa only [map_zero, eq_comm] using lt_iff_re_im (z := 0) (w := z)

Premises used: map_zero, eq_comm, RCLike.lt_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ z ≤ 0 ↔ LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
simpa only [map_zero] using le_iff_re_im (z := z) (w := 0)

Premises used: RCLike.le_iff_re_im, map_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ z < 0 ↔ LT.lt (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
simpa only [map_zero] using lt_iff_re_im (z := z) (w := 0)

Premises used: map_zero, RCLike.lt_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
simp_rw :
  LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ↔
    ∃ x ≥ 0,
      Eq (α := ℝ) ((re : (a : K) → ℝ) (↑x : K) : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) (↑x : K) : ℝ) ((im : (a : K) → ℝ) z : ℝ)
⊢ 0 ≤ z ↔ ∃ x ≥ 0, (↑x : K) = z

Tactic:
simp_rw [nonneg_iff (K := K), ext_iff (K := K)]

Premises used: RCLike.ext_iff, RCLike.nonneg_iff
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ↔
    ∃ x ≥ 0,
      Eq (α := ℝ) ((re : (a : K) → ℝ) (↑x : K) : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) (↑x : K) : ℝ) ((im : (a : K) → ℝ) z : ℝ)

Tactic:
aesop
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
simp_rw :
  LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ↔
    ∃ x > 0,
      Eq (α := ℝ) ((re : (a : K) → ℝ) (↑x : K) : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) (↑x : K) : ℝ) ((im : (a : K) → ℝ) z : ℝ)
⊢ 0 < z ↔ ∃ x > 0, (↑x : K) = z

Tactic:
simp_rw [pos_iff (K := K), ext_iff (K := K)]

Premises used: RCLike.pos_iff, RCLike.ext_iff
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ↔
    ∃ x > 0,
      Eq (α := ℝ) ((re : (a : K) → ℝ) (↑x : K) : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) (↑x : K) : ℝ) ((im : (a : K) → ℝ) z : ℝ)

Tactic:
aesop
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
simp_rw :
  LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ↔
    ∃ x ≤ 0,
      Eq (α := ℝ) ((re : (a : K) → ℝ) (↑x : K) : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) (↑x : K) : ℝ) ((im : (a : K) → ℝ) z : ℝ)
⊢ z ≤ 0 ↔ ∃ x ≤ 0, (↑x : K) = z

Tactic:
simp_rw [nonpos_iff (K := K), ext_iff (K := K)]

Premises used: RCLike.nonpos_iff, RCLike.ext_iff
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ↔
    ∃ x ≤ 0,
      Eq (α := ℝ) ((re : (a : K) → ℝ) (↑x : K) : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) (↑x : K) : ℝ) ((im : (a : K) → ℝ) z : ℝ)

Tactic:
aesop
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
simp_rw :
  LT.lt (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ↔
    ∃ x < 0,
      Eq (α := ℝ) ((re : (a : K) → ℝ) (↑x : K) : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) (↑x : K) : ℝ) ((im : (a : K) → ℝ) z : ℝ)
⊢ z < 0 ↔ ∃ x < 0, (↑x : K) = z

Tactic:
simp_rw [neg_iff (K := K), ext_iff (K := K)]

Premises used: RCLike.ext_iff, RCLike.neg_iff
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ LT.lt (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ↔
    ∃ x < 0,
      Eq (α := ℝ) ((re : (a : K) → ℝ) (↑x : K) : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) (↑x : K) : ℝ) ((im : (a : K) → ℝ) z : ℝ)

Tactic:
aesop
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : ℝ
rw :
  LE.le (α := ℝ) ((re : (a : K) → ℝ) (↑x : K) : ℝ) ((re : (a : K) → ℝ) (↑y : K) : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) (↑x : K) : ℝ) ((im : (a : K) → ℝ) (↑y : K) : ℝ) ↔
    x ≤ y
⊢ LE.le.{u_1} (α := K) (↑x : K) (↑y : K) ↔ x ≤ y

Tactic:
rw [le_iff_re_im]

Premises used: RCLike.le_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : ℝ
⊢ LE.le (α := ℝ) ((re : (a : K) → ℝ) (↑x : K) : ℝ) ((re : (a : K) → ℝ) (↑y : K) : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) (↑x : K) : ℝ) ((im : (a : K) → ℝ) (↑y : K) : ℝ) ↔
    x ≤ y

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : ℝ
rw :
  LT.lt (α := ℝ) ((re : (a : K) → ℝ) (↑x : K) : ℝ) ((re : (a : K) → ℝ) (↑y : K) : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) (↑x : K) : ℝ) ((im : (a : K) → ℝ) (↑y : K) : ℝ) ↔
    x < y
⊢ LT.lt.{u_1} (α := K) (↑x : K) (↑y : K) ↔ x < y

Tactic:
rw [lt_iff_re_im]

Premises used: RCLike.lt_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : ℝ
⊢ LT.lt (α := ℝ) ((re : (a : K) → ℝ) (↑x : K) : ℝ) ((re : (a : K) → ℝ) (↑y : K) : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) (↑x : K) : ℝ) ((im : (a : K) → ℝ) (↑y : K) : ℝ) ↔
    x < y

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
rw : LE.le.{u_1} (α := K) (↑0 : K) (↑x : K) ↔ 0 ≤ x
rw₁ rw₂ : 0 ≤ x ↔ 0 ≤ x
⊢ LE.le.{u_1} (α := K) 0 (↑x : K) ↔ 0 ≤ x

Tactic:
rw [← ofReal_zero, ofReal_le_ofReal]

Premises used: RCLike.ofReal_le_ofReal, RCLike.ofReal_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
rw : LE.le.{u_1} (α := K) (↑x : K) (↑0 : K) ↔ x ≤ 0
rw₁ rw₂ : x ≤ 0 ↔ x ≤ 0
⊢ LE.le.{u_1} (α := K) (↑x : K) 0 ↔ x ≤ 0

Tactic:
rw [← ofReal_zero, ofReal_le_ofReal]

Premises used: RCLike.ofReal_le_ofReal, RCLike.ofReal_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
rw : LT.lt.{u_1} (α := K) (↑0 : K) (↑x : K) ↔ 0 < x
rw₁ rw₂ : 0 < x ↔ 0 < x
⊢ LT.lt.{u_1} (α := K) 0 (↑x : K) ↔ 0 < x

Tactic:
rw [← ofReal_zero, ofReal_lt_ofReal]

Premises used: RCLike.ofReal_zero, RCLike.ofReal_lt_ofReal
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
rw : LT.lt.{u_1} (α := K) (↑x : K) (↑0 : K) ↔ x < 0
rw₁ rw₂ : x < 0 ↔ x < 0
⊢ LT.lt.{u_1} (α := K) (↑x : K) 0 ↔ x < 0

Tactic:
rw [← ofReal_zero, ofReal_lt_ofReal]

Premises used: RCLike.ofReal_zero, RCLike.ofReal_lt_ofReal
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ ‖z‖ ≤ (re : (a : K) → ℝ) z ↔ z = (↑‖z‖ : K)

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
refine_1 : ∀ (h : ‖z‖ ≤ (re : (a : K) → ℝ) z), z = (↑‖z‖ : K)
refine_2 : ∀ (h : z = (↑‖z‖ : K)), ‖z‖ ≤ (re : (a : K) → ℝ) z
⊢ ‖z‖ ≤ (re : (a : K) → ℝ) z ↔ z = (↑‖z‖ : K)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : ‖z‖ ≤ (re : (a : K) → ℝ) z
⊢ ‖z‖ = (re : (a : K) → ℝ) z

Tactic:
have h' : ‖z‖ = re z := (le_antisymm (re_le_norm z) h).symm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : ‖z‖ ≤ (re : (a : K) → ℝ) z
h' : ‖z‖ = (re : (a : K) → ℝ) z
refine_1 : z = (↑((re : (a : K) → ℝ) z) : K)
refine_1₁ refine_1₂ : z = z
⊢ z = (↑‖z‖ : K)

Tactic:
rw [h', re_eq_self_of_le h]

Premises used: RCLike.re_eq_self_of_le
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : z = (↑‖z‖ : K)
refine_2 : norm.{u_1} (E := K) (↑‖z‖ : K) ≤ (re : (a : K) → ℝ) (↑‖z‖ : K)
⊢ ‖z‖ ≤ (re : (a : K) → ℝ) z

Tactic:
rw [h]
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : z = (↑‖z‖ : K)
⊢ norm.{u_1} (E := K) (↑‖z‖ : K) ≤ (re : (a : K) → ℝ) (↑‖z‖ : K)

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (re : (a : K) → ℝ) z ≤ -‖z‖ ↔ z = -(↑‖z‖ : K)

Tactic:
simpa [neg_eq_iff_eq_neg, le_neg] using norm_le_re_iff_eq_norm (z := -z)

Premises used: le_neg, neg_eq_iff_eq_neg, RCLike.norm_le_re_iff_eq_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
hx : 0 ≤ x
rw :
  √(HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) x : ℝ) +
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) x : ℝ)) ≤
    (re : (a : K) → ℝ) x
⊢ (↑‖x‖ : K) = x

Tactic:
rw [eq_comm, ← norm_le_re_iff_eq_norm, ← sqrt_normSq_eq_norm, normSq_apply]

Premises used: RCLike.norm_le_re_iff_eq_norm, eq_comm, RCLike.sqrt_normSq_eq_norm, RCLike.normSq_apply
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
hx : 0 ≤ x
⊢ √(HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) x : ℝ) +
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) x : ℝ)) ≤
    (re : (a : K) → ℝ) x

Tactic:
simp [nonneg_iff.mp hx]

Premises used: RCLike.nonneg_iff, Iff.mp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
hx : IsSelfAdjoint x
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) x : ℝ) ↔ 0 ≤ x

Tactic:
simp [nonneg_iff (K := K), conj_eq_iff_im.mp hx]

Premises used: RCLike.nonneg_iff, RCLike.conj_eq_iff_im, Iff.mp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
h : x ≤ y
⊢ LE.le (α := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)

Tactic:
rw [RCLike.le_iff_re_im] at h

Premises used: RCLike.le_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
h :
  LE.le (α := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)
⊢ LE.le (α := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
h :
  LE.le (α := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)
⊢ LE.le (α := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Monotone.{u_1, 0} (α := K) (β := ℝ) (⇑re : (a : K) → ℝ)

Tactic:
fun _ _ => re_le_re

Premises used: Monotone, RCLike.re_le_re
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
hz : 0 < z
⊢ ∃ x > 0, (↑x : K) = z

Tactic:
rw [pos_iff_exists_ofReal] at hz

Premises used: RCLike.pos_iff_exists_ofReal
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
hz : ∃ x > 0, (↑x : K) = z
obtain : ∀ (x : ℝ) (hx : x > 0) (hx' : (↑x : K) = z), 0 < z⁻¹
⊢ 0 < z⁻¹

Tactic:
obtain ⟨x, hx, hx'⟩ := hz
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
x : ℝ
hx : x > 0
hx' : (↑x : K) = z
rw : 0 < x⁻¹
⊢ 0 < z⁻¹

Tactic:
rw [← hx', ← ofReal_inv, ofReal_pos]

Premises used: RCLike.ofReal_pos, RCLike.ofReal_inv
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
x : ℝ
hx : x > 0
hx' : (↑x : K) = z
⊢ 0 < x⁻¹

Tactic:
inv_pos_of_pos hx

Premises used: inv_pos_of_pos
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
x : ℝ
hx : x > 0
hx' : (↑x : K) = z
⊢ 0 < x⁻¹

Tactic:
exact inv_pos_of_pos hx

Premises used: inv_pos_of_pos
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ 0 < z⁻¹ ↔ 0 < z

Tactic:
⟨fun h => ?_, fun h => RCLike.inv_pos_of_pos h⟩

Premises used: RCLike.inv_pos_of_pos, Iff.intro
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
refine : ∀ (h : 0 < z⁻¹), 0 < z
⊢ 0 < z⁻¹ ↔ 0 < z

Tactic:
refine ⟨fun h => ?_, fun h => RCLike.inv_pos_of_pos h⟩
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : 0 < z⁻¹
rw : 0 < z⁻¹⁻¹
⊢ 0 < z

Tactic:
rw [← inv_inv z]

Premises used: inv_inv
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : 0 < z⁻¹
⊢ 0 < z⁻¹⁻¹

Tactic:
RCLike.inv_pos_of_pos h

Premises used: RCLike.inv_pos_of_pos
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : 0 < z⁻¹
⊢ 0 < z⁻¹⁻¹

Tactic:
exact RCLike.inv_pos_of_pos h

Premises used: RCLike.inv_pos_of_pos
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
hxy : x ≤ y
z : K
rw :
  ∀
    (hxy :
      LE.le (α := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ))
    (z : K),
    LE.le (α := ℝ) ((re : (a : K) → ℝ) (z + x) : ℝ) ((re : (a : K) → ℝ) (z + y) : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) (z + x) : ℝ) ((im : (a : K) → ℝ) (z + y) : ℝ)
⊢ z + x ≤ z + y

Tactic:
rw [RCLike.le_iff_re_im] at *

Premises used: RCLike.le_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
hxy :
  LE.le (α := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)
z : K
⊢ LE.le (α := ℝ) ((re : (a : K) → ℝ) (z + x) : ℝ) ((re : (a : K) → ℝ) (z + y) : ℝ) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) (z + x) : ℝ) ((im : (a : K) → ℝ) (z + y) : ℝ)

Tactic:
simpa [map_add, add_le_add_iff_left, add_right_inj] using hxy

Premises used: add_le_add_iff_left, map_add, add_right_inj
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
rw :
  LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) x : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ∃ (s : K), x = star s * s
⊢ 0 ≤ x ↔ ∃ (s : K), x = star s * s

Tactic:
rw [nonneg_iff]

Premises used: RCLike.nonneg_iff
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
h : LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) x : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) (0 : ℝ)
⊢ x = HMul.hMul (α := K) (star (↑√((re : (a : K) → ℝ) x) : K)) (↑√((re : (a : K) → ℝ) x) : K)

Tactic:
simp [ext_iff (K := K), h.1, h.2]

Premises used: RCLike.ext_iff, And.right, And.left
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
refine :
  (∃ (s : K), x = star s * s) →
    LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) x : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) (0 : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) x : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ∃ (s : K), x = star s * s

Tactic:
refine ⟨fun h ↦ ⟨√(re x), by simp [ext_iff (K := K), h.1, h.2]⟩, ?_⟩
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
s : K
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) (star s * s) : ℝ) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) (star s * s) : ℝ) (0 : ℝ)

Tactic:
simp [mul_comm, mul_self_nonneg, add_nonneg]

Premises used: mul_self_nonneg, add_nonneg, mul_comm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ LE.le.{u_1} (α := K) 0 1

Tactic:
simp [@RCLike.le_iff_re_im K]

Premises used: RCLike.le_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
hz : 0 < z
hw : 0 < w
rw :
  ∀
    (hz :
      LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) 0 : ℝ) ((im : (a : K) → ℝ) z : ℝ))
    (hw :
      LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) 0 : ℝ) ((im : (a : K) → ℝ) w : ℝ)),
    LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) (z * w) : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) 0 : ℝ) ((im : (a : K) → ℝ) (z * w) : ℝ)
⊢ 0 < z * w

Tactic:
rw [lt_iff_re_im, map_zero] at hz hw ⊢

Premises used: map_zero, RCLike.lt_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
hz :
  LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) 0 : ℝ) ((im : (a : K) → ℝ) z : ℝ)
hw :
  LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) 0 : ℝ) ((im : (a : K) → ℝ) w : ℝ)
⊢ LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) (z * w) : ℝ) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) 0 : ℝ) ((im : (a : K) → ℝ) (z * w) : ℝ)

Tactic:
simp [mul_re, mul_im, ← hz.2, ← hw.2, mul_pos hz.1 hw.1]

Premises used: mul_pos, And.right, And.left, RCLike.mul_im, RCLike.mul_re
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
hx : 0 ≤ x
y z : K
hyz : x * y < x * z
rw :
  ∀ (hx : LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) x : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) (0 : ℝ)) {y z : K}
    (hyz : x * y < x * z), y < z
⊢ y < z

Tactic:
rw [RCLike.le_iff_re_im, map_zero, map_zero, eq_comm] at hx

Premises used: RCLike.le_iff_re_im, map_zero, eq_comm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
hx : LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) x : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) (0 : ℝ)
y z : K
hyz : x * y < x * z
obtain :
  ∀ (r : ℝ)
    (hx :
      LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) (↑r : K) : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑r : K) : ℝ) (0 : ℝ))
    (hyz : (↑r : K) * y < (↑r : K) * z), y < z
⊢ y < z

Tactic:
obtain ⟨r, rfl⟩ := ((is_real_TFAE x).out 3 1).1 hx.2

Premises used: RCLike.is_real_TFAE, List.TFAE.out, And.right, Iff.mp, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
y z : K
r : ℝ
hx : LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) (↑r : K) : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑r : K) : ℝ) (0 : ℝ)
hyz : (↑r : K) * y < (↑r : K) * z
simp :
  ∀
    (hyz :
      HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) y : ℝ) < HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ) ∧
        (Eq (α := ℝ) ((im : (a : K) → ℝ) y : ℝ) ((im : (a : K) → ℝ) z : ℝ) ∨ r = 0)),
    LT.lt (α := ℝ) ((re : (a : K) → ℝ) y : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) y : ℝ) ((im : (a : K) → ℝ) z : ℝ)
⊢ y < z

Tactic:
simp only [RCLike.lt_iff_re_im (K := K), mul_re, ofReal_re, ofReal_im, zero_mul, sub_zero,
      mul_im, add_zero, mul_eq_mul_left_iff] at hyz ⊢

Premises used: RCLike.ofReal_re, sub_zero, MulZeroClass.zero_mul, mul_eq_mul_left_iff, RCLike.ofReal_im, RCLike.lt_iff_re_im, RCLike.mul_im, RCLike.mul_re, add_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
y z : K
r : ℝ
hx : LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) (↑r : K) : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑r : K) : ℝ) (0 : ℝ)
hyz :
  HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) y : ℝ) < HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ) ∧
    (Eq (α := ℝ) ((im : (a : K) → ℝ) y : ℝ) ((im : (a : K) → ℝ) z : ℝ) ∨ r = 0)
⊢ 0 ≤ r

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
y z : K
r : ℝ
hx : LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) (↑r : K) : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑r : K) : ℝ) (0 : ℝ)
hyz :
  HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) y : ℝ) < HMul.hMul (β := ℝ) r ((re : (a : K) → ℝ) z : ℝ) ∧
    (Eq (α := ℝ) ((im : (a : K) → ℝ) y : ℝ) ((im : (a : K) → ℝ) z : ℝ) ∨ r = 0)
refine : ¬r = 0
⊢ LT.lt (α := ℝ) ((re : (a : K) → ℝ) y : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) y : ℝ) ((im : (a : K) → ℝ) z : ℝ)

Tactic:
refine ⟨lt_of_mul_lt_mul_of_nonneg_left hyz.1 <| by simpa using hx, hyz.2.resolve_right ?_⟩
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
y z : K
hx : LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) (↑0 : K) : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑0 : K) : ℝ) (0 : ℝ)
hyz :
  HMul.hMul (α := ℝ) (β := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) y : ℝ) <
      HMul.hMul (α := ℝ) (β := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧
    (Eq (α := ℝ) ((im : (a : K) → ℝ) y : ℝ) ((im : (a : K) → ℝ) z : ℝ) ∨ Eq (α := ℝ) 0 0)
⊢ False

Tactic:
simp at hyz
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
hr : 0 < r
a b : K
hab : a < b
⊢ r • a < r • b

Tactic:
simpa [RCLike.lt_iff_re_im (K := K), smul_re, smul_im, hr, hr.ne'] using hab

Premises used: RCLike.smul_re, RCLike.smul_im, LT.lt.ne', RCLike.lt_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : K
ha : 0 < a
r₁ r₂ : ℝ
hr : r₁ < r₂
⊢ LT.lt (α := ℝ) ((re : (a : K) → ℝ) 0 : ℝ) ((re : (a : K) → ℝ) a : ℝ)

Tactic:
obtain ⟨hare, haim⟩ := RCLike.lt_iff_re_im.1 ha

Premises used: RCLike.lt_iff_re_im, Iff.mp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : K
ha : 0 < a
r₁ r₂ : ℝ
hr : r₁ < r₂
hare : LT.lt (α := ℝ) ((re : (a : K) → ℝ) 0 : ℝ) ((re : (a : K) → ℝ) a : ℝ)
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) 0 : ℝ) ((im : (a : K) → ℝ) a : ℝ)

Tactic:
obtain ⟨hare, haim⟩ := RCLike.lt_iff_re_im.1 ha

Premises used: RCLike.lt_iff_re_im, Iff.mp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : K
ha : 0 < a
r₁ r₂ : ℝ
hr : r₁ < r₂
hare : LT.lt (α := ℝ) ((re : (a : K) → ℝ) 0 : ℝ) ((re : (a : K) → ℝ) a : ℝ)
haim : Eq (α := ℝ) ((im : (a : K) → ℝ) 0 : ℝ) ((im : (a : K) → ℝ) a : ℝ)
⊢ r₁ • a < r₂ • a

Tactic:
simp_all [RCLike.lt_iff_re_im (K := K), smul_re, smul_im]

Premises used: RCLike.smul_re, RCLike.smul_im, RCLike.lt_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
z : K
simp :
  0 < HMul.hMul (β := ℝ) x ((re : (a : K) → ℝ) z : ℝ) ∧ HMul.hMul (β := ℝ) x ((im : (a : K) → ℝ) z : ℝ) = 0 ↔
    x < 0 ∧ LT.lt (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∨
      0 < x ∧ LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
⊢ 0 < (↑x : K) * z ↔ x < 0 ∧ z < 0 ∨ 0 < x ∧ 0 < z

Tactic:
simp only [pos_iff (K := K), neg_iff (K := K), re_ofReal_mul, im_ofReal_mul]

Premises used: RCLike.pos_iff, RCLike.neg_iff, RCLike.im_ofReal_mul, RCLike.re_ofReal_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
z : K
inl :
  ∀ (hx : x < 0),
    0 < HMul.hMul (β := ℝ) x ((re : (a : K) → ℝ) z : ℝ) ∧ HMul.hMul (β := ℝ) x ((im : (a : K) → ℝ) z : ℝ) = 0 ↔
      x < 0 ∧ LT.lt (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∨
        0 < x ∧ LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
inr :
  ∀ (hx : x = 0),
    0 < HMul.hMul (β := ℝ) x ((re : (a : K) → ℝ) z : ℝ) ∧ HMul.hMul (β := ℝ) x ((im : (a : K) → ℝ) z : ℝ) = 0 ↔
      x < 0 ∧ LT.lt (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∨
        0 < x ∧ LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
inr₁ :
  ∀ (hx : 0 < x),
    0 < HMul.hMul (β := ℝ) x ((re : (a : K) → ℝ) z : ℝ) ∧ HMul.hMul (β := ℝ) x ((im : (a : K) → ℝ) z : ℝ) = 0 ↔
      x < 0 ∧ LT.lt (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∨
        0 < x ∧ LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
⊢ 0 < HMul.hMul (β := ℝ) x ((re : (a : K) → ℝ) z : ℝ) ∧ HMul.hMul (β := ℝ) x ((im : (a : K) → ℝ) z : ℝ) = 0 ↔
    x < 0 ∧ LT.lt (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∨
      0 < x ∧ LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
obtain hx | hx | hx := lt_trichotomy x 0

Premises used: OfNat.ofNat, lt_trichotomy