awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (↑a : WithTop α) 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
a : α
⊢ (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))

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 (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))

Tactic:
congr_arg some (add_mul _ _ _)

Premises used: add_mul, WithTop.map₂, WithTop.some, congr_arg, 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 (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))

Tactic:
exact congr_arg some (add_mul _ _ _)

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

Tactic:
cases c with
    | top => by_cases ha : a = 0 <;> simp [ha]
    | coe c =>
      by_cases hc : c = 0; · simp [hc]
      simp only [mul_coe_eq_bind hc]
      cases a <;> cases b <;> try rfl
      exact congr_arg some (add_mul _ _ _)

Premises used: add_mul, WithTop.some, congr_arg, WithTop.top, WithTop.coe
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
inst_4 : NoZeroDivisors α
inst_5 : Nontrivial α
⊢ IsOrderedRing.{u_1} (WithTop α)

Tactic:
CanonicallyOrderedAdd.toIsOrderedRing

Premises used: CanonicallyOrderedAdd.toIsOrderedRing
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
a₁ a₂ b₁ b₂ : WithTop α
ha : a₁ < a₂
hb : b₁ < b₂
⊢ MulPosStrictMono α

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
a₁ a₂ b₁ b₂ : WithTop α
ha : a₁ < a₂
hb : b₁ < b₂
this : MulPosStrictMono α
⊢ a₁ ≠ ⊤

Tactic:
ha.lt_top.ne

Premises used: LT.lt.lt_top, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
a₁ a₂ b₁ b₂ : WithTop α
ha : a₁ < a₂
hb : b₁ < b₂
this : MulPosStrictMono α
lift : ∀ (a₁ : α) (ha : (↑a₁ : WithTop α) < a₂), (↑a₁ : WithTop α) * b₁ < a₂ * b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
lift a₁ to α using ha.lt_top.ne

Premises used: LT.lt.lt_top, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
a₂ b₁ b₂ : WithTop α
hb : b₁ < b₂
this : MulPosStrictMono α
a₁ : α
ha : (↑a₁ : WithTop α) < a₂
⊢ b₁ ≠ ⊤

Tactic:
hb.lt_top.ne

Premises used: LT.lt.lt_top, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
a₂ b₁ b₂ : WithTop α
hb : b₁ < b₂
this : MulPosStrictMono α
a₁ : α
ha : (↑a₁ : WithTop α) < a₂
lift : ∀ (b₁ : α) (hb : (↑b₁ : WithTop α) < b₂), (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * b₂
⊢ (↑a₁ : WithTop α) * b₁ < a₂ * b₂

Tactic:
lift b₁ to α using hb.lt_top.ne

Premises used: LT.lt.lt_top, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : (↑a₁ : WithTop α) < a₂
b₁ : α
hb : (↑b₁ : WithTop α) < b₂
inl : ∀ (ha : (↑a₁ : WithTop α) < ⊤), (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < ⊤ * b₂
inr : ∀ (ha₂ : a₂ ≠ ⊤), (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * b₂
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * b₂

Tactic:
obtain rfl | ha₂ := eq_or_ne a₂ ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : (↑b₁ : WithTop α) < b₂
ha : (↑a₁ : WithTop α) < ⊤
⊢ b₂ ≠ 0

Tactic:
simpa [bot_eq_zero] using hb.bot_lt.ne'

Premises used: LT.lt.ne', LT.lt.bot_lt, bot_eq_zero
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : (↑b₁ : WithTop α) < b₂
ha : (↑a₁ : WithTop α) < ⊤
inl : (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < ⊤
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < ⊤ * b₂

Tactic:
rw [top_mul (by simpa [bot_eq_zero] using hb.bot_lt.ne')]

Premises used: WithTop.top_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : (↑b₁ : WithTop α) < b₂
ha : (↑a₁ : WithTop α) < ⊤
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < ⊤

Tactic:
coe_lt_top _

Premises used: WithTop.coe_lt_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : (↑b₁ : WithTop α) < b₂
ha : (↑a₁ : WithTop α) < ⊤
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < ⊤

Tactic:
exact coe_lt_top _

Premises used: WithTop.coe_lt_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : (↑a₁ : WithTop α) < a₂
b₁ : α
hb : (↑b₁ : WithTop α) < b₂
ha₂ : a₂ ≠ ⊤
inr : ∀ (hb : (↑b₁ : WithTop α) < ⊤), (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * ⊤
inr₁ : ∀ (hb₂ : b₂ ≠ ⊤), (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * b₂
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * b₂

Tactic:
obtain rfl | hb₂ := eq_or_ne b₂ ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : (↑a₁ : WithTop α) < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : (↑b₁ : WithTop α) < ⊤
⊢ a₂ ≠ 0

Tactic:
simpa [bot_eq_zero] using ha.bot_lt.ne'

Premises used: LT.lt.ne', LT.lt.bot_lt, bot_eq_zero
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : (↑a₁ : WithTop α) < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : (↑b₁ : WithTop α) < ⊤
inr : (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < ⊤
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * ⊤

Tactic:
rw [mul_top (by simpa [bot_eq_zero] using ha.bot_lt.ne')]

Premises used: WithTop.mul_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : (↑a₁ : WithTop α) < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : (↑b₁ : WithTop α) < ⊤
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < ⊤

Tactic:
coe_lt_top _

Premises used: WithTop.coe_lt_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : (↑a₁ : WithTop α) < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : (↑b₁ : WithTop α) < ⊤
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < ⊤

Tactic:
exact coe_lt_top _

Premises used: WithTop.coe_lt_top
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : (↑a₁ : WithTop α) < a₂
b₁ : α
hb : (↑b₁ : WithTop α) < b₂
ha₂ : a₂ ≠ ⊤
hb₂ : b₂ ≠ ⊤
⊢ a₂ ≠ ⊤

Tactic:
ha₂
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : (↑a₁ : WithTop α) < a₂
b₁ : α
hb : (↑b₁ : WithTop α) < b₂
ha₂ : a₂ ≠ ⊤
hb₂ : b₂ ≠ ⊤
inr :
  ∀ (a₂ : α) (ha : (↑a₁ : WithTop α) < (↑a₂ : WithTop α)),
    (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < (↑a₂ : WithTop α) * b₂
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * b₂

Tactic:
lift a₂ to α using ha₂
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : (↑b₁ : WithTop α) < b₂
hb₂ : b₂ ≠ ⊤
a₂ : α
ha : (↑a₁ : WithTop α) < (↑a₂ : WithTop α)
⊢ b₂ ≠ ⊤

Tactic:
hb₂
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : (↑b₁ : WithTop α) < b₂
hb₂ : b₂ ≠ ⊤
a₂ : α
ha : (↑a₁ : WithTop α) < (↑a₂ : WithTop α)
inr :
  ∀ (b₂ : α) (hb : (↑b₁ : WithTop α) < (↑b₂ : WithTop α)),
    (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < (↑a₂ : WithTop α) * (↑b₂ : WithTop α)
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < (↑a₂ : WithTop α) * b₂

Tactic:
lift b₂ to α using hb₂
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
this : MulPosStrictMono α
a₁ b₁ a₂ : α
ha : (↑a₁ : WithTop α) < (↑a₂ : WithTop α)
b₂ : α
hb : (↑b₁ : WithTop α) < (↑b₂ : WithTop α)
inr : ∀ (ha : a₁ < a₂) (hb : b₁ < b₂), a₁ * b₁ < a₂ * b₂
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < (↑a₂ : WithTop α) * (↑b₂ : WithTop α)

Tactic:
norm_cast at *
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
this : MulPosStrictMono α
a₁ b₁ a₂ b₂ : α
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
CanonicallyOrderedAdd.mul_lt_mul_of_lt_of_lt ha hb

Premises used: CanonicallyOrderedAdd.mul_lt_mul_of_lt_of_lt
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
this : MulPosStrictMono α
a₁ b₁ a₂ b₂ : α
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
exact CanonicallyOrderedAdd.mul_lt_mul_of_lt_of_lt ha hb

Premises used: CanonicallyOrderedAdd.mul_lt_mul_of_lt_of_lt
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
inst_6 : NoZeroDivisors α
inst_7 : Nontrivial α
h : Ne (α := ℕ) 1 0
⊢ StrictMono (β := WithTop α) fun (a : WithTop α) ↦ HPow.hPow (β := ℕ) a 1

Tactic:
simpa only [pow_one] using strictMono_id

Premises used: strictMono_id, pow_one
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
inst_6 : NoZeroDivisors α
inst_7 : Nontrivial α
n : ℕ
h_1 : n + 2 ≠ 0
x y : WithTop α
h : x < y
simp_rw : x ^ (n + 1) * x < y ^ (n + 1) * y
⊢ LT.lt.{u_1} (α := WithTop α) ((fun (a : WithTop α) ↦ a ^ (n + 2)) x) ((fun (a : WithTop α) ↦ a ^ (n + 2)) y)

Tactic:
simp_rw [pow_succ _ (n + 1)]

Premises used: pow_succ, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
inst_6 : NoZeroDivisors α
inst_7 : Nontrivial α
n : ℕ
h_1 : n + 2 ≠ 0
x y : WithTop α
h : x < y
⊢ x ^ (n + 1) * x < y ^ (n + 1) * y

Tactic:
WithTop.mul_lt_mul (WithTop.pow_right_strictMono n.succ_ne_zero h) h

Premises used: Nat.succ_ne_zero, WithTop.mul_lt_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
inst_6 : NoZeroDivisors α
inst_7 : Nontrivial α
n : ℕ
h_1 : n + 2 ≠ 0
x y : WithTop α
h : x < y
⊢ x ^ (n + 1) * x < y ^ (n + 1) * y

Tactic:
exact WithTop.mul_lt_mul (WithTop.pow_right_strictMono n.succ_ne_zero h) h

Premises used: Nat.succ_ne_zero, WithTop.mul_lt_mul
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommSemiring α
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : CanonicallyOrderedAdd α
inst_5 : PosMulStrictMono α
inst_6 : NoZeroDivisors α
inst_7 : Nontrivial α
a b : WithTop α
hab : a < b
n : ℕ
hn : n ≠ 0
⊢ a ^ n < b ^ n

Tactic:
WithTop.pow_right_strictMono hn hab

Premises used: WithTop.pow_right_strictMono
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : α
⊢ (↑(a * b) : WithBot α) = (↑a : WithBot α) * (↑b : WithBot α)

Tactic:
rfl

Premises used: WithBot.some, WithTop.some, rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : WithBot α
h : a ≠ 0
rw : Eq.{u_1 + 1} (α := WithBot α) (if a = 0 then 0 else ⊥) ⊥
rw₁ rw₂ : Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
⊢ a * ⊥ = ⊥

Tactic:
rw [mul_bot', if_neg h]

Premises used: WithBot.mul_bot', if_neg
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithBot α
hb : b ≠ 0
rw : Eq.{u_1 + 1} (α := WithBot α) (if b = 0 then 0 else ⊥) ⊥
rw₁ rw₂ : Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
⊢ ⊥ * b = ⊥

Tactic:
rw [bot_mul', if_neg hb]

Premises used: WithBot.bot_mul', if_neg
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
⊢ HMul.hMul (α := WithBot α) ⊥ ⊥ = ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithBot α
bot : ⊥ * b = if Eq.{u_1 + 1} (α := WithBot α) ⊥ 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊥ b
coe :
  ∀ (a : α),
    (↑a : WithBot α) * b =
      if (↑a : WithBot α) = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithBot α) b
⊢ a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) a b

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithBot α
bot :
  HMul.hMul (α := WithBot α) ⊥ ⊥ =
    if Eq.{u_1 + 1} (α := WithBot α) ⊥ 0 ∨ Eq.{u_1 + 1} (α := WithBot α) ⊥ 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊥ ⊥
bot₁ :
  ∀ (a : α),
    ⊥ * (↑a : WithBot α) =
      if Eq.{u_1 + 1} (α := WithBot α) ⊥ 0 ∨ (↑a : WithBot α) = 0 then 0
      else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊥ (↑a : WithBot α)
⊢ ⊥ * b = if Eq.{u_1 + 1} (α := WithBot α) ⊥ 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊥ b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithBot α
a : α
coe :
  (↑a : WithBot α) * ⊥ =
    if (↑a : WithBot α) = 0 ∨ Eq.{u_1 + 1} (α := WithBot α) ⊥ 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithBot α) ⊥
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithBot α) * (↑a_1 : WithBot α) =
      if (↑a : WithBot α) = 0 ∨ (↑a_1 : WithBot α) = 0 then 0
      else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithBot α) (↑a_1 : WithBot α)
⊢ (↑a : WithBot α) * b = if (↑a : WithBot α) = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithBot α) b

Tactic:
cases b
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
⊢ HMul.hMul (α := WithBot α) ⊥ ⊥ =
    if Eq.{u_1 + 1} (α := WithBot α) ⊥ 0 ∨ Eq.{u_1 + 1} (α := WithBot α) ⊥ 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊥ ⊥

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
⊢ ⊥ * (↑a : WithBot α) =
    if Eq.{u_1 + 1} (α := WithBot α) ⊥ 0 ∨ (↑a : WithBot α) = 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊥ (↑a : WithBot α)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
⊢ (↑a : WithBot α) * ⊥ =
    if (↑a : WithBot α) = 0 ∨ Eq.{u_1 + 1} (α := WithBot α) ⊥ 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithBot α) ⊥

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a a_1 : α
⊢ (↑a : WithBot α) * (↑a_1 : WithBot α) =
    if (↑a : WithBot α) = 0 ∨ (↑a_1 : WithBot α) = 0 then 0
    else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithBot α) (↑a_1 : WithBot α)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithBot α
rw :
  Eq (α := WithBot α) (if a = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) a b) ⊥ ↔
    a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0
⊢ a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0

Tactic:
rw [mul_def]

Premises used: WithBot.mul_def
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithBot α
⊢ Eq (α := WithBot α) (if a = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) a b) ⊥ ↔
    a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : α
hb : b ≠ 0
simp : Eq.{u_1 + 1} (α := WithBot α) ⊥ (Option.bind ⊥ fun (a : α) ↦ Option.some (a * b))
⊢ ⊥ * (↑b : WithBot α) = Option.bind ⊥ fun (a : α) ↦ Option.some (a * b)

Tactic:
simp only [ne_eq, coe_eq_zero, hb, not_false_eq_true, bot_mul]

Premises used: WithBot.coe_eq_zero, ne_eq, WithBot.bot_mul, not_false_eq_true
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : α
hb : b ≠ 0
⊢ Eq.{u_1 + 1} (α := WithBot α) ⊥ (Option.bind ⊥ fun (a : α) ↦ Option.some (a * b))

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : a ≠ 0
simp : Eq.{u_1 + 1} (α := WithBot α) ⊥ (Option.bind ⊥ fun (b : α) ↦ Option.some (a * b))
⊢ (↑a : WithBot α) * ⊥ = Option.bind ⊥ fun (b : α) ↦ Option.some (a * b)

Tactic:
simp only [ne_eq, coe_eq_zero, ha, not_false_eq_true, mul_bot]

Premises used: WithBot.coe_eq_zero, ne_eq, WithBot.mul_bot, not_false_eq_true
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : a ≠ 0
⊢ Eq.{u_1 + 1} (α := WithBot α) ⊥ (Option.bind ⊥ fun (b : α) ↦ Option.some (a * b))

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithBot α
pos : ∀ (ha : a = 0), unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
neg : ∀ (ha : ¬a = 0), unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithBot α
ha : a = 0
pos : unbotD 0 (0 * b) = unbotD 0 0 * unbotD 0 b
pos₁ : unbotD 0 0 = unbotD 0 0 * unbotD 0 b
pos₂ : unbotD 0 (↑0 : WithBot α) = unbotD 0 (↑0 : WithBot α) * unbotD 0 b
pos₃ : 0 = 0 * unbotD 0 b
pos₄ pos₅ : Eq.{u_1 + 1} (α := α) 0 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
rw [ha, zero_mul, ← coe_zero, unbotD_coe, zero_mul]

Premises used: MulZeroClass.zero_mul, WithBot.unbotD_coe, WithBot.coe_zero
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
pos : ∀ (hb : b = 0), unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
neg : ∀ (hb : ¬b = 0), unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
by_cases hb : b = 0
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
pos : unbotD 0 (a * 0) = unbotD 0 a * unbotD 0 0
pos₁ : unbotD 0 0 = unbotD 0 a * unbotD 0 0
pos₂ : unbotD 0 (↑0 : WithBot α) = unbotD 0 a * unbotD 0 (↑0 : WithBot α)
pos₃ : 0 = unbotD 0 a * 0
pos₄ pos₅ : Eq.{u_1 + 1} (α := α) 0 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
rw [hb, mul_zero, ← coe_zero, unbotD_coe, mul_zero]

Premises used: MulZeroClass.mul_zero, WithBot.unbotD_coe, WithBot.coe_zero
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : ¬b = 0
neg : ∀ (ha : ¬Eq.{u_1 + 1} (α := WithBot α) ⊥ 0), unbotD 0 (⊥ * b) = unbotD 0 ⊥ * unbotD 0 b
neg₁ : ∀ (a : α) (ha : ¬(↑a : WithBot α) = 0), unbotD 0 ((↑a : WithBot α) * b) = unbotD 0 (↑a : WithBot α) * unbotD 0 b
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
cases a
-- Module: Mathlib.Algebra.Order.Ring.WithTop
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithBot α
hb : ¬b = 0
ha : ¬Eq.{u_1 + 1} (α := WithBot α) ⊥ 0
neg : unbotD 0 ⊥ = unbotD 0 ⊥ * unbotD 0 b
neg₁ : 0 = 0 * unbotD 0 b
neg₂ neg₃ : Eq.{u_1 + 1} (α := α) 0 0
⊢ unbotD 0 (⊥ * b) = unbotD 0 ⊥ * unbotD 0 b

Tactic:
rw [bot_mul hb, unbotD_bot, zero_mul]

Premises used: MulZeroClass.zero_mul, WithBot.unbotD_bot, WithBot.bot_mul