awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
⊢ (HPow.hPow (β := ℕ) x 0)⁻¹ = HPow.hPow (β := ℕ) x⁻¹ 0

Tactic:
simp only [pow_zero, inv_one]

Premises used: inv_one, pow_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
n : ℕ
⊢ (HPow.hPow (α := ℝ≥0∞) ∞ (n + 1))⁻¹ = HPow.hPow (α := ℝ≥0∞) ∞⁻¹ (n + 1)

Tactic:
simp [top_pow]

Premises used: ENNReal.top_pow
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
n : ℕ
inl : ((↑0 : ℝ≥0∞) ^ (n + 1))⁻¹ = (↑0 : ℝ≥0∞)⁻¹ ^ (n + 1)
inr : ∀ (ha : a ≠ 0), ((↑a : ℝ≥0∞) ^ (n + 1))⁻¹ = (↑a : ℝ≥0∞)⁻¹ ^ (n + 1)
⊢ ((↑a : ℝ≥0∞) ^ (n + 1))⁻¹ = (↑a : ℝ≥0∞)⁻¹ ^ (n + 1)

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
n : ℕ
⊢ ((↑0 : ℝ≥0∞) ^ (n + 1))⁻¹ = (↑0 : ℝ≥0∞)⁻¹ ^ (n + 1)

Tactic:
simp [top_pow]

Premises used: ENNReal.top_pow
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
n : ℕ
ha : a ≠ 0
⊢ a ^ (n + 1) ≠ 0

Tactic:
have := pow_ne_zero (n + 1) ha
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
inr : (a ^ (n + 1))⁻¹ = a⁻¹ ^ (n + 1)
⊢ ((↑a : ℝ≥0∞) ^ (n + 1))⁻¹ = (↑a : ℝ≥0∞)⁻¹ ^ (n + 1)

Tactic:
norm_cast
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
inr inr₁ : (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹
⊢ (a ^ (n + 1))⁻¹ = a⁻¹ ^ (n + 1)

Tactic:
rw [inv_pow]

Premises used: inv_pow
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
h0 : a ≠ 0
ht : a ≠ ∞
⊢ a ≠ ∞

Tactic:
ht
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
h0 : a ≠ 0
ht : a ≠ ∞
lift : ∀ (a : ℝ≥0) (h0 : (↑a : ℝ≥0∞) ≠ 0), (↑a : ℝ≥0∞) * (↑a : ℝ≥0∞)⁻¹ = 1
⊢ a * a⁻¹ = 1

Tactic:
lift a to ℝ≥0 using ht
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
h0 : (↑a : ℝ≥0∞) ≠ 0
⊢ ¬a = 0

Tactic:
norm_cast at h0
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
h0 : ¬a = 0
norm_cast : a * a⁻¹ = 1
⊢ (↑a : ℝ≥0∞) * (↑a : ℝ≥0∞)⁻¹ = 1

Tactic:
norm_cast
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
h0 : ¬a = 0
⊢ a * a⁻¹ = 1

Tactic:
mul_inv_cancel₀ h0

Premises used: mul_inv_cancel₀
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
h0 : ¬a = 0
⊢ a * a⁻¹ = 1

Tactic:
exact mul_inv_cancel₀ h0

Premises used: mul_inv_cancel₀
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
h0 : a ≠ 0
ht : a ≠ ∞
⊢ a⁻¹ * a = 1

Tactic:
mul_comm a a⁻¹ ▸ ENNReal.mul_inv_cancel h0 ht

Premises used: Eq.rec, ENNReal.mul_inv_cancel, Inv.inv, mul_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ∞ → b = 0
inl : ∀ (ha₀ : Eq (α := ℝ≥0∞) 0 0 → b = 0) (ha : Eq (α := ℝ≥0∞) 0 ∞ → b = 0), 0⁻¹ * (0 * b) = b
inr : ∀ (ha₀ : a ≠ 0), a⁻¹ * (a * b) = b
⊢ a⁻¹ * (a * b) = b

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
b : ℝ≥0∞
ha₀ : Eq (α := ℝ≥0∞) 0 0 → b = 0
ha : Eq (α := ℝ≥0∞) 0 ∞ → b = 0
⊢ 0⁻¹ * (0 * b) = b

Tactic:
simp_all
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha₀_1 : a = 0 → b = 0
ha : a = ∞ → b = 0
ha₀ : a ≠ 0
inr :
  ∀ (ha₀ : Eq (α := ℝ≥0∞) ∞ 0 → b = 0) (ha : Eq (α := ℝ≥0∞) ∞ ∞ → b = 0) (ha₀ : Ne (α := ℝ≥0∞) ∞ 0), ∞⁻¹ * (∞ * b) = b
inr₁ : ∀ (ha : a ≠ ∞), a⁻¹ * (a * b) = b
⊢ a⁻¹ * (a * b) = b

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
b : ℝ≥0∞
ha₀_1 : Eq (α := ℝ≥0∞) ∞ 0 → b = 0
ha : Eq (α := ℝ≥0∞) ∞ ∞ → b = 0
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
⊢ ∞⁻¹ * (∞ * b) = b

Tactic:
simp_all
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha₀_1 : a = 0 → b = 0
ha_1 : a = ∞ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a⁻¹ * (a * b) = b

Tactic:
simp [← mul_assoc, ENNReal.inv_mul_cancel, *]

Premises used: mul_assoc, ENNReal.inv_mul_cancel
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a = 0 → b = 0

Tactic:
simp [ha₀]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a = ∞ → b = 0

Tactic:
simp [ha]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ∞ → b = 0
inl : ∀ (ha₀ : Eq (α := ℝ≥0∞) 0 0 → b = 0) (ha : Eq (α := ℝ≥0∞) 0 ∞ → b = 0), 0 * (0⁻¹ * b) = b
inr : ∀ (ha₀ : a ≠ 0), a * (a⁻¹ * b) = b
⊢ a * (a⁻¹ * b) = b

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
b : ℝ≥0∞
ha₀ : Eq (α := ℝ≥0∞) 0 0 → b = 0
ha : Eq (α := ℝ≥0∞) 0 ∞ → b = 0
⊢ 0 * (0⁻¹ * b) = b

Tactic:
simp_all
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha₀_1 : a = 0 → b = 0
ha : a = ∞ → b = 0
ha₀ : a ≠ 0
inr :
  ∀ (ha₀ : Eq (α := ℝ≥0∞) ∞ 0 → b = 0) (ha : Eq (α := ℝ≥0∞) ∞ ∞ → b = 0) (ha₀ : Ne (α := ℝ≥0∞) ∞ 0), ∞ * (∞⁻¹ * b) = b
inr₁ : ∀ (ha : a ≠ ∞), a * (a⁻¹ * b) = b
⊢ a * (a⁻¹ * b) = b

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
b : ℝ≥0∞
ha₀_1 : Eq (α := ℝ≥0∞) ∞ 0 → b = 0
ha : Eq (α := ℝ≥0∞) ∞ ∞ → b = 0
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
⊢ ∞ * (∞⁻¹ * b) = b

Tactic:
simp_all
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha₀_1 : a = 0 → b = 0
ha_1 : a = ∞ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * (a⁻¹ * b) = b

Tactic:
simp [← mul_assoc, ENNReal.mul_inv_cancel, *]

Premises used: mul_assoc, ENNReal.mul_inv_cancel
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
hb₀ : b = 0 → a = 0
hb : b = ∞ → a = 0
inl : ∀ (hb₀ : Eq (α := ℝ≥0∞) 0 0 → a = 0) (hb : Eq (α := ℝ≥0∞) 0 ∞ → a = 0), a * 0 * 0⁻¹ = a
inr : ∀ (hb₀ : b ≠ 0), a * b * b⁻¹ = a
⊢ a * b * b⁻¹ = a

Tactic:
obtain rfl | hb₀ := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
hb₀ : Eq (α := ℝ≥0∞) 0 0 → a = 0
hb : Eq (α := ℝ≥0∞) 0 ∞ → a = 0
⊢ a * 0 * 0⁻¹ = a

Tactic:
simp_all
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
hb₀_1 : b = 0 → a = 0
hb : b = ∞ → a = 0
hb₀ : b ≠ 0
inr : ∀ (hb₀ : Eq (α := ℝ≥0∞) ∞ 0 → a = 0) (hb : Eq (α := ℝ≥0∞) ∞ ∞ → a = 0) (hb₀ : Ne (α := ℝ≥0∞) ∞ 0), a * ∞ * ∞⁻¹ = a
inr₁ : ∀ (hb : b ≠ ∞), a * b * b⁻¹ = a
⊢ a * b * b⁻¹ = a

Tactic:
obtain rfl | hb := eq_or_ne b ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
hb₀_1 : Eq (α := ℝ≥0∞) ∞ 0 → a = 0
hb : Eq (α := ℝ≥0∞) ∞ ∞ → a = 0
hb₀ : Ne (α := ℝ≥0∞) ∞ 0
⊢ a * ∞ * ∞⁻¹ = a

Tactic:
simp_all
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
hb₀_1 : b = 0 → a = 0
hb_1 : b = ∞ → a = 0
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a * b * b⁻¹ = a

Tactic:
simp [mul_assoc, ENNReal.mul_inv_cancel, *]

Premises used: mul_assoc, ENNReal.mul_inv_cancel
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ b = 0 → a = 0

Tactic:
simp [hb₀]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ b = ∞ → a = 0

Tactic:
simp [hb]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
hb₀ : b = 0 → a = 0
hb : b = ∞ → a = 0
inl : ∀ (hb₀ : Eq (α := ℝ≥0∞) 0 0 → a = 0) (hb : Eq (α := ℝ≥0∞) 0 ∞ → a = 0), a * 0⁻¹ * 0 = a
inr : ∀ (hb₀ : b ≠ 0), a * b⁻¹ * b = a
⊢ a * b⁻¹ * b = a

Tactic:
obtain rfl | hb₀ := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
hb₀ : Eq (α := ℝ≥0∞) 0 0 → a = 0
hb : Eq (α := ℝ≥0∞) 0 ∞ → a = 0
⊢ a * 0⁻¹ * 0 = a

Tactic:
simp_all
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
hb₀_1 : b = 0 → a = 0
hb : b = ∞ → a = 0
hb₀ : b ≠ 0
inr : ∀ (hb₀ : Eq (α := ℝ≥0∞) ∞ 0 → a = 0) (hb : Eq (α := ℝ≥0∞) ∞ ∞ → a = 0) (hb₀ : Ne (α := ℝ≥0∞) ∞ 0), a * ∞⁻¹ * ∞ = a
inr₁ : ∀ (hb : b ≠ ∞), a * b⁻¹ * b = a
⊢ a * b⁻¹ * b = a

Tactic:
obtain rfl | hb := eq_or_ne b ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
hb₀_1 : Eq (α := ℝ≥0∞) ∞ 0 → a = 0
hb : Eq (α := ℝ≥0∞) ∞ ∞ → a = 0
hb₀ : Ne (α := ℝ≥0∞) ∞ 0
⊢ a * ∞⁻¹ * ∞ = a

Tactic:
simp_all
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
hb₀_1 : b = 0 → a = 0
hb_1 : b = ∞ → a = 0
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a * b⁻¹ * b = a

Tactic:
simp [mul_assoc, ENNReal.inv_mul_cancel, *]

Premises used: mul_assoc, ENNReal.inv_mul_cancel
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
hb₀ : b = 0 → a = 0
hb : b = ∞ → a = 0
⊢ a * b / b = a

Tactic:
ENNReal.mul_inv_cancel_right' hb₀ hb

Premises used: ENNReal.mul_inv_cancel_right', DivInvMonoid.div'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ∞ → b = 0
⊢ b / a * a = b

Tactic:
ENNReal.inv_mul_cancel_right' ha₀ ha

Premises used: DivInvMonoid.div', ENNReal.inv_mul_cancel_right'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ∞ → b = 0
rw : b / a * a = b
rw₁ rw₂ : b = b
⊢ a * (b / a) = b

Tactic:
rw [mul_comm, ENNReal.div_mul_cancel' ha₀ ha]

Premises used: mul_comm, ENNReal.div_mul_cancel'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
⊢ a / b * c = a * (c / b)

Tactic:
simp only [div_eq_mul_inv, mul_left_comm, mul_comm]

Premises used: mul_left_comm, div_eq_mul_inv, mul_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
⊢ a * b / c = a / c * b

Tactic:
simp only [div_eq_mul_inv, mul_right_comm]

Premises used: div_eq_mul_inv, mul_right_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
pos : a = 0 → a⁻¹⁻¹ = a
neg : ¬a = 0 → a⁻¹⁻¹ = a
⊢ a⁻¹⁻¹ = a

Tactic:
by_cases a = 0
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h : a = 0
pos : Eq (α := ℝ≥0∞) ∞ 0 → Eq (α := ℝ≥0∞) ∞⁻¹⁻¹ ∞
pos₁ : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞) = 0 → (↑x : ℝ≥0∞)⁻¹⁻¹ = (↑x : ℝ≥0∞)
⊢ a⁻¹⁻¹ = a

Tactic:
cases a
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h : ¬a = 0
neg : ¬Eq (α := ℝ≥0∞) ∞ 0 → Eq (α := ℝ≥0∞) ∞⁻¹⁻¹ ∞
neg₁ : ∀ (x : ℝ≥0), ¬(↑x : ℝ≥0∞) = 0 → (↑x : ℝ≥0∞)⁻¹⁻¹ = (↑x : ℝ≥0∞)
⊢ a⁻¹⁻¹ = a

Tactic:
cases a
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : Eq (α := ℝ≥0∞) ∞ 0
⊢ Eq (α := ℝ≥0∞) ∞⁻¹⁻¹ ∞

Tactic:
simp_all [-coe_inv, (coe_inv _).symm]

Premises used: ENNReal.coe_inv, Eq.symm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
r p q x : ℝ≥0
h : (↑x : ℝ≥0∞) = 0
⊢ (↑x : ℝ≥0∞)⁻¹⁻¹ = (↑x : ℝ≥0∞)

Tactic:
simp_all [-coe_inv, (coe_inv _).symm]

Premises used: ENNReal.coe_inv, Eq.symm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : ¬Eq (α := ℝ≥0∞) ∞ 0
⊢ Eq (α := ℝ≥0∞) ∞⁻¹⁻¹ ∞

Tactic:
simp_all [-coe_inv, (coe_inv _).symm]

Premises used: ENNReal.coe_inv, Eq.symm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
r p q x : ℝ≥0
h : ¬(↑x : ℝ≥0∞) = 0
⊢ (↑x : ℝ≥0∞)⁻¹⁻¹ = (↑x : ℝ≥0∞)

Tactic:
simp_all [-coe_inv, (coe_inv _).symm]

Premises used: ENNReal.coe_inv, Eq.symm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
rw : a⁻¹⁻¹ = 1⁻¹ ↔ a = 1
rw₁ : a = 1⁻¹ ↔ a = 1
rw₂ rw₃ : a = 1 ↔ a = 1
⊢ a⁻¹ = 1 ↔ a = 1

Tactic:
rw [← inv_inj, inv_inv, inv_one]

Premises used: inv_one, inv_inj, inv_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
⊢ a⁻¹ = ∞ ↔ a = 0

Tactic:
inv_zero ▸ inv_inj

Premises used: Eq.rec, ENNReal.inv_zero, inv_inj
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
⊢ a⁻¹ ≠ ∞ ↔ a ≠ 0

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
⊢ x⁻¹ < ∞ ↔ 0 < x

Tactic:
simp only [lt_top_iff_ne_top, inv_ne_top, pos_iff_ne_zero]

Premises used: ENNReal.inv_ne_top, lt_top_iff_ne_top, pos_iff_ne_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ≥0∞
h1 : x ≠ ∞
h2 : y ≠ 0
⊢ x / y < ∞

Tactic:
mul_lt_top h1.lt_top (inv_ne_top.mpr h2).lt_top

Premises used: Iff.mpr, ENNReal.inv_ne_top, DivInvMonoid.div', ENNReal.mul_lt_top, Ne.lt_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ≥0∞
h1 : x ≠ ∞
h2 : y ≠ 0
⊢ x / y ≠ ∞

Tactic:
(div_lt_top h1 h2).ne

Premises used: ENNReal.div_lt_top, LT.lt.ne
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
⊢ a⁻¹ = 0 ↔ a = ∞

Tactic:
inv_top ▸ inv_inj

Premises used: Eq.rec, inv_inj, ENNReal.inv_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
⊢ a⁻¹ ≠ 0 ↔ a ≠ ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ 0
hb : b ≠ ∞
⊢ 0 < a / b

Tactic:
ENNReal.mul_pos ha <| ENNReal.inv_ne_zero.2 hb

Premises used: Iff.mpr, ENNReal.mul_pos, DivInvMonoid.div', ENNReal.inv_ne_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y z : ℝ≥0∞
h1 : x ≠ 0
h2 : x ≠ ∞
rw : x * (x⁻¹ * y) ≤ x * z ↔ y ≤ x * z
rw₁ : x * x⁻¹ * y ≤ x * z ↔ y ≤ x * z
rw₂ : 1 * y ≤ x * z ↔ y ≤ x * z
rw₃ rw₄ : y ≤ x * z ↔ y ≤ x * z
⊢ x⁻¹ * y ≤ z ↔ y ≤ x * z

Tactic:
rw [← ENNReal.mul_le_mul_iff_right h1 h2, ← mul_assoc, ENNReal.mul_inv_cancel h1 h2, one_mul]

Premises used: mul_assoc, ENNReal.mul_inv_cancel, ENNReal.mul_le_mul_iff_right, one_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
rw : y⁻¹ * x ≤ z ↔ x ≤ z * y
rw₁ : x ≤ y * z ↔ x ≤ z * y
rw₂ rw₃ : x ≤ z * y ↔ x ≤ z * y
⊢ x * y⁻¹ ≤ z ↔ x ≤ z * y

Tactic:
rw [mul_comm, ENNReal.inv_mul_le_iff h1 h2, mul_comm]

Premises used: ENNReal.inv_mul_le_iff, mul_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
rw : x * y⁻¹ ≤ z ↔ x ≤ z * y
rw₁ rw₂ : x ≤ z * y ↔ x ≤ z * y
⊢ x / y ≤ z ↔ x ≤ z * y

Tactic:
rw [div_eq_mul_inv, ENNReal.mul_inv_le_iff h1 h2]

Premises used: div_eq_mul_inv, ENNReal.mul_inv_le_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
rw : x / y ≤ z ↔ x ≤ z * y
rw₁ rw₂ : x ≤ z * y ↔ x ≤ z * y
⊢ x / y ≤ z ↔ x ≤ y * z

Tactic:
rw [mul_comm, ENNReal.div_le_iff h1 h2]

Premises used: ENNReal.div_le_iff, mul_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : a ≠ ∞ ∨ b ≠ 0
cases : ∀ (ha : a ≠ 0 ∨ Ne (α := ℝ≥0∞) ∞ ∞) (hb : a ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ 0), (a * ∞)⁻¹ = a⁻¹ * ∞⁻¹
coe :
  ∀ (x : ℝ≥0) (ha : a ≠ 0 ∨ (↑x : ℝ≥0∞) ≠ ∞) (hb : a ≠ ∞ ∨ (↑x : ℝ≥0∞) ≠ 0), (a * (↑x : ℝ≥0∞))⁻¹ = a⁻¹ * (↑x : ℝ≥0∞)⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
cases b
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0 ∨ Ne (α := ℝ≥0∞) ∞ ∞
hb : a ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ 0
⊢ (a * ∞)⁻¹ = a⁻¹ * ∞⁻¹

Tactic:
simp_all only [Ne, not_true_eq_false, or_false, top_ne_zero, not_false_eq_true, or_true,
      mul_top, inv_top, mul_zero]

Premises used: not_true_eq_false, Ne, MulZeroClass.mul_zero, ENNReal.mul_top, ENNReal.inv_top, or_false, ENNReal.top_ne_zero, not_false_eq_true, or_true
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ 0 ∨ Ne (α := ℝ≥0∞) ∞ ∞
hb : a ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ 0
⊢ (a * ∞)⁻¹ = a⁻¹ * ∞⁻¹

Tactic:
case top =>
    simp_all only [Ne, not_true_eq_false, or_false, top_ne_zero, not_false_eq_true, or_true,
      mul_top, inv_top, mul_zero]

Premises used: not_true_eq_false, Ne, MulZeroClass.mul_zero, ENNReal.mul_top, ENNReal.inv_top, or_false, ENNReal.top_ne_zero, not_false_eq_true, or_true
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
x : ℝ≥0
ha : a ≠ 0 ∨ (↑x : ℝ≥0∞) ≠ ∞
hb : a ≠ ∞ ∨ (↑x : ℝ≥0∞) ≠ 0
cases :
  ∀ (ha : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑x : ℝ≥0∞) ≠ ∞) (hb : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑x : ℝ≥0∞) ≠ 0),
    (∞ * (↑x : ℝ≥0∞))⁻¹ = ∞⁻¹ * (↑x : ℝ≥0∞)⁻¹
coe :
  ∀ (x_1 : ℝ≥0) (ha : (↑x_1 : ℝ≥0∞) ≠ 0 ∨ (↑x : ℝ≥0∞) ≠ ∞) (hb : (↑x_1 : ℝ≥0∞) ≠ ∞ ∨ (↑x : ℝ≥0∞) ≠ 0),
    ((↑x_1 : ℝ≥0∞) * (↑x : ℝ≥0∞))⁻¹ = (↑x_1 : ℝ≥0∞)⁻¹ * (↑x : ℝ≥0∞)⁻¹
⊢ (a * (↑x : ℝ≥0∞))⁻¹ = a⁻¹ * (↑x : ℝ≥0∞)⁻¹

Tactic:
cases a
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0
ha : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑x : ℝ≥0∞) ≠ ∞
hb : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑x : ℝ≥0∞) ≠ 0
⊢ (∞ * (↑x : ℝ≥0∞))⁻¹ = ∞⁻¹ * (↑x : ℝ≥0∞)⁻¹

Tactic:
simp_all only [Ne, top_ne_zero, not_false_eq_true, coe_ne_top, or_self, not_true_eq_false,
      coe_eq_zero, false_or, top_mul, inv_top, zero_mul]

Premises used: MulZeroClass.zero_mul, not_true_eq_false, Ne, false_or, ENNReal.coe_eq_zero, ENNReal.top_mul, or_self, ENNReal.inv_top, ENNReal.top_ne_zero, not_false_eq_true, ENNReal.coe_ne_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0
ha : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑x : ℝ≥0∞) ≠ ∞
hb : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑x : ℝ≥0∞) ≠ 0
⊢ (∞ * (↑x : ℝ≥0∞))⁻¹ = ∞⁻¹ * (↑x : ℝ≥0∞)⁻¹

Tactic:
case top =>
    simp_all only [Ne, top_ne_zero, not_false_eq_true, coe_ne_top, or_self, not_true_eq_false,
      coe_eq_zero, false_or, top_mul, inv_top, zero_mul]

Premises used: MulZeroClass.zero_mul, not_true_eq_false, Ne, false_or, ENNReal.coe_eq_zero, ENNReal.top_mul, or_self, ENNReal.inv_top, ENNReal.top_ne_zero, not_false_eq_true, ENNReal.coe_ne_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x x_1 : ℝ≥0
ha : (↑x_1 : ℝ≥0∞) ≠ 0 ∨ (↑x : ℝ≥0∞) ≠ ∞
hb : (↑x_1 : ℝ≥0∞) ≠ ∞ ∨ (↑x : ℝ≥0∞) ≠ 0
⊢ ((↑x_1 : ℝ≥0∞) * (↑x : ℝ≥0∞))⁻¹ = (↑x_1 : ℝ≥0∞)⁻¹ * (↑x : ℝ≥0∞)⁻¹

Tactic:
grind [_=_ coe_mul, coe_zero, inv_zero, = mul_inv, coe_ne_top, ENNReal.inv_eq_zero,
    =_ coe_inv, zero_mul, = mul_eq_zero, mul_top, mul_zero, top_mul]

Premises used: ENNReal.coe_inv, mul_inv, MulZeroClass.zero_mul, ENNReal.inv_zero, mul_eq_zero, MulZeroClass.mul_zero, ENNReal.top_mul, ENNReal.coe_zero, ENNReal.coe_mul, ENNReal.mul_top, ENNReal.inv_eq_zero, ENNReal.coe_ne_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
htop : b ≠ ∞ ∨ a ≠ ∞
hzero : b ≠ 0 ∨ a ≠ 0
⊢ b⁻¹ ≠ 0 ∨ a ≠ ∞

Tactic:
rw [← ENNReal.inv_ne_zero] at htop

Premises used: ENNReal.inv_ne_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
htop : b ≠ ∞ ∨ a ≠ ∞
hzero : b ≠ 0 ∨ a ≠ 0
htop₁ : b⁻¹ ≠ 0 ∨ a ≠ ∞
⊢ b ≠ 0 ∨ a ≠ 0

Tactic:
rw [← ENNReal.inv_ne_zero] at htop

Premises used: ENNReal.inv_ne_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b ≠ 0 ∨ a ≠ 0
⊢ b⁻¹ ≠ ∞ ∨ a ≠ 0

Tactic:
rw [← ENNReal.inv_ne_top] at hzero

Premises used: ENNReal.inv_ne_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
rw : (b⁻¹ * a)⁻¹ = b / a
rw₁ : (b⁻¹ * a)⁻¹ = a⁻¹ * b
rw₂ : b⁻¹⁻¹ * a⁻¹ = a⁻¹ * b
rw₃ : a⁻¹ * b⁻¹⁻¹ = a⁻¹ * b
rw₄ rw₅ : a⁻¹ * b = a⁻¹ * b
⊢ (a / b)⁻¹ = b / a

Tactic:
rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ENNReal.mul_inv htop hzero, mul_comm, inv_inv]

Premises used: inv_inv, mul_comm, ENNReal.mul_inv, ENNReal.div_eq_inv_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
rw : c * a * (c * b)⁻¹ = a / b
rw₁ : c * a * (c * b)⁻¹ = a * b⁻¹
rw₂ : c * a * (c⁻¹ * b⁻¹) = a * b⁻¹
rw₃ : c * c⁻¹ * (a * b⁻¹) = a * b⁻¹
rw₄ : 1 * (a * b⁻¹) = a * b⁻¹
rw₅ rw₆ : a * b⁻¹ = a * b⁻¹
⊢ c * a / (c * b) = a / b

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ENNReal.mul_inv (Or.inl hc) (Or.inl hc'), mul_mul_mul_comm,
    ENNReal.mul_inv_cancel hc hc', one_mul]

Premises used: mul_mul_mul_comm, div_eq_mul_inv, ENNReal.mul_inv_cancel, Or.inl, ENNReal.mul_inv, one_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
rw : a * c * (b * c)⁻¹ = a / b
rw₁ : a * c * (b * c)⁻¹ = a * b⁻¹
rw₂ : a * c * (b⁻¹ * c⁻¹) = a * b⁻¹
rw₃ : a * b⁻¹ * (c * c⁻¹) = a * b⁻¹
rw₄ : a * b⁻¹ * 1 = a * b⁻¹
rw₅ rw₆ : a * b⁻¹ = a * b⁻¹
⊢ a * c / (b * c) = a / b

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ENNReal.mul_inv (Or.inr hc') (Or.inr hc), mul_mul_mul_comm,
    ENNReal.mul_inv_cancel hc hc', mul_one]

Premises used: mul_mul_mul_comm, div_eq_mul_inv, ENNReal.mul_inv_cancel, mul_one, ENNReal.mul_inv, Or.inr
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
simp_rw : (a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹
⊢ (a - b) / c = a / c - b / c

Tactic:
simp_rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ 0 < b → b < a → c⁻¹ ≠ ∞

Tactic:
simpa using h
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹

Tactic:
exact ENNReal.sub_mul (by simpa using h)

Premises used: ENNReal.sub_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
⊢ 0 < a⁻¹ ↔ a ≠ ∞

Tactic:
pos_iff_ne_zero.trans ENNReal.inv_ne_zero

Premises used: ENNReal.inv_ne_zero, Iff.trans, pos_iff_ne_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h : a < b
⊢ a ≠ ∞

Tactic:
h.ne_top

Premises used: LT.lt.ne_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h : a < b
lift : ∀ (a : ℝ≥0) (h : (↑a : ℝ≥0∞) < b), b⁻¹ < (↑a : ℝ≥0∞)⁻¹
⊢ b⁻¹ < a⁻¹

Tactic:
lift a to ℝ≥0 using h.ne_top

Premises used: LT.lt.ne_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
b : ℝ≥0∞
a : ℝ≥0
h : (↑a : ℝ≥0∞) < b
top : ∀ (h : (↑a : ℝ≥0∞) < ∞), ∞⁻¹ < (↑a : ℝ≥0∞)⁻¹
coe : ∀ (x : ℝ≥0) (h : (↑a : ℝ≥0∞) < (↑x : ℝ≥0∞)), (↑x : ℝ≥0∞)⁻¹ < (↑a : ℝ≥0∞)⁻¹
⊢ b⁻¹ < (↑a : ℝ≥0∞)⁻¹

Tactic:
cases b
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
h : (↑a : ℝ≥0∞) < ∞
⊢ ∞⁻¹ < (↑a : ℝ≥0∞)⁻¹

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a x : ℝ≥0
h : (↑a : ℝ≥0∞) < (↑x : ℝ≥0∞)
⊢ a < x

Tactic:
rw [coe_lt_coe] at h

Premises used: ENNReal.coe_lt_coe
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a x : ℝ≥0
h : a < x
coe : ∀ (h : 0 < x), (↑x : ℝ≥0∞)⁻¹ < (↑0 : ℝ≥0∞)⁻¹
coe₁ : ∀ (ha : a ≠ 0), (↑x : ℝ≥0∞)⁻¹ < (↑a : ℝ≥0∞)⁻¹
⊢ (↑x : ℝ≥0∞)⁻¹ < (↑a : ℝ≥0∞)⁻¹

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0
h : 0 < x
⊢ (↑x : ℝ≥0∞)⁻¹ < (↑0 : ℝ≥0∞)⁻¹

Tactic:
simp [h]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a x : ℝ≥0
h : a < x
ha : a ≠ 0
coe : x⁻¹ < a⁻¹
⊢ (↑x : ℝ≥0∞)⁻¹ < (↑a : ℝ≥0∞)⁻¹

Tactic:
rw [← coe_inv h.ne_bot, ← coe_inv ha, coe_lt_coe]

Premises used: ENNReal.coe_inv, ENNReal.coe_lt_coe, LT.lt.ne_bot
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a x : ℝ≥0
h : a < x
ha : a ≠ 0
⊢ x⁻¹ < a⁻¹

Tactic:
NNReal.inv_lt_inv ha h

Premises used: NNReal.inv_lt_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a x : ℝ≥0
h : a < x
ha : a ≠ 0
⊢ x⁻¹ < a⁻¹

Tactic:
exact NNReal.inv_lt_inv ha h

Premises used: NNReal.inv_lt_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
inv_strictAnti.lt_iff_gt

Premises used: ENNReal.inv_strictAnti, StrictAnti.lt_iff_gt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
⊢ a⁻¹ < b ↔ b⁻¹ < a

Tactic:
simpa only [inv_inv] using @ENNReal.inv_lt_inv a b⁻¹

Premises used: inv_inv, ENNReal.inv_lt_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
⊢ a < b⁻¹ ↔ b < a⁻¹

Tactic:
simpa only [inv_inv] using @ENNReal.inv_lt_inv a⁻¹ b

Premises used: inv_inv, ENNReal.inv_lt_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Tactic:
inv_strictAnti.le_iff_ge

Premises used: ENNReal.inv_strictAnti, StrictAnti.le_iff_ge
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
simpa only [inv_inv] using @ENNReal.inv_le_inv a b⁻¹

Premises used: ENNReal.inv_le_inv, inv_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹

Tactic:
simpa only [inv_inv] using @ENNReal.inv_le_inv a⁻¹ b

Premises used: ENNReal.inv_le_inv, inv_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h : a ≤ b
⊢ b⁻¹ ≤ a⁻¹

Tactic:
ENNReal.inv_strictAnti.antitone h

Premises used: ENNReal.inv_strictAnti, StrictAnti.antitone
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h : a < b
⊢ b⁻¹ < a⁻¹

Tactic:
ENNReal.inv_strictAnti h

Premises used: ENNReal.inv_strictAnti
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
rw : 1⁻¹ ≤ a ↔ 1 ≤ a
rw₁ rw₂ : 1 ≤ a ↔ 1 ≤ a
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a

Tactic:
rw [inv_le_iff_inv_le, inv_one]

Premises used: inv_one, ENNReal.inv_le_iff_inv_le
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
rw : a ≤ 1⁻¹ ↔ a ≤ 1
rw₁ rw₂ : a ≤ 1 ↔ a ≤ 1
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1

Tactic:
rw [le_inv_iff_le_inv, inv_one]

Premises used: inv_one, ENNReal.le_inv_iff_le_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
rw : 1⁻¹ < a ↔ 1 < a
rw₁ rw₂ : 1 < a ↔ 1 < a
⊢ a⁻¹ < 1 ↔ 1 < a

Tactic:
rw [inv_lt_iff_inv_lt, inv_one]

Premises used: inv_one, ENNReal.inv_lt_iff_inv_lt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
rw : a < 1⁻¹ ↔ a < 1
rw₁ rw₂ : a < 1 ↔ a < 1
⊢ 1 < a⁻¹ ↔ a < 1

Tactic:
rw [lt_inv_iff_lt_inv, inv_one]

Premises used: inv_one, ENNReal.lt_inv_iff_lt_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞ᵒᵈ
⊢ Eq (α := ℝ≥0∞) ((OrderIso.invENNReal.symm : (a : ℝ≥0∞ᵒᵈ) → ℝ≥0∞) a : ℝ≥0∞)
    (((OrderDual.ofDual : (a : ℝ≥0∞ᵒᵈ) → ℝ≥0∞) a)⁻¹ : ℝ≥0∞)

Tactic:
rfl

Premises used: setOf, rfl, ite
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
rw : a * ∞⁻¹ = 0
rw₁ : a * 0 = 0
rw₂ rw₃ : Eq (α := ℝ≥0∞) 0 0
⊢ a / ∞ = 0

Tactic:
rw [div_eq_mul_inv, inv_top, mul_zero]

Premises used: div_eq_mul_inv, MulZeroClass.mul_zero, ENNReal.inv_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
⊢ ∞ / a = if a = ∞ then 0 else ∞

Tactic:
simp [div_eq_mul_inv, top_mul']

Premises used: div_eq_mul_inv, ENNReal.top_mul'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
h : a ≠ ∞
⊢ ∞ / a = ∞

Tactic:
simp [top_div, h]

Premises used: ENNReal.top_div