-- Mathlib/Algebra/Order/Ring/WithTop.lean
@[gcongr]
protected lemma mul_lt_mul (ha : a₁ < a₂) (hb : b₁ < b₂) : a₁ * b₁ < a₂ * b₂

Proof state:
case intro.intro.inr.inr.intro.intro.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
this : MulPosStrictMono α
a₁ a₂ b₂ : α
ha : a₁ < a₂
hb : 0 < b₂
⊢ 0 < a₂ * b₂

Tactic:
exact mul_pos (by simpa [bot_eq_zero] using ha.bot_lt) hb

Result:
no goals

Proof state:
case intro.intro.inr.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : ↑b₁ < ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * ⊤

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

Result:
case intro.intro.inr.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : ↑b₁ < ⊤
⊢ ↑a₁ * ↑b₁ < ⊤

Proof state:
case intro.intro.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
hb : ↑b₁ < b₂
ha₂ : a₂ ≠ ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * b₂

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

Result:
case intro.intro.inr.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : ↑b₁ < ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * ⊤

case intro.intro.inr.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
hb : ↑b₁ < b₂
ha₂ : a₂ ≠ ⊤
hb₂ : b₂ ≠ ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * b₂

Proof state:
case intro.intro.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
ha : ↑a₁ < ⊤
⊢ ↑a₁ * ↑b₁ < ⊤ * b₂

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

Result:
case intro.intro.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
ha : ↑a₁ < ⊤
⊢ ↑a₁ * ↑b₁ < ⊤

Proof state:
case intro.intro.inr.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : ↑b₁ < ⊤
⊢ ↑a₁ * ↑b₁ < ⊤

Tactic:
exact coe_lt_top _

Result:
no goals

Proof state:
case intro.intro.inr.inr.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
hb₂ : b₂ ≠ ⊤
a₂ : α
ha : ↑a₁ < ↑a₂
⊢ ↑a₁ * ↑b₁ < ↑a₂ * b₂

Tactic:
lift b₂ to α using hb₂

Result:
case intro.intro.inr.inr.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
this : MulPosStrictMono α
a₁ b₁ a₂ : α
ha : ↑a₁ < ↑a₂
b₂ : α
hb : ↑b₁ < ↑b₂
⊢ ↑a₁ * ↑b₁ < ↑a₂ * ↑b₂

Proof state:
case intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
hb : ↑b₁ < b₂
⊢ ↑a₁ * ↑b₁ < a₂ * b₂

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

Result:
case intro.intro.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
ha : ↑a₁ < ⊤
⊢ ↑a₁ * ↑b₁ < ⊤ * b₂

case intro.intro.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
hb : ↑b₁ < b₂
ha₂ : a₂ ≠ ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * b₂

Proof state:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₁ a₂ b₁ b₂ : WithTop α
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›

Result:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₁ a₂ b₁ b₂ : WithTop α
ha : a₁ < a₂
hb : b₁ < b₂
this : MulPosStrictMono α
⊢ a₁ * b₁ < a₂ * b₂

Proof state:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
ha : ↑a₁ < ⊤
⊢ b₂ ≠ 0

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

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : ↑b₁ < ⊤
⊢ a₂ ≠ 0

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

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₁ a₂ b₁ b₂ : WithTop α
ha : a₁ < a₂
hb : b₁ < b₂
this : MulPosStrictMono α
⊢ a₁ * b₁ < a₂ * b₂

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

Result:
case intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₁ b₂ : WithTop α
hb : b₁ < b₂
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
⊢ ↑a₁ * b₁ < a₂ * b₂

Proof state:
case intro.intro.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
ha : ↑a₁ < ⊤
⊢ ↑a₁ * ↑b₁ < ⊤

Tactic:
exact coe_lt_top _

Result:
no goals

Proof state:
case intro.intro.inr.inr.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
this : MulPosStrictMono α
a₁ b₁ a₂ b₂ : α
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
obtain rfl | hb₁ := eq_zero_or_pos b₁

Result:
case intro.intro.inr.inr.intro.intro.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
this : MulPosStrictMono α
a₁ a₂ b₂ : α
ha : a₁ < a₂
hb : 0 < b₂
⊢ a₁ * 0 < a₂ * b₂

case intro.intro.inr.inr.intro.intro.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
this : MulPosStrictMono α
a₁ b₁ a₂ b₂ : α
ha : a₁ < a₂
hb : b₁ < b₂
hb₁ : 0 < b₁
⊢ a₁ * b₁ < a₂ * b₂

Proof state:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
this : MulPosStrictMono α
a₁ a₂ b₂ : α
ha : a₁ < a₂
hb : 0 < b₂
⊢ 0 < a₂

Tactic:
simpa [bot_eq_zero] using ha.bot_lt

Result:
no goals