awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 < x - a ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₁ : a < x ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
⊢ 0 < (x - a) * (x - b) ↔ x < a ∨ b < x
have rw₂ : a < x ∧ b < x ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
Tactic: rw [mul_pos_iff, sub_pos, sub_pos, sub_neg, sub_neg, and_iff_right_of_imp h.trans_lt,
    and_iff_left_of_imp h.trans_lt', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 < x - a ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₁ : a < x ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₂ : a < x ∧ b < x ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
⊢ 0 < (x - a) * (x - b) ↔ x < a ∨ b < x
have rw₃ : a < x ∧ b < x ∨ x < a ∧ x - b < 0 ↔ x < a ∨ b < x
Tactic: rw [mul_pos_iff, sub_pos, sub_pos, sub_neg, sub_neg, and_iff_right_of_imp h.trans_lt,
    and_iff_left_of_imp h.trans_lt', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 < x - a ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₁ : a < x ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₂ : a < x ∧ b < x ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₃ : a < x ∧ b < x ∨ x < a ∧ x - b < 0 ↔ x < a ∨ b < x
⊢ 0 < (x - a) * (x - b) ↔ x < a ∨ b < x
have rw₄ : a < x ∧ b < x ∨ x < a ∧ x < b ↔ x < a ∨ b < x
Tactic: rw [mul_pos_iff, sub_pos, sub_pos, sub_neg, sub_neg, and_iff_right_of_imp h.trans_lt,
    and_iff_left_of_imp h.trans_lt', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 < x - a ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₁ : a < x ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₂ : a < x ∧ b < x ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₃ : a < x ∧ b < x ∨ x < a ∧ x - b < 0 ↔ x < a ∨ b < x
rw₄ : a < x ∧ b < x ∨ x < a ∧ x < b ↔ x < a ∨ b < x
⊢ 0 < (x - a) * (x - b) ↔ x < a ∨ b < x
have rw₅ : b < x ∨ x < a ∧ x < b ↔ x < a ∨ b < x
Tactic: rw [mul_pos_iff, sub_pos, sub_pos, sub_neg, sub_neg, and_iff_right_of_imp h.trans_lt,
    and_iff_left_of_imp h.trans_lt', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 < x - a ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₁ : a < x ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₂ : a < x ∧ b < x ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₃ : a < x ∧ b < x ∨ x < a ∧ x - b < 0 ↔ x < a ∨ b < x
rw₄ : a < x ∧ b < x ∨ x < a ∧ x < b ↔ x < a ∨ b < x
rw₅ : b < x ∨ x < a ∧ x < b ↔ x < a ∨ b < x
⊢ 0 < (x - a) * (x - b) ↔ x < a ∨ b < x
have rw₆ : b < x ∨ x < a ↔ x < a ∨ b < x
Tactic: rw [mul_pos_iff, sub_pos, sub_pos, sub_neg, sub_neg, and_iff_right_of_imp h.trans_lt,
    and_iff_left_of_imp h.trans_lt', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
rw : 0 < x - a ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₁ : a < x ∧ 0 < x - b ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₂ : a < x ∧ b < x ∨ x - a < 0 ∧ x - b < 0 ↔ x < a ∨ b < x
rw₃ : a < x ∧ b < x ∨ x < a ∧ x - b < 0 ↔ x < a ∨ b < x
rw₄ : a < x ∧ b < x ∨ x < a ∧ x < b ↔ x < a ∨ b < x
rw₅ : b < x ∨ x < a ∧ x < b ↔ x < a ∨ b < x
rw₆ : b < x ∨ x < a ↔ x < a ∨ b < x
⊢ 0 < (x - a) * (x - b) ↔ x < a ∨ b < x
have rw₇ : x < a ∨ b < x ↔ x < a ∨ b < x
Tactic: rw [mul_pos_iff, sub_pos, sub_pos, sub_neg, sub_neg, and_iff_right_of_imp h.trans_lt,
    and_iff_left_of_imp h.trans_lt', or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : LinearOrder R
a b : R
inst_2 : MulPosStrictMono R
inst_3 : PosMulStrictMono R
inst_4 : AddLeftMono R
x : R
h : a ≤ b
⊢ (x - a) * (x - b) < 0 ↔ a < x ∧ x < b
have rw : b < x ∧ x < a → a < x ∧ x < b
Tactic: rw [mul_neg_iff, sub_pos, sub_pos, sub_neg, sub_neg, or_iff_left_iff_imp, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Rat (goal)
Goal:
m : ℕ
s : Bool
e : ℕ
⊢ 0 ≤ Rat.ofScientific m s e
have rw : 0 ≤ if s = true then normalize (↑m : ℤ) (HPow.hPow (α := ℕ) 10 e) sorry else (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ)
Tactic: rw [Rat.ofScientific]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Rat (goal)
Goal:
m : ℕ
s : Bool
e : ℕ
⊢ 0 ≤ if s = true then normalize (↑m : ℤ) (HPow.hPow (α := ℕ) 10 e) ⋯ else (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ)
have false : 0 ≤ if false = true then normalize (↑m : ℤ) (HPow.hPow (α := ℕ) 10 e) sorry else (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Rat (goal)
Goal:
m : ℕ
s : Bool
e : ℕ
false :
  0 ≤ if Bool.false = true then normalize (↑m : ℤ) (HPow.hPow (α := ℕ) 10 e) ⋯ else (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ)
⊢ 0 ≤ if s = true then normalize (↑m : ℤ) (HPow.hPow (α := ℕ) 10 e) ⋯ else (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ)
have true : 0 ≤ if true = true then normalize (↑m : ℤ) (HPow.hPow (α := ℕ) 10 e) sorry else (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Rat (goal)
Goal:
a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ a /. b ≤ c /. d ↔ a * d ≤ c * b
have rw : 0 ≤ c /. d - a /. b ↔ 0 ≤ c * b - a * d
Tactic: rw [Rat.le_iff_sub_nonneg, ← Int.sub_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Rat (goal)
Goal:
a : ℤ
ha : a ≤ 0
b : ℕ
⊢ mkRat a b ≤ 0
have inl : mkRat a 0 ≤ 0
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Rat (goal)
Goal:
a : ℤ
ha : a ≤ 0
b : ℕ
inl : mkRat a 0 ≤ 0
⊢ mkRat a b ≤ 0
have inr : ∀ (hb : b ≠ 0), mkRat a b ≤ 0
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Rat (goal)
Goal:
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) < HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ↔ a * d < c * b
have simp : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ∧
    ¬HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ↔
  a * d ≤ c * b ∧ ¬c * b ≤ a * d
Tactic: simp only [lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Rat (goal)
Goal:
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ∧
      ¬HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ↔
    a * d ≤ c * b ∧ ¬c * b ≤ a * d
have h₁ : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ↔ a * d ≤ c * b
Tactic: apply and_congr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Rat (goal)
Goal:
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
h₁ : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ↔ a * d ≤ c * b
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ∧
      ¬HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ↔
    a * d ≤ c * b ∧ ¬c * b ≤ a * d
have h₂ : ¬HDiv.hDiv (α := ℚ) (↑c : ℚ) (↑d : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ↔ ¬c * b ≤ a * d
Tactic: apply and_congr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Rat (goal)
Goal:
q : ℚ
⊢ |q| = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }
have refine_1 : |q|.num = { num := |q.num|, den := q.den, den_nz := sorry, reduced := sorry }.num
Tactic: refine ext ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Rat (goal)
Goal:
q : ℚ
refine_1 : |q|.num = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.num
⊢ |q| = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }
have refine_2 : |q|.den = { num := |q.num|, den := q.den, den_nz := sorry, reduced := sorry }.den
Tactic: refine ext ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Rat (goal)
Goal:
q : ℚ
⊢ |q|.num = |q.num|
have rw : { num := |q.num|, den := q.den, den_nz := sorry, reduced := sorry : ℚ }.num = |q.num|
Tactic: rw [abs_def']
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Rat (goal)
Goal:
q : ℚ
⊢ |q|.den = q.den
have rw : { num := |q.num|, den := q.den, den_nz := sorry, reduced := sorry : ℚ }.den = q.den
Tactic: rw [abs_def']
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Units (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
⊢ Subgroup.index (G := Rˣ) (posSubgroup R) = 2
have rw : ∃ (a : Rˣ),
  ∀ (b : Rˣ),
    Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (b * a))
      (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) b)
Tactic: rw [Subgroup.index_eq_two_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Units (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
⊢ ∃ (a : Rˣ),
    ∀ (b : Rˣ),
      Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (b * a))
        (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) b)
have refine : ∀ (a : Rˣ),
  Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (a * -1)) (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) a)
Tactic: refine ⟨-1, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Units (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : Rˣ
⊢ Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (a * -1)) (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) a)
have inl : ∀ (h : (↑a : R) < 0),
  Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (a * -1)) (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) a)
Tactic: obtain h | h := lt_or_gt_of_ne a.ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Units (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : Rˣ
inl :
  ∀ (h : (↑a : R) < 0),
    Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (a * -1))
      (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) a)
⊢ Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (a * -1)) (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) a)
have inr : ∀ (h : 0 < (↑a : R)),
  Xor (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) (a * -1)) (Membership.mem (γ := Subgroup Rˣ) (posSubgroup R) a)
Tactic: obtain h | h := lt_or_gt_of_ne a.ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : WithTop α
h : a ≠ 0
⊢ a * ⊤ = ⊤
have rw : Eq.{u_1 + 1} (α := WithTop α) (if a = 0 then 0 else ⊤) ⊤
Tactic: rw [mul_top', if_neg h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : WithTop α
h : a ≠ 0
rw : Eq.{u_1 + 1} (α := WithTop α) (if a = 0 then 0 else ⊤) ⊤
⊢ a * ⊤ = ⊤
have rw₁ : Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤
Tactic: rw [mul_top', if_neg h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
hb : b ≠ 0
⊢ ⊤ * b = ⊤
have rw : Eq.{u_1 + 1} (α := WithTop α) (if b = 0 then 0 else ⊤) ⊤
Tactic: rw [top_mul', if_neg hb]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
hb : b ≠ 0
rw : Eq.{u_1 + 1} (α := WithTop α) (if b = 0 then 0 else ⊤) ⊤
⊢ ⊤ * b = ⊤
have rw₁ : Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤
Tactic: rw [top_mul', if_neg hb]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
⊢ a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) a b
have top : ⊤ * b = if Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊤ b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
top : ⊤ * b = if Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊤ b
⊢ a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) a b
have coe : ∀ (a : α),
  (↑a : WithTop α) * b = if (↑a : WithTop α) = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithTop α) b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
⊢ ⊤ * b = if Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊤ b
have top : HMul.hMul (α := WithTop α) ⊤ ⊤ =
  if Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 ∨ Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 then 0
  else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊤ ⊤
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
top :
  HMul.hMul (α := WithTop α) ⊤ ⊤ =
    if Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 ∨ Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊤ ⊤
⊢ ⊤ * b = if Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊤ b
have top₁ : ∀ (a : α),
  ⊤ * (↑a : WithTop α) =
    if Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 ∨ (↑a : WithTop α) = 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊤ (↑a : WithTop α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
a : α
⊢ (↑a : WithTop α) * b = if (↑a : WithTop α) = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithTop α) b
have coe : (↑a : WithTop α) * ⊤ =
  if (↑a : WithTop α) = 0 ∨ Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 then 0
  else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithTop α) ⊤
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
a : α
coe :
  (↑a : WithTop α) * ⊤ =
    if (↑a : WithTop α) = 0 ∨ Eq.{u_1 + 1} (α := WithTop α) ⊤ 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithTop α) ⊤
⊢ (↑a : WithTop α) * b = if (↑a : WithTop α) = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithTop α) b
have coe₁ : ∀ (a_1 : α),
  (↑a : WithTop α) * (↑a_1 : WithTop α) =
    if (↑a : WithTop α) = 0 ∨ (↑a_1 : WithTop α) = 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithTop α) (↑a_1 : WithTop α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
⊢ a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
have rw : Eq (α := WithTop α) (if a = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) a b) ⊤ ↔
  a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
Tactic: rw [mul_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊤ * (↑b : WithTop α) = Option.bind ⊤ fun (a : α) ↦ Option.some (a * b)
have simp : Eq.{u_1 + 1} (α := WithTop α) ⊤ (Option.bind ⊤ fun (a : α) ↦ Option.some (a * b))
Tactic: simp [top_mul, hb]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : a ≠ 0
⊢ (↑a : WithTop α) * ⊤ = Option.bind ⊤ fun (b : α) ↦ Option.some (a * b)
have simp : Eq.{u_1 + 1} (α := WithTop α) ⊤ (Option.bind ⊤ fun (b : α) ↦ Option.some (a * b))
Tactic: simp [ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have pos : ∀ (ha : a = 0), untopD 0 (a * b) = untopD 0 a * untopD 0 b
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
pos : ∀ (ha : a = 0), untopD 0 (a * b) = untopD 0 a * untopD 0 b
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have neg : ∀ (ha : ¬a = 0), untopD 0 (a * b) = untopD 0 a * untopD 0 b
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : a = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have pos : untopD 0 (0 * b) = untopD 0 0 * untopD 0 b
Tactic: rw [ha, zero_mul, ← coe_zero, untopD_coe, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : a = 0
pos : untopD 0 (0 * b) = untopD 0 0 * untopD 0 b
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have pos₁ : untopD 0 0 = untopD 0 0 * untopD 0 b
Tactic: rw [ha, zero_mul, ← coe_zero, untopD_coe, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : a = 0
pos : untopD 0 (0 * b) = untopD 0 0 * untopD 0 b
pos₁ : untopD 0 0 = untopD 0 0 * untopD 0 b
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have pos₂ : untopD 0 (↑0 : WithTop α) = untopD 0 (↑0 : WithTop α) * untopD 0 b
Tactic: rw [ha, zero_mul, ← coe_zero, untopD_coe, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : a = 0
pos : untopD 0 (0 * b) = untopD 0 0 * untopD 0 b
pos₁ : untopD 0 0 = untopD 0 0 * untopD 0 b
pos₂ : untopD 0 (↑0 : WithTop α) = untopD 0 (↑0 : WithTop α) * untopD 0 b
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have pos₃ : 0 = 0 * untopD 0 b
Tactic: rw [ha, zero_mul, ← coe_zero, untopD_coe, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : a = 0
pos : untopD 0 (0 * b) = untopD 0 0 * untopD 0 b
pos₁ : untopD 0 0 = untopD 0 0 * untopD 0 b
pos₂ : untopD 0 (↑0 : WithTop α) = untopD 0 (↑0 : WithTop α) * untopD 0 b
pos₃ : 0 = 0 * untopD 0 b
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have pos₄ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [ha, zero_mul, ← coe_zero, untopD_coe, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have pos : ∀ (hb : b = 0), untopD 0 (a * b) = untopD 0 a * untopD 0 b
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
pos : ∀ (hb : b = 0), untopD 0 (a * b) = untopD 0 a * untopD 0 b
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have neg : ∀ (hb : ¬b = 0), untopD 0 (a * b) = untopD 0 a * untopD 0 b
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have pos : untopD 0 (a * 0) = untopD 0 a * untopD 0 0
Tactic: rw [hb, mul_zero, ← coe_zero, untopD_coe, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
pos : untopD 0 (a * 0) = untopD 0 a * untopD 0 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have pos₁ : untopD 0 0 = untopD 0 a * untopD 0 0
Tactic: rw [hb, mul_zero, ← coe_zero, untopD_coe, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
pos : untopD 0 (a * 0) = untopD 0 a * untopD 0 0
pos₁ : untopD 0 0 = untopD 0 a * untopD 0 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have pos₂ : untopD 0 (↑0 : WithTop α) = untopD 0 a * untopD 0 (↑0 : WithTop α)
Tactic: rw [hb, mul_zero, ← coe_zero, untopD_coe, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
pos : untopD 0 (a * 0) = untopD 0 a * untopD 0 0
pos₁ : untopD 0 0 = untopD 0 a * untopD 0 0
pos₂ : untopD 0 (↑0 : WithTop α) = untopD 0 a * untopD 0 (↑0 : WithTop α)
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have pos₃ : 0 = untopD 0 a * 0
Tactic: rw [hb, mul_zero, ← coe_zero, untopD_coe, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
pos : untopD 0 (a * 0) = untopD 0 a * untopD 0 0
pos₁ : untopD 0 0 = untopD 0 a * untopD 0 0
pos₂ : untopD 0 (↑0 : WithTop α) = untopD 0 a * untopD 0 (↑0 : WithTop α)
pos₃ : 0 = untopD 0 a * 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have pos₄ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [hb, mul_zero, ← coe_zero, untopD_coe, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : ¬b = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have neg : ∀ (ha : ¬Eq.{u_1 + 1} (α := WithTop α) ⊤ 0), untopD 0 (⊤ * b) = untopD 0 ⊤ * untopD 0 b
Tactic: cases a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : ¬b = 0
neg : ∀ (ha : ¬Eq.{u_1 + 1} (α := WithTop α) ⊤ 0), untopD 0 (⊤ * b) = untopD 0 ⊤ * untopD 0 b
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
have neg₁ : ∀ (a : α) (ha : ¬(↑a : WithTop α) = 0), untopD 0 ((↑a : WithTop α) * b) = untopD 0 (↑a : WithTop α) * untopD 0 b
Tactic: cases a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
hb : ¬b = 0
ha : ¬Eq.{u_1 + 1} (α := WithTop α) ⊤ 0
⊢ untopD 0 (⊤ * b) = untopD 0 ⊤ * untopD 0 b
have neg : untopD 0 ⊤ = untopD 0 ⊤ * untopD 0 b
Tactic: rw [top_mul hb, untopD_top, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
hb : ¬b = 0
ha : ¬Eq.{u_1 + 1} (α := WithTop α) ⊤ 0
neg : untopD 0 ⊤ = untopD 0 ⊤ * untopD 0 b
⊢ untopD 0 (⊤ * b) = untopD 0 ⊤ * untopD 0 b
have neg₁ : 0 = 0 * untopD 0 b
Tactic: rw [top_mul hb, untopD_top, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
hb : ¬b = 0
ha : ¬Eq.{u_1 + 1} (α := WithTop α) ⊤ 0
neg : untopD 0 ⊤ = untopD 0 ⊤ * untopD 0 b
neg₁ : 0 = 0 * untopD 0 b
⊢ untopD 0 (⊤ * b) = untopD 0 ⊤ * untopD 0 b
have neg₂ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [top_mul hb, untopD_top, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithTop α
hb : ¬b = 0
a : α
ha : ¬(↑a : WithTop α) = 0
⊢ untopD 0 ((↑a : WithTop α) * b) = untopD 0 (↑a : WithTop α) * untopD 0 b
have neg : ∀ (hb : ¬Eq.{u_1 + 1} (α := WithTop α) ⊤ 0), untopD 0 ((↑a : WithTop α) * ⊤) = untopD 0 (↑a : WithTop α) * untopD 0 ⊤
Tactic: cases b
Cleared hypotheses: b, hb