-- Mathlib/Algebra/Order/Ring/WithTop.lean
@[simp]
lemma unbotD_zero_mul (a b : WithBot α) : (a * b).unbotD 0 = a.unbotD 0 * b.unbotD 0

Proof state:
case neg.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
ha : ¬⊥ = 0
⊢ unbotD 0 (⊥ * b) = unbotD 0 ⊥ * unbotD 0 b

Tactic:
rw [bot_mul hb, unbotD_bot, zero_mul]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
by_cases ha : a = 0

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : a = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Proof state:
case neg.coe.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊥ = 0
⊢ unbotD 0 (↑a✝ * ⊥) = unbotD 0 ↑a✝ * unbotD 0 ⊥

Tactic:
rw [mul_bot ha, unbotD_bot, mul_zero]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

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

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
by_cases hb : b = 0

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : ¬b = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : ¬b = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
induction a

Result:
case neg.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
ha : ¬⊥ = 0
⊢ unbotD 0 (⊥ * b) = unbotD 0 ⊥ * unbotD 0 b

case neg.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
a✝ : α
ha : ¬↑a✝ = 0
⊢ unbotD 0 (↑a✝ * b) = unbotD 0 ↑a✝ * unbotD 0 b

Proof state:
case neg.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
a✝ : α
ha : ¬↑a✝ = 0
⊢ unbotD 0 (↑a✝ * b) = unbotD 0 ↑a✝ * unbotD 0 b

Tactic:
induction b

Result:
case neg.coe.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊥ = 0
⊢ unbotD 0 (↑a✝ * ⊥) = unbotD 0 ↑a✝ * unbotD 0 ⊥

case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ unbotD 0 (↑a✝¹ * ↑a✝) = unbotD 0 ↑a✝¹ * unbotD 0 ↑a✝

Proof state:
case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ unbotD 0 (↑a✝¹ * ↑a✝) = unbotD 0 ↑a✝¹ * unbotD 0 ↑a✝

Tactic:
rw [← coe_mul, unbotD_coe, unbotD_coe, unbotD_coe]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : a = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

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

Result:
no goals