-- Mathlib/Data/ENNReal/Inv.lean
theorem mul_inv {a b : ℝ≥0∞} (ha : a ≠ 0 ∨ b ≠ ∞) (hb : a ≠ ∞ ∨ b ≠ 0) :
    (a * b)⁻¹ = a⁻¹ * b⁻¹

Proof state:
case neg
b a : ℝ≥0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : ¬b = 0
⊢ a * b ≠ 0

Tactic:
simp [h'a, h'b]

Result:
no goals

Proof state:
case coe.coe
b a : ℝ≥0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹

Tactic:
by_cases h'a : a = 0

Result:
case pos
b a : ℝ≥0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : a = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹

case neg
b a : ℝ≥0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹

Proof state:
case pos
b a : ℝ≥0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : a = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹

Tactic:
simp only [h'a, top_mul, ENNReal.inv_zero, ENNReal.coe_ne_top, zero_mul, Ne,
  not_false_iff, ENNReal.coe_zero, ENNReal.inv_eq_zero]

Result:
no goals

Proof state:
case neg
b a : ℝ≥0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹

Tactic:
by_cases h'b : b = 0

Result:
case pos
b a : ℝ≥0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : b = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹

case neg
b a : ℝ≥0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : ¬b = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹

Proof state:
case coe
a : ℝ≥0∞
b : ℝ≥0
ha : a ≠ 0 ∨ ↑b ≠ ⊤
hb : a ≠ ⊤ ∨ ↑b ≠ 0
⊢ (a * ↑b)⁻¹ = a⁻¹ * (↑b)⁻¹

Tactic:
induction' a with a

Result:
case coe.top
b : ℝ≥0
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ⊤ ≠ ⊤ ∨ ↑b ≠ 0
⊢ (⊤ * ↑b)⁻¹ = ⊤⁻¹ * (↑b)⁻¹

case coe.coe
b a : ℝ≥0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹

Proof state:
case neg
b a : ℝ≥0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : ¬b = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹

Tactic:
rw [← ENNReal.coe_mul, ← ENNReal.coe_inv, ← ENNReal.coe_inv h'a, ← ENNReal.coe_inv h'b, ←
  ENNReal.coe_mul, mul_inv_rev, mul_comm]

Result:
case neg
b a : ℝ≥0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : ¬b = 0
⊢ a * b ≠ 0

Proof state:
case top
a : ℝ≥0∞
ha : a ≠ 0 ∨ ⊤ ≠ ⊤
hb : a ≠ ⊤ ∨ ⊤ ≠ 0
⊢ (a * ⊤)⁻¹ = a⁻¹ * ⊤⁻¹

Tactic:
replace ha : a ≠ 0 := ha.neg_resolve_right rfl

Result:
case top
a : ℝ≥0∞
hb : a ≠ ⊤ ∨ ⊤ ≠ 0
ha : a ≠ 0
⊢ (a * ⊤)⁻¹ = a⁻¹ * ⊤⁻¹

Proof state:
case coe.top
b : ℝ≥0
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : b ≠ 0
⊢ (⊤ * ↑b)⁻¹ = ⊤⁻¹ * (↑b)⁻¹

Tactic:
simp [hb]

Result:
no goals

Proof state:
case pos
b a : ℝ≥0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : b = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹

Tactic:
simp only [h'b, ENNReal.inv_zero, ENNReal.coe_ne_top, mul_top, Ne, not_false_iff,
  mul_zero, ENNReal.coe_zero, ENNReal.inv_eq_zero]

Result:
no goals

Proof state:
a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : a ≠ ⊤ ∨ b ≠ 0
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
induction' b with b

Result:
case top
a : ℝ≥0∞
ha : a ≠ 0 ∨ ⊤ ≠ ⊤
hb : a ≠ ⊤ ∨ ⊤ ≠ 0
⊢ (a * ⊤)⁻¹ = a⁻¹ * ⊤⁻¹

case coe
a : ℝ≥0∞
b : ℝ≥0
ha : a ≠ 0 ∨ ↑b ≠ ⊤
hb : a ≠ ⊤ ∨ ↑b ≠ 0
⊢ (a * ↑b)⁻¹ = a⁻¹ * (↑b)⁻¹

Proof state:
case top
a : ℝ≥0∞
hb : a ≠ ⊤ ∨ ⊤ ≠ 0
ha : a ≠ 0
⊢ (a * ⊤)⁻¹ = a⁻¹ * ⊤⁻¹

Tactic:
simp [ha]

Result:
no goals

Proof state:
case coe.top
b : ℝ≥0
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ⊤ ≠ ⊤ ∨ ↑b ≠ 0
⊢ (⊤ * ↑b)⁻¹ = ⊤⁻¹ * (↑b)⁻¹

Tactic:
replace hb : b ≠ 0 := coe_ne_zero.1 (hb.neg_resolve_left rfl)

Result:
case coe.top
b : ℝ≥0
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : b ≠ 0
⊢ (⊤ * ↑b)⁻¹ = ⊤⁻¹ * (↑b)⁻¹