awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a c : ℝ≥0∞
h0 : Ne (α := ℝ≥0∞) ∞ 0 ∨ c ≠ 0
ht : Ne (α := ℝ≥0∞) ∞ ∞ ∨ c ≠ ∞
⊢ a ≤ c / ∞ ↔ a * ∞ ≤ c
have top : ∀ (c : ℝ≥0) (h0 : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑c : ℝ≥0∞) ≠ 0) (ht : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑c : ℝ≥0∞) ≠ ∞),
  a ≤ (↑c : ℝ≥0∞) / ∞ ↔ a * ∞ ≤ (↑c : ℝ≥0∞)
Tactic: lift c to ℝ≥0 using ht.neg_resolve_left rfl
Cleared hypotheses: c, h0, ht
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
c : ℝ≥0
h0 : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑c : ℝ≥0∞) ≠ 0
ht : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑c : ℝ≥0∞) ≠ ∞
⊢ a ≤ (↑c : ℝ≥0∞) / ∞ ↔ a * ∞ ≤ (↑c : ℝ≥0∞)
have top : a = 0 ↔ a * ∞ ≤ (↑c : ℝ≥0∞)
Tactic: rw [div_top, nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
c : ℝ≥0
h0 : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑c : ℝ≥0∞) ≠ 0
ht : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑c : ℝ≥0∞) ≠ ∞
⊢ a = 0 ↔ a * ∞ ≤ (↑c : ℝ≥0∞)
have top : Eq (α := ℝ≥0∞) 0 0 ↔ HMul.hMul (α := ℝ≥0∞) 0 ∞ ≤ (↑c : ℝ≥0∞)
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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∞)
⊢ a = 0 ↔ a * ∞ ≤ (↑c : ℝ≥0∞)
have top₁ : ∀ (ha : a ≠ 0), a = 0 ↔ a * ∞ ≤ (↑c : ℝ≥0∞)
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
ht : b ≠ ∞ ∨ c ≠ ∞
⊢ a ≤ c / b ↔ a * b ≤ c
have coe : ∀ (b : ℝ≥0) (h0 : (↑b : ℝ≥0∞) ≠ 0 ∨ c ≠ 0) (ht : (↑b : ℝ≥0∞) ≠ ∞ ∨ c ≠ ∞), a ≤ c / (↑b : ℝ≥0∞) ↔ a * (↑b : ℝ≥0∞) ≤ 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 => ?_
Cleared hypotheses: b, h0, ht
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a c : ℝ≥0∞
b : ℝ≥0
h0 : (↑b : ℝ≥0∞) ≠ 0 ∨ c ≠ 0
ht : (↑b : ℝ≥0∞) ≠ ∞ ∨ c ≠ ∞
⊢ a ≤ c / (↑b : ℝ≥0∞) ↔ a * (↑b : ℝ≥0∞) ≤ c
have coe : ∀ (h0 : (↑0 : ℝ≥0∞) ≠ 0 ∨ c ≠ 0) (ht : (↑0 : ℝ≥0∞) ≠ ∞ ∨ c ≠ ∞), a ≤ c / (↑0 : ℝ≥0∞) ↔ a * (↑0 : ℝ≥0∞) ≤ c
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
Cleared hypotheses: b, h0, ht
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a ≤ c / (↑b : ℝ≥0∞) ↔ a * (↑b : ℝ≥0∞) ≤ c
have coe₁ : ∀ (hb : b ≠ 0), a ≤ c / (↑b : ℝ≥0∞) ↔ a * (↑b : ℝ≥0∞) ≤ c
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
a c : ℝ≥0∞
h0 : (↑0 : ℝ≥0∞) ≠ 0 ∨ c ≠ 0
ht : (↑0 : ℝ≥0∞) ≠ ∞ ∨ c ≠ ∞
⊢ a ≤ c / (↑0 : ℝ≥0∞) ↔ a * (↑0 : ℝ≥0∞) ≤ c
have hc : c ≠ 0
Tactic: have hc : c ≠ 0 := h0.neg_resolve_left rfl
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
a c : ℝ≥0∞
b : ℝ≥0
h0 : (↑b : ℝ≥0∞) ≠ 0 ∨ c ≠ 0
ht : (↑b : ℝ≥0∞) ≠ ∞ ∨ c ≠ ∞
hb : b ≠ 0
⊢ a ≤ c / (↑b : ℝ≥0∞) ↔ a * (↑b : ℝ≥0∞) ≤ c
have hb₁ : (↑b : ℝ≥0∞) ≠ 0
Tactic: rw [← coe_ne_zero] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a c : ℝ≥0∞
b : ℝ≥0
h0 : (↑b : ℝ≥0∞) ≠ 0 ∨ c ≠ 0
ht : (↑b : ℝ≥0∞) ≠ ∞ ∨ c ≠ ∞
hb : (↑b : ℝ≥0∞) ≠ 0
⊢ a ≤ c / (↑b : ℝ≥0∞) ↔ a * (↑b : ℝ≥0∞) ≤ c
have coe : a * (↑b : ℝ≥0∞) ≤ c / (↑b : ℝ≥0∞) * (↑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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a ≤ c / (↑b : ℝ≥0∞) ↔ a * (↑b : ℝ≥0∞) ≤ c
have coe₁ : a * (↑b : ℝ≥0∞) ≤ c ↔ a * (↑b : ℝ≥0∞) ≤ c
Tactic: rw [← ENNReal.mul_le_mul_iff_left hb coe_ne_top, ENNReal.div_mul_cancel hb coe_ne_top]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ a / b ≤ c ↔ a ≤ c * b
have suffices : a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹
Tactic: suffices a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹ by simpa [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹
have refine_1 : b⁻¹ ≠ 0 ∨ c ≠ 0
Tactic: refine (ENNReal.le_div_iff_mul_le ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
refine_1 : b⁻¹ ≠ 0 ∨ c ≠ 0
⊢ a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹
have refine_2 : b⁻¹ ≠ ∞ ∨ c ≠ ∞
Tactic: refine (ENNReal.le_div_iff_mul_le ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
h : a ≤ b * c
⊢ a / c ≤ b
have pos : ∀ (h0 : c = 0), a / c ≤ b
Tactic: by_cases h0 : c = 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
h : a ≤ b * c
pos : ∀ (h0 : c = 0), a / c ≤ b
⊢ a / c ≤ b
have neg : ∀ (h0 : ¬c = 0), a / c ≤ b
Tactic: by_cases h0 : c = 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
⊢ a / c ≤ b
have this : a = 0
Tactic: have : a = 0 := by simpa [h0] using h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
⊢ a / c ≤ b
have pos : ∀ (hinf : c = ∞), a / c ≤ b
Tactic: by_cases hinf : c = ∞
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
pos : ∀ (hinf : c = ∞), a / c ≤ b
⊢ a / c ≤ b
have neg : ∀ (hinf : ¬c = ∞), a / c ≤ b
Tactic: by_cases hinf : c = ∞
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
⊢ a ≤ 1 * a
have rw : a ≤ a
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
h : a ≤ b / c
⊢ a * c ≤ b
have rw : a * c⁻¹⁻¹ ≤ b
Tactic: rw [← inv_inv c]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
h : a < b / c
⊢ a * c < b
have contrapose! : ∀ (h : b ≤ a * c), b / c ≤ a
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
h : a < b * c
⊢ a < b / c⁻¹
have rwa : a < b * c⁻¹⁻¹
Tactic: rwa [div_eq_mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
⊢ ∃ (c : ℝ≥0∞), 0 < c ∧ c * a < b
have inl : ∀ (hb₀ : Ne (α := ℝ≥0∞) ∞ 0), ∃ (c : ℝ≥0∞), 0 < c ∧ c * a < ∞
Tactic: obtain rfl | hb := eq_or_ne b ∞
Cleared hypotheses: b, hb₀
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
inl : ∀ (hb₀ : Ne (α := ℝ≥0∞) ∞ 0), ∃ (c : ℝ≥0∞), 0 < c ∧ c * a < ∞
⊢ ∃ (c : ℝ≥0∞), 0 < c ∧ c * a < b
have inr : ∀ (hb : b ≠ ∞), ∃ (c : ℝ≥0∞), 0 < c ∧ c * a < b
Tactic: obtain rfl | hb := eq_or_ne b ∞
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ ∃ (c : ℝ≥0∞), 0 < c ∧ c * a < b
have inr : b / (a + 1) < b / a
Tactic: refine ⟨b / (a + 1), ENNReal.div_pos hb₀ (by finiteness), ENNReal.mul_lt_of_lt_div ?_⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ b / (a + 1) < b / a
have inr : a < a + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
h₁ : b = ∞ → a ≠ 0
h₂ : a = ∞ → b ≠ 0
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b
have hb0 : a ≠ 0 ∨ b ≠ ∞
Tactic: rw [← one_div, ENNReal.div_le_iff_le_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
h₁ : b = ∞ → a ≠ 0
h₂ : a = ∞ → b ≠ 0
hb0 : a ≠ 0 ∨ b ≠ ∞
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b
have hbt : a ≠ ∞ ∨ b ≠ 0
Tactic: rw [← one_div, ENNReal.div_le_iff_le_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
⊢ a ≤ b⁻¹ ↔ a * b ≤ 1
have h0 : b ≠ 0 ∨ Ne (α := ℝ≥0∞) 1 0
Tactic: rw [← one_div, ENNReal.le_div_iff_mul_le]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
h0 : b ≠ 0 ∨ Ne (α := ℝ≥0∞) 1 0
⊢ a ≤ b⁻¹ ↔ a * b ≤ 1
have ht : b ≠ ∞ ∨ Ne (α := ℝ≥0∞) 1 ∞
Tactic: rw [← one_div, ENNReal.le_div_iff_mul_le]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
⊢ b ≠ 0 ∨ Ne (α := ℝ≥0∞) 1 0
have h0 : Ne (α := ℝ≥0∞) 1 0
Tactic: right
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
⊢ b ≠ ∞ ∨ Ne (α := ℝ≥0∞) 1 ∞
have ht : Ne (α := ℝ≥0∞) 1 ∞
Tactic: right
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
h : a * b = 1
⊢ a = b⁻¹
have rw : b ≠ ∞
Tactic: rw [← mul_one a, ← ENNReal.mul_inv_cancel (right_ne_zero_of_mul_eq_one h), ← mul_assoc, h,
    one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b r : ℝ≥0∞
hr₀ : r ≠ 0
hr₁ : r ≠ ∞
⊢ r * a ≤ b ↔ a ≤ r⁻¹ * b
have rw : r * a ≤ b ↔ r * a ≤ r * (r⁻¹ * b)
Tactic: rw [← @ENNReal.mul_le_mul_iff_right _ a _ hr₀ hr₁, ← mul_assoc, ENNReal.mul_inv_cancel hr₀ hr₁,
    one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b r : ℝ≥0∞
hr₀ : r ≠ 0
hr₁ : r ≠ ∞
rw : r * a ≤ b ↔ r * a ≤ r * (r⁻¹ * b)
⊢ r * a ≤ b ↔ a ≤ r⁻¹ * b
have rw₁ : r * a ≤ b ↔ r * a ≤ r * r⁻¹ * b
Tactic: rw [← @ENNReal.mul_le_mul_iff_right _ a _ hr₀ hr₁, ← mul_assoc, ENNReal.mul_inv_cancel hr₀ hr₁,
    one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ r * a ≤ b ↔ a ≤ r⁻¹ * b
have rw₂ : r * a ≤ b ↔ r * a ≤ 1 * b
Tactic: rw [← @ENNReal.mul_le_mul_iff_right _ a _ hr₀ hr₁, ← mul_assoc, ENNReal.mul_inv_cancel hr₀ hr₁,
    one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ r * a ≤ b ↔ a ≤ r⁻¹ * b
have rw₃ : r * a ≤ b ↔ r * a ≤ b
Tactic: rw [← @ENNReal.mul_le_mul_iff_right _ a _ hr₀ hr₁, ← mul_assoc, ENNReal.mul_inv_cancel hr₀ hr₁,
    one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) < x → (↑r : ℝ≥0∞) ≤ y
⊢ x ≤ y
have refine : ∀ (r : ℝ≥0∞) (hr : r < x), r ≤ y
Tactic: refine le_of_forall_lt_imp_le_of_dense fun r hr => ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : b = c / a
⊢ a * b = c
have rw : a * (c / a) = c
Tactic: rw [h, ENNReal.mul_div_cancel ha ha']
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : b = c / a
rw : a * (c / a) = c
⊢ a * b = c
have rw₁ : c = c
Tactic: rw [h, ENNReal.mul_div_cancel ha ha']
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : a * b = c
⊢ b = c / a
have rw : b = a * b / a
Tactic: rw [← h, mul_div_assoc, ENNReal.mul_div_cancel ha ha']
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : a * b = c
rw : b = a * b / a
⊢ b = c / a
have rw₁ : b = a * (b / a)
Tactic: rw [← h, mul_div_assoc, ENNReal.mul_div_cancel ha ha']
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : a * b = c
rw : b = a * b / a
rw₁ : b = a * (b / a)
⊢ b = c / a
have rw₂ : b = b
Tactic: rw [← h, mul_div_assoc, ENNReal.mul_div_cancel ha ha']
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
⊢ c / b = d / a ↔ a * c = b * d
have rw : a * (c / b) = d ↔ a * c = b * d
Tactic: rw [eq_div_iff ha ha']
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
| a * c = b * d
have rw : b * d = a * c
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
⊢ a * (c / b) = d ↔ a * c = b * d
have conv_rhs : a * (c / b) = d ↔ b * d = a * c
Tactic: conv_rhs => rw [eq_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
hb : b ≠ 0
hb' : b ≠ ∞
⊢ a * (c / b) = d ↔ b * d = a * c
have rw : a * (c / b) = d ↔ d = a * c / b
Tactic: rw [← eq_div_iff hb hb', mul_div_assoc, eq_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a * (c / b) = d ↔ b * d = a * c
have rw₁ : a * (c / b) = d ↔ d = a * (c / b)
Tactic: rw [← eq_div_iff hb hb', mul_div_assoc, eq_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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)
⊢ a * (c / b) = d ↔ b * d = a * c
have rw₂ : d = a * (c / b) ↔ d = a * (c / b)
Tactic: rw [← eq_div_iff hb hb', mul_div_assoc, eq_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb₁ : b ≠ ∞
h : a / b = 1
⊢ a = b
have rw : b * 1 = b
Tactic: rw [← (eq_div_iff hb₀ hb₁).mp h.symm, mul_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb₁ : b ≠ ∞
h : a / b = 1
rw : b * 1 = b
⊢ a = b
have rw₁ : b = b
Tactic: rw [← (eq_div_iff hb₀ hb₁).mp h.symm, mul_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
⊢ HAdd.hAdd (α := ℝ≥0∞) 2⁻¹ 2⁻¹ = 1
have rw : HMul.hMul (α := ℝ≥0∞) 2 2⁻¹ = 1
Tactic: rw [← two_mul, ← div_eq_mul_inv, ENNReal.div_self two_ne_zero ofNat_ne_top]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
rw : HMul.hMul (α := ℝ≥0∞) 2 2⁻¹ = 1
⊢ HAdd.hAdd (α := ℝ≥0∞) 2⁻¹ 2⁻¹ = 1
have rw₁ : 2 / 2 = 1
Tactic: rw [← two_mul, ← div_eq_mul_inv, ENNReal.div_self two_ne_zero ofNat_ne_top]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
rw : HMul.hMul (α := ℝ≥0∞) 2 2⁻¹ = 1
rw₁ : 2 / 2 = 1
⊢ HAdd.hAdd (α := ℝ≥0∞) 2⁻¹ 2⁻¹ = 1
have rw₂ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [← two_mul, ← div_eq_mul_inv, ENNReal.div_self two_ne_zero ofNat_ne_top]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
⊢ HAdd.hAdd (α := ℝ≥0∞) 3⁻¹ 3⁻¹ + 3⁻¹ = 1
have rw : HAdd.hAdd (α := ℝ≥0∞) 3⁻¹ 3⁻¹ + 3⁻¹ = HMul.hMul (α := ℝ≥0∞) 3 3⁻¹
Tactic: rw [← ENNReal.mul_inv_cancel three_ne_zero ofNat_ne_top]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
⊢ a / 2 + a / 2 = a
have rw : a * 2⁻¹ + a * 2⁻¹ = a
Tactic: rw [div_eq_mul_inv, ← mul_add, inv_two_add_inv_two, mul_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
rw : a * 2⁻¹ + a * 2⁻¹ = a
⊢ a / 2 + a / 2 = a
have rw₁ : a * HAdd.hAdd (α := ℝ≥0∞) 2⁻¹ 2⁻¹ = a
Tactic: rw [div_eq_mul_inv, ← mul_add, inv_two_add_inv_two, mul_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
rw : a * 2⁻¹ + a * 2⁻¹ = a
rw₁ : a * HAdd.hAdd (α := ℝ≥0∞) 2⁻¹ 2⁻¹ = a
⊢ a / 2 + a / 2 = a
have rw₂ : a * 1 = a
Tactic: rw [div_eq_mul_inv, ← mul_add, inv_two_add_inv_two, mul_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
rw : a * 2⁻¹ + a * 2⁻¹ = a
rw₁ : a * HAdd.hAdd (α := ℝ≥0∞) 2⁻¹ 2⁻¹ = a
rw₂ : a * 1 = a
⊢ a / 2 + a / 2 = a
have rw₃ : a = a
Tactic: rw [div_eq_mul_inv, ← mul_add, inv_two_add_inv_two, mul_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
⊢ a / 3 + a / 3 + a / 3 = a
have rw : a * 3⁻¹ + a * 3⁻¹ + a * 3⁻¹ = a
Tactic: rw [div_eq_mul_inv, ← mul_add, ← mul_add, inv_three_add_inv_three, mul_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
rw : a * 3⁻¹ + a * 3⁻¹ + a * 3⁻¹ = a
⊢ a / 3 + a / 3 + a / 3 = a
have rw₁ : a * HAdd.hAdd (α := ℝ≥0∞) 3⁻¹ 3⁻¹ + a * 3⁻¹ = a
Tactic: rw [div_eq_mul_inv, ← mul_add, ← mul_add, inv_three_add_inv_three, mul_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
rw : a * 3⁻¹ + a * 3⁻¹ + a * 3⁻¹ = a
rw₁ : a * HAdd.hAdd (α := ℝ≥0∞) 3⁻¹ 3⁻¹ + a * 3⁻¹ = a
⊢ a / 3 + a / 3 + a / 3 = a
have rw₂ : a * (HAdd.hAdd (α := ℝ≥0∞) 3⁻¹ 3⁻¹ + 3⁻¹) = a
Tactic: rw [div_eq_mul_inv, ← mul_add, ← mul_add, inv_three_add_inv_three, mul_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a / 3 + a / 3 + a / 3 = a
have rw₃ : a * 1 = a
Tactic: rw [div_eq_mul_inv, ← mul_add, ← mul_add, inv_three_add_inv_three, mul_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a / 3 + a / 3 + a / 3 = a
have rw₄ : a = a
Tactic: rw [div_eq_mul_inv, ← mul_add, ← mul_add, inv_three_add_inv_three, mul_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
⊢ a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ∞
have rw : 0 < a / b ↔ a ≠ 0 ∧ b ≠ ∞
Tactic: rw [← pos_iff_ne_zero, div_pos_iff]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
rw : 0 < a / b ↔ a ≠ 0 ∧ b ≠ ∞
⊢ a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ∞
have rw₁ : a ≠ 0 ∧ b ≠ ∞ ↔ a ≠ 0 ∧ b ≠ ∞
Tactic: rw [← pos_iff_ne_zero, div_pos_iff]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ a / b * c = a / (b / c)
have simp : a * b⁻¹ * c = a * (b * c⁻¹)⁻¹
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ a * b⁻¹ * c = a * (b * c⁻¹)⁻¹
have rw : a * b⁻¹ * c = a * (b⁻¹ * c)
Tactic: rw [ENNReal.mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
rw : a * b⁻¹ * c = a * (b⁻¹ * c)
⊢ a * b⁻¹ * c = a * (b * c⁻¹)⁻¹
have ha : b ≠ 0 ∨ c⁻¹ ≠ ∞
Tactic: rw [ENNReal.mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
rw : a * b⁻¹ * c = a * (b⁻¹ * c)
ha : b ≠ 0 ∨ c⁻¹ ≠ ∞
⊢ a * b⁻¹ * c = a * (b * c⁻¹)⁻¹
have hb : b ≠ ∞ ∨ c⁻¹ ≠ 0
Tactic: rw [ENNReal.mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c d : ℝ≥0∞
hc : c ≠ 0 ∨ d ≠ ∞
hd : c ≠ ∞ ∨ d ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)
have simp : a * b * (c⁻¹ * d⁻¹) = a * c⁻¹ * (b * d⁻¹)
Tactic: simp only [div_eq_mul_inv, ENNReal.mul_inv hc hd]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
hz : a ≠ 0
ht : a ≠ ∞
⊢ a / 2 < a
have lift : ∀ (a : ℝ≥0) (hz : (↑a : ℝ≥0∞) ≠ 0), (↑a : ℝ≥0∞) / 2 < (↑a : ℝ≥0∞)
Tactic: lift a to ℝ≥0 using ht
Cleared hypotheses: a, hz, ht
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
a : ℝ≥0
hz : (↑a : ℝ≥0∞) ≠ 0
⊢ (↑a : ℝ≥0∞) / 2 < (↑a : ℝ≥0∞)
have hz₁ : a ≠ 0
Tactic: rw [coe_ne_zero] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0
hz : a ≠ 0
⊢ (↑a : ℝ≥0∞) / 2 < (↑a : ℝ≥0∞)
have rw : a / 2 < a
Tactic: rw [← coe_two, ← coe_div, coe_lt_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0
hz : a ≠ 0
rw : a / 2 < a
⊢ (↑a : ℝ≥0∞) / 2 < (↑a : ℝ≥0∞)
have rw₁ : Ne (α := ℝ≥0) 2 0
Tactic: rw [← coe_two, ← coe_div, coe_lt_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
⊢ HSub.hSub (α := ℝ≥0∞) 1 2⁻¹ = 2⁻¹
have rw : 1 - 1 / 2 = 1 / 2
Tactic: rw [← one_div, sub_half one_ne_top]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
rw : 1 - 1 / 2 = 1 / 2
⊢ HSub.hSub (α := ℝ≥0∞) 1 2⁻¹ = 2⁻¹
have rw₁ : 1 / 2 = 1 / 2
Tactic: rw [← one_div, sub_half one_ne_top]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
hc : c < a * b
⊢ ∃ a' < a, c < a' * b
have obtain : ∀ (a' : ℝ≥0∞) (hc : c / b < a') (ha' : a' < a), ∃ a' < a, c < a' * b
Tactic: obtain ⟨a', hc, ha'⟩ := exists_between (ENNReal.div_lt_of_lt_mul hc)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
hc : c < a * b
⊢ ∃ b' < b, c < a * b'
have simp_rw : ∀ (hc : c < b * a), ∃ b' < b, c < b' * a
Tactic: simp_rw [mul_comm a] at hc ⊢
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
⊢ a * b ≤ c
have refine : ∀ (d : ℝ≥0∞) (hd : d < a * b), d ≤ c
Tactic: refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd : d < a * b
⊢ d ≤ c
have obtain : ∀ (a' : ℝ≥0∞) (ha' : a' < a) (hd : d < a' * b), d ≤ c
Tactic: obtain ⟨a', ha', hd⟩ := exists_lt_mul_left hd
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
d : ℝ≥0∞
hd_1 : d < a * b
a' : ℝ≥0∞
ha' : a' < a
hd : d < a' * b
⊢ d ≤ c
have obtain : ∀ (b' : ℝ≥0∞) (hb' : b' < b) (hd : d < a' * b'), d ≤ c
Tactic: obtain ⟨b', hb', hd⟩ := exists_lt_mul_right hd
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
h₁ : a ≠ 0 ∨ b ≠ ∞
h₂ : a ≠ ∞ ∨ b ≠ 0
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b
have rw : a⁻¹ * b⁻¹ ≤ c⁻¹
Tactic: rw [← ENNReal.inv_le_inv, ENNReal.mul_inv h₁ h₂]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ℝ≥0∞ ≃o (↑(Iic 1) : Type)
have refine_1 : ∀ (x y : ℝ≥0∞) (hxy : x < y),
  LT.lt (α := (↑(Iic 1) : Type))
    ((fun (x : ℝ≥0∞) ↦ Subtype.mk (p := fun (x : ℝ≥0∞) ↦ Membership.mem (γ := Set ℝ≥0∞) (Iic 1) x) (x⁻¹ + 1)⁻¹ sorry) x)
    ((fun (x : ℝ≥0∞) ↦ Subtype.mk (p := fun (x : ℝ≥0∞) ↦ Membership.mem (γ := Set ℝ≥0∞) (Iic 1) x) (x⁻¹ + 1)⁻¹ sorry) y)
Tactic: refine StrictMono.orderIsoOfRightInverse
    (fun x => ⟨(x⁻¹ + 1)⁻¹, ENNReal.inv_le_one.2 <| le_add_self⟩)
    (fun x y hxy => ?_) (fun x => (x.1⁻¹ - 1)⁻¹) fun x => Subtype.ext ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c d : ℝ≥0∞
r p q : ℝ≥0
refine_1 :
  ∀ (x y : ℝ≥0∞) (hxy : x < y),
    LT.lt (α := (↑(Iic 1) : Type))
      ((fun (x : ℝ≥0∞) ↦ Subtype.mk (p := fun (x : ℝ≥0∞) ↦ Membership.mem (γ := Set ℝ≥0∞) (Iic 1) x) (x⁻¹ + 1)⁻¹ ⋯) x)
      ((fun (x : ℝ≥0∞) ↦ Subtype.mk (p := fun (x : ℝ≥0∞) ↦ Membership.mem (γ := Set ℝ≥0∞) (Iic 1) x) (x⁻¹ + 1)⁻¹ ⋯) y)
⊢ ℝ≥0∞ ≃o (↑(Iic 1) : Type)
have refine_2 : ∀ (x : (↑(Iic 1) : Type)),
  (↑((fun (x : ℝ≥0∞) ↦ Subtype.mk (p := fun (x : ℝ≥0∞) ↦ Membership.mem (γ := Set ℝ≥0∞) (Iic 1) x) (x⁻¹ + 1)⁻¹ sorry)
          ((fun (x : (↑(Iic 1) : Type)) ↦ ((↑x : ℝ≥0∞)⁻¹ - 1)⁻¹) x)) :
      ℝ≥0∞) =
    (↑x : ℝ≥0∞)
Tactic: refine StrictMono.orderIsoOfRightInverse
    (fun x => ⟨(x⁻¹ + 1)⁻¹, ENNReal.inv_le_one.2 <| le_add_self⟩)
    (fun x y hxy => ?_) (fun x => (x.1⁻¹ - 1)⁻¹) fun x => Subtype.ext ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : (↑(Iic 1) : Type)
⊢ (↑((fun (x : ℝ≥0∞) ↦ Subtype.mk (p := fun (x : ℝ≥0∞) ↦ Membership.mem (γ := Set ℝ≥0∞) (Iic 1) x) (x⁻¹ + 1)⁻¹ ⋯)
          ((fun (x : (↑(Iic 1) : Type)) ↦ ((↑x : ℝ≥0∞)⁻¹ - 1)⁻¹) x)) :
      ℝ≥0∞) =
    (↑x : ℝ≥0∞)
have this : 1 ≤ (↑x : ℝ≥0∞)⁻¹
Tactic: have : (1 : ℝ≥0∞) ≤ x.1⁻¹ := ENNReal.one_le_inv.2 x.2
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
⊢ ∃ n > 0, (↑n : ℝ≥0∞)⁻¹ * a < b
have rcases : ∀ (n : ℕ) (npos : n > 0) (hn : a < (↑n : ℝ≥0∞) * b), ∃ n > 0, (↑n : ℝ≥0∞)⁻¹ * a < b
Tactic: rcases exists_nat_pos_mul_gt hb ha with ⟨n, npos, hn⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < (↑n : ℝ≥0∞) * b
⊢ ∃ n > 0, (↑n : ℝ≥0∞)⁻¹ * a < b
have right : (↑n : ℝ≥0∞)⁻¹ * a < b
Tactic: use n, npos
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < (↑n : ℝ≥0∞) * b
⊢ (↑n : ℝ≥0∞)⁻¹ * a < b
have right : a / (↑n : ℝ≥0∞) < b
Tactic: rw [← ENNReal.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
⊢ ∃ n > 0, (↑n : ℝ≥0∞) * a < b
have rcases : ∀ (n : ℕ) (npos : 0 < n) (hn : (↑n : ℝ≥0∞)⁻¹ * a < b), ∃ n > 0, (↑n : ℝ≥0∞) * a < b
Tactic: rcases exists_nat_pos_inv_mul_lt ha hb with ⟨n, npos : 0 < n, hn⟩