case top
α : Type ?u.257111
β : Type ?u.257114
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
ha✝ : a ≠ 0 ∨ b ≠ ⊤
hb✝ : a ≠ ⊤ ∨ b ≠ 0
ha : a ≠ 0 ∨ ⊤ ≠ ⊤
hb : a ≠ ⊤ ∨ ⊤ ≠ 0
⊢ (a * ⊤)⁻¹ = a⁻¹ * ⊤⁻¹

case coe
α : Type ?u.257111
β : Type ?u.257114
a✝ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a b✝ : ℝ≥0∞
ha✝ : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : a ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha : a ≠ 0 ∨ ↑b ≠ ⊤
hb : a ≠ ⊤ ∨ ↑b ≠ 0
⊢ (a * ↑b)⁻¹ = a⁻¹ * (↑b)⁻¹
α : Type ?u.257111
β : Type ?u.257114
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : a ≠ ⊤ ∨ b ≠ 0
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
induction' b using recTopCoe with b
case coe.top
α : Type ?u.257111
β : Type ?u.257114
a✝ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a b✝ : ℝ≥0∞
ha✝² : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a ≠ ⊤ ∨ ↑b ≠ 0
ha✝ : ⊤ ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ⊤ ≠ ⊤ ∨ b✝ ≠ 0
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ⊤ ≠ ⊤ ∨ ↑b ≠ 0
⊢ (⊤ * ↑b)⁻¹ = ⊤⁻¹ * (↑b)⁻¹

case coe.coe
α : Type ?u.257111
β : Type ?u.257114
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹
case coe
α : Type ?u.257111
β : Type ?u.257114
a✝ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a b✝ : ℝ≥0∞
ha✝ : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : a ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha : a ≠ 0 ∨ ↑b ≠ ⊤
hb : a ≠ ⊤ ∨ ↑b ≠ 0
⊢ (a * ↑b)⁻¹ = a⁻¹ * (↑b)⁻¹
induction' a using recTopCoe with a
case pos
α : Type ?u.257111
β : Type ?u.257114
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : a = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹

case neg
α : Type ?u.257111
β : Type ?u.257114
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹
case coe.coe
α : Type ?u.257111
β : Type ?u.257114
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹
by_cases h'a : a = 0
case pos
α : Type ?u.257111
β : Type ?u.257114
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : b = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹

case neg
α : Type ?u.257111
β : Type ?u.257114
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : ¬b = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹
case neg
α : Type ?u.257111
β : Type ?u.257114
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹
by_cases h'b : b = 0
case neg
α : Type ?u.257111
β : Type ?u.257114
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : ¬b = 0
⊢ a * b ≠ 0
case neg
α : Type ?u.257111
β : Type ?u.257114
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : ¬b = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹
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]
no goals
case neg
α : Type ?u.257111
β : Type ?u.257114
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : ¬b = 0
⊢ a * b ≠ 0
simp [h'a, h'b]
case top
α : Type ?u.257111
β : Type ?u.257114
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
ha✝ : a ≠ 0 ∨ b ≠ ⊤
hb✝ : a ≠ ⊤ ∨ b ≠ 0
hb : a ≠ ⊤ ∨ ⊤ ≠ 0
ha : a ≠ 0
⊢ (a * ⊤)⁻¹ = a⁻¹ * ⊤⁻¹
case top
α : Type ?u.257111
β : Type ?u.257114
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
ha✝ : a ≠ 0 ∨ b ≠ ⊤
hb✝ : a ≠ ⊤ ∨ b ≠ 0
ha : a ≠ 0 ∨ ⊤ ≠ ⊤
hb : a ≠ ⊤ ∨ ⊤ ≠ 0
⊢ (a * ⊤)⁻¹ = a⁻¹ * ⊤⁻¹
replace ha : a ≠ 0 := ha.neg_resolve_right rfl
no goals
case top
α : Type ?u.257111
β : Type ?u.257114
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
ha✝ : a ≠ 0 ∨ b ≠ ⊤
hb✝ : a ≠ ⊤ ∨ b ≠ 0
hb : a ≠ ⊤ ∨ ⊤ ≠ 0
ha : a ≠ 0
⊢ (a * ⊤)⁻¹ = a⁻¹ * ⊤⁻¹
simp [ha]
case coe.top
α : Type ?u.257111
β : Type ?u.257114
a✝ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a b✝ : ℝ≥0∞
ha✝² : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a ≠ ⊤ ∨ ↑b ≠ 0
ha✝ : ⊤ ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ⊤ ≠ ⊤ ∨ b✝ ≠ 0
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : b ≠ 0
⊢ (⊤ * ↑b)⁻¹ = ⊤⁻¹ * (↑b)⁻¹
case coe.top
α : Type ?u.257111
β : Type ?u.257114
a✝ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a b✝ : ℝ≥0∞
ha✝² : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a ≠ ⊤ ∨ ↑b ≠ 0
ha✝ : ⊤ ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ⊤ ≠ ⊤ ∨ b✝ ≠ 0
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ⊤ ≠ ⊤ ∨ ↑b ≠ 0
⊢ (⊤ * ↑b)⁻¹ = ⊤⁻¹ * (↑b)⁻¹
replace hb : b ≠ 0 := coe_ne_zero.1 (hb.neg_resolve_left rfl)
no goals
case coe.top
α : Type ?u.257111
β : Type ?u.257114
a✝ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a b✝ : ℝ≥0∞
ha✝² : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a ≠ ⊤ ∨ ↑b ≠ 0
ha✝ : ⊤ ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ⊤ ≠ ⊤ ∨ b✝ ≠ 0
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : b ≠ 0
⊢ (⊤ * ↑b)⁻¹ = ⊤⁻¹ * (↑b)⁻¹
simp [hb]
no goals
case pos
α : Type ?u.257111
β : Type ?u.257114
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : a = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹
simp only [h'a, top_mul, ENNReal.inv_zero, ENNReal.coe_ne_top, zero_mul, Ne.def,
  not_false_iff, ENNReal.coe_zero, ENNReal.inv_eq_zero]
no goals
case pos
α : Type ?u.257111
β : Type ?u.257114
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : b = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹
simp only [h'b, ENNReal.inv_zero, ENNReal.coe_ne_top, mul_top, Ne.def, not_false_iff,
  mul_zero, ENNReal.coe_zero, ENNReal.inv_eq_zero]