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 : NonUnitalNonAssocSemiring α
inst_2 : PartialOrder α
inst_3 : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (a + b) * (↑c : WithTop α) = a * (↑c : WithTop α) + b * (↑c : WithTop α)
have 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))
Tactic: simp only [mul_coe_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 (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))
have 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))
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 (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))
⊢ (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))
have 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))
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 (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))
have 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))
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 (a : α) ↦ Option.some (a * c)) =
    HAdd.hAdd (α := WithTop α) (Option.bind ⊤ fun (a : α) ↦ Option.some (a * c))
      (Option.bind ⊤ 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))
have 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))
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 (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))
have 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))
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 (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))
⊢ (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))
have 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))
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 α
a b c : WithTop α
⊢ (a + b) * c = a * c + b * c
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 [mul_coe_eq_bind hc]
      cases a <;> cases b <;> try rfl
      exact congr_arg some (add_mul _ _ _)
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 c : WithTop α
top : (a + b) * ⊤ = a * ⊤ + b * ⊤
⊢ (a + b) * c = a * c + b * c
have coe : ∀ (c : α), (a + b) * (↑c : WithTop α) = a * (↑c : WithTop α) + b * (↑c : WithTop α)
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 _ _ _)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (hypothesis)
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₂
⊢ a₁ * b₁ < a₂ * b₂
have this : MulPosStrictMono α
Tactic: have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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₁ * b₁ < a₂ * b₂
have lift : ∀ (a₁ : α) (ha : (↑a₁ : WithTop α) < a₂), (↑a₁ : WithTop α) * b₁ < a₂ * b₂
Tactic: lift a₁ to α using ha.lt_top.ne
Cleared hypotheses: a₁, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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₂
⊢ (↑a₁ : WithTop α) * b₁ < a₂ * b₂
have lift : ∀ (b₁ : α) (hb : (↑b₁ : WithTop α) < b₂), (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * b₂
Tactic: lift b₁ to α using hb.lt_top.ne
Cleared hypotheses: b₁, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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₂
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * b₂
have inl : ∀ (ha : (↑a₁ : WithTop α) < ⊤), (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < ⊤ * b₂
Tactic: obtain rfl | ha₂ := eq_or_ne a₂ ⊤
Cleared hypotheses: a₂, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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₂
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * b₂
have inr : ∀ (ha₂ : a₂ ≠ ⊤), (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * b₂
Tactic: obtain rfl | ha₂ := eq_or_ne a₂ ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α) < ⊤ * b₂
have inl : (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < ⊤
Tactic: rw [top_mul (by simpa [bot_eq_zero] using hb.bot_lt.ne')]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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₂ ≠ ⊤
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * b₂
have inr : ∀ (hb : (↑b₁ : WithTop α) < ⊤), (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * ⊤
Tactic: obtain rfl | hb₂ := eq_or_ne b₂ ⊤
Cleared hypotheses: b₂, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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₂ * ⊤
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * b₂
have inr₁ : ∀ (hb₂ : b₂ ≠ ⊤), (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * b₂
Tactic: obtain rfl | hb₂ := eq_or_ne b₂ ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α) < a₂ * ⊤
have inr : (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < ⊤
Tactic: rw [mul_top (by simpa [bot_eq_zero] using ha.bot_lt.ne')]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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₁ : WithTop α) * (↑b₁ : WithTop α) < a₂ * b₂
have inr : ∀ (a₂ : α) (ha : (↑a₁ : WithTop α) < (↑a₂ : WithTop α)), (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < (↑a₂ : WithTop α) * b₂
Tactic: lift a₂ to α using ha₂
Cleared hypotheses: a₂, ha, ha₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α)
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < (↑a₂ : WithTop α) * b₂
have inr : ∀ (b₂ : α) (hb : (↑b₁ : WithTop α) < (↑b₂ : WithTop α)),
  (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < (↑a₂ : WithTop α) * (↑b₂ : WithTop α)
Tactic: lift b₂ to α using hb₂
Cleared hypotheses: b₂, hb, hb₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 α)
⊢ (↑a₁ : WithTop α) * (↑b₁ : WithTop α) < (↑a₂ : WithTop α) * (↑b₂ : WithTop α)
have inr : ∀ (ha : a₁ < a₂) (hb : b₁ < b₂), a₁ * b₁ < a₂ * b₂
Tactic: norm_cast at *
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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
⊢ LT.lt.{u_1} (α := WithTop α) ((fun (a : WithTop α) ↦ a ^ (n + 2)) x) ((fun (a : WithTop α) ↦ a ^ (n + 2)) y)
have simp_rw : x ^ (n + 1) * x < y ^ (n + 1) * y
Tactic: simp_rw [pow_succ _ (n + 1)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : WithBot α
h : a ≠ 0
⊢ a * ⊥ = ⊥
have rw : Eq.{u_1 + 1} (α := WithBot α) (if a = 0 then 0 else ⊥) ⊥
Tactic: rw [mul_bot', if_neg h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
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 ⊥) ⊥
⊢ a * ⊥ = ⊥
have rw₁ : Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
Tactic: rw [mul_bot', if_neg h]
-- 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
⊢ ⊥ * b = ⊥
have rw : Eq.{u_1 + 1} (α := WithBot α) (if b = 0 then 0 else ⊥) ⊥
Tactic: rw [bot_mul', if_neg 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
rw : Eq.{u_1 + 1} (α := WithBot α) (if b = 0 then 0 else ⊥) ⊥
⊢ ⊥ * b = ⊥
have rw₁ : Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
Tactic: rw [bot_mul', if_neg hb]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithBot α
⊢ a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) a b
have bot : ⊥ * b = if Eq.{u_1 + 1} (α := WithBot α) ⊥ 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊥ 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 : 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
⊢ a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) a b
have coe : ∀ (a : α),
  (↑a : WithBot α) * b = if (↑a : WithBot α) = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithBot α) 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 : MulZeroClass α
b : WithBot α
⊢ ⊥ * b = if Eq.{u_1 + 1} (α := WithBot α) ⊥ 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊥ b
have 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) ⊥ ⊥
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 : 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) ⊥ ⊥
⊢ ⊥ * b = if Eq.{u_1 + 1} (α := WithBot α) ⊥ 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) ⊥ b
have 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 α)
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 : MulZeroClass α
b : WithBot α
a : α
⊢ (↑a : WithBot α) * b = if (↑a : WithBot α) = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithBot α) b
have coe : (↑a : WithBot α) * ⊥ =
  if (↑a : WithBot α) = 0 ∨ Eq.{u_1 + 1} (α := WithBot α) ⊥ 0 then 0
  else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithBot α) ⊥
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 : 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 α) ⊥
⊢ (↑a : WithBot α) * b = if (↑a : WithBot α) = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) ↦ x1 * x2) (↑a : WithBot α) b
have 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 α)
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 : MulZeroClass α
a b : WithBot α
⊢ a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0
have 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
Tactic: rw [mul_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊥ * (↑b : WithBot α) = Option.bind ⊥ fun (a : α) ↦ Option.some (a * b)
have simp : Eq.{u_1 + 1} (α := WithBot α) ⊥ (Option.bind ⊥ fun (a : α) ↦ Option.some (a * b))
Tactic: simp only [ne_eq, coe_eq_zero, hb, not_false_eq_true, bot_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a : α
ha : a ≠ 0
⊢ (↑a : WithBot α) * ⊥ = Option.bind ⊥ fun (b : α) ↦ Option.some (a * b)
have simp : Eq.{u_1 + 1} (α := WithBot α) ⊥ (Option.bind ⊥ fun (b : α) ↦ Option.some (a * b))
Tactic: simp only [ne_eq, coe_eq_zero, ha, not_false_eq_true, mul_bot]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.WithTop (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithBot α
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have pos : ∀ (ha : a = 0), unbotD 0 (a * b) = unbotD 0 a * unbotD 0 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 : MulZeroClass α
a b : WithBot α
pos : ∀ (ha : a = 0), unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have neg : ∀ (ha : ¬a = 0), unbotD 0 (a * b) = unbotD 0 a * unbotD 0 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 : MulZeroClass α
a b : WithBot α
ha : a = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have pos : unbotD 0 (0 * b) = unbotD 0 0 * unbotD 0 b
Tactic: rw [ha, zero_mul, ← coe_zero, unbotD_coe, zero_mul]
-- 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
pos : unbotD 0 (0 * b) = unbotD 0 0 * unbotD 0 b
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have pos₁ : unbotD 0 0 = unbotD 0 0 * unbotD 0 b
Tactic: rw [ha, zero_mul, ← coe_zero, unbotD_coe, zero_mul]
-- 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
pos : unbotD 0 (0 * b) = unbotD 0 0 * unbotD 0 b
pos₁ : unbotD 0 0 = unbotD 0 0 * unbotD 0 b
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have pos₂ : unbotD 0 (↑0 : WithBot α) = unbotD 0 (↑0 : WithBot α) * unbotD 0 b
Tactic: rw [ha, zero_mul, ← coe_zero, unbotD_coe, zero_mul]
-- 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
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
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have pos₃ : 0 = 0 * unbotD 0 b
Tactic: rw [ha, zero_mul, ← coe_zero, unbotD_coe, zero_mul]
-- 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
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
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have pos₄ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [ha, zero_mul, ← coe_zero, unbotD_coe, zero_mul]
-- 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
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have pos : ∀ (hb : b = 0), unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
Tactic: by_cases hb : b = 0
-- 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
pos : ∀ (hb : b = 0), unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have neg : ∀ (hb : ¬b = 0), unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
Tactic: by_cases hb : b = 0
-- 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 pos : unbotD 0 (a * 0) = unbotD 0 a * unbotD 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
pos : unbotD 0 (a * 0) = unbotD 0 a * unbotD 0 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have pos₁ : unbotD 0 0 = unbotD 0 a * unbotD 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
pos : unbotD 0 (a * 0) = unbotD 0 a * unbotD 0 0
pos₁ : unbotD 0 0 = unbotD 0 a * unbotD 0 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have pos₂ : unbotD 0 (↑0 : WithBot α) = unbotD 0 a * unbotD 0 (↑0 : WithBot α)
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
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 α)
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
have pos₃ : 0 = unbotD 0 a * 0
Tactic: rw [hb, mul_zero, ← coe_zero, unbotD_coe, mul_zero]