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 : 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
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have pos₄ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [hb, mul_zero, ← coe_zero, unbotD_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 : WithBot α
ha : ¬a = 0
hb : ¬b = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have neg : ∀ (ha : ¬Eq.{u_1 + 1} (α := WithBot α) ⊥ 0), unbotD 0 (⊥ * b) = unbotD 0 ⊥ * unbotD 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 : WithBot α
ha : ¬a = 0
hb : ¬b = 0
neg : ∀ (ha : ¬Eq.{u_1 + 1} (α := WithBot α) ⊥ 0), unbotD 0 (⊥ * b) = unbotD 0 ⊥ * unbotD 0 b
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have neg₁ : ∀ (a : α) (ha : ¬(↑a : WithBot α) = 0), unbotD 0 ((↑a : WithBot α) * b) = unbotD 0 (↑a : WithBot α) * unbotD 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 : WithBot α
hb : ¬b = 0
ha : ¬Eq.{u_1 + 1} (α := WithBot α) ⊥ 0
⊢ unbotD 0 (⊥ * b) = unbotD 0 ⊥ * unbotD 0 b
have neg : unbotD 0 ⊥ = unbotD 0 ⊥ * unbotD 0 b
Tactic: rw [bot_mul hb, unbotD_bot, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ unbotD 0 (⊥ * b) = unbotD 0 ⊥ * unbotD 0 b
have neg₁ : 0 = 0 * unbotD 0 b
Tactic: rw [bot_mul hb, unbotD_bot, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ unbotD 0 (⊥ * b) = unbotD 0 ⊥ * unbotD 0 b
have neg₂ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [bot_mul hb, unbotD_bot, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithBot α
hb : ¬b = 0
a : α
ha : ¬(↑a : WithBot α) = 0
⊢ unbotD 0 ((↑a : WithBot α) * b) = unbotD 0 (↑a : WithBot α) * unbotD 0 b
have neg : ∀ (hb : ¬Eq.{u_1 + 1} (α := WithBot α) ⊥ 0), unbotD 0 ((↑a : WithBot α) * ⊥) = unbotD 0 (↑a : WithBot α) * unbotD 0 ⊥
Tactic: cases b
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : WithBot α
hb : ¬b = 0
a : α
ha : ¬(↑a : WithBot α) = 0
neg :
  ∀ (hb : ¬Eq.{u_1 + 1} (α := WithBot α) ⊥ 0), unbotD 0 ((↑a : WithBot α) * ⊥) = unbotD 0 (↑a : WithBot α) * unbotD 0 ⊥
⊢ unbotD 0 ((↑a : WithBot α) * b) = unbotD 0 (↑a : WithBot α) * unbotD 0 b
have neg₁ : ∀ (a_1 : α) (hb : ¬(↑a_1 : WithBot α) = 0),
  unbotD 0 ((↑a : WithBot α) * (↑a_1 : WithBot α)) = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
Tactic: cases b
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithBot α) = 0
hb : ¬Eq.{u_1 + 1} (α := WithBot α) ⊥ 0
⊢ unbotD 0 ((↑a : WithBot α) * ⊥) = unbotD 0 (↑a : WithBot α) * unbotD 0 ⊥
have neg : unbotD 0 ⊥ = unbotD 0 (↑a : WithBot α) * unbotD 0 ⊥
Tactic: rw [mul_bot ha, unbotD_bot, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithBot α) = 0
hb : ¬Eq.{u_1 + 1} (α := WithBot α) ⊥ 0
neg : unbotD 0 ⊥ = unbotD 0 (↑a : WithBot α) * unbotD 0 ⊥
⊢ unbotD 0 ((↑a : WithBot α) * ⊥) = unbotD 0 (↑a : WithBot α) * unbotD 0 ⊥
have neg₁ : 0 = unbotD 0 (↑a : WithBot α) * 0
Tactic: rw [mul_bot ha, unbotD_bot, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithBot α) = 0
hb : ¬Eq.{u_1 + 1} (α := WithBot α) ⊥ 0
neg : unbotD 0 ⊥ = unbotD 0 (↑a : WithBot α) * unbotD 0 ⊥
neg₁ : 0 = unbotD 0 (↑a : WithBot α) * 0
⊢ unbotD 0 ((↑a : WithBot α) * ⊥) = unbotD 0 (↑a : WithBot α) * unbotD 0 ⊥
have neg₂ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [mul_bot ha, unbotD_bot, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithBot α) = 0
a_1 : α
hb : ¬(↑a_1 : WithBot α) = 0
⊢ unbotD 0 ((↑a : WithBot α) * (↑a_1 : WithBot α)) = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
have neg : unbotD 0 (↑(a * a_1) : WithBot α) = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
Tactic: rw [← coe_mul, unbotD_coe, unbotD_coe, unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithBot α) = 0
a_1 : α
hb : ¬(↑a_1 : WithBot α) = 0
neg : unbotD 0 (↑(a * a_1) : WithBot α) = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
⊢ unbotD 0 ((↑a : WithBot α) * (↑a_1 : WithBot α)) = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
have neg₁ : a * a_1 = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
Tactic: rw [← coe_mul, unbotD_coe, unbotD_coe, unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithBot α) = 0
a_1 : α
hb : ¬(↑a_1 : WithBot α) = 0
neg : unbotD 0 (↑(a * a_1) : WithBot α) = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
neg₁ : a * a_1 = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
⊢ unbotD 0 ((↑a : WithBot α) * (↑a_1 : WithBot α)) = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
have neg₂ : a * a_1 = a * unbotD 0 (↑a_1 : WithBot α)
Tactic: rw [← coe_mul, unbotD_coe, unbotD_coe, unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : ¬(↑a : WithBot α) = 0
a_1 : α
hb : ¬(↑a_1 : WithBot α) = 0
neg : unbotD 0 (↑(a * a_1) : WithBot α) = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
neg₁ : a * a_1 = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
neg₂ : a * a_1 = a * unbotD 0 (↑a_1 : WithBot α)
⊢ unbotD 0 ((↑a : WithBot α) * (↑a_1 : WithBot α)) = unbotD 0 (↑a : WithBot α) * unbotD 0 (↑a_1 : WithBot α)
have neg₃ : a * a_1 = a * a_1
Tactic: rw [← coe_mul, unbotD_coe, unbotD_coe, unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
⊢ x * a ≤ x * b
have inl : ∀ (x0 : LE.le.{u_1} (α := WithBot α) 0 0), 0 * a ≤ 0 * b
Tactic: rcases eq_or_ne x 0 with rfl | x0'
Cleared hypotheses: x, x0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
inl : ∀ (x0 : LE.le.{u_1} (α := WithBot α) 0 0), 0 * a ≤ 0 * b
⊢ x * a ≤ x * b
have inr : ∀ (x0' : x ≠ 0), x * a ≤ x * b
Tactic: rcases eq_or_ne x 0 with rfl | x0'
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ x * a ≤ x * b
have lift : x ≠ ⊥
Tactic: lift x to α
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
lift : x ≠ ⊥
⊢ x * a ≤ x * b
have inr : ∀ (x : α) (x0 : 0 ≤ (↑x : WithBot α)) (x0' : (↑x : WithBot α) ≠ 0), (↑x : WithBot α) * a ≤ (↑x : WithBot α) * b
Tactic: lift x to α
Cleared hypotheses: x, x0, x0'
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
a b : WithBot α
h : a ≤ b
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
⊢ (↑x : WithBot α) * a ≤ (↑x : WithBot α) * b
have inr : ∀ (h : ⊥ ≤ b), (↑x : WithBot α) * ⊥ ≤ (↑x : WithBot α) * b
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
a b : WithBot α
h : a ≤ b
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
inr : ∀ (h : ⊥ ≤ b), (↑x : WithBot α) * ⊥ ≤ (↑x : WithBot α) * b
⊢ (↑x : WithBot α) * a ≤ (↑x : WithBot α) * b
have inr₁ : ∀ (a : α) (h : (↑a : WithBot α) ≤ b), (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * b
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
b : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
h : ⊥ ≤ b
⊢ (↑x : WithBot α) * ⊥ ≤ (↑x : WithBot α) * b
have inr : ⊥ ≤ (↑x : WithBot α) * b
Tactic: simp_rw [mul_bot x0', bot_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
b : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a : α
h : (↑a : WithBot α) ≤ b
⊢ (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * b
have inr : ∀ (h : (↑a : WithBot α) ≤ ⊥), (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * ⊥
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
b : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a : α
h : (↑a : WithBot α) ≤ b
inr : ∀ (h : (↑a : WithBot α) ≤ ⊥), (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * ⊥
⊢ (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * b
have inr₁ : ∀ (a_1 : α) (h : (↑a : WithBot α) ≤ (↑a_1 : WithBot α)),
  (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * (↑a_1 : WithBot α)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
⊢ (↑x : WithBot α) * (↑a : WithBot α) ≤ (↑x : WithBot α) * (↑a_1 : WithBot α)
have inr : ∀ (h : a ≤ a_1), x * a ≤ x * a_1
Tactic: simp only [← coe_mul, coe_le_coe] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulMono α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : a ≤ a_1
⊢ x * a ≤ x * a_1
have x0₁ : 0 ≤ x
Tactic: norm_cast at x0
Cleared hypotheses: x0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
⊢ a * x ≤ b * x
have inl : ∀ (x0 : LE.le.{u_1} (α := WithBot α) 0 0), a * 0 ≤ b * 0
Tactic: rcases eq_or_ne x 0 with rfl | x0'
Cleared hypotheses: x, x0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
inl : ∀ (x0 : LE.le.{u_1} (α := WithBot α) 0 0), a * 0 ≤ b * 0
⊢ a * x ≤ b * x
have inr : ∀ (x0' : x ≠ 0), a * x ≤ b * x
Tactic: rcases eq_or_ne x 0 with rfl | x0'
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ a * x ≤ b * x
have lift : x ≠ ⊥
Tactic: lift x to α
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
lift : x ≠ ⊥
⊢ a * x ≤ b * x
have inr : ∀ (x : α) (x0 : 0 ≤ (↑x : WithBot α)) (x0' : (↑x : WithBot α) ≠ 0), a * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
Tactic: lift x to α
Cleared hypotheses: x, x0, x0'
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
a b : WithBot α
h : a ≤ b
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
⊢ a * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
have inr : ∀ (h : ⊥ ≤ b), ⊥ * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
a b : WithBot α
h : a ≤ b
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
inr : ∀ (h : ⊥ ≤ b), ⊥ * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
⊢ a * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
have inr₁ : ∀ (a : α) (h : (↑a : WithBot α) ≤ b), (↑a : WithBot α) * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
h : ⊥ ≤ b
⊢ ⊥ * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
have inr : ⊥ ≤ b * (↑x : WithBot α)
Tactic: simp_rw [bot_mul x0', bot_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a : α
h : (↑a : WithBot α) ≤ b
⊢ (↑a : WithBot α) * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
have inr : ∀ (h : (↑a : WithBot α) ≤ ⊥), (↑a : WithBot α) * (↑x : WithBot α) ≤ ⊥ * (↑x : WithBot α)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a : α
h : (↑a : WithBot α) ≤ b
inr : ∀ (h : (↑a : WithBot α) ≤ ⊥), (↑a : WithBot α) * (↑x : WithBot α) ≤ ⊥ * (↑x : WithBot α)
⊢ (↑a : WithBot α) * (↑x : WithBot α) ≤ b * (↑x : WithBot α)
have inr₁ : ∀ (a_1 : α) (h : (↑a : WithBot α) ≤ (↑a_1 : WithBot α)),
  (↑a : WithBot α) * (↑x : WithBot α) ≤ (↑a_1 : WithBot α) * (↑x : WithBot α)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
⊢ (↑a : WithBot α) * (↑x : WithBot α) ≤ (↑a_1 : WithBot α) * (↑x : WithBot α)
have inr : ∀ (h : a ≤ a_1), a * x ≤ a_1 * x
Tactic: simp only [← coe_mul, coe_le_coe] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosMono α
x : α
x0 : 0 ≤ (↑x : WithBot α)
x0' : (↑x : WithBot α) ≠ 0
a a_1 : α
h : a ≤ a_1
⊢ a * x ≤ a_1 * x
have x0₁ : 0 ≤ x
Tactic: norm_cast at x0
Cleared hypotheses: x0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : a < b
⊢ x * a < x * b
have lift : ∀ (x : α) (x0 : 0 < (↑x : WithBot α)), (↑x : WithBot α) * a < (↑x : WithBot α) * b
Tactic: lift x to α using x0.ne_bot
Cleared hypotheses: x, x0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a b : WithBot α
h : a < b
x : α
x0 : 0 < (↑x : WithBot α)
⊢ (↑x : WithBot α) * a < (↑x : WithBot α) * b
have bot : ∀ (h : a < ⊥), (↑x : WithBot α) * a < (↑x : WithBot α) * ⊥
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a b : WithBot α
h : a < b
x : α
x0 : 0 < (↑x : WithBot α)
bot : ∀ (h : a < ⊥), (↑x : WithBot α) * a < (↑x : WithBot α) * ⊥
⊢ (↑x : WithBot α) * a < (↑x : WithBot α) * b
have coe : ∀ (a_1 : α) (h : a < (↑a_1 : WithBot α)), (↑x : WithBot α) * a < (↑x : WithBot α) * (↑a_1 : WithBot α)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
a_1 : α
h : a < (↑a_1 : WithBot α)
⊢ (↑x : WithBot α) * a < (↑x : WithBot α) * (↑a_1 : WithBot α)
have coe : ∀ (h : ⊥ < (↑a_1 : WithBot α)), (↑x : WithBot α) * ⊥ < (↑x : WithBot α) * (↑a_1 : WithBot α)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
a : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
a_1 : α
h : a < (↑a_1 : WithBot α)
coe : ∀ (h : ⊥ < (↑a_1 : WithBot α)), (↑x : WithBot α) * ⊥ < (↑x : WithBot α) * (↑a_1 : WithBot α)
⊢ (↑x : WithBot α) * a < (↑x : WithBot α) * (↑a_1 : WithBot α)
have coe₁ : ∀ (a : α) (h : (↑a : WithBot α) < (↑a_1 : WithBot α)),
  (↑x : WithBot α) * (↑a : WithBot α) < (↑x : WithBot α) * (↑a_1 : WithBot α)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
x : α
x0 : 0 < (↑x : WithBot α)
a : α
h : ⊥ < (↑a : WithBot α)
⊢ (↑x : WithBot α) * ⊥ < (↑x : WithBot α) * (↑a : WithBot α)
have coe : ⊥ < (↑x : WithBot α) * (↑a : WithBot α)
Tactic: simp_rw [mul_bot x0.ne.symm, ← coe_mul, bot_lt_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
x : α
x0 : 0 < (↑x : WithBot α)
a : α
h : ⊥ < (↑a : WithBot α)
coe : ⊥ < (↑x : WithBot α) * (↑a : WithBot α)
⊢ (↑x : WithBot α) * ⊥ < (↑x : WithBot α) * (↑a : WithBot α)
have coe₁ : ⊥ < (↑(x * a) : WithBot α)
Tactic: simp_rw [mul_bot x0.ne.symm, ← coe_mul, bot_lt_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
x : α
x0 : 0 < (↑x : WithBot α)
a a_1 : α
h : (↑a_1 : WithBot α) < (↑a : WithBot α)
⊢ (↑x : WithBot α) * (↑a_1 : WithBot α) < (↑x : WithBot α) * (↑a : WithBot α)
have coe : ∀ (h : a_1 < a), x * a_1 < x * a
Tactic: simp only [← coe_mul, coe_lt_coe] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : PosMulStrictMono α
x : α
x0 : 0 < (↑x : WithBot α)
a a_1 : α
h : a_1 < a
⊢ x * a_1 < x * a
have x0₁ : 0 < x
Tactic: norm_cast at x0
Cleared hypotheses: x0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : a < b
⊢ a * x < b * x
have lift : ∀ (x : α) (x0 : 0 < (↑x : WithBot α)), a * (↑x : WithBot α) < b * (↑x : WithBot α)
Tactic: lift x to α using x0.ne_bot
Cleared hypotheses: x, x0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a b : WithBot α
h : a < b
x : α
x0 : 0 < (↑x : WithBot α)
⊢ a * (↑x : WithBot α) < b * (↑x : WithBot α)
have bot : ∀ (h : a < ⊥), a * (↑x : WithBot α) < ⊥ * (↑x : WithBot α)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a b : WithBot α
h : a < b
x : α
x0 : 0 < (↑x : WithBot α)
bot : ∀ (h : a < ⊥), a * (↑x : WithBot α) < ⊥ * (↑x : WithBot α)
⊢ a * (↑x : WithBot α) < b * (↑x : WithBot α)
have coe : ∀ (a_1 : α) (h : a < (↑a_1 : WithBot α)), a * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
a_1 : α
h : a < (↑a_1 : WithBot α)
⊢ a * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)
have coe : ∀ (h : ⊥ < (↑a_1 : WithBot α)), ⊥ * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
a : WithBot α
x : α
x0 : 0 < (↑x : WithBot α)
a_1 : α
h : a < (↑a_1 : WithBot α)
coe : ∀ (h : ⊥ < (↑a_1 : WithBot α)), ⊥ * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)
⊢ a * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)
have coe₁ : ∀ (a : α) (h : (↑a : WithBot α) < (↑a_1 : WithBot α)),
  (↑a : WithBot α) * (↑x : WithBot α) < (↑a_1 : WithBot α) * (↑x : WithBot α)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
x : α
x0 : 0 < (↑x : WithBot α)
a : α
h : ⊥ < (↑a : WithBot α)
⊢ ⊥ * (↑x : WithBot α) < (↑a : WithBot α) * (↑x : WithBot α)
have coe : ⊥ < (↑a : WithBot α) * (↑x : WithBot α)
Tactic: simp_rw [bot_mul x0.ne.symm, ← coe_mul, bot_lt_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
x : α
x0 : 0 < (↑x : WithBot α)
a : α
h : ⊥ < (↑a : WithBot α)
coe : ⊥ < (↑a : WithBot α) * (↑x : WithBot α)
⊢ ⊥ * (↑x : WithBot α) < (↑a : WithBot α) * (↑x : WithBot α)
have coe₁ : ⊥ < (↑(a * x) : WithBot α)
Tactic: simp_rw [bot_mul x0.ne.symm, ← coe_mul, bot_lt_coe]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
inst_2 : Preorder α
inst_3 : MulPosStrictMono α
x : α
x0 : 0 < (↑x : WithBot α)
a a_1 : α
h : (↑a_1 : WithBot α) < (↑a : WithBot α)
⊢ (↑a_1 : WithBot α) * (↑x : WithBot α) < (↑a : WithBot α) * (↑x : WithBot α)
have coe : ∀ (h : a_1 < a), a_1 * x < a * x
Tactic: simp only [← coe_mul, coe_lt_coe] at *
Cleared hypotheses: h