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
z w : K
mp :
  (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)) ∧
      z ≠ w →
    (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Ne (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)
⊢ (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)) ∧
      z ≠ w ↔
    (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Ne (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)
have mpr : (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
      Ne (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ) →
  (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)) ∧
    z ≠ w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ 0 ≤ z ↔ ∃ x ≥ 0, (↑x : K) = z
have 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 : ℝ)
Tactic: simp_rw [nonneg_iff (K := K), ext_iff (K := K)]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ 0 < z ↔ ∃ x > 0, (↑x : K) = z
have 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 : ℝ)
Tactic: simp_rw [pos_iff (K := K), ext_iff (K := K)]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ z ≤ 0 ↔ ∃ x ≤ 0, (↑x : K) = z
have 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 : ℝ)
Tactic: simp_rw [nonpos_iff (K := K), ext_iff (K := K)]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ z < 0 ↔ ∃ x < 0, (↑x : K) = z
have 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 : ℝ)
Tactic: simp_rw [neg_iff (K := K), ext_iff (K := K)]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x y : ℝ
⊢ LE.le.{u_1} (α := K) (↑x : K) (↑y : K) ↔ x ≤ y
have 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
Tactic: rw [le_iff_re_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x y : ℝ
⊢ LT.lt.{u_1} (α := K) (↑x : K) (↑y : K) ↔ x < y
have 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
Tactic: rw [lt_iff_re_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
⊢ LE.le.{u_1} (α := K) 0 (↑x : K) ↔ 0 ≤ x
have rw : LE.le.{u_1} (α := K) (↑0 : K) (↑x : K) ↔ 0 ≤ x
Tactic: rw [← ofReal_zero, ofReal_le_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
rw : LE.le.{u_1} (α := K) (↑0 : K) (↑x : K) ↔ 0 ≤ x
⊢ LE.le.{u_1} (α := K) 0 (↑x : K) ↔ 0 ≤ x
have rw₁ : 0 ≤ x ↔ 0 ≤ x
Tactic: rw [← ofReal_zero, ofReal_le_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
⊢ LE.le.{u_1} (α := K) (↑x : K) 0 ↔ x ≤ 0
have rw : LE.le.{u_1} (α := K) (↑x : K) (↑0 : K) ↔ x ≤ 0
Tactic: rw [← ofReal_zero, ofReal_le_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
rw : LE.le.{u_1} (α := K) (↑x : K) (↑0 : K) ↔ x ≤ 0
⊢ LE.le.{u_1} (α := K) (↑x : K) 0 ↔ x ≤ 0
have rw₁ : x ≤ 0 ↔ x ≤ 0
Tactic: rw [← ofReal_zero, ofReal_le_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
⊢ LT.lt.{u_1} (α := K) 0 (↑x : K) ↔ 0 < x
have rw : LT.lt.{u_1} (α := K) (↑0 : K) (↑x : K) ↔ 0 < x
Tactic: rw [← ofReal_zero, ofReal_lt_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
rw : LT.lt.{u_1} (α := K) (↑0 : K) (↑x : K) ↔ 0 < x
⊢ LT.lt.{u_1} (α := K) 0 (↑x : K) ↔ 0 < x
have rw₁ : 0 < x ↔ 0 < x
Tactic: rw [← ofReal_zero, ofReal_lt_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
⊢ LT.lt.{u_1} (α := K) (↑x : K) 0 ↔ x < 0
have rw : LT.lt.{u_1} (α := K) (↑x : K) (↑0 : K) ↔ x < 0
Tactic: rw [← ofReal_zero, ofReal_lt_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
rw : LT.lt.{u_1} (α := K) (↑x : K) (↑0 : K) ↔ x < 0
⊢ LT.lt.{u_1} (α := K) (↑x : K) 0 ↔ x < 0
have rw₁ : x < 0 ↔ x < 0
Tactic: rw [← ofReal_zero, ofReal_lt_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ ‖z‖ ≤ (re : (a : K) → ℝ) z ↔ z = (↑‖z‖ : K)
have refine_1 : ∀ (h : ‖z‖ ≤ (re : (a : K) → ℝ) z), z = (↑‖z‖ : K)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
refine_1 : ∀ (h : ‖z‖ ≤ (re : (a : K) → ℝ) z), z = (↑‖z‖ : K)
⊢ ‖z‖ ≤ (re : (a : K) → ℝ) z ↔ z = (↑‖z‖ : K)
have refine_2 : ∀ (h : z = (↑‖z‖ : K)), ‖z‖ ≤ (re : (a : K) → ℝ) z
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (hypothesis)
Goal:
K : Type u_1
inst : RCLike K
z : K
h : ‖z‖ ≤ (re : (a : K) → ℝ) z
⊢ z = (↑‖z‖ : K)
have h' : ‖z‖ = (re : (a : K) → ℝ) z
Tactic: have h' : ‖z‖ = re z := (le_antisymm (re_le_norm z) h).symm
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
h : ‖z‖ ≤ (re : (a : K) → ℝ) z
h' : ‖z‖ = (re : (a : K) → ℝ) z
⊢ z = (↑‖z‖ : K)
have refine_1 : z = (↑((re : (a : K) → ℝ) z) : K)
Tactic: rw [h', re_eq_self_of_le h]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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)
⊢ z = (↑‖z‖ : K)
have refine_1₁ : z = z
Tactic: rw [h', re_eq_self_of_le h]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
h : z = (↑‖z‖ : K)
⊢ ‖z‖ ≤ (re : (a : K) → ℝ) z
have refine_2 : norm.{u_1} (E := K) (↑‖z‖ : K) ≤ (re : (a : K) → ℝ) (↑‖z‖ : K)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
hx : 0 ≤ x
⊢ (↑‖x‖ : K) = x
have 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
Tactic: rw [eq_comm, ← norm_le_re_iff_eq_norm, ← sqrt_normSq_eq_norm, normSq_apply]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (hypothesis)
Goal:
K : Type u_1
inst : RCLike K
x y : K
h : x ≤ y
⊢ LE.le (α := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (hypothesis)
Goal:
K : Type u_1
inst : RCLike K
z : K
hz : 0 < z
⊢ 0 < z⁻¹
have hz₁ : ∃ x > 0, (↑x : K) = z
Tactic: rw [pos_iff_exists_ofReal] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
hz : ∃ x > 0, (↑x : K) = z
⊢ 0 < z⁻¹
have obtain : ∀ (x : ℝ) (hx : x > 0) (hx' : (↑x : K) = z), 0 < z⁻¹
Tactic: obtain ⟨x, hx, hx'⟩ := hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
x : ℝ
hx : x > 0
hx' : (↑x : K) = z
⊢ 0 < z⁻¹
have rw : 0 < x⁻¹
Tactic: rw [← hx', ← ofReal_inv, ofReal_pos]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ 0 < z⁻¹ ↔ 0 < z
have refine : ∀ (h : 0 < z⁻¹), 0 < z
Tactic: refine ⟨fun h => ?_, fun h => RCLike.inv_pos_of_pos h⟩
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
h : 0 < z⁻¹
⊢ 0 < z
have rw : 0 < z⁻¹⁻¹
Tactic: rw [← inv_inv z]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x y : K
hxy : x ≤ y
z : K
⊢ z + x ≤ z + y
have 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) : ℝ)
Tactic: rw [RCLike.le_iff_re_im] at *
Cleared hypotheses: hxy, z
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
⊢ 0 ≤ x ↔ ∃ (s : K), x = star s * s
have rw : LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) x : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) (0 : ℝ) ↔
  ∃ (s : K), x = star s * s
Tactic: rw [nonneg_iff]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) x : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ∃ (s : K), x = star s * s
have refine : (∃ (s : K), x = star s * s) →
  LE.le (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) x : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) (0 : ℝ)
Tactic: refine ⟨fun h ↦ ⟨√(re x), by simp [ext_iff (K := K), h.1, h.2]⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z w : K
hz : 0 < z
hw : 0 < w
⊢ 0 < z * w
have 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) : ℝ)
Tactic: rw [lt_iff_re_im, map_zero] at hz hw ⊢
Cleared hypotheses: hz, hw
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
hx : 0 ≤ x
y z : K
hyz : x * y < x * z
⊢ y < z
have 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
Tactic: rw [RCLike.le_iff_re_im, map_zero, map_zero, eq_comm] at hx
Cleared hypotheses: hx, y, z, hyz
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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
⊢ y < z
have 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
Tactic: obtain ⟨r, rfl⟩ := ((is_real_TFAE x).out 3 1).1 hx.2
Cleared hypotheses: x, hx, hyz
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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
⊢ y < z
have 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 : ℝ)
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 ⊢
Cleared hypotheses: hyz
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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)
⊢ LT.lt (α := ℝ) ((re : (a : K) → ℝ) y : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) y : ℝ) ((im : (a : K) → ℝ) z : ℝ)
have refine : ¬r = 0
Tactic: refine ⟨lt_of_mul_lt_mul_of_nonneg_left hyz.1 <| by simpa using hx, hyz.2.resolve_right ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (hypothesis)
Goal:
K : Type u_1
inst : RCLike K
a : K
ha : 0 < a
r₁ r₂ : ℝ
hr : r₁ < r₂
⊢ r₁ • a < r₂ • a
have hare : LT.lt (α := ℝ) ((re : (a : K) → ℝ) 0 : ℝ) ((re : (a : K) → ℝ) a : ℝ)
Tactic: obtain ⟨hare, haim⟩ := RCLike.lt_iff_re_im.1 ha
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (hypothesis)
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 : ℝ)
⊢ r₁ • a < r₂ • a
have haim : Eq (α := ℝ) ((im : (a : K) → ℝ) 0 : ℝ) ((im : (a : K) → ℝ) a : ℝ)
Tactic: obtain ⟨hare, haim⟩ := RCLike.lt_iff_re_im.1 ha
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
z : K
⊢ 0 < (↑x : K) * z ↔ x < 0 ∧ z < 0 ∨ 0 < x ∧ 0 < z
have 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 : ℝ)
Tactic: simp only [pos_iff (K := K), neg_iff (K := K), re_ofReal_mul, im_ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
z : K
⊢ 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 : ℝ)
have 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 : ℝ)
Tactic: obtain hx | hx | hx := lt_trichotomy x 0
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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 : ℝ)
⊢ 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 : ℝ)
have 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 : ℝ)
Tactic: obtain hx | hx | hx := lt_trichotomy x 0
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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 : ℝ)
⊢ 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 : ℝ)
have 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 : ℝ)
Tactic: obtain hx | hx | hx := lt_trichotomy x 0
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
h :
  (fun (x1 x2 : K) ↦ x1 ≤ x2) ((fun (x : { x : K // 0 < x }) (y : K) ↦ (↑x : K) * y) a b)
    ((fun (x : { x : K // 0 < x }) (y : K) ↦ (↑x : K) * y) a c)
⊢ (fun (x1 x2 : K) ↦ x1 ≤ x2) b c
have obtain : ∀ (a' : ℝ) (ha1 : a' > 0) (ha2 : (↑a' : K) = (↑a : K)), b ≤ c
Tactic: obtain ⟨a', ha1, ha2⟩ := pos_iff_exists_ofReal.mp a.2
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
h :
  (fun (x1 x2 : K) ↦ x1 ≤ x2) ((fun (x : { x : K // 0 < x }) (y : K) ↦ (↑x : K) * y) a b)
    ((fun (x : { x : K // 0 < x }) (y : K) ↦ (↑x : K) * y) a c)
a' : ℝ
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
⊢ b ≤ c
have rw : 0 ≤ c - b
Tactic: rw [← sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
h :
  (fun (x1 x2 : K) ↦ x1 ≤ x2) ((fun (x : { x : K // 0 < x }) (y : K) ↦ (↑x : K) * y) a b)
    ((fun (x : { x : K // 0 < x }) (y : K) ↦ (↑x : K) * y) a c)
a' : ℝ
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
⊢ 0 ≤ c - b
have beta_reduce : ∀ (h : (↑a : K) * b ≤ (↑a : K) * c) (a' : ℝ) (ha1 : a' > 0) (ha2 : (↑a' : K) = (↑a : K)), 0 ≤ c - b
Tactic: beta_reduce at h
Cleared hypotheses: h, a', ha1, ha2
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (hypothesis)
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
h : (↑a : K) * b ≤ (↑a : K) * c
a' : ℝ
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
⊢ 0 ≤ c - b
have h₁ : 0 < (↑a' : K) * (c - b) ∨ 0 = (↑a' : K) * (c - b)
Tactic: rw [← ha2, ← sub_nonneg, ← mul_sub, le_iff_lt_or_eq] at h
Cleared hypotheses: h, ha1, ha2
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
a' : ℝ
h : 0 < (↑a' : K) * (c - b) ∨ 0 = (↑a' : K) * (c - b)
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
⊢ 0 ≤ c - b
have inl : ∀ (h : 0 < (↑a' : K) * (c - b)), 0 ≤ c - b
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
a' : ℝ
h : 0 < (↑a' : K) * (c - b) ∨ 0 = (↑a' : K) * (c - b)
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
inl : ∀ (h : 0 < (↑a' : K) * (c - b)), 0 ≤ c - b
⊢ 0 ≤ c - b
have inr : ∀ (h : 0 = (↑a' : K) * (c - b)), 0 ≤ c - b
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (hypothesis)
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
h : 0 < (↑a' : K) * (c - b)
⊢ 0 ≤ c - b
have h₁ : a' < 0 ∧ c - b < 0 ∨ 0 < a' ∧ 0 < c - b
Tactic: rw [ofReal_mul_pos_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
x : K
⊢ norm (E := ℝ) ((reLm : (a : K) → ℝ) x : ℝ) ≤ 1 * ‖x‖
have rw : norm (E := ℝ) ((reLm : (a : K) → ℝ) x : ℝ) ≤ ‖x‖
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
x : K
⊢ norm (E := ℝ) ((imLm : (a : K) → ℝ) x : ℝ) ≤ 1 * ‖x‖
have rw : norm (E := ℝ) ((imLm : (a : K) → ℝ) x : ℝ) ≤ ‖x‖
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x y : K
⊢ edist (α := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ) ≤ (↑1 : ENNReal) * edist x y
have simp : ‖HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)‖ₑ ≤ ‖x - y‖ₑ
Tactic: simp only [ENNReal.coe_one, one_mul, edist_eq_enorm_sub]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x y : K
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)‖ₑ =
    enorm (E := ℝ) ((re : (a : K) → ℝ) (x - y) : ℝ)
have rw : ‖HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)‖ₑ =
  ‖HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)‖ₑ
Tactic: rw [map_sub re x y]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x y : K
⊢ enorm (E := ℝ) ((re : (a : K) → ℝ) (x - y) : ℝ) ≤ ‖x - y‖ₑ
have rw : norm (E := ℝ) ((re : (a : K) → ℝ) (x - y) : ℝ) ≤ ‖x - y‖
Tactic: rw [enorm_le_iff_norm_le]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x y : K
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)‖ₑ ≤ ‖x - y‖ₑ
have calc : ‖HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)‖ₑ =
  enorm (E := ℝ) ((re : (a : K) → ℝ) (x - y) : ℝ)
Tactic: calc ‖re x - re y‖ₑ
  _ = ‖re (x - y)‖ₑ := by rw [map_sub re x y]
  _ ≤ ‖x - y‖ₑ := by rw [enorm_le_iff_norm_le]; exact norm_re_le_norm (x - y)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x y : K
calc :
  ‖HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)‖ₑ =
    enorm (E := ℝ) ((re : (a : K) → ℝ) (x - y) : ℝ)
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)‖ₑ ≤ ‖x - y‖ₑ
have calc₁ : enorm (E := ℝ) ((re : (a : K) → ℝ) (x - y) : ℝ) ≤ ‖x - y‖ₑ
Tactic: calc ‖re x - re y‖ₑ
  _ = ‖re (x - y)‖ₑ := by rw [map_sub re x y]
  _ ≤ ‖x - y‖ₑ := by rw [enorm_le_iff_norm_le]; exact norm_re_le_norm (x - y)