awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
c : WithTop α
hc : c ≠ 0
a : α
ha : (↑a : WithTop α) ≠ 0
b : α
hb : (↑b : WithTop α) ≠ 0
⊢ (↑a : WithTop α) * (↑b : WithTop α) * c = (↑a : WithTop α) * ((↑b : WithTop α) * c)
have inr : ∀ (hc : Ne.{u_1 + 1} (α := WithTop α) ⊤ 0),
  (↑a : WithTop α) * (↑b : WithTop α) * ⊤ = (↑a : WithTop α) * ((↑b : WithTop α) * ⊤)
Tactic: cases c with
    | top =>
      rw [mul_top hb, mul_top ha]
      rw [← coe_zero, ne_eq, coe_eq_coe] at ha hb
      simp [ha, hb]
    | coe c => simp only [← coe_mul, mul_assoc]
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : SemigroupWithZero α
inst_2 : NoZeroDivisors α
c : WithTop α
hc : c ≠ 0
a : α
ha : (↑a : WithTop α) ≠ 0
b : α
hb : (↑b : WithTop α) ≠ 0
inr :
  ∀ (hc : Ne.{u_1 + 1} (α := WithTop α) ⊤ 0),
    (↑a : WithTop α) * (↑b : WithTop α) * ⊤ = (↑a : WithTop α) * ((↑b : WithTop α) * ⊤)
⊢ (↑a : WithTop α) * (↑b : WithTop α) * c = (↑a : WithTop α) * ((↑b : WithTop α) * c)
have inr₁ : ∀ (c : α) (hc : (↑c : WithTop α) ≠ 0),
  (↑a : WithTop α) * (↑b : WithTop α) * (↑c : WithTop α) = (↑a : WithTop α) * ((↑b : WithTop α) * (↑c : WithTop α))
Tactic: cases c with
    | top =>
      rw [mul_top hb, mul_top ha]
      rw [← coe_zero, ne_eq, coe_eq_coe] at ha hb
      simp [ha, hb]
    | coe c => simp only [← coe_mul, mul_assoc]
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
⊢ Eq (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) a, 0 with
      | Option.some a, n => (↑(a ^ n) : WithTop α)
      | none, 0 => 1
      | none, _n.succ => ⊤ :
      WithTop α)
    (1 : WithTop α)
have top : Eq.{u_1 + 1} (α := WithTop α)
  (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤ :
    WithTop α)
  (1 : WithTop α)
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 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
top :
  Eq.{u_1 + 1} (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
      | Option.some a, n => (↑(a ^ n) : WithTop α)
      | none, 0 => 1
      | none, _n.succ => ⊤ :
      WithTop α)
    (1 : WithTop α)
⊢ Eq (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) a, 0 with
      | Option.some a, n => (↑(a ^ n) : WithTop α)
      | none, 0 => 1
      | none, _n.succ => ⊤ :
      WithTop α)
    (1 : WithTop α)
have coe : ∀ (a : α),
  Eq (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), 0 with
      | Option.some a, n => (↑(a ^ n) : WithTop α)
      | none, 0 => 1
      | none, _n.succ => ⊤ :
      WithTop α)
    (1 : WithTop α)
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 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n_1 n : ℕ
a : WithTop α
⊢ (match (motive := WithTop α → ℕ → WithTop α) a, n + 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, n with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      a
have zero : (match (motive := WithTop α → ℕ → WithTop α) a, HAdd.hAdd (α := ℕ) 0 1 with
  | Option.some a, n => (↑(a ^ n) : WithTop α)
  | none, 0 => 1
  | none, _n.succ => ⊤) =
  HMul.hMul (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) a, 0 with
      | Option.some a, n => (↑(a ^ n) : WithTop α)
      | none, 0 => 1
      | none, _n.succ => ⊤ :
      WithTop α)
    a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n_1 n : ℕ
a : WithTop α
zero :
  (match (motive := WithTop α → ℕ → WithTop α) a, HAdd.hAdd (α := ℕ) 0 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, 0 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      a
⊢ (match (motive := WithTop α → ℕ → WithTop α) a, n + 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, n with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      a
have succ : ∀ (n : ℕ),
  (match (motive := WithTop α → ℕ → WithTop α) a, n + 1 + 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, n + 1 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
⊢ (match (motive := WithTop α → ℕ → WithTop α) a, HAdd.hAdd (α := ℕ) 0 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, 0 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      a
have zero : (match (motive := WithTop α → ℕ → WithTop α) ⊤, HAdd.hAdd (α := ℕ) 0 1 with
  | Option.some a, n => (↑(a ^ n) : WithTop α)
  | none, 0 => 1
  | none, _n.succ => ⊤) =
  HMul.hMul (α := WithTop α) (β := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
      | Option.some a, n => (↑(a ^ n) : WithTop α)
      | none, 0 => 1
      | none, _n.succ => ⊤ :
      WithTop α)
    (⊤ : WithTop α)
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 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
zero :
  (match (motive := WithTop α → ℕ → WithTop α) ⊤, HAdd.hAdd (α := ℕ) 0 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α) (β := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      (⊤ : WithTop α)
⊢ (match (motive := WithTop α → ℕ → WithTop α) a, HAdd.hAdd (α := ℕ) 0 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, 0 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      a
have zero₁ : ∀ (a : α),
  (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), HAdd.hAdd (α := ℕ) 0 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), 0 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      (↑a : WithTop α)
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 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
n_1 : ℕ
⊢ (match (motive := WithTop α → ℕ → WithTop α) a, n_1 + 1 + 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, n_1 + 1 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      a
have succ : (match (motive := WithTop α → ℕ → WithTop α) ⊤, n_1 + 1 + 1 with
  | Option.some a, n => (↑(a ^ n) : WithTop α)
  | none, 0 => 1
  | none, _n.succ => ⊤) =
  HMul.hMul (α := WithTop α) (β := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) ⊤, n_1 + 1 with
      | Option.some a, n => (↑(a ^ n) : WithTop α)
      | none, 0 => 1
      | none, _n.succ => ⊤ :
      WithTop α)
    (⊤ : WithTop α)
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 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
n_1 : ℕ
succ :
  (match (motive := WithTop α → ℕ → WithTop α) ⊤, n_1 + 1 + 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α) (β := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) ⊤, n_1 + 1 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      (⊤ : WithTop α)
⊢ (match (motive := WithTop α → ℕ → WithTop α) a, n_1 + 1 + 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, n_1 + 1 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      a
have succ₁ : ∀ (a : α),
  (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n_1 + 1 + 1 with
    | Option.some a, n => (↑(a ^ n) : WithTop α)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    HMul.hMul (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n_1 + 1 with
        | Option.some a, n => (↑(a ^ n) : WithTop α)
        | none, 0 => 1
        | none, _n.succ => ⊤ :
        WithTop α)
      (↑a : WithTop α)
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 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
⊢ x ^ n = ⊤ ↔ x = ⊤ ∧ n ≠ 0
have top : HPow.hPow (α := WithTop α) ⊤ n = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ n ≠ 0
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
top : HPow.hPow (α := WithTop α) ⊤ n = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ n ≠ 0
⊢ x ^ n = ⊤ ↔ x = ⊤ ∧ n ≠ 0
have coe : ∀ (a : α), (↑a : WithTop α) ^ n = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ n ≠ 0
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
n : ℕ
⊢ HPow.hPow (α := WithTop α) ⊤ n = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ n ≠ 0
have top : HPow.hPow (α := WithTop α) (β := ℕ) ⊤ 0 = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ Ne (α := ℕ) 0 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
n : ℕ
top : HPow.hPow (α := WithTop α) (β := ℕ) ⊤ 0 = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ Ne (α := ℕ) 0 0
⊢ HPow.hPow (α := WithTop α) ⊤ n = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ n ≠ 0
have top₁ : ∀ (n : ℕ), HPow.hPow (α := WithTop α) ⊤ (n + 1) = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ n + 1 ≠ 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
n : ℕ
a : α
⊢ (↑a : WithTop α) ^ n = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ n ≠ 0
have coe : HPow.hPow (β := ℕ) (↑a : WithTop α) 0 = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ Ne (α := ℕ) 0 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
n : ℕ
a : α
coe : HPow.hPow (β := ℕ) (↑a : WithTop α) 0 = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ Ne (α := ℕ) 0 0
⊢ (↑a : WithTop α) ^ n = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ n ≠ 0
have coe₁ : ∀ (n : ℕ), (↑a : WithTop α) ^ (n + 1) = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ n + 1 ≠ 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
inst_4 : Preorder α
⊢ x ^ n < ⊤ ↔ x < ⊤ ∨ n = 0
have simp_rw : x ^ n ≠ ⊤ ↔ x ≠ ⊤ ∨ n = 0
Tactic: simp_rw [WithTop.lt_top_iff_ne_top, pow_ne_top_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
a b : WithTop α
⊢ a * b = b * a
have simp_rw : Eq (α := WithTop α) (if a = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) a b)
  (if b = 0 ∨ a = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) b a)
Tactic: simp_rw [mul_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
⊢ ⊤ * (a + b) = ⊤ * a + ⊤ * b
have pos : ∀ (ha : a = 0), ⊤ * (a + b) = ⊤ * a + ⊤ * 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 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
pos : ∀ (ha : a = 0), ⊤ * (a + b) = ⊤ * a + ⊤ * b
⊢ ⊤ * (a + b) = ⊤ * a + ⊤ * b
have neg : ∀ (ha : ¬a = 0), ⊤ * (a + b) = ⊤ * a + ⊤ * 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 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
c : α
⊢ (↑c : WithTop α) * (a + b) = (↑c : WithTop α) * a + (↑c : WithTop α) * b
have pos : ∀ (hc : c = 0), (↑c : WithTop α) * (a + b) = (↑c : WithTop α) * a + (↑c : WithTop α) * b
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
c : α
pos : ∀ (hc : c = 0), (↑c : WithTop α) * (a + b) = (↑c : WithTop α) * a + (↑c : WithTop α) * b
⊢ (↑c : WithTop α) * (a + b) = (↑c : WithTop α) * a + (↑c : WithTop α) * b
have neg : ∀ (hc : ¬c = 0), (↑c : WithTop α) * (a + b) = (↑c : WithTop α) * a + (↑c : WithTop α) * b
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (↑c : WithTop α) * (a + b) = (↑c : WithTop α) * a + (↑c : WithTop α) * b
have neg : (Option.bind (a + b) fun (b : α) ↦ Option.some (c * b)) =
  HAdd.hAdd (α := WithTop α) (Option.bind a fun (b : α) ↦ Option.some (c * b))
    (Option.bind b fun (b : α) ↦ Option.some (c * b))
Tactic: simp only [coe_mul_eq_bind hc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (Option.bind (a + b) fun (b : α) ↦ Option.some (c * b)) =
    HAdd.hAdd (α := WithTop α) (Option.bind a fun (b : α) ↦ Option.some (c * b))
      (Option.bind b fun (b : α) ↦ Option.some (c * b))
have neg : (Option.bind (⊤ + b) fun (b : α) ↦ Option.some (c * b)) =
  HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (b : α) ↦ Option.some (c * b))
    (Option.bind b fun (b : α) ↦ Option.some (c * 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 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
neg :
  (Option.bind (⊤ + b) fun (b : α) ↦ Option.some (c * b)) =
    HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (b : α) ↦ Option.some (c * b))
      (Option.bind b fun (b : α) ↦ Option.some (c * b))
⊢ (Option.bind (a + b) fun (b : α) ↦ Option.some (c * b)) =
    HAdd.hAdd (α := WithTop α) (Option.bind a fun (b : α) ↦ Option.some (c * b))
      (Option.bind b fun (b : α) ↦ Option.some (c * b))
have neg₁ : ∀ (a : α),
  (Option.bind ((↑a : WithTop α) + b) fun (b : α) ↦ Option.some (c * b)) =
    HAdd.hAdd (α := WithTop α) (Option.bind (↑a : WithTop α) fun (b : α) ↦ Option.some (c * b))
      (Option.bind b fun (b : α) ↦ Option.some (c * 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 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
b : WithTop α
c : α
hc : ¬c = 0
⊢ (Option.bind (⊤ + b) fun (b : α) ↦ Option.some (c * b)) =
    HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (b : α) ↦ Option.some (c * b))
      (Option.bind b fun (b : α) ↦ Option.some (c * b))
have neg : (Option.bind (HAdd.hAdd (α := WithTop α) ⊤ ⊤) fun (b : α) ↦ Option.some (c * b)) =
  HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (b : α) ↦ Option.some (c * b))
    (Option.bind ⊤ fun (b : α) ↦ Option.some (c * b))
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 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
b : WithTop α
c : α
hc : ¬c = 0
neg :
  (Option.bind (HAdd.hAdd (α := WithTop α) ⊤ ⊤) fun (b : α) ↦ Option.some (c * b)) =
    HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (b : α) ↦ Option.some (c * b))
      (Option.bind ⊤ fun (b : α) ↦ Option.some (c * b))
⊢ (Option.bind (⊤ + b) fun (b : α) ↦ Option.some (c * b)) =
    HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (b : α) ↦ Option.some (c * b))
      (Option.bind b fun (b : α) ↦ Option.some (c * b))
have neg₁ : ∀ (a : α),
  (Option.bind (⊤ + (↑a : WithTop α)) fun (b : α) ↦ Option.some (c * b)) =
    HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (b : α) ↦ Option.some (c * b))
      (Option.bind (↑a : WithTop α) fun (b : α) ↦ Option.some (c * b))
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 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
b : WithTop α
c : α
hc : ¬c = 0
a : α
⊢ (Option.bind ((↑a : WithTop α) + b) fun (b : α) ↦ Option.some (c * b)) =
    HAdd.hAdd (α := WithTop α) (Option.bind (↑a : WithTop α) fun (b : α) ↦ Option.some (c * b))
      (Option.bind b fun (b : α) ↦ Option.some (c * b))
have neg : (Option.bind ((↑a : WithTop α) + ⊤) fun (b : α) ↦ Option.some (c * b)) =
  HAdd.hAdd (α := WithTop α) (Option.bind (↑a : WithTop α) fun (b : α) ↦ Option.some (c * b))
    (Option.bind ⊤ fun (b : α) ↦ Option.some (c * b))
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 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
b : WithTop α
c : α
hc : ¬c = 0
a : α
neg :
  (Option.bind ((↑a : WithTop α) + ⊤) fun (b : α) ↦ Option.some (c * b)) =
    HAdd.hAdd (α := WithTop α) (Option.bind (↑a : WithTop α) fun (b : α) ↦ Option.some (c * b))
      (Option.bind ⊤ fun (b : α) ↦ Option.some (c * b))
⊢ (Option.bind ((↑a : WithTop α) + b) fun (b : α) ↦ Option.some (c * b)) =
    HAdd.hAdd (α := WithTop α) (Option.bind (↑a : WithTop α) fun (b : α) ↦ Option.some (c * b))
      (Option.bind b fun (b : α) ↦ Option.some (c * b))
have neg₁ : ∀ (a_1 : α),
  (Option.bind ((↑a : WithTop α) + (↑a_1 : WithTop α)) fun (b : α) ↦ Option.some (c * b)) =
    HAdd.hAdd (α := WithTop α) (Option.bind (↑a : WithTop α) fun (b : α) ↦ Option.some (c * b))
      (Option.bind (↑a_1 : WithTop α) fun (b : α) ↦ Option.some (c * b))
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 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c a b : WithTop α
⊢ c * (a + b) = c * a + c * b
have top : ⊤ * (a + b) = ⊤ * a + ⊤ * b
Tactic: cases c with
    | top => by_cases ha : a = 0 <;> simp [ha]
    | coe c =>
      by_cases hc : c = 0; · simp [hc]
      simp only [coe_mul_eq_bind hc]
      cases a <;> cases b <;> try rfl
      exact congr_arg some (mul_add _ _ _)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c a b : WithTop α
top : ⊤ * (a + b) = ⊤ * a + ⊤ * b
⊢ c * (a + b) = c * a + c * b
have coe : ∀ (c : α), (↑c : WithTop α) * (a + b) = (↑c : WithTop α) * a + (↑c : WithTop α) * b
Tactic: cases c with
    | top => by_cases ha : a = 0 <;> simp [ha]
    | coe c =>
      by_cases hc : c = 0; · simp [hc]
      simp only [coe_mul_eq_bind hc]
      cases a <;> cases b <;> try rfl
      exact congr_arg some (mul_add _ _ _)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤
have pos : ∀ (ha : a = 0), (a + b) * ⊤ = a * ⊤ + 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 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
pos : ∀ (ha : a = 0), (a + b) * ⊤ = a * ⊤ + b * ⊤
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤
have neg : ∀ (ha : ¬a = 0), (a + b) * ⊤ = a * ⊤ + 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 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
c : α
⊢ (a + b) * (↑c : WithTop α) = a * (↑c : WithTop α) + b * (↑c : WithTop α)
have pos : ∀ (hc : c = 0), (a + b) * (↑c : WithTop α) = a * (↑c : WithTop α) + b * (↑c : WithTop α)
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
c : α
pos : ∀ (hc : c = 0), (a + b) * (↑c : WithTop α) = a * (↑c : WithTop α) + b * (↑c : WithTop α)
⊢ (a + b) * (↑c : WithTop α) = a * (↑c : WithTop α) + b * (↑c : WithTop α)
have neg : ∀ (hc : ¬c = 0), (a + b) * (↑c : WithTop α) = a * (↑c : WithTop α) + b * (↑c : WithTop α)
Tactic: by_cases hc : c = 0