awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
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:
simp [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n n_1 : ℕ
⊢ (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:
simp [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n n_1 : ℕ
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:
simp [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
a : α
n : ℕ
⊢ (↑(a ^ n) : WithTop α) = (↑a : WithTop α) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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
coe : ∀ (a : α), (↑a : WithTop α) ^ n = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ n ≠ 0
⊢ x ^ n = ⊤ ↔ x = ⊤ ∧ n ≠ 0

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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
top₁ : ∀ (n : ℕ), HPow.hPow (α := WithTop α) ⊤ (n + 1) = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ n + 1 ≠ 0
⊢ HPow.hPow (α := WithTop α) ⊤ n = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ n ≠ 0

Tactic:
cases n
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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
coe₁ : ∀ (n : ℕ), (↑a : WithTop α) ^ (n + 1) = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ n + 1 ≠ 0
⊢ (↑a : WithTop α) ^ n = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ n ≠ 0

Tactic:
cases n
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
⊢ HPow.hPow (α := WithTop α) (β := ℕ) ⊤ 0 = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ Ne (α := ℕ) 0 0

Tactic:
simp [← coe_pow]

Premises used: WithTop.coe_pow
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
n : ℕ
⊢ HPow.hPow (α := WithTop α) ⊤ (n + 1) = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ n + 1 ≠ 0

Tactic:
simp [← coe_pow]

Premises used: WithTop.coe_pow
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
a : α
⊢ HPow.hPow (β := ℕ) (↑a : WithTop α) 0 = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ Ne (α := ℕ) 0 0

Tactic:
simp [← coe_pow]

Premises used: WithTop.coe_pow
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
a : α
n : ℕ
⊢ (↑a : WithTop α) ^ (n + 1) = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ n + 1 ≠ 0

Tactic:
simp [← coe_pow]

Premises used: WithTop.coe_pow
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
⊢ x ^ n ≠ ⊤ ↔ x ≠ ⊤ ∨ n = 0

Tactic:
simp [pow_eq_top_iff, or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left, WithTop.pow_eq_top_iff
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
inst_4 : Preorder α
simp_rw : x ^ n ≠ ⊤ ↔ x ≠ ⊤ ∨ n = 0
⊢ x ^ n < ⊤ ↔ x < ⊤ ∨ n = 0

Tactic:
simp_rw [WithTop.lt_top_iff_ne_top, pow_ne_top_iff]

Premises used: WithTop.pow_ne_top_iff, WithTop.lt_top_iff_ne_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
hx : x ^ n = ⊤
⊢ x = ⊤

Tactic:
(pow_eq_top_iff.1 hx).1

Premises used: And.left, WithTop.pow_eq_top_iff, Iff.mp
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
hx : x ≠ ⊤
⊢ x ^ n ≠ ⊤

Tactic:
pow_ne_top_iff.2 <| .inl hx

Premises used: Iff.mpr, Or.inl, WithTop.pow_ne_top_iff
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
x : WithTop α
n : ℕ
inst_4 : Preorder α
hx : x < ⊤
⊢ x ^ n < ⊤

Tactic:
pow_lt_top_iff.2 <| .inl hx

Premises used: Iff.mpr, WithTop.pow_lt_top_iff, Or.inl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
a b : WithTop α
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)
⊢ a * b = b * a

Tactic:
simp_rw [mul_def]

Premises used: WithTop.mul_def
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
a b : WithTop α
⊢ 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:
if_congr or_comm rfl (Option.map₂_comm mul_comm)

Premises used: if_congr, mul_comm, Option.map₂_comm, or_comm, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoidWithZero α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
a b : WithTop α
⊢ 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:
exact if_congr or_comm rfl (Option.map₂_comm mul_comm)

Premises used: if_congr, mul_comm, Option.map₂_comm, or_comm, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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
neg : ∀ (ha : ¬a = 0), ⊤ * (a + b) = ⊤ * a + ⊤ * b
⊢ ⊤ * (a + b) = ⊤ * a + ⊤ * b

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
ha : a = 0
⊢ ⊤ * (a + b) = ⊤ * a + ⊤ * b

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
ha : ¬a = 0
⊢ ⊤ * (a + b) = ⊤ * a + ⊤ * b

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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
neg : ∀ (hc : ¬c = 0), (↑c : WithTop α) * (a + b) = (↑c : WithTop α) * a + (↑c : WithTop α) * b
⊢ (↑c : WithTop α) * (a + b) = (↑c : WithTop α) * a + (↑c : WithTop α) * b

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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

Tactic:
simp [hc]
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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 (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))
⊢ (↑c : WithTop α) * (a + b) = (↑c : WithTop α) * a + (↑c : WithTop α) * b

Tactic:
simp only [coe_mul_eq_bind hc]

Premises used: WithTop.coe_mul_eq_bind
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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))
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))
⊢ (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:
cases a
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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))
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))
⊢ (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 b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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))
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))
⊢ (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 b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
⊢ (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:
rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
⊢ (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:
try rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
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:
rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
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:
try rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a : α
⊢ (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:
rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a : α
⊢ (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:
try rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a 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:
congr_arg some (mul_add _ _ _)

Premises used: WithTop.map₂, WithTop.some, congr_arg, mul_add, Option.map₂
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a 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:
exact congr_arg some (mul_add _ _ _)

Premises used: WithTop.some, congr_arg, mul_add
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c a b : WithTop α
top : ⊤ * (a + b) = ⊤ * a + ⊤ * b
coe : ∀ (c : α), (↑c : WithTop α) * (a + b) = (↑c : WithTop α) * a + (↑c : WithTop α) * b
⊢ c * (a + b) = c * a + c * 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 _ _ _)

Premises used: WithTop.some, congr_arg, WithTop.top, mul_add, WithTop.coe
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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 * ⊤
neg : ∀ (ha : ¬a = 0), (a + b) * ⊤ = a * ⊤ + b * ⊤
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
ha : a = 0
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
ha : ¬a = 0
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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 α)
neg : ∀ (hc : ¬c = 0), (a + b) * (↑c : WithTop α) = a * (↑c : WithTop α) + b * (↑c : WithTop α)
⊢ (a + b) * (↑c : WithTop α) = a * (↑c : WithTop α) + b * (↑c : WithTop α)

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : c = 0
⊢ (a + b) * (↑c : WithTop α) = a * (↑c : WithTop α) + b * (↑c : WithTop α)

Tactic:
simp [hc]
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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 (a + b) fun (a : α) ↦ Option.some (a * c)) =
    HAdd.hAdd (α := WithTop α) (Option.bind a fun (a : α) ↦ Option.some (a * c))
      (Option.bind b fun (a : α) ↦ Option.some (a * c))
⊢ (a + b) * (↑c : WithTop α) = a * (↑c : WithTop α) + b * (↑c : WithTop α)

Tactic:
simp only [mul_coe_eq_bind hc]

Premises used: WithTop.mul_coe_eq_bind
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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 (a : α) ↦ Option.some (a * c)) =
    HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (a : α) ↦ Option.some (a * c))
      (Option.bind b fun (a : α) ↦ Option.some (a * c))
neg₁ :
  ∀ (a : α),
    (Option.bind ((↑a : WithTop α) + b) fun (a : α) ↦ Option.some (a * c)) =
      HAdd.hAdd (α := WithTop α) (Option.bind (↑a : WithTop α) fun (a : α) ↦ Option.some (a * c))
        (Option.bind b fun (a : α) ↦ Option.some (a * c))
⊢ (Option.bind (a + b) fun (a : α) ↦ Option.some (a * c)) =
    HAdd.hAdd (α := WithTop α) (Option.bind a fun (a : α) ↦ Option.some (a * c))
      (Option.bind b fun (a : α) ↦ Option.some (a * c))

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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 (a : α) ↦ Option.some (a * c)) =
    HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (a : α) ↦ Option.some (a * c))
      (Option.bind ⊤ fun (a : α) ↦ Option.some (a * c))
neg₁ :
  ∀ (a : α),
    (Option.bind (⊤ + (↑a : WithTop α)) fun (a : α) ↦ Option.some (a * c)) =
      HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (a : α) ↦ Option.some (a * c))
        (Option.bind (↑a : WithTop α) fun (a : α) ↦ Option.some (a * c))
⊢ (Option.bind (⊤ + b) fun (a : α) ↦ Option.some (a * c)) =
    HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (a : α) ↦ Option.some (a * c))
      (Option.bind b fun (a : α) ↦ Option.some (a * c))

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
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 (a : α) ↦ Option.some (a * c)) =
    HAdd.hAdd (α := WithTop α) (Option.bind (↑a : WithTop α) fun (a : α) ↦ Option.some (a * c))
      (Option.bind ⊤ fun (a : α) ↦ Option.some (a * c))
neg₁ :
  ∀ (a_1 : α),
    (Option.bind ((↑a : WithTop α) + (↑a_1 : WithTop α)) fun (a : α) ↦ Option.some (a * c)) =
      HAdd.hAdd (α := WithTop α) (Option.bind (↑a : WithTop α) fun (a : α) ↦ Option.some (a * c))
        (Option.bind (↑a_1 : WithTop α) fun (a : α) ↦ Option.some (a * c))
⊢ (Option.bind ((↑a : WithTop α) + b) fun (a : α) ↦ Option.some (a * c)) =
    HAdd.hAdd (α := WithTop α) (Option.bind (↑a : WithTop α) fun (a : α) ↦ Option.some (a * c))
      (Option.bind b fun (a : α) ↦ Option.some (a * c))

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
⊢ (Option.bind (HAdd.hAdd (α := WithTop α) ⊤ ⊤) fun (a : α) ↦ Option.some (a * c)) =
    HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (a : α) ↦ Option.some (a * c))
      (Option.bind ⊤ fun (a : α) ↦ Option.some (a * c))

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
⊢ (Option.bind (HAdd.hAdd (α := WithTop α) ⊤ ⊤) fun (a : α) ↦ Option.some (a * c)) =
    HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (a : α) ↦ Option.some (a * c))
      (Option.bind ⊤ fun (a : α) ↦ Option.some (a * c))

Tactic:
try rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a : α
⊢ (Option.bind (⊤ + (↑a : WithTop α)) fun (a : α) ↦ Option.some (a * c)) =
    HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (a : α) ↦ Option.some (a * c))
      (Option.bind (↑a : WithTop α) fun (a : α) ↦ Option.some (a * c))

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a : α
⊢ (Option.bind (⊤ + (↑a : WithTop α)) fun (a : α) ↦ Option.some (a * c)) =
    HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (a : α) ↦ Option.some (a * c))
      (Option.bind (↑a : WithTop α) fun (a : α) ↦ Option.some (a * c))

Tactic:
try rfl