awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
pos : ∀ (hf : ∀ (i : ι), f i = 0), a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
have neg : ∀ (hf : ¬∀ (i : ι), f i = 0), a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
Tactic: by_cases hf : ∀ i, f i = 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
have neg : HMul.hMul (α := ℝ≥0∞) 0 (⨆ (i : ι), f i) = ⨆ (i : ι), 0 * f i
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
neg : HMul.hMul (α := ℝ≥0∞) 0 (⨆ (i : ι), f i) = ⨆ (i : ι), 0 * f i
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
have neg₁ : ∀ (ha₀ : a ≠ 0), a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
have neg : ∀ (ha₀ : Ne (α := ℝ≥0∞) ∞ 0), HMul.hMul (α := ℝ≥0∞) ∞ (⨆ (i : ι), f i) = ⨆ (i : ι), ∞ * f i
Tactic: obtain rfl | ha := eq_or_ne a ∞
Cleared hypotheses: a, ha₀
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
neg : ∀ (ha₀ : Ne (α := ℝ≥0∞) ∞ 0), HMul.hMul (α := ℝ≥0∞) ∞ (⨆ (i : ι), f i) = ⨆ (i : ι), ∞ * f i
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
have neg₁ : ∀ (ha : a ≠ ∞), a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
Tactic: obtain rfl | ha := eq_or_ne a ∞
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
⊢ HMul.hMul (α := ℝ≥0∞) ∞ (⨆ (i : ι), f i) = ⨆ (i : ι), ∞ * f i
have neg : ∀ (i : ι) (hi : ¬f i = 0), HMul.hMul (α := ℝ≥0∞) ∞ (⨆ (i : ι), f i) = ⨆ (i : ι), ∞ * f i
Tactic: obtain ⟨i, hi⟩ := not_forall.1 hf
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : a = 0 → Nonempty ι
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
have inl : ∀ (hinfty : Eq (α := ℝ≥0∞) 0 ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0)
  (h₀ : Eq (α := ℝ≥0∞) 0 0 → Nonempty ι), HMul.hMul (α := ℝ≥0∞) 0 (⨅ (i : ι), f i) = ⨅ (i : ι), 0 * f i
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
Cleared hypotheses: a, hinfty, h₀
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : a = 0 → Nonempty ι
inl :
  ∀ (hinfty : Eq (α := ℝ≥0∞) 0 ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0)
    (h₀ : Eq (α := ℝ≥0∞) 0 0 → Nonempty ι), HMul.hMul (α := ℝ≥0∞) 0 (⨅ (i : ι), f i) = ⨅ (i : ι), 0 * f i
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
have inr : ∀ (ha₀ : a ≠ 0), a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : a = 0 → Nonempty ι
ha₀ : a ≠ 0
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
have inr : ∀ (hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0)
  (h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι) (ha₀ : Ne (α := ℝ≥0∞) ∞ 0),
  HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i
Tactic: obtain rfl | ha := eq_or_ne a ∞
Cleared hypotheses: a, hinfty, h₀, ha₀
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : a = 0 → Nonempty ι
ha₀ : a ≠ 0
inr :
  ∀ (hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0)
    (h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι) (ha₀ : Ne (α := ℝ≥0∞) ∞ 0),
    HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
have inr₁ : ∀ (ha : a ≠ ∞), a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
Tactic: obtain rfl | ha := eq_or_ne a ∞
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
⊢ HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i
have inr : ∀ (i : ι) (hi : f i = 0), HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i
Tactic: obtain ⟨i, hi⟩ | hf := em (∃ i, f i = 0)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
inr : ∀ (i : ι) (hi : f i = 0), HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i
⊢ HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i
have inr₁ : ∀ (hf : ¬∃ (i : ι), f i = 0), HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i
Tactic: obtain ⟨i, hi⟩ | hf := em (∃ i, f i = 0)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
i : ι
hi : f i = 0
⊢ HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i
have inr : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ι), ∞ * f i < b
Tactic: rw [iInf_eq_bot.2, iInf_eq_bot.2, bot_eq_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
i : ι
hi : f i = 0
inr : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ι), ∞ * f i < b
⊢ HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i
have inr₁ : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ι), f i < b
Tactic: rw [iInf_eq_bot.2, iInf_eq_bot.2, bot_eq_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
hf : ¬∃ (i : ι), f i = 0
⊢ HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i
have inr : ∀ (i : ι), ∞ * f i = ∞
Tactic: rw [top_mul (mt (hinfty rfl) hf), eq_comm, iInf_eq_top]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ (i : ι), f i ≠ ∞
hg : ∃ (j : κ), g j ≠ ∞
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
⊢ a ≤ HMul.hMul (α := ℝ≥0∞) (⨅ (i : ι), f i) (⨅ (j : κ), g j)
have rw : a ≤ HMul.hMul (α := ℝ≥0∞) (⨅ (i : { i : ι // f i ≠ ∞ }), f (↑i : ι)) (⨅ (j : κ), g j)
Tactic: rw [← iInf_ne_top_subtype]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ (i : ι), f i ≠ ∞
hg : ∃ (j : κ), g j ≠ ∞
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
⊢ a ≤ HMul.hMul (α := ℝ≥0∞) (⨅ (i : { i : ι // f i ≠ ∞ }), f (↑i : ι)) (⨅ (j : κ), g j)
have this : Nonempty.{max 1 u_1} { a : ι // f a ≠ ∞ }
Tactic: have := nonempty_subtype.2 hf
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ (i : ι), f i ≠ ∞
hg : ∃ (j : κ), g j ≠ ∞
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this : Nonempty.{max 1 u_1} { a : ι // f a ≠ ∞ }
⊢ a ≤ HMul.hMul (α := ℝ≥0∞) (⨅ (i : { i : ι // f i ≠ ∞ }), f (↑i : ι)) (⨅ (j : κ), g j)
have this₁ : Nonempty κ
Tactic: have := hg.nonempty
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (hypothesis)
Goal:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ (i : ι), f i ≠ ∞
hg : ∃ (j : κ), g j ≠ ∞
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this_1 : Nonempty.{max 1 u_1} { a : ι // f a ≠ ∞ }
this : Nonempty κ
⊢ a ≤ HMul.hMul (α := ℝ≥0∞) (⨅ (i : { i : ι // f i ≠ ∞ }), f (↑i : ι)) (⨅ (j : κ), g j)
have hg₁ : Ne (α := ℝ≥0∞) (⨅ (j : κ), g j) ∞
Tactic: replace hg : ⨅ j, g j ≠ ∞ := by simpa using hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ (i : ι), f i ≠ ∞
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this_1 : Nonempty.{max 1 u_1} { a : ι // f a ≠ ∞ }
this : Nonempty κ
hg : Ne (α := ℝ≥0∞) (⨅ (j : κ), g j) ∞
⊢ a ≤ HMul.hMul (α := ℝ≥0∞) (⨅ (i : { i : ι // f i ≠ ∞ }), f (↑i : ι)) (⨅ (j : κ), g j)
have rw : ∀ (i : { i : ι // f i ≠ ∞ }), a ≤ f (↑i : ι) * ⨅ (j : κ), g j
Tactic: rw [iInf_mul fun h ↦ (hg h).elim, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ (i : ι), f i ≠ ∞
hg : ∃ (j : ι), g j ≠ ∞
h : ∀ (i j : ι), ∃ (k : ι), f k * g k ≤ f i * g j
⊢ HMul.hMul (α := ℝ≥0∞) (⨅ (i : ι), f i) (⨅ (i : ι), g i) = ⨅ (i : ι), f i * g i
have refine : ∀ (i j : ι), ⨅ (i : ι), f i * g i ≤ f i * g j
Tactic: refine le_antisymm (le_iInf fun i ↦ mul_le_mul' (iInf_le ..) (iInf_le ..))
    (le_iInf_mul_iInf hf hg fun i j ↦ ?_)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ (i : ι), f i ≠ ∞
hg : ∃ (j : ι), g j ≠ ∞
h : ∀ (i j : ι), ∃ (k : ι), f k * g k ≤ f i * g j
i j : ι
⊢ ⨅ (i : ι), f i * g i ≤ f i * g j
have obtain : ∀ (k : ι) (hk : f k * g k ≤ f i * g j), ⨅ (i : ι), f i * g i ≤ f i * g j
Tactic: obtain ⟨k, hk⟩ := h i j
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
s : Set ℝ≥0∞
c : R
⊢ c • sSup s = ⨆ a ∈ s, c • a
have simp_rw : HSMul.hSMul (β := ℝ≥0∞) c 1 * sSup s = ⨆ a ∈ s, c • a
Tactic: simp_rw [← smul_one_mul c (sSup s), ENNReal.mul_sSup, smul_one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
s : Set ℝ≥0∞
c : R
simp_rw : HSMul.hSMul (β := ℝ≥0∞) c 1 * sSup s = ⨆ a ∈ s, c • a
⊢ c • sSup s = ⨆ a ∈ s, c • a
have simp_rw₁ : Eq (α := ℝ≥0∞) (⨆ b ∈ s, HSMul.hSMul (β := ℝ≥0∞) c 1 * b) (⨆ a ∈ s, c • a)
Tactic: simp_rw [← smul_one_mul c (sSup s), ENNReal.mul_sSup, smul_one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹
have rw : (↑x⁻¹.toNNReal : ℝ≥0∞) = (ENNReal.ofReal x)⁻¹
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, ← @coe_inv (Real.toNNReal x) (by simp [hx]), coe_inj,
    ← Real.toNNReal_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ
hx : 0 < x
rw : (↑x⁻¹.toNNReal : ℝ≥0∞) = (ENNReal.ofReal x)⁻¹
⊢ ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹
have rw₁ : (↑x⁻¹.toNNReal : ℝ≥0∞) = (↑x.toNNReal : ℝ≥0∞)⁻¹
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, ← @coe_inv (Real.toNNReal x) (by simp [hx]), coe_inj,
    ← Real.toNNReal_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ
hx : 0 < x
rw : (↑x⁻¹.toNNReal : ℝ≥0∞) = (ENNReal.ofReal x)⁻¹
rw₁ : (↑x⁻¹.toNNReal : ℝ≥0∞) = (↑x.toNNReal : ℝ≥0∞)⁻¹
⊢ ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹
have rw₂ : (↑x⁻¹.toNNReal : ℝ≥0∞) = (↑x.toNNReal⁻¹ : ℝ≥0∞)
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, ← @coe_inv (Real.toNNReal x) (by simp [hx]), coe_inj,
    ← Real.toNNReal_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ
hx : 0 < x
rw : (↑x⁻¹.toNNReal : ℝ≥0∞) = (ENNReal.ofReal x)⁻¹
rw₁ : (↑x⁻¹.toNNReal : ℝ≥0∞) = (↑x.toNNReal : ℝ≥0∞)⁻¹
rw₂ : (↑x⁻¹.toNNReal : ℝ≥0∞) = (↑x.toNNReal⁻¹ : ℝ≥0∞)
⊢ ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹
have rw₃ : x⁻¹.toNNReal = x.toNNReal⁻¹
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, ← @coe_inv (Real.toNNReal x) (by simp [hx]), coe_inj,
    ← Real.toNNReal_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ
hx : 0 < x
rw : (↑x⁻¹.toNNReal : ℝ≥0∞) = (ENNReal.ofReal x)⁻¹
rw₁ : (↑x⁻¹.toNNReal : ℝ≥0∞) = (↑x.toNNReal : ℝ≥0∞)⁻¹
rw₂ : (↑x⁻¹.toNNReal : ℝ≥0∞) = (↑x.toNNReal⁻¹ : ℝ≥0∞)
rw₃ : x⁻¹.toNNReal = x.toNNReal⁻¹
⊢ ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹
have rw₄ : x⁻¹.toNNReal = x⁻¹.toNNReal
Tactic: rw [ENNReal.ofReal, ENNReal.ofReal, ← @coe_inv (Real.toNNReal x) (by simp [hx]), coe_inj,
    ← Real.toNNReal_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ
⊢ ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹
have inl : ∀ (hx : 0 < x), ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹
Tactic: obtain hx | hx := lt_or_ge 0 x
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x : ℝ
inl : ∀ (hx : 0 < x), ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹
⊢ ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹
have inr : ∀ (hx : x ≤ 0), ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹
Tactic: obtain hx | hx := lt_or_ge 0 x
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
⊢ ENNReal.ofReal (x / y) ≤ ENNReal.ofReal x / ENNReal.ofReal y
have simp_rw : ENNReal.ofReal x * ENNReal.ofReal y⁻¹ ≤ ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
Tactic: simp_rw [div_eq_mul_inv, ofReal_mul' (inv_nonneg.2 hy)]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y : ℝ
hy : 0 ≤ y
⊢ ENNReal.ofReal x * ENNReal.ofReal y⁻¹ ≤ ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
have bc : ENNReal.ofReal y⁻¹ ≤ (ENNReal.ofReal y)⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y : ℝ
hy : 0 < y
⊢ ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y
have rw : ENNReal.ofReal (x * y⁻¹) = ENNReal.ofReal x / ENNReal.ofReal y
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ofReal_mul' (inv_nonneg.2 hy.le), ofReal_inv_of_pos hy]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y : ℝ
hy : 0 < y
rw : ENNReal.ofReal (x * y⁻¹) = ENNReal.ofReal x / ENNReal.ofReal y
⊢ ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y
have rw₁ : ENNReal.ofReal (x * y⁻¹) = ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ofReal_mul' (inv_nonneg.2 hy.le), ofReal_inv_of_pos hy]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y : ℝ
hy : 0 < y
rw : ENNReal.ofReal (x * y⁻¹) = ENNReal.ofReal x / ENNReal.ofReal y
rw₁ : ENNReal.ofReal (x * y⁻¹) = ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
⊢ ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y
have rw₂ : ENNReal.ofReal x * ENNReal.ofReal y⁻¹ = ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ofReal_mul' (inv_nonneg.2 hy.le), ofReal_inv_of_pos hy]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
x y : ℝ
hy : 0 < y
rw : ENNReal.ofReal (x * y⁻¹) = ENNReal.ofReal x / ENNReal.ofReal y
rw₁ : ENNReal.ofReal (x * y⁻¹) = ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
rw₂ : ENNReal.ofReal x * ENNReal.ofReal y⁻¹ = ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
⊢ ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y
have rw₃ : ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹ = ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ofReal_mul' (inv_nonneg.2 hy.le), ofReal_inv_of_pos hy]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0
⊢ (↑a : ℝ≥0∞)⁻¹.toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹
have coe : (↑0 : ℝ≥0∞)⁻¹.toNNReal = (↑0 : ℝ≥0∞).toNNReal⁻¹
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
coe : (↑0 : ℝ≥0∞)⁻¹.toNNReal = (↑0 : ℝ≥0∞).toNNReal⁻¹
⊢ (↑a : ℝ≥0∞)⁻¹.toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹
have coe₁ : ∀ (ha : a ≠ 0), (↑a : ℝ≥0∞)⁻¹.toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0
ha : a ≠ 0
⊢ (↑a : ℝ≥0∞)⁻¹.toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹
have coe : (↑a⁻¹ : ℝ≥0∞).toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹
Tactic: rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0
ha : a ≠ 0
coe : (↑a⁻¹ : ℝ≥0∞).toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹
⊢ (↑a : ℝ≥0∞)⁻¹.toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹
have coe₁ : a⁻¹ = (↑a : ℝ≥0∞).toNNReal⁻¹
Tactic: rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0
ha : a ≠ 0
coe : (↑a⁻¹ : ℝ≥0∞).toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹
coe₁ : a⁻¹ = (↑a : ℝ≥0∞).toNNReal⁻¹
⊢ (↑a : ℝ≥0∞)⁻¹.toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹
have coe₂ : a⁻¹ = a⁻¹
Tactic: rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
⊢ a⁻¹.toNNReal = a.toNNReal⁻¹
have top : ENNReal.toNNReal ∞⁻¹ = (ENNReal.toNNReal ∞)⁻¹
Tactic: cases a with
  | top => simp
  | coe a =>
    rcases eq_or_ne a 0 with (rfl | ha); · simp
    rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a : ℝ≥0∞
top : ENNReal.toNNReal ∞⁻¹ = (ENNReal.toNNReal ∞)⁻¹
⊢ a⁻¹.toNNReal = a.toNNReal⁻¹
have coe : ∀ (a : ℝ≥0), (↑a : ℝ≥0∞)⁻¹.toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹
Tactic: cases a with
  | top => simp
  | coe a =>
    rcases eq_or_ne a 0 with (rfl | ha); · simp
    rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
⊢ (a / b).toNNReal = a.toNNReal / b.toNNReal
have rw : (a * b⁻¹).toNNReal = a.toNNReal / b.toNNReal
Tactic: rw [div_eq_mul_inv, toNNReal_mul, toNNReal_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
rw : (a * b⁻¹).toNNReal = a.toNNReal / b.toNNReal
⊢ (a / b).toNNReal = a.toNNReal / b.toNNReal
have rw₁ : a.toNNReal * b⁻¹.toNNReal = a.toNNReal / b.toNNReal
Tactic: rw [div_eq_mul_inv, toNNReal_mul, toNNReal_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
rw : (a * b⁻¹).toNNReal = a.toNNReal / b.toNNReal
rw₁ : a.toNNReal * b⁻¹.toNNReal = a.toNNReal / b.toNNReal
⊢ (a / b).toNNReal = a.toNNReal / b.toNNReal
have rw₂ : a.toNNReal * b.toNNReal⁻¹ = a.toNNReal / b.toNNReal
Tactic: rw [div_eq_mul_inv, toNNReal_mul, toNNReal_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
rw : (a * b⁻¹).toNNReal = a.toNNReal / b.toNNReal
rw₁ : a.toNNReal * b⁻¹.toNNReal = a.toNNReal / b.toNNReal
rw₂ : a.toNNReal * b.toNNReal⁻¹ = a.toNNReal / b.toNNReal
⊢ (a / b).toNNReal = a.toNNReal / b.toNNReal
have rw₃ : a.toNNReal * b.toNNReal⁻¹ = a.toNNReal * b.toNNReal⁻¹
Tactic: rw [div_eq_mul_inv, toNNReal_mul, toNNReal_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
⊢ (a / b).toReal = a.toReal / b.toReal
have rw : (a * b⁻¹).toReal = a.toReal / b.toReal
Tactic: rw [div_eq_mul_inv, toReal_mul, toReal_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
rw : (a * b⁻¹).toReal = a.toReal / b.toReal
⊢ (a / b).toReal = a.toReal / b.toReal
have rw₁ : a.toReal * b⁻¹.toReal = a.toReal / b.toReal
Tactic: rw [div_eq_mul_inv, toReal_mul, toReal_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
rw : (a * b⁻¹).toReal = a.toReal / b.toReal
rw₁ : a.toReal * b⁻¹.toReal = a.toReal / b.toReal
⊢ (a / b).toReal = a.toReal / b.toReal
have rw₂ : a.toReal * b.toReal⁻¹ = a.toReal / b.toReal
Tactic: rw [div_eq_mul_inv, toReal_mul, toReal_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Inv (goal)
Goal:
a b : ℝ≥0∞
rw : (a * b⁻¹).toReal = a.toReal / b.toReal
rw₁ : a.toReal * b⁻¹.toReal = a.toReal / b.toReal
rw₂ : a.toReal * b.toReal⁻¹ = a.toReal / b.toReal
⊢ (a / b).toReal = a.toReal / b.toReal
have rw₃ : a.toReal * b.toReal⁻¹ = a.toReal * b.toReal⁻¹
Tactic: rw [div_eq_mul_inv, toReal_mul, toReal_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
⊢ a < a + b
have rwa : ∀ (hb : 0 < b), a < a + b
Tactic: rwa [← pos_iff_ne_zero, ← ENNReal.add_lt_add_iff_left ha, add_zero] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
rwa : ∀ (hb : 0 < b), a < a + b
⊢ a < a + b
have rwa₁ : ∀ (hb : a + 0 < a + b), a < a + b
Tactic: rwa [← pos_iff_ne_zero, ← ENNReal.add_lt_add_iff_left ha, add_zero] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
rwa : ∀ (hb : 0 < b), a < a + b
rwa₁ : ∀ (hb : a + 0 < a + b), a < a + b
⊢ a < a + b
have rwa₂ : ∀ (hb : a < a + b), a < a + b
Tactic: rwa [← pos_iff_ne_zero, ← ENNReal.add_lt_add_iff_left ha, add_zero] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
r₁ r₂ : ℝ≥0∞
h₁ : r₁ ≠ ∞
h₂ : r₂ ≠ ∞
⊢ (r₁ + r₂).toNNReal = r₁.toNNReal + r₂.toNNReal
have lift : ∀ (r₁ : ℝ≥0), ((↑r₁ : ℝ≥0∞) + r₂).toNNReal = (↑r₁ : ℝ≥0∞).toNNReal + r₂.toNNReal
Tactic: lift r₁ to ℝ≥0 using h₁
Cleared hypotheses: r₁, h₁
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
r₂ : ℝ≥0∞
h₂ : r₂ ≠ ∞
r₁ : ℝ≥0
⊢ ((↑r₁ : ℝ≥0∞) + r₂).toNNReal = (↑r₁ : ℝ≥0∞).toNNReal + r₂.toNNReal
have lift : ∀ (r₂ : ℝ≥0), ((↑r₁ : ℝ≥0∞) + (↑r₂ : ℝ≥0∞)).toNNReal = (↑r₁ : ℝ≥0∞).toNNReal + (↑r₂ : ℝ≥0∞).toNNReal
Tactic: lift r₂ to ℝ≥0 using h₂
Cleared hypotheses: r₂, h₂
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
hle : a ≤ b + c
hb : b = ∞ → a = ∞
hc : c = ∞ → a = ∞
⊢ a.toReal ≤ b.toReal + c.toReal
have refine : b + c = ∞ → a = ∞
Tactic: refine le_trans (toReal_mono' hle ?_) toReal_add_le
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
x : ℝ≥0∞
⊢ ¬x < ∞ ↔ x = ∞
have rw : ¬x ≠ ∞ ↔ x = ∞
Tactic: rw [lt_top_iff_ne_top, Classical.not_not]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
x : ℝ≥0∞
rw : ¬x ≠ ∞ ↔ x = ∞
⊢ ¬x < ∞ ↔ x = ∞
have rw₁ : x = ∞ ↔ x = ∞
Tactic: rw [lt_top_iff_ne_top, Classical.not_not]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b : ℝ≥0∞
⊢ a * b < ∞ ↔ a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0
have mp : a * b < ∞ → a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b : ℝ≥0∞
mp : a * b < ∞ → a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0
⊢ a * b < ∞ ↔ a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0
have mpr : a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0 → a * b < ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b : ℝ≥0∞
h : a * b < ∞
⊢ a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0
have mp : ¬b = 0 → ¬a = 0 → a < ∞ ∧ b < ∞
Tactic: rw [← or_assoc, or_iff_not_imp_right, or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a : ℝ≥0∞
⊢ a * a < ∞ ↔ a < ∞
have rw : a = 0 → a < ∞
Tactic: rw [ENNReal.mul_lt_top_iff, and_self, or_self, or_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
⊢ ∞ - a = ∞
have lift : ∀ (a : ℝ≥0), ∞ - (↑a : ℝ≥0∞) = ∞
Tactic: lift a to ℝ≥0 using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
m n : ℕ
⊢ (↑(m - n) : ℝ≥0∞) = HSub.hSub (α := ℝ≥0∞) (↑m : ℝ≥0∞) (↑n : ℝ≥0∞)
have rw : (↑(↑(m - n) : ℝ≥0) : ℝ≥0∞) = HSub.hSub (α := ℝ≥0∞) (↑m : ℝ≥0∞) (↑n : ℝ≥0∞)
Tactic: rw [← coe_natCast, Nat.cast_tsub, coe_sub, coe_natCast, coe_natCast]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
m n : ℕ
rw : (↑(↑(m - n) : ℝ≥0) : ℝ≥0∞) = HSub.hSub (α := ℝ≥0∞) (↑m : ℝ≥0∞) (↑n : ℝ≥0∞)
⊢ (↑(m - n) : ℝ≥0∞) = HSub.hSub (α := ℝ≥0∞) (↑m : ℝ≥0∞) (↑n : ℝ≥0∞)
have rw₁ : (↑(HSub.hSub (α := ℝ≥0) (↑m : ℝ≥0) (↑n : ℝ≥0)) : ℝ≥0∞) = HSub.hSub (α := ℝ≥0∞) (↑m : ℝ≥0∞) (↑n : ℝ≥0∞)
Tactic: rw [← coe_natCast, Nat.cast_tsub, coe_sub, coe_natCast, coe_natCast]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
m n : ℕ
rw : (↑(↑(m - n) : ℝ≥0) : ℝ≥0∞) = HSub.hSub (α := ℝ≥0∞) (↑m : ℝ≥0∞) (↑n : ℝ≥0∞)
rw₁ : (↑(HSub.hSub (α := ℝ≥0) (↑m : ℝ≥0) (↑n : ℝ≥0)) : ℝ≥0∞) = HSub.hSub (α := ℝ≥0∞) (↑m : ℝ≥0∞) (↑n : ℝ≥0∞)
⊢ (↑(m - n) : ℝ≥0∞) = HSub.hSub (α := ℝ≥0∞) (↑m : ℝ≥0∞) (↑n : ℝ≥0∞)
have rw₂ : (↑(↑m : ℝ≥0) : ℝ≥0∞) - (↑(↑n : ℝ≥0) : ℝ≥0∞) = HSub.hSub (α := ℝ≥0∞) (↑m : ℝ≥0∞) (↑n : ℝ≥0∞)
Tactic: rw [← coe_natCast, Nat.cast_tsub, coe_sub, coe_natCast, coe_natCast]