awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a⁻¹ * (a * b) = b
have inr₁ : ∀ (ha : a ≠ ∞), a⁻¹ * (a * b) = b
Tactic: obtain rfl | ha := eq_or_ne a ⊤
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ∞ → b = 0
⊢ a * (a⁻¹ * b) = b
have inl : ∀ (ha₀ : Eq (α := ℝ≥0∞) 0 0 → b = 0) (ha : Eq (α := ℝ≥0∞) 0 ∞ → b = 0), 0 * (0⁻¹ * b) = b
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
Cleared hypotheses: a, ha₀, ha
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a * (a⁻¹ * b) = b
have inr : ∀ (ha₀ : a ≠ 0), a * (a⁻¹ * b) = b
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha₀_1 : a = 0 → b = 0
ha : a = ∞ → b = 0
ha₀ : a ≠ 0
⊢ a * (a⁻¹ * b) = b
have inr : ∀ (ha₀ : Eq (α := ℝ≥0∞) ∞ 0 → b = 0) (ha : Eq (α := ℝ≥0∞) ∞ ∞ → b = 0) (ha₀ : Ne (α := ℝ≥0∞) ∞ 0), ∞ * (∞⁻¹ * b) = b
Tactic: obtain rfl | ha := eq_or_ne a ⊤
Cleared hypotheses: a, ha₀_1, ha, ha₀
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a * (a⁻¹ * b) = b
have inr₁ : ∀ (ha : a ≠ ∞), a * (a⁻¹ * b) = b
Tactic: obtain rfl | ha := eq_or_ne a ⊤
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
hb₀ : b = 0 → a = 0
hb : b = ∞ → a = 0
⊢ a * b * b⁻¹ = a
have inl : ∀ (hb₀ : Eq (α := ℝ≥0∞) 0 0 → a = 0) (hb : Eq (α := ℝ≥0∞) 0 ∞ → a = 0), a * 0 * 0⁻¹ = a
Tactic: obtain rfl | hb₀ := eq_or_ne b 0
Cleared hypotheses: b, hb₀, hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a * b * b⁻¹ = a
have inr : ∀ (hb₀ : b ≠ 0), a * b * b⁻¹ = a
Tactic: obtain rfl | hb₀ := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
hb₀_1 : b = 0 → a = 0
hb : b = ∞ → a = 0
hb₀ : b ≠ 0
⊢ a * b * b⁻¹ = a
have inr : ∀ (hb₀ : Eq (α := ℝ≥0∞) ∞ 0 → a = 0) (hb : Eq (α := ℝ≥0∞) ∞ ∞ → a = 0) (hb₀ : Ne (α := ℝ≥0∞) ∞ 0), a * ∞ * ∞⁻¹ = a
Tactic: obtain rfl | hb := eq_or_ne b ⊤
Cleared hypotheses: b, hb₀_1, hb, hb₀
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a * b * b⁻¹ = a
have inr₁ : ∀ (hb : b ≠ ∞), a * b * b⁻¹ = a
Tactic: obtain rfl | hb := eq_or_ne b ⊤
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
hb₀ : b = 0 → a = 0
hb : b = ∞ → a = 0
⊢ a * b⁻¹ * b = a
have inl : ∀ (hb₀ : Eq (α := ℝ≥0∞) 0 0 → a = 0) (hb : Eq (α := ℝ≥0∞) 0 ∞ → a = 0), a * 0⁻¹ * 0 = a
Tactic: obtain rfl | hb₀ := eq_or_ne b 0
Cleared hypotheses: b, hb₀, hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a * b⁻¹ * b = a
have inr : ∀ (hb₀ : b ≠ 0), a * b⁻¹ * b = a
Tactic: obtain rfl | hb₀ := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
hb₀_1 : b = 0 → a = 0
hb : b = ∞ → a = 0
hb₀ : b ≠ 0
⊢ a * b⁻¹ * b = a
have inr : ∀ (hb₀ : Eq (α := ℝ≥0∞) ∞ 0 → a = 0) (hb : Eq (α := ℝ≥0∞) ∞ ∞ → a = 0) (hb₀ : Ne (α := ℝ≥0∞) ∞ 0), a * ∞⁻¹ * ∞ = a
Tactic: obtain rfl | hb := eq_or_ne b ⊤
Cleared hypotheses: b, hb₀_1, hb, hb₀
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a * b⁻¹ * b = a
have inr₁ : ∀ (hb : b ≠ ∞), a * b⁻¹ * b = a
Tactic: obtain rfl | hb := eq_or_ne b ⊤
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ∞ → b = 0
⊢ a * (b / a) = b
have rw : b / a * a = b
Tactic: rw [mul_comm, ENNReal.div_mul_cancel' ha₀ ha]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ∞ → b = 0
rw : b / a * a = b
⊢ a * (b / a) = b
have rw₁ : b = b
Tactic: rw [mul_comm, ENNReal.div_mul_cancel' ha₀ ha]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a⁻¹⁻¹ = a
have pos : a = 0 → a⁻¹⁻¹ = a
Tactic: by_cases a = 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
pos : a = 0 → a⁻¹⁻¹ = a
⊢ a⁻¹⁻¹ = a
have neg : ¬a = 0 → a⁻¹⁻¹ = a
Tactic: by_cases a = 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h : a = 0
⊢ a⁻¹⁻¹ = a
have pos : Eq (α := ℝ≥0∞) ∞ 0 → Eq (α := ℝ≥0∞) ∞⁻¹⁻¹ ∞
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h : a = 0
pos : Eq (α := ℝ≥0∞) ∞ 0 → Eq (α := ℝ≥0∞) ∞⁻¹⁻¹ ∞
⊢ a⁻¹⁻¹ = a
have pos₁ : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞) = 0 → (↑x : ℝ≥0∞)⁻¹⁻¹ = (↑x : ℝ≥0∞)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h : ¬a = 0
⊢ a⁻¹⁻¹ = a
have neg : ¬Eq (α := ℝ≥0∞) ∞ 0 → Eq (α := ℝ≥0∞) ∞⁻¹⁻¹ ∞
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h : ¬a = 0
neg : ¬Eq (α := ℝ≥0∞) ∞ 0 → Eq (α := ℝ≥0∞) ∞⁻¹⁻¹ ∞
⊢ a⁻¹⁻¹ = a
have neg₁ : ∀ (x : ℝ≥0), ¬(↑x : ℝ≥0∞) = 0 → (↑x : ℝ≥0∞)⁻¹⁻¹ = (↑x : ℝ≥0∞)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
⊢ a⁻¹ = 1 ↔ a = 1
have rw : a⁻¹⁻¹ = 1⁻¹ ↔ a = 1
Tactic: rw [← inv_inj, inv_inv, inv_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
rw : a⁻¹⁻¹ = 1⁻¹ ↔ a = 1
⊢ a⁻¹ = 1 ↔ a = 1
have rw₁ : a = 1⁻¹ ↔ a = 1
Tactic: rw [← inv_inj, inv_inv, inv_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
rw : a⁻¹⁻¹ = 1⁻¹ ↔ a = 1
rw₁ : a = 1⁻¹ ↔ a = 1
⊢ a⁻¹ = 1 ↔ a = 1
have rw₂ : a = 1 ↔ a = 1
Tactic: rw [← inv_inj, inv_inv, inv_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y z : ℝ≥0∞
h1 : x ≠ 0
h2 : x ≠ ∞
⊢ x⁻¹ * y ≤ z ↔ y ≤ x * z
have rw : x * (x⁻¹ * y) ≤ x * z ↔ y ≤ x * z
Tactic: rw [← ENNReal.mul_le_mul_iff_right h1 h2, ← mul_assoc, ENNReal.mul_inv_cancel h1 h2, one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y z : ℝ≥0∞
h1 : x ≠ 0
h2 : x ≠ ∞
rw : x * (x⁻¹ * y) ≤ x * z ↔ y ≤ x * z
⊢ x⁻¹ * y ≤ z ↔ y ≤ x * z
have rw₁ : x * x⁻¹ * y ≤ x * z ↔ y ≤ x * z
Tactic: rw [← ENNReal.mul_le_mul_iff_right h1 h2, ← mul_assoc, ENNReal.mul_inv_cancel h1 h2, one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ x⁻¹ * y ≤ z ↔ y ≤ x * z
have rw₂ : 1 * y ≤ x * z ↔ y ≤ x * z
Tactic: rw [← ENNReal.mul_le_mul_iff_right h1 h2, ← mul_assoc, ENNReal.mul_inv_cancel h1 h2, one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ x⁻¹ * y ≤ z ↔ y ≤ x * z
have rw₃ : y ≤ x * z ↔ y ≤ x * z
Tactic: rw [← ENNReal.mul_le_mul_iff_right h1 h2, ← mul_assoc, ENNReal.mul_inv_cancel h1 h2, one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
⊢ x * y⁻¹ ≤ z ↔ x ≤ z * y
have rw : y⁻¹ * x ≤ z ↔ x ≤ z * y
Tactic: rw [mul_comm, ENNReal.inv_mul_le_iff h1 h2, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
rw : y⁻¹ * x ≤ z ↔ x ≤ z * y
⊢ x * y⁻¹ ≤ z ↔ x ≤ z * y
have rw₁ : x ≤ y * z ↔ x ≤ z * y
Tactic: rw [mul_comm, ENNReal.inv_mul_le_iff h1 h2, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
rw : y⁻¹ * x ≤ z ↔ x ≤ z * y
rw₁ : x ≤ y * z ↔ x ≤ z * y
⊢ x * y⁻¹ ≤ z ↔ x ≤ z * y
have rw₂ : x ≤ z * y ↔ x ≤ z * y
Tactic: rw [mul_comm, ENNReal.inv_mul_le_iff h1 h2, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
⊢ x / y ≤ z ↔ x ≤ z * y
have rw : x * y⁻¹ ≤ z ↔ x ≤ z * y
Tactic: rw [div_eq_mul_inv, ENNReal.mul_inv_le_iff h1 h2]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
rw : x * y⁻¹ ≤ z ↔ x ≤ z * y
⊢ x / y ≤ z ↔ x ≤ z * y
have rw₁ : x ≤ z * y ↔ x ≤ z * y
Tactic: rw [div_eq_mul_inv, ENNReal.mul_inv_le_iff h1 h2]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
⊢ x / y ≤ z ↔ x ≤ y * z
have rw : x / y ≤ z ↔ x ≤ z * y
Tactic: rw [mul_comm, ENNReal.div_le_iff h1 h2]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
rw : x / y ≤ z ↔ x ≤ z * y
⊢ x / y ≤ z ↔ x ≤ y * z
have rw₁ : x ≤ z * y ↔ x ≤ z * y
Tactic: rw [mul_comm, ENNReal.div_le_iff h1 h2]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : a ≠ ∞ ∨ b ≠ 0
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have cases : ∀ (ha : a ≠ 0 ∨ Ne (α := ℝ≥0∞) ∞ ∞) (hb : a ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ 0), (a * ∞)⁻¹ = a⁻¹ * ∞⁻¹
Tactic: cases b
Cleared hypotheses: b, ha, hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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⁻¹ * ∞⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
have coe : ∀ (x : ℝ≥0) (ha : a ≠ 0 ∨ (↑x : ℝ≥0∞) ≠ ∞) (hb : a ≠ ∞ ∨ (↑x : ℝ≥0∞) ≠ 0), (a * (↑x : ℝ≥0∞))⁻¹ = a⁻¹ * (↑x : ℝ≥0∞)⁻¹
Tactic: cases b
Cleared hypotheses: b, ha, hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
x : ℝ≥0
ha : a ≠ 0 ∨ (↑x : ℝ≥0∞) ≠ ∞
hb : a ≠ ∞ ∨ (↑x : ℝ≥0∞) ≠ 0
⊢ (a * (↑x : ℝ≥0∞))⁻¹ = a⁻¹ * (↑x : ℝ≥0∞)⁻¹
have cases : ∀ (ha : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑x : ℝ≥0∞) ≠ ∞) (hb : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑x : ℝ≥0∞) ≠ 0),
  (∞ * (↑x : ℝ≥0∞))⁻¹ = ∞⁻¹ * (↑x : ℝ≥0∞)⁻¹
Tactic: cases a
Cleared hypotheses: a, ha, hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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∞)⁻¹
⊢ (a * (↑x : ℝ≥0∞))⁻¹ = a⁻¹ * (↑x : ℝ≥0∞)⁻¹
have 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∞)⁻¹
Tactic: cases a
Cleared hypotheses: a, ha, hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
a b : ℝ≥0∞
htop : b ≠ ∞ ∨ a ≠ ∞
hzero : b ≠ 0 ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a
have htop₁ : b⁻¹ ≠ 0 ∨ a ≠ ∞
Tactic: rw [← ENNReal.inv_ne_zero] at htop
Cleared hypotheses: htop, hzero
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b ≠ 0 ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a
have hzero₁ : b⁻¹ ≠ ∞ ∨ a ≠ 0
Tactic: rw [← ENNReal.inv_ne_top] at hzero
Cleared hypotheses: hzero
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a
have rw : (b⁻¹ * a)⁻¹ = b / a
Tactic: rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ENNReal.mul_inv htop hzero, mul_comm, inv_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
rw : (b⁻¹ * a)⁻¹ = b / a
⊢ (a / b)⁻¹ = b / a
have rw₁ : (b⁻¹ * a)⁻¹ = a⁻¹ * b
Tactic: rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ENNReal.mul_inv htop hzero, mul_comm, inv_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
rw : (b⁻¹ * a)⁻¹ = b / a
rw₁ : (b⁻¹ * a)⁻¹ = a⁻¹ * b
⊢ (a / b)⁻¹ = b / a
have rw₂ : b⁻¹⁻¹ * a⁻¹ = a⁻¹ * b
Tactic: rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ENNReal.mul_inv htop hzero, mul_comm, inv_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ (a / b)⁻¹ = b / a
have rw₃ : a⁻¹ * b⁻¹⁻¹ = a⁻¹ * b
Tactic: rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ENNReal.mul_inv htop hzero, mul_comm, inv_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ (a / b)⁻¹ = b / a
have rw₄ : a⁻¹ * b = a⁻¹ * b
Tactic: rw [ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, ENNReal.mul_inv htop hzero, mul_comm, inv_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ c * a / (c * b) = a / b
have rw : 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
rw : c * a * (c * b)⁻¹ = a / b
⊢ c * a / (c * b) = a / b
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
rw : c * a * (c * b)⁻¹ = a / b
rw₁ : c * a * (c * b)⁻¹ = a * b⁻¹
⊢ c * a / (c * b) = a / b
have rw₂ : 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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⁻¹
⊢ c * a / (c * b) = a / b
have rw₃ : c * c⁻¹ * (a * 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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⁻¹
⊢ c * a / (c * b) = a / b
have rw₄ : 1 * (a * 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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⁻¹
⊢ c * a / (c * b) = a / b
have rw₅ : a * 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
⊢ a * c / (b * c) = a / b
have rw : 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
rw : a * c * (b * c)⁻¹ = a / b
⊢ a * c / (b * c) = a / b
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ∞
rw : a * c * (b * c)⁻¹ = a / b
rw₁ : a * c * (b * c)⁻¹ = a * b⁻¹
⊢ a * c / (b * c) = a / b
have rw₂ : 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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⁻¹
⊢ a * c / (b * c) = a / b
have rw₃ : a * b⁻¹ * (c * 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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⁻¹
⊢ a * c / (b * c) = a / b
have rw₄ : a * b⁻¹ * 1 = 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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⁻¹
⊢ a * c / (b * c) = a / b
have rw₅ : a * b⁻¹ = 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]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) / c = a / c - b / c
have simp_rw : (a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹
Tactic: simp_rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
h : a < b
⊢ b⁻¹ < a⁻¹
have lift : ∀ (a : ℝ≥0) (h : (↑a : ℝ≥0∞) < b), b⁻¹ < (↑a : ℝ≥0∞)⁻¹
Tactic: lift a to ℝ≥0 using h.ne_top
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
b : ℝ≥0∞
a : ℝ≥0
h : (↑a : ℝ≥0∞) < b
⊢ b⁻¹ < (↑a : ℝ≥0∞)⁻¹
have top : ∀ (h : (↑a : ℝ≥0∞) < ∞), ∞⁻¹ < (↑a : ℝ≥0∞)⁻¹
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
b : ℝ≥0∞
a : ℝ≥0
h : (↑a : ℝ≥0∞) < b
top : ∀ (h : (↑a : ℝ≥0∞) < ∞), ∞⁻¹ < (↑a : ℝ≥0∞)⁻¹
⊢ b⁻¹ < (↑a : ℝ≥0∞)⁻¹
have coe : ∀ (x : ℝ≥0) (h : (↑a : ℝ≥0∞) < (↑x : ℝ≥0∞)), (↑x : ℝ≥0∞)⁻¹ < (↑a : ℝ≥0∞)⁻¹
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
a x : ℝ≥0
h : (↑a : ℝ≥0∞) < (↑x : ℝ≥0∞)
⊢ (↑x : ℝ≥0∞)⁻¹ < (↑a : ℝ≥0∞)⁻¹
have h₁ : a < x
Tactic: rw [coe_lt_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a x : ℝ≥0
h : a < x
⊢ (↑x : ℝ≥0∞)⁻¹ < (↑a : ℝ≥0∞)⁻¹
have coe : ∀ (h : 0 < x), (↑x : ℝ≥0∞)⁻¹ < (↑0 : ℝ≥0∞)⁻¹
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a x : ℝ≥0
h : a < x
coe : ∀ (h : 0 < x), (↑x : ℝ≥0∞)⁻¹ < (↑0 : ℝ≥0∞)⁻¹
⊢ (↑x : ℝ≥0∞)⁻¹ < (↑a : ℝ≥0∞)⁻¹
have coe₁ : ∀ (ha : a ≠ 0), (↑x : ℝ≥0∞)⁻¹ < (↑a : ℝ≥0∞)⁻¹
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a x : ℝ≥0
h : a < x
ha : a ≠ 0
⊢ (↑x : ℝ≥0∞)⁻¹ < (↑a : ℝ≥0∞)⁻¹
have coe : x⁻¹ < a⁻¹
Tactic: rw [← coe_inv h.ne_bot, ← coe_inv ha, coe_lt_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a
have rw : 1⁻¹ ≤ a ↔ 1 ≤ a
Tactic: rw [inv_le_iff_inv_le, inv_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
rw : 1⁻¹ ≤ a ↔ 1 ≤ a
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a
have rw₁ : 1 ≤ a ↔ 1 ≤ a
Tactic: rw [inv_le_iff_inv_le, inv_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1
have rw : a ≤ 1⁻¹ ↔ a ≤ 1
Tactic: rw [le_inv_iff_le_inv, inv_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
rw : a ≤ 1⁻¹ ↔ a ≤ 1
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1
have rw₁ : a ≤ 1 ↔ a ≤ 1
Tactic: rw [le_inv_iff_le_inv, inv_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
⊢ a⁻¹ < 1 ↔ 1 < a
have rw : 1⁻¹ < a ↔ 1 < a
Tactic: rw [inv_lt_iff_inv_lt, inv_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
rw : 1⁻¹ < a ↔ 1 < a
⊢ a⁻¹ < 1 ↔ 1 < a
have rw₁ : 1 < a ↔ 1 < a
Tactic: rw [inv_lt_iff_inv_lt, inv_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
⊢ 1 < a⁻¹ ↔ a < 1
have rw : a < 1⁻¹ ↔ a < 1
Tactic: rw [lt_inv_iff_lt_inv, inv_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
rw : a < 1⁻¹ ↔ a < 1
⊢ 1 < a⁻¹ ↔ a < 1
have rw₁ : a < 1 ↔ a < 1
Tactic: rw [lt_inv_iff_lt_inv, inv_one]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
⊢ a / ∞ = 0
have rw : a * ∞⁻¹ = 0
Tactic: rw [div_eq_mul_inv, inv_top, mul_zero]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
rw : a * ∞⁻¹ = 0
⊢ a / ∞ = 0
have rw₁ : a * 0 = 0
Tactic: rw [div_eq_mul_inv, inv_top, mul_zero]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
rw : a * ∞⁻¹ = 0
rw₁ : a * 0 = 0
⊢ a / ∞ = 0
have rw₂ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [div_eq_mul_inv, inv_top, mul_zero]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
⊢ a / (a / b) = b
have inl : ∀ (h₀ : Eq (α := ℝ≥0∞) 0 0 → b = 0) (h₁ : Eq (α := ℝ≥0∞) 0 ∞ → b = 0), 0 / (0 / b) = b
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a, h₀, h₁
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a / (a / b) = b
have inr : ∀ (ha : a ≠ 0), a / (a / b) = b
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
ha : a ≠ 0
⊢ a / (a / b) = b
have inr : ∀ (h₀ : Eq (α := ℝ≥0∞) ∞ 0 → b = 0) (h₁ : Eq (α := ℝ≥0∞) ∞ ∞ → b = 0) (ha : Ne (α := ℝ≥0∞) ∞ 0), ∞ / (∞ / b) = b
Tactic: obtain rfl | ha' := eq_or_ne a ∞
Cleared hypotheses: a, h₀, h₁, ha
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a / (a / b) = b
have inr₁ : ∀ (ha' : a ≠ ∞), a / (a / b) = b
Tactic: obtain rfl | ha' := eq_or_ne a ∞
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
ha : a ≠ 0
ha' : a ≠ ∞
⊢ a / (a / b) = b
have inr : (a / b)⁻¹ * a = b
Tactic: rw [ENNReal.div_eq_inv_mul, ENNReal.inv_div (Or.inr ha') (Or.inr ha),
    ENNReal.div_mul_cancel ha ha']
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
ha : a ≠ 0
ha' : a ≠ ∞
inr : (a / b)⁻¹ * a = b
⊢ a / (a / b) = b
have inr₁ : b / a * a = b
Tactic: rw [ENNReal.div_eq_inv_mul, ENNReal.inv_div (Or.inr ha') (Or.inr ha),
    ENNReal.div_mul_cancel ha ha']
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
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
⊢ a / (a / b) = b
have inr₂ : b = b
Tactic: rw [ENNReal.div_eq_inv_mul, ENNReal.inv_div (Or.inr ha') (Or.inr ha),
    ENNReal.div_mul_cancel ha ha']