awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
p : ℝ≥0
⊢ ∞ / (↑p : ℝ≥0∞) = ∞

Tactic:
top_div_of_ne_top coe_ne_top

Premises used: ENNReal.top_div_of_ne_top, ENNReal.coe_ne_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
h : a < ∞
⊢ ∞ / a = ∞

Tactic:
top_div_of_ne_top h.ne

Premises used: ENNReal.top_div_of_ne_top, LT.lt.ne
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
⊢ 0 / a = 0

Tactic:
zero_mul a⁻¹

Premises used: MulZeroClass.zero_mul, DivInvMonoid.div', Inv.inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
⊢ a / b = ∞ ↔ a ≠ 0 ∧ b = 0 ∨ a = ∞ ∧ b ≠ ∞

Tactic:
simp [div_eq_mul_inv, ENNReal.mul_eq_top]

Premises used: ENNReal.mul_eq_top, div_eq_mul_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
inl : ∀ (h₀ : Eq (α := ℝ≥0∞) 0 0 → b = 0) (h₁ : 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∞
h₀ : Eq (α := ℝ≥0∞) 0 0 → b = 0
h₁ : Eq (α := ℝ≥0∞) 0 ∞ → b = 0
⊢ 0 / (0 / b) = b

Tactic:
simp [h₀]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
ha : a ≠ 0
inr : ∀ (h₀ : Eq (α := ℝ≥0∞) ∞ 0 → b = 0) (h₁ : 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∞
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → b = 0
h₁ : Eq (α := ℝ≥0∞) ∞ ∞ → b = 0
ha : Ne (α := ℝ≥0∞) ∞ 0
⊢ ∞ / (∞ / b) = b

Tactic:
simp [h₁, top_div_of_lt_top]

Premises used: ENNReal.top_div_of_lt_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
ha : a ≠ 0
ha' : a ≠ ∞
inr : (a / b)⁻¹ * a = b
inr₁ : b / a * a = b
inr₂ inr₃ : b = b
⊢ a / (a / b) = b

Tactic:
rw [ENNReal.div_eq_inv_mul, ENNReal.inv_div (Or.inr ha') (Or.inr ha),
    ENNReal.div_mul_cancel ha ha']

Premises used: ENNReal.div_mul_cancel, ENNReal.inv_div, Or.inr, ENNReal.div_eq_inv_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h₀ : a ≠ 0
h₁ : a ≠ ∞
⊢ a = 0 → b = 0

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

Tactic:
simp [h₁]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a c : ℝ≥0∞
h0 : Ne (α := ℝ≥0∞) ∞ 0 ∨ c ≠ 0
ht : Ne (α := ℝ≥0∞) ∞ ∞ ∨ c ≠ ∞
⊢ c ≠ ∞

Tactic:
ht.neg_resolve_left rfl

Premises used: Or.neg_resolve_left, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a c : ℝ≥0∞
h0 : Ne (α := ℝ≥0∞) ∞ 0 ∨ c ≠ 0
ht : Ne (α := ℝ≥0∞) ∞ ∞ ∨ c ≠ ∞
top :
  ∀ (c : ℝ≥0) (h0 : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑c : ℝ≥0∞) ≠ 0) (ht : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑c : ℝ≥0∞) ≠ ∞),
    a ≤ (↑c : ℝ≥0∞) / ∞ ↔ a * ∞ ≤ (↑c : ℝ≥0∞)
⊢ a ≤ c / ∞ ↔ a * ∞ ≤ c

Tactic:
lift c to ℝ≥0 using ht.neg_resolve_left rfl

Premises used: Or.neg_resolve_left, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
c : ℝ≥0
h0 : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑c : ℝ≥0∞) ≠ 0
ht : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑c : ℝ≥0∞) ≠ ∞
top : a = 0 ↔ a * ∞ ≤ (↑c : ℝ≥0∞)
⊢ a ≤ (↑c : ℝ≥0∞) / ∞ ↔ a * ∞ ≤ (↑c : ℝ≥0∞)

Tactic:
rw [div_top, nonpos_iff_eq_zero]

Premises used: ENNReal.div_top, nonpos_iff_eq_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
c : ℝ≥0
h0 : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑c : ℝ≥0∞) ≠ 0
ht : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑c : ℝ≥0∞) ≠ ∞
top : Eq (α := ℝ≥0∞) 0 0 ↔ HMul.hMul (α := ℝ≥0∞) 0 ∞ ≤ (↑c : ℝ≥0∞)
top₁ : ∀ (ha : a ≠ 0), a = 0 ↔ a * ∞ ≤ (↑c : ℝ≥0∞)
⊢ a = 0 ↔ a * ∞ ≤ (↑c : ℝ≥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:
c : ℝ≥0
h0 : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑c : ℝ≥0∞) ≠ 0
ht : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑c : ℝ≥0∞) ≠ ∞
⊢ Eq (α := ℝ≥0∞) 0 0 ↔ HMul.hMul (α := ℝ≥0∞) 0 ∞ ≤ (↑c : ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
c : ℝ≥0
h0 : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑c : ℝ≥0∞) ≠ 0
ht : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑c : ℝ≥0∞) ≠ ∞
ha : a ≠ 0
⊢ a = 0 ↔ a * ∞ ≤ (↑c : ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a c : ℝ≥0∞
b : ℝ≥0
h0 : (↑b : ℝ≥0∞) ≠ 0 ∨ c ≠ 0
ht : (↑b : ℝ≥0∞) ≠ ∞ ∨ c ≠ ∞
⊢ a ≤ c / (↑b : ℝ≥0∞) ↔ a * (↑b : ℝ≥0∞) ≤ c

Tactic:
?_
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
ht : b ≠ ∞ ∨ c ≠ ∞
coe :
  ∀ (b : ℝ≥0) (h0 : (↑b : ℝ≥0∞) ≠ 0 ∨ c ≠ 0) (ht : (↑b : ℝ≥0∞) ≠ ∞ ∨ c ≠ ∞), a ≤ c / (↑b : ℝ≥0∞) ↔ a * (↑b : ℝ≥0∞) ≤ c
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
cases b with
  | top =>
    lift c to ℝ≥0 using ht.neg_resolve_left rfl
    rw [div_top, nonpos_iff_eq_zero]
    rcases eq_or_ne a 0 with (rfl | ha) <;> simp [*]
  | coe b => ?_

Premises used: ENNReal.div_top, eq_or_ne, Or.neg_resolve_left, OfNat.ofNat, rfl, nonpos_iff_eq_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a c : ℝ≥0∞
b : ℝ≥0
h0 : (↑b : ℝ≥0∞) ≠ 0 ∨ c ≠ 0
ht : (↑b : ℝ≥0∞) ≠ ∞ ∨ c ≠ ∞
coe : ∀ (h0 : (↑0 : ℝ≥0∞) ≠ 0 ∨ c ≠ 0) (ht : (↑0 : ℝ≥0∞) ≠ ∞ ∨ c ≠ ∞), a ≤ c / (↑0 : ℝ≥0∞) ↔ a * (↑0 : ℝ≥0∞) ≤ c
coe₁ : ∀ (hb : b ≠ 0), a ≤ c / (↑b : ℝ≥0∞) ↔ a * (↑b : ℝ≥0∞) ≤ c
⊢ a ≤ c / (↑b : ℝ≥0∞) ↔ a * (↑b : ℝ≥0∞) ≤ c

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a c : ℝ≥0∞
h0 : (↑0 : ℝ≥0∞) ≠ 0 ∨ c ≠ 0
ht : (↑0 : ℝ≥0∞) ≠ ∞ ∨ c ≠ ∞
⊢ c ≠ 0

Tactic:
have hc : c ≠ 0 := h0.neg_resolve_left rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a c : ℝ≥0∞
h0 : (↑0 : ℝ≥0∞) ≠ 0 ∨ c ≠ 0
ht : (↑0 : ℝ≥0∞) ≠ ∞ ∨ c ≠ ∞
hc : c ≠ 0
⊢ a ≤ c / (↑0 : ℝ≥0∞) ↔ a * (↑0 : ℝ≥0∞) ≤ c

Tactic:
simp [div_zero hc]

Premises used: ENNReal.div_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a c : ℝ≥0∞
b : ℝ≥0
h0 : (↑b : ℝ≥0∞) ≠ 0 ∨ c ≠ 0
ht : (↑b : ℝ≥0∞) ≠ ∞ ∨ c ≠ ∞
hb : b ≠ 0
⊢ (↑b : ℝ≥0∞) ≠ 0

Tactic:
rw [← coe_ne_zero] at hb

Premises used: ENNReal.coe_ne_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a c : ℝ≥0∞
b : ℝ≥0
h0 : (↑b : ℝ≥0∞) ≠ 0 ∨ c ≠ 0
ht : (↑b : ℝ≥0∞) ≠ ∞ ∨ c ≠ ∞
hb : (↑b : ℝ≥0∞) ≠ 0
coe : a * (↑b : ℝ≥0∞) ≤ c / (↑b : ℝ≥0∞) * (↑b : ℝ≥0∞) ↔ a * (↑b : ℝ≥0∞) ≤ c
coe₁ coe₂ : a * (↑b : ℝ≥0∞) ≤ c ↔ a * (↑b : ℝ≥0∞) ≤ c
⊢ a ≤ c / (↑b : ℝ≥0∞) ↔ a * (↑b : ℝ≥0∞) ≤ c

Tactic:
rw [← ENNReal.mul_le_mul_iff_left hb coe_ne_top, ENNReal.div_mul_cancel hb coe_ne_top]

Premises used: ENNReal.mul_le_mul_iff_left, ENNReal.div_mul_cancel, ENNReal.coe_ne_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
this : a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹
⊢ a / b ≤ c ↔ a ≤ c * b

Tactic:
simpa [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
suffices : a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹
⊢ a / b ≤ c ↔ a ≤ c * b

Tactic:
suffices a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹ by simpa [div_eq_mul_inv]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹

Tactic:
(ENNReal.le_div_iff_mul_le ?_ ?_).symm

Premises used: ENNReal.le_div_iff_mul_le, Iff.symm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
refine_1 : b⁻¹ ≠ 0 ∨ c ≠ 0
refine_2 : b⁻¹ ≠ ∞ ∨ c ≠ ∞
⊢ a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹

Tactic:
refine (ENNReal.le_div_iff_mul_le ?_ ?_).symm

Premises used: ENNReal.le_div_iff_mul_le, Iff.symm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ b⁻¹ ≠ 0 ∨ c ≠ 0

Tactic:
simpa
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ b⁻¹ ≠ ∞ ∨ c ≠ ∞

Tactic:
simpa
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ c < a / b ↔ c * b < a

Tactic:
lt_iff_lt_of_le_iff_le (ENNReal.div_le_iff_le_mul hb0 hbt)

Premises used: ENNReal.div_le_iff_le_mul, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a ≤ b * c
pos : ∀ (h0 : c = 0), a / c ≤ b
neg : ∀ (h0 : ¬c = 0), a / c ≤ b
⊢ a / c ≤ b

Tactic:
by_cases h0 : c = 0
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
⊢ a = 0

Tactic:
simpa [h0] using h
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
⊢ a = 0

Tactic:
have : a = 0 := by simpa [h0] using h
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
this : a = 0
⊢ a / c ≤ b

Tactic:
simp [*]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
pos : ∀ (hinf : c = ∞), a / c ≤ b
neg : ∀ (hinf : ¬c = ∞), a / c ≤ b
⊢ a / c ≤ b

Tactic:
by_cases hinf : c = ∞
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : c = ∞
⊢ a / c ≤ b

Tactic:
simp [hinf]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : ¬c = ∞
⊢ a / c ≤ b

Tactic:
(ENNReal.div_le_iff_le_mul (Or.inl h0) (Or.inl hinf)).2 h

Premises used: Iff.mpr, ENNReal.div_le_iff_le_mul, Or.inl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : ¬c = ∞
⊢ a / c ≤ b

Tactic:
exact (ENNReal.div_le_iff_le_mul (Or.inl h0) (Or.inl hinf)).2 h

Premises used: Iff.mpr, ENNReal.div_le_iff_le_mul, Or.inl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a ≤ b * c
⊢ a / b ≤ c

Tactic:
div_le_of_le_mul <| mul_comm b c ▸ h

Premises used: Eq.rec, ENNReal.div_le_of_le_mul, mul_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
rw rw₁ : a ≤ a
⊢ a ≤ 1 * a

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
⊢ a * a⁻¹ ≤ 1

Tactic:
ENNReal.div_self_le_one

Premises used: ENNReal.div_self_le_one, DivInvMonoid.div'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
⊢ a⁻¹ * a ≤ 1

Tactic:
simp [mul_comm]

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

Tactic:
ne_top_of_le_ne_top one_ne_top a.mul_inv_le_one

Premises used: ne_top_of_le_ne_top, ENNReal.mul_inv_le_one, ENNReal.one_ne_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
⊢ a⁻¹ * a ≠ ∞

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a ≤ b / c
rw : a * c⁻¹⁻¹ ≤ b
⊢ a * c ≤ b

Tactic:
rw [← inv_inv c]

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

Tactic:
div_le_of_le_mul h

Premises used: DivInvMonoid.div', ENNReal.div_le_of_le_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a ≤ b / c
⊢ a * c⁻¹⁻¹ ≤ b

Tactic:
exact div_le_of_le_mul h

Premises used: ENNReal.div_le_of_le_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a ≤ b / c
⊢ c * a ≤ b

Tactic:
mul_comm a c ▸ mul_le_of_le_div h

Premises used: Eq.rec, ENNReal.mul_le_of_le_div, mul_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
ht : b ≠ ∞ ∨ c ≠ ∞
⊢ c / b < a ↔ c < a * b

Tactic:
lt_iff_lt_of_le_iff_le <| ENNReal.le_div_iff_mul_le h0 ht

Premises used: ENNReal.le_div_iff_mul_le, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a < b / c
contrapose! : ∀ (h : b ≤ a * c), b / c ≤ a
⊢ a * c < b

Tactic:
contrapose! h
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : b ≤ a * c
⊢ b / c ≤ a

Tactic:
ENNReal.div_le_of_le_mul h

Premises used: ENNReal.div_le_of_le_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : b ≤ a * c
⊢ b / c ≤ a

Tactic:
exact ENNReal.div_le_of_le_mul h

Premises used: ENNReal.div_le_of_le_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a < b / c
⊢ c * a < b

Tactic:
mul_comm a c ▸ mul_lt_of_lt_div h

Premises used: Eq.rec, mul_comm, ENNReal.mul_lt_of_lt_div
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a < b * c
rwa : a < b * c⁻¹⁻¹
rwa₁ rwa₂ rwa₃ rwa₄ : a < b * c
⊢ a < b / c⁻¹

Tactic:
rwa [div_eq_mul_inv, inv_inv]

Premises used: div_eq_mul_inv, inv_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
h : a < b * c
rwa rwa₁ rwa₂ rwa₃ : a < b * c
⊢ a < c * b

Tactic:
rwa [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hc₀ : c ≠ 0
hc : c ≠ ∞
⊢ c⁻¹ ≠ 0

Tactic:
simpa
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hc₀ : c ≠ 0
hc : c ≠ ∞
⊢ c⁻¹ ≠ ∞

Tactic:
simpa
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ b⁻¹ < c⁻¹ ↔ c < b

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
hc₀ : c ≠ 0
hc : c ≠ ∞
hab : a < b
⊢ a / c < b / c

Tactic:
(ENNReal.div_lt_div_iff_left hc₀ hc).2 hab

Premises used: Iff.mpr, ENNReal.div_lt_div_iff_left
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
hcb : c < b
⊢ a / b < a / c

Tactic:
(ENNReal.div_lt_div_iff_right ha₀ ha).2 hcb

Premises used: Iff.mpr, ENNReal.div_lt_div_iff_right
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
inl : ∀ (hb₀ : Ne (α := ℝ≥0∞) ∞ 0), ∃ (c : ℝ≥0∞), 0 < c ∧ c * a < ∞
inr : ∀ (hb : b ≠ ∞), ∃ (c : ℝ≥0∞), 0 < c ∧ c * a < b
⊢ ∃ (c : ℝ≥0∞), 0 < c ∧ c * a < b

Tactic:
obtain rfl | hb := eq_or_ne b ∞

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
hb₀ : Ne (α := ℝ≥0∞) ∞ 0
⊢ LT.lt (α := ℝ≥0∞) 0 1 ∧ 1 * a < ∞

Tactic:
simpa [lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
hb₀ : Ne (α := ℝ≥0∞) ∞ 0
⊢ ∃ (c : ℝ≥0∞), 0 < c ∧ c * a < ∞

Tactic:
exact ⟨1, by simpa [lt_top_iff_ne_top]⟩
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a + 1 ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
inr : b / (a + 1) < b / a
⊢ ∃ (c : ℝ≥0∞), 0 < c ∧ c * a < b

Tactic:
refine ⟨b / (a + 1), ENNReal.div_pos hb₀ (by finiteness), ENNReal.mul_lt_of_lt_div ?_⟩
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
inr : a < a + 1
⊢ b / (a + 1) < b / a

Tactic:
gcongr
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a < a + 1

Tactic:
ENNReal.lt_add_right ha one_ne_zero

Premises used: ENNReal.lt_add_right, one_ne_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a < a + 1

Tactic:
exact ENNReal.lt_add_right ha one_ne_zero

Premises used: ENNReal.lt_add_right, one_ne_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h₁ : b = ∞ → a ≠ 0
h₂ : a = ∞ → b ≠ 0
hb0 : a ≠ 0 ∨ b ≠ ∞
hbt : a ≠ ∞ ∨ b ≠ 0
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b

Tactic:
rw [← one_div, ENNReal.div_le_iff_le_mul, mul_comm]

Premises used: ENNReal.div_le_iff_le_mul, one_div, mul_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h₁ : b = ∞ → a ≠ 0
h₂ : a = ∞ → b ≠ 0
⊢ a ≠ 0 ∨ b ≠ ∞

Tactic:
or_not_of_imp h₁

Premises used: or_not_of_imp
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h₁ : b = ∞ → a ≠ 0
h₂ : a = ∞ → b ≠ 0
⊢ a ≠ ∞ ∨ b ≠ 0

Tactic:
not_or_of_imp h₂

Premises used: not_or_of_imp
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h₁ : b = ∞ → a ≠ 0
h₂ : a = ∞ → b ≠ 0
⊢ a ≠ 0 ∨ b ≠ ∞

Tactic:
exacts [or_not_of_imp h₁, not_or_of_imp h₂]

Premises used: or_not_of_imp, not_or_of_imp
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h0 : b ≠ 0 ∨ Ne (α := ℝ≥0∞) 1 0
ht : b ≠ ∞ ∨ Ne (α := ℝ≥0∞) 1 ∞
⊢ a ≤ b⁻¹ ↔ a * b ≤ 1

Tactic:
rw [← one_div, ENNReal.le_div_iff_mul_le]

Premises used: ENNReal.le_div_iff_mul_le, one_div
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h0 : Ne (α := ℝ≥0∞) 1 0
⊢ b ≠ 0 ∨ Ne (α := ℝ≥0∞) 1 0

Tactic:
right
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
⊢ Ne (α := ℝ≥0∞) 1 0

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
ht : Ne (α := ℝ≥0∞) 1 ∞
⊢ b ≠ ∞ ∨ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
right
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
⊢ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
hab : a ≤ b
hdc : d ≤ c
⊢ a / c ≤ b / d

Tactic:
div_eq_mul_inv b d ▸ div_eq_mul_inv a c ▸ mul_le_mul' hab (ENNReal.inv_le_inv.mpr hdc)

Premises used: Iff.mpr, Eq.rec, ENNReal.inv_le_inv, div_eq_mul_inv, Eq.symm, mul_le_mul'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h : a ≤ b
c : ℝ≥0∞
⊢ c / b ≤ c / a

Tactic:
ENNReal.div_le_div le_rfl h

Premises used: le_rfl, ENNReal.div_le_div
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h : a ≤ b
c : ℝ≥0∞
⊢ a / c ≤ b / c

Tactic:
ENNReal.div_le_div h le_rfl

Premises used: le_rfl, ENNReal.div_le_div
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
h : a * b = 1
rw : b ≠ ∞
⊢ a = b⁻¹

Tactic:
rw [← mul_one a, ← ENNReal.mul_inv_cancel (right_ne_zero_of_mul_eq_one h), ← mul_assoc, h,
    one_mul]

Premises used: mul_assoc, right_ne_zero_of_mul_eq_one, ENNReal.mul_inv_cancel, mul_one, one_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
h : a * ∞ = 1
⊢ False

Tactic:
simp [left_ne_zero_of_mul_eq_one h] at h

Premises used: left_ne_zero_of_mul_eq_one
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b r : ℝ≥0∞
hr₀ : r ≠ 0
hr₁ : r ≠ ∞
rw : r * a ≤ b ↔ r * a ≤ r * (r⁻¹ * b)
rw₁ : r * a ≤ b ↔ r * a ≤ r * r⁻¹ * b
rw₂ : r * a ≤ b ↔ r * a ≤ 1 * b
rw₃ rw₄ : r * a ≤ b ↔ r * a ≤ b
⊢ r * a ≤ b ↔ a ≤ r⁻¹ * b

Tactic:
rw [← @ENNReal.mul_le_mul_iff_right _ a _ hr₀ hr₁, ← mul_assoc, ENNReal.mul_inv_cancel hr₀ hr₁,
    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 : ℝ≥0∞
h : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) < x → (↑r : ℝ≥0∞) ≤ y
⊢ x ≤ y

Tactic:
le_of_forall_lt_imp_le_of_dense fun r hr => ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) < x → (↑r : ℝ≥0∞) ≤ y
refine : ∀ (r : ℝ≥0∞) (hr : r < x), r ≤ y
⊢ x ≤ y

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun r hr => ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) < x → (↑r : ℝ≥0∞) ≤ y
r : ℝ≥0∞
hr : r < x
⊢ r ≠ ∞

Tactic:
ne_top_of_lt hr

Premises used: ne_top_of_lt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) < x → (↑r : ℝ≥0∞) ≤ y
r : ℝ≥0∞
hr : r < x
lift : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < x), (↑r : ℝ≥0∞) ≤ y
⊢ r ≤ y

Tactic:
lift r to ℝ≥0 using ne_top_of_lt hr

Premises used: ne_top_of_lt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) < x → (↑r : ℝ≥0∞) ≤ y
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < x
⊢ (↑r : ℝ≥0∞) ≤ y

Tactic:
h r hr
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) < x → (↑r : ℝ≥0∞) ≤ y
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < x
⊢ (↑r : ℝ≥0∞) ≤ y

Tactic:
exact h r hr
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ≥0∞
⊢ (∀ (r : ℝ≥0), (↑r : ℝ≥0∞) ≤ x ↔ (↑r : ℝ≥0∞) ≤ y) → x = y

Tactic:
WithTop.eq_of_forall_coe_le_iff

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.eq_of_forall_coe_le_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ≥0∞
⊢ (∀ (r : ℝ≥0), x ≤ (↑r : ℝ≥0∞) ↔ y ≤ (↑r : ℝ≥0∞)) → x = y

Tactic:
WithTop.eq_of_forall_le_coe_iff

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.eq_of_forall_le_coe_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), 0 < r → (↑r : ℝ≥0∞) < x → (↑r : ℝ≥0∞) ≤ y
⊢ x ≤ y

Tactic:
le_of_forall_nnreal_lt fun r hr =>
    (eq_zero_or_pos r).elim (fun h => h ▸ zero_le) fun h0 => h r h0 hr

Premises used: zero_le, Eq.rec, eq_zero_or_pos, ENNReal.le_of_forall_nnreal_lt, Or.elim, Eq.symm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ≥0∞
h : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) ≤ x
⊢ x = ∞

Tactic:
top_unique <| le_of_forall_nnreal_lt fun r _ => h r

Premises used: top_unique, ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
⊢ (a + b) / c = a / c + b / c

Tactic:
right_distrib a b c⁻¹

Premises used: DivInvMonoid.div', Inv.inv, right_distrib
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
⊢ a / c + b / c = (a + b) / c

Tactic:
ENNReal.add_div.symm

Premises used: ENNReal.add_div, Eq.symm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
h0 : a ≠ 0
hI : a ≠ ∞
⊢ a / a = 1

Tactic:
ENNReal.mul_inv_cancel h0 hI

Premises used: DivInvMonoid.div', ENNReal.mul_inv_cancel
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
⊢ a * (b / a) ≤ b

Tactic:
mul_le_of_le_div' le_rfl

Premises used: le_rfl, ENNReal.mul_le_of_le_div'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : b = c / a
rw : a * (c / a) = c
rw₁ rw₂ : c = c
⊢ a * b = c

Tactic:
rw [h, ENNReal.mul_div_cancel ha ha']

Premises used: ENNReal.mul_div_cancel
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : a * b = c
rw : b = a * b / a
rw₁ : b = a * (b / a)
rw₂ rw₃ : b = b
⊢ b = c / a

Tactic:
rw [← h, mul_div_assoc, ENNReal.mul_div_cancel ha ha']

Premises used: mul_div_assoc, ENNReal.mul_div_cancel
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
rw : a * (c / b) = d ↔ a * c = b * d
⊢ c / b = d / a ↔ a * c = b * d

Tactic:
rw [eq_div_iff ha ha']

Premises used: ENNReal.eq_div_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
rw : b * d = a * c
| a * c = b * d

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
conv_rhs : a * (c / b) = d ↔ b * d = a * c
⊢ a * (c / b) = d ↔ a * c = b * d

Tactic:
conv_rhs => rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
rw : a * (c / b) = d ↔ d = a * c / b
rw₁ : a * (c / b) = d ↔ d = a * (c / b)
rw₂ rw₃ : d = a * (c / b) ↔ d = a * (c / b)
⊢ a * (c / b) = d ↔ b * d = a * c

Tactic:
rw [← eq_div_iff hb hb', mul_div_assoc, eq_comm]

Premises used: mul_div_assoc, eq_comm, ENNReal.eq_div_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb₁ : b ≠ ∞
h : a / b = 1
rw : b * 1 = b
rw₁ rw₂ : b = b
⊢ a = b

Tactic:
rw [← (eq_div_iff hb₀ hb₁).mp h.symm, mul_one]

Premises used: Iff.mp, mul_one, Eq.symm, ENNReal.eq_div_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
rw : HMul.hMul (α := ℝ≥0∞) 2 2⁻¹ = 1
rw₁ : 2 / 2 = 1
rw₂ rw₃ : Eq (α := ℝ≥0∞) 1 1
⊢ HAdd.hAdd (α := ℝ≥0∞) 2⁻¹ 2⁻¹ = 1

Tactic:
rw [← two_mul, ← div_eq_mul_inv, ENNReal.div_self two_ne_zero ofNat_ne_top]

Premises used: ENNReal.ofNat_ne_top, two_mul, div_eq_mul_inv, two_ne_zero, ENNReal.div_self
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
rw : HAdd.hAdd (α := ℝ≥0∞) 3⁻¹ 3⁻¹ + 3⁻¹ = HMul.hMul (α := ℝ≥0∞) 3 3⁻¹
⊢ HAdd.hAdd (α := ℝ≥0∞) 3⁻¹ 3⁻¹ + 3⁻¹ = 1

Tactic:
rw [← ENNReal.mul_inv_cancel three_ne_zero ofNat_ne_top]

Premises used: ENNReal.ofNat_ne_top, ENNReal.mul_inv_cancel, three_ne_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
⊢ HAdd.hAdd (α := ℝ≥0∞) 3⁻¹ 3⁻¹ + 3⁻¹ = HMul.hMul (α := ℝ≥0∞) 3 3⁻¹

Tactic:
ring
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
rw : a * 2⁻¹ + a * 2⁻¹ = a
rw₁ : a * HAdd.hAdd (α := ℝ≥0∞) 2⁻¹ 2⁻¹ = a
rw₂ : a * 1 = a
rw₃ rw₄ : a = a
⊢ a / 2 + a / 2 = a

Tactic:
rw [div_eq_mul_inv, ← mul_add, inv_two_add_inv_two, mul_one]

Premises used: div_eq_mul_inv, mul_add, mul_one, ENNReal.inv_two_add_inv_two
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
rw : a * 3⁻¹ + a * 3⁻¹ + a * 3⁻¹ = a
rw₁ : a * HAdd.hAdd (α := ℝ≥0∞) 3⁻¹ 3⁻¹ + a * 3⁻¹ = a
rw₂ : a * (HAdd.hAdd (α := ℝ≥0∞) 3⁻¹ 3⁻¹ + 3⁻¹) = a
rw₃ : a * 1 = a
rw₄ rw₅ : a = a
⊢ a / 3 + a / 3 + a / 3 = a

Tactic:
rw [div_eq_mul_inv, ← mul_add, ← mul_add, inv_three_add_inv_three, mul_one]

Premises used: div_eq_mul_inv, mul_add, mul_one, ENNReal.inv_three_add_inv_three
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
⊢ a / b = 0 ↔ a = 0 ∨ b = ∞

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
⊢ 0 < a / b ↔ a ≠ 0 ∧ b ≠ ∞

Tactic:
simp [pos_iff_ne_zero, not_or]

Premises used: not_or, pos_iff_ne_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
rw : 0 < a / b ↔ a ≠ 0 ∧ b ≠ ∞
rw₁ rw₂ : a ≠ 0 ∧ b ≠ ∞ ↔ a ≠ 0 ∧ b ≠ ∞
⊢ a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ∞

Tactic:
rw [← pos_iff_ne_zero, div_pos_iff]

Premises used: ENNReal.div_pos_iff, pos_iff_ne_zero
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
simp : a * b⁻¹ * c = a * (b * c⁻¹)⁻¹
⊢ a / b * c = a / (b / c)

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv