awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ENNReal.Action (goal)
Goal:
R : Type u_1
r : R
s : ℝ≥0
inst : SMul R ℝ≥0
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0 ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
rw : (↑(r • s) : ℝ≥0∞) = HSMul.hSMul (β := ℝ≥0) r 1 • (↑s : ℝ≥0∞)
rw₁ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ≥0∞) • (↑s : ℝ≥0∞)
rw₂ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ≥0∞) * (↑s : ℝ≥0∞)
⊢ (↑(r • s) : ℝ≥0∞) = r • (↑s : ℝ≥0∞)
have rw₃ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1 * s) : ℝ≥0∞)
Tactic: rw [← smul_one_smul ℝ≥0 r (s : ℝ≥0∞), smul_def, smul_eq_mul, ← ENNReal.coe_mul, smul_mul_assoc,
    one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Action (goal)
Goal:
R : Type u_1
r : R
s : ℝ≥0
inst : SMul R ℝ≥0
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0 ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
rw : (↑(r • s) : ℝ≥0∞) = HSMul.hSMul (β := ℝ≥0) r 1 • (↑s : ℝ≥0∞)
rw₁ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ≥0∞) • (↑s : ℝ≥0∞)
rw₂ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ≥0∞) * (↑s : ℝ≥0∞)
rw₃ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1 * s) : ℝ≥0∞)
⊢ (↑(r • s) : ℝ≥0∞) = r • (↑s : ℝ≥0∞)
have rw₄ : (↑(r • s) : ℝ≥0∞) = (↑(r • (1 * s)) : ℝ≥0∞)
Tactic: rw [← smul_one_smul ℝ≥0 r (s : ℝ≥0∞), smul_def, smul_eq_mul, ← ENNReal.coe_mul, smul_mul_assoc,
    one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Action (goal)
Goal:
R : Type u_1
r : R
s : ℝ≥0
inst : SMul R ℝ≥0
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0 ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
rw : (↑(r • s) : ℝ≥0∞) = HSMul.hSMul (β := ℝ≥0) r 1 • (↑s : ℝ≥0∞)
rw₁ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ≥0∞) • (↑s : ℝ≥0∞)
rw₂ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ≥0∞) * (↑s : ℝ≥0∞)
rw₃ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1 * s) : ℝ≥0∞)
rw₄ : (↑(r • s) : ℝ≥0∞) = (↑(r • (1 * s)) : ℝ≥0∞)
⊢ (↑(r • s) : ℝ≥0∞) = r • (↑s : ℝ≥0∞)
have rw₅ : (↑(r • s) : ℝ≥0∞) = (↑(r • s) : ℝ≥0∞)
Tactic: rw [← smul_one_smul ℝ≥0 r (s : ℝ≥0∞), smul_def, smul_eq_mul, ← ENNReal.coe_mul, smul_mul_assoc,
    one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Action (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsDomain R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
inst_5 : DecidableEq R
c : R
⊢ HSMul.hSMul (β := ℝ≥0∞) c ∞ = if c = 0 then 0 else ∞
have rw : Eq (α := ℝ≥0∞) (if HSMul.hSMul (β := ℝ≥0∞) c 1 = 0 then 0 else ∞) (if c = 0 then 0 else ∞)
Tactic: rw [← smul_one_mul, mul_top']
-- Lean 4 proof step from Mathlib.Data.ENNReal.Action (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsDomain R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
inst_5 : DecidableEq R
c : R
⊢ Eq (α := ℝ≥0∞) (if HSMul.hSMul (β := ℝ≥0∞) c 1 = 0 then 0 else ∞) (if c = 0 then 0 else ∞)
have simp_rw : Eq (α := ℝ≥0∞) (if c = 0 ∨ Eq (α := ℝ≥0∞) 1 0 then 0 else ∞) (if c = 0 then 0 else ∞)
Tactic: simp_rw [smul_eq_zero, or_iff_left one_ne_zero]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Action (goal)
Goal:
x : ℝ≥0
y : ℝ≥0∞
hx : x ≠ 0
⊢ x • y < ∞ ↔ y < ∞
have rw : x • y ≠ ∞ ↔ y < ∞
Tactic: rw [lt_top_iff_ne_top, lt_top_iff_ne_top, nnreal_smul_ne_top_iff hx]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Action (goal)
Goal:
x : ℝ≥0
y : ℝ≥0∞
hx : x ≠ 0
rw : x • y ≠ ∞ ↔ y < ∞
⊢ x • y < ∞ ↔ y < ∞
have rw₁ : x • y ≠ ∞ ↔ y ≠ ∞
Tactic: rw [lt_top_iff_ne_top, lt_top_iff_ne_top, nnreal_smul_ne_top_iff hx]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Action (goal)
Goal:
x : ℝ≥0
y : ℝ≥0∞
hx : x ≠ 0
rw : x • y ≠ ∞ ↔ y < ∞
rw₁ : x • y ≠ ∞ ↔ y ≠ ∞
⊢ x • y < ∞ ↔ y < ∞
have rw₂ : y ≠ ∞ ↔ y ≠ ∞
Tactic: rw [lt_top_iff_ne_top, lt_top_iff_ne_top, nnreal_smul_ne_top_iff hx]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Action (goal)
Goal:
r : ℝ≥0
s : ℝ≥0∞
⊢ (r • s).toReal = r • s.toReal
have rw : (↑r : ℝ) * s.toReal = r • s.toReal
Tactic: rw [ENNReal.smul_def, smul_eq_mul, toReal_mul, coe_toReal]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
α : Type u_1
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
a : AddUnits ℝ≥0∞
⊢ (↑a : ℝ≥0∞) ≤ 0
have rw : (↑a : ℝ≥0∞) ≤ (↑a : ℝ≥0∞) + (↑(-a) : ℝ≥0∞)
Tactic: rw [← a.add_neg]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
ι : Type u_2
f : ι → ℝ≥0∞
hf : ∀ (x : ι), f x ≠ ∞
⊢ (fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞)) ∘ ENNReal.toNNReal ∘ f = f
have h : ∀ (x : ι), ((fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞)) ∘ ENNReal.toNNReal ∘ f) x = f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
r : ℝ≥0
⊢ (↑(↑r : ℝ≥0∞).toNNReal : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)
have rw : (↑r : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)
Tactic: rw [toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) = ENNReal.ofReal (↑r : ℝ)
have rw : (↑r : ℝ≥0∞) = (↑(↑r : ℝ).toNNReal : ℝ≥0∞)
Tactic: rw [ENNReal.ofReal, Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
r : ℝ≥0
rw : (↑r : ℝ≥0∞) = (↑(↑r : ℝ).toNNReal : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) = ENNReal.ofReal (↑r : ℝ)
have rw₁ : (↑r : ℝ≥0∞) = (↑r : ℝ≥0∞)
Tactic: rw [ENNReal.ofReal, Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
z : ℝ≥0∞
⊢ z.toReal.toNNReal = z.toNNReal
have a : (↑z.toReal.toNNReal : ℝ) = (↑z.toNNReal : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
x : ℝ≥0∞
⊢ x.toReal = 1 ↔ x = 1
have rw : (↑x.toNNReal : ℝ) = 1 ↔ x = 1
Tactic: rw [ENNReal.toReal, NNReal.coe_eq_one, ENNReal.toNNReal_eq_one_iff]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
x : ℝ≥0∞
rw : (↑x.toNNReal : ℝ) = 1 ↔ x = 1
⊢ x.toReal = 1 ↔ x = 1
have rw₁ : x.toNNReal = 1 ↔ x = 1
Tactic: rw [ENNReal.toReal, NNReal.coe_eq_one, ENNReal.toNNReal_eq_one_iff]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
x : ℝ≥0∞
rw : (↑x.toNNReal : ℝ) = 1 ↔ x = 1
rw₁ : x.toNNReal = 1 ↔ x = 1
⊢ x.toReal = 1 ↔ x = 1
have rw₂ : x = 1 ↔ x = 1
Tactic: rw [ENNReal.toReal, NNReal.coe_eq_one, ENNReal.toNNReal_eq_one_iff]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
a : ℝ≥0∞
h : ENNReal.ofReal a.toReal = a
⊢ a ≠ ∞
have rw : ENNReal.ofReal a.toReal ≠ ∞
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
a : ℝ
h : (ENNReal.ofReal a).toReal = a
⊢ 0 ≤ a
have rw : 0 ≤ (ENNReal.ofReal a).toReal
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℝ≥0∞ → α
⊢ Eq.{u_1 + 1} (α := α) (⨅ (x : ℝ≥0∞), ⨅ (_ : x ≠ ∞), f x) (⨅ (x : ℝ≥0), f (↑x : ℝ≥0∞))
have rw : Eq.{u_1 + 1} (α := α) (⨅ (x : { x : ℝ≥0∞ // x ≠ ∞ }), f (↑x : ℝ≥0∞)) (⨅ (x : ℝ≥0), f (↑x : ℝ≥0∞))
Tactic: rw [iInf_subtype', cinfi_ne_top]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℝ≥0∞ → α
rw : Eq.{u_1 + 1} (α := α) (⨅ (x : { x : ℝ≥0∞ // x ≠ ∞ }), f (↑x : ℝ≥0∞)) (⨅ (x : ℝ≥0), f (↑x : ℝ≥0∞))
⊢ Eq.{u_1 + 1} (α := α) (⨅ (x : ℝ≥0∞), ⨅ (_ : x ≠ ∞), f x) (⨅ (x : ℝ≥0), f (↑x : ℝ≥0∞))
have rw₁ : Eq.{u_1 + 1} (α := α) (⨅ (x : ℝ≥0), f (↑x : ℝ≥0∞)) (⨅ (x : ℝ≥0), f (↑x : ℝ≥0∞))
Tactic: rw [iInf_subtype', cinfi_ne_top]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
n : ℕ
⊢ ENNReal.toNNReal (↑n : ℝ≥0∞) = (↑n : ℝ≥0)
have rw : (↑(↑n : ℝ≥0) : ℝ≥0∞).toNNReal = (↑n : ℝ≥0)
Tactic: rw [← ENNReal.coe_natCast n, ENNReal.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
n : ℕ
rw : (↑(↑n : ℝ≥0) : ℝ≥0∞).toNNReal = (↑n : ℝ≥0)
⊢ ENNReal.toNNReal (↑n : ℝ≥0∞) = (↑n : ℝ≥0)
have rw₁ : Eq (α := ℝ≥0) (↑n : ℝ≥0) (↑n : ℝ≥0)
Tactic: rw [← ENNReal.coe_natCast n, ENNReal.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
n : ℕ
⊢ ENNReal.toReal (↑n : ℝ≥0∞) = (↑n : ℝ)
have rw : (ENNReal.ofReal (↑n : ℝ)).toReal = (↑n : ℝ)
Tactic: rw [← ENNReal.ofReal_natCast n, ENNReal.toReal_ofReal (Nat.cast_nonneg _)]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
n : ℕ
rw : (ENNReal.ofReal (↑n : ℝ)).toReal = (↑n : ℝ)
⊢ ENNReal.toReal (↑n : ℝ≥0∞) = (↑n : ℝ)
have rw₁ : Eq (α := ℝ) (↑n : ℝ) (↑n : ℝ)
Tactic: rw [← ENNReal.ofReal_natCast n, ENNReal.toReal_ofReal (Nat.cast_nonneg _)]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
n : ℕ
⊢ ENNReal.toNNReal (↑n : ℝ≥0∞) = Real.toNNReal (↑n : ℝ)
have rw : ENNReal.toNNReal (↑n : ℝ≥0∞) = NNReal.mk (↑n : ℝ) sorry
Tactic: rw [Real.toNNReal_of_nonneg (by positivity), ENNReal.toNNReal_natCast, mk_natCast]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
n : ℕ
rw : ENNReal.toNNReal (↑n : ℝ≥0∞) = NNReal.mk (↑n : ℝ) ⋯
⊢ ENNReal.toNNReal (↑n : ℝ≥0∞) = Real.toNNReal (↑n : ℝ)
have rw₁ : (↑n : ℝ≥0) = NNReal.mk (↑n : ℝ) sorry
Tactic: rw [Real.toNNReal_of_nonneg (by positivity), ENNReal.toNNReal_natCast, mk_natCast]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
n : ℕ
rw : ENNReal.toNNReal (↑n : ℝ≥0∞) = NNReal.mk (↑n : ℝ) ⋯
rw₁ : (↑n : ℝ≥0) = NNReal.mk (↑n : ℝ) ⋯
⊢ ENNReal.toNNReal (↑n : ℝ≥0∞) = Real.toNNReal (↑n : ℝ)
have rw₂ : Eq (α := ℝ≥0) (↑n : ℝ≥0) (↑n : ℝ≥0)
Tactic: rw [Real.toNNReal_of_nonneg (by positivity), ENNReal.toNNReal_natCast, mk_natCast]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
a : ℝ≥0∞
b : ℝ≥0
h : a ≤ (↑b : ℝ≥0∞)
⊢ a.toReal ≤ (↑b : ℝ)
have lift : ∀ (a : ℝ≥0) (h : (↑a : ℝ≥0∞) ≤ (↑b : ℝ≥0∞)), (↑a : ℝ≥0∞).toReal ≤ (↑b : ℝ)
Tactic: lift a to ℝ≥0 using ne_top_of_le_ne_top coe_ne_top h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
a b : ℝ≥0∞
h : a < b
⊢ ∃ (q : ℚ), 0 ≤ q ∧ a < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b
have rcases : ∀ (p : ℝ≥0),
  (↑p : ℝ≥0∞) < b →
    ∀ (h : (↑p : ℝ≥0∞) < b),
      ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b
Tactic: rcases lt_iff_exists_coe.1 h with ⟨p, rfl, _⟩
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
b : ℝ≥0∞
p : ℝ≥0
right h : (↑p : ℝ≥0∞) < b
⊢ ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b
have rcases : ∀ (c : ℝ≥0∞) (pc : (↑p : ℝ≥0∞) < c) (cb : c < b),
  ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b
Tactic: rcases exists_between h with ⟨c, pc, cb⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
b : ℝ≥0∞
p : ℝ≥0
right h : (↑p : ℝ≥0∞) < b
c : ℝ≥0∞
pc : (↑p : ℝ≥0∞) < c
cb : c < b
⊢ ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b
have rcases : ∀ (r : ℝ≥0),
  (↑r : ℝ≥0∞) < b →
    ∀ (pc : (↑p : ℝ≥0∞) < (↑r : ℝ≥0∞)) (cb : (↑r : ℝ≥0∞) < b),
      ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b
Tactic: rcases lt_iff_exists_coe.1 cb with ⟨r, rfl, _⟩
Cleared hypotheses: c, pc, cb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
b : ℝ≥0∞
p : ℝ≥0
right h : (↑p : ℝ≥0∞) < b
r : ℝ≥0
right_1 : (↑r : ℝ≥0∞) < b
pc : (↑p : ℝ≥0∞) < (↑r : ℝ≥0∞)
cb : (↑r : ℝ≥0∞) < b
⊢ ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b
have rcases : ∀ (q : ℚ) (hq0 : 0 ≤ q) (pq : p < Real.toNNReal (↑q : ℝ)) (qr : Real.toNNReal (↑q : ℝ) < r),
  ∃ (q : ℚ), 0 ≤ q ∧ (↑p : ℝ≥0∞) < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ∧ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < b
Tactic: rcases (NNReal.lt_iff_exists_rat_btwn _ _).1 (coe_lt_coe.1 pc) with ⟨q, hq0, pq, qr⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
a b : ℝ≥0∞
⊢ a < b ↔ ∃ (r : ℝ≥0), 0 < r ∧ a + (↑r : ℝ≥0∞) < b
have refine : ∀ (hab : a < b), ∃ (r : ℝ≥0), 0 < r ∧ a + (↑r : ℝ≥0∞) < b
Tactic: refine ⟨fun hab => ?_, fun ⟨r, _, hr⟩ => lt_of_le_of_lt le_self_add hr⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
a b : ℝ≥0∞
hab : a < b
⊢ ∃ (r : ℝ≥0), 0 < r ∧ a + (↑r : ℝ≥0∞) < b
have rcases : ∀ (c : ℝ≥0) (ac : a < (↑c : ℝ≥0∞)) (cb : (↑c : ℝ≥0∞) < b), ∃ (r : ℝ≥0), 0 < r ∧ a + (↑r : ℝ≥0∞) < b
Tactic: rcases lt_iff_exists_nnreal_btwn.1 hab with ⟨c, ac, cb⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
a b : ℝ≥0∞
hab : a < b
c : ℝ≥0
ac : a < (↑c : ℝ≥0∞)
cb : (↑c : ℝ≥0∞) < b
⊢ ∃ (r : ℝ≥0), 0 < r ∧ a + (↑r : ℝ≥0∞) < b
have lift : ∀ (a : ℝ≥0) (hab : (↑a : ℝ≥0∞) < b) (ac : (↑a : ℝ≥0∞) < (↑c : ℝ≥0∞)), ∃ (r : ℝ≥0), 0 < r ∧ (↑a : ℝ≥0∞) + (↑r : ℝ≥0∞) < b
Tactic: lift a to ℝ≥0 using ac.ne_top
Cleared hypotheses: a, hab, ac
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (hypothesis)
Goal:
b : ℝ≥0∞
c : ℝ≥0
cb : (↑c : ℝ≥0∞) < b
a : ℝ≥0
hab : (↑a : ℝ≥0∞) < b
ac : (↑a : ℝ≥0∞) < (↑c : ℝ≥0∞)
⊢ ∃ (r : ℝ≥0), 0 < r ∧ (↑a : ℝ≥0∞) + (↑r : ℝ≥0∞) < b
have ac₁ : a < c
Tactic: rw [coe_lt_coe] at ac
Cleared hypotheses: ac
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
b : ℝ≥0∞
c : ℝ≥0
cb : (↑c : ℝ≥0∞) < b
a : ℝ≥0
hab : (↑a : ℝ≥0∞) < b
ac : a < c
⊢ ∃ (r : ℝ≥0), 0 < r ∧ (↑a : ℝ≥0∞) + (↑r : ℝ≥0∞) < b
have refine : (↑a : ℝ≥0∞) + (↑(c - a) : ℝ≥0∞) < b
Tactic: refine ⟨c - a, tsub_pos_iff_lt.2 ac, ?_⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
b : ℝ≥0∞
c : ℝ≥0
cb : (↑c : ℝ≥0∞) < b
a : ℝ≥0
hab : (↑a : ℝ≥0∞) < b
ac : a < c
⊢ (↑a : ℝ≥0∞) + (↑(c - a) : ℝ≥0∞) < b
have rwa : (↑(a + (c - a)) : ℝ≥0∞) < b
Tactic: rwa [← coe_add, add_tsub_cancel_of_le ac.le]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
a b : ℝ≥0∞
h : ∀ (ε : ℝ≥0), 0 < ε → b < ∞ → a ≤ b + (↑ε : ℝ≥0∞)
⊢ a ≤ b
have contrapose! : ∀ (h : b < a), ∃ (ε : ℝ≥0), 0 < ε ∧ b < ∞ ∧ b + (↑ε : ℝ≥0∞) < a
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
a b : ℝ≥0∞
h : b < a
⊢ ∃ (ε : ℝ≥0), 0 < ε ∧ b < ∞ ∧ b + (↑ε : ℝ≥0∞) < a
have rcases : ∀ (r : ℝ≥0) (hr0 : 0 < r) (hr : b + (↑r : ℝ≥0∞) < a), ∃ (ε : ℝ≥0), 0 < ε ∧ b < ∞ ∧ b + (↑ε : ℝ≥0∞) < a
Tactic: rcases lt_iff_exists_add_pos_lt.1 h with ⟨r, hr0, hr⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
r : ℝ≥0∞
h : r ≠ ∞
⊢ ∃ (n : ℕ), r < (↑n : ℝ≥0∞)
have lift : ∀ (r : ℝ≥0), ∃ (n : ℕ), (↑r : ℝ≥0∞) < (↑n : ℝ≥0∞)
Tactic: lift r to ℝ≥0 using h
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
r : ℝ≥0
⊢ ∃ (n : ℕ), (↑r : ℝ≥0∞) < (↑n : ℝ≥0∞)
have rcases : ∀ (n : ℕ) (hn : r < (↑n : ℝ≥0)), ∃ (n : ℕ), (↑r : ℝ≥0∞) < (↑n : ℝ≥0∞)
Tactic: rcases exists_nat_gt r with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
⊢ Eq (α := Set ℝ≥0∞) (⋃ (n : ℕ), Iio (↑n : ℝ≥0∞)) {∞}ᶜ
have h : ∀ (x : ℝ≥0∞), Membership.mem (γ := Set ℝ≥0∞) (⋃ (n : ℕ), Iio (↑n : ℝ≥0∞)) x ↔ Membership.mem (γ := Set ℝ≥0∞) {∞}ᶜ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
x : ℝ≥0∞
⊢ Membership.mem (γ := Set ℝ≥0∞) (⋃ (n : ℕ), Iio (↑n : ℝ≥0∞)) x ↔ Membership.mem (γ := Set ℝ≥0∞) {∞}ᶜ x
have h : (∃ (i : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Iio (↑i : ℝ≥0∞)) x) ↔ Membership.mem (γ := Set ℝ≥0∞) {∞}ᶜ x
Tactic: rw [mem_iUnion]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
a b : ℝ≥0∞
h : a = ∞ → b = ∞
h_nnreal : a ≠ ∞ → b ≠ ∞ → a.toNNReal ≤ b.toNNReal
⊢ a ≤ b
have by_contra! : ∀ (hlt : b < a), False
Tactic: by_contra! hlt
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
a b : ℝ≥0∞
h : a = ∞ → b = ∞
h_nnreal : a ≠ ∞ → b ≠ ∞ → a.toNNReal ≤ b.toNNReal
hlt : b < a
⊢ False
have lift : ∀ (b : ℝ≥0) (h : a = ∞ → (↑b : ℝ≥0∞) = ∞) (h_nnreal : a ≠ ∞ → (↑b : ℝ≥0∞) ≠ ∞ → a.toNNReal ≤ (↑b : ℝ≥0∞).toNNReal)
  (hlt : (↑b : ℝ≥0∞) < a), False
Tactic: lift b to ℝ≥0 using hlt.ne_top
Cleared hypotheses: b, h, h_nnreal, hlt
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
a : ℝ≥0∞
b : ℝ≥0
h : a = ∞ → (↑b : ℝ≥0∞) = ∞
h_nnreal : a ≠ ∞ → (↑b : ℝ≥0∞) ≠ ∞ → a.toNNReal ≤ (↑b : ℝ≥0∞).toNNReal
hlt : (↑b : ℝ≥0∞) < a
⊢ False
have lift : ∀ (a : ℝ≥0) (h : (↑a : ℝ≥0∞) = ∞ → (↑b : ℝ≥0∞) = ∞)
  (h_nnreal : (↑a : ℝ≥0∞) ≠ ∞ → (↑b : ℝ≥0∞) ≠ ∞ → (↑a : ℝ≥0∞).toNNReal ≤ (↑b : ℝ≥0∞).toNNReal)
  (hlt : (↑b : ℝ≥0∞) < (↑a : ℝ≥0∞)), False
Tactic: lift a to ℝ≥0 using mt h coe_ne_top
Cleared hypotheses: a, h, h_nnreal, hlt
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
b a : ℝ≥0
h : (↑a : ℝ≥0∞) = ∞ → (↑b : ℝ≥0∞) = ∞
h_nnreal : (↑a : ℝ≥0∞) ≠ ∞ → (↑b : ℝ≥0∞) ≠ ∞ → (↑a : ℝ≥0∞).toNNReal ≤ (↑b : ℝ≥0∞).toNNReal
hlt : (↑b : ℝ≥0∞) < (↑a : ℝ≥0∞)
⊢ False
have refine : (↑a : ℝ≥0∞) ≤ (↑b : ℝ≥0∞)
Tactic: refine hlt.not_ge ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
x : ℝ≥0∞
⊢ |x.toReal| = x.toReal
have top : |ENNReal.toReal ∞| = ENNReal.toReal ∞
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
x : ℝ≥0∞
top : |ENNReal.toReal ∞| = ENNReal.toReal ∞
⊢ |x.toReal| = x.toReal
have coe : ∀ (x : ℝ≥0), |(↑x : ℝ≥0∞).toReal| = (↑x : ℝ≥0∞).toReal
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
t : Set ℝ≥0
h : t.OrdConnected
⊢ (ofNNReal '' t).OrdConnected
have refine : ∀ (x : ℝ≥0) (hx : x ∈ t) (y : ℝ≥0) (hy : y ∈ t) (z : ℝ≥0∞) (hz : z ∈ Icc (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)), z ∈ ofNNReal '' t
Tactic: refine ⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun y hy z hz => ?_⟩
-- Lean 4 proof step from Mathlib.Data.ENNReal.Basic (goal)
Goal:
t : Set ℝ≥0
h : t.OrdConnected
x : ℝ≥0
hx : x ∈ t
y : ℝ≥0
hy : y ∈ t
z : ℝ≥0∞
hz : z ∈ Icc (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)
⊢ z ∈ ofNNReal '' t
have rcases : ∀ (z : ℝ≥0) (hz : (↑z : ℝ≥0∞) ∈ Icc (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)), (↑z : ℝ≥0∞) ∈ ofNNReal '' t
Tactic: rcases ENNReal.le_coe_iff.1 hz.2 with ⟨z, rfl, -⟩
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
α : Type u_2
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ENNReal.ofReal (∏ i ∈ s, f i) = ∏ i ∈ s, ENNReal.ofReal (f i)
have simp_rw : Real.toNNReal (∏ i ∈ s, f i) = ∏ a ∈ s, (f a).toNNReal
Tactic: simp_rw [ENNReal.ofReal, ← coe_finsetProd, coe_inj]
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
⊢ Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ Finset.cons a s ha, f i a) (∑ a ∈ Finset.cons a s ha, ⨅ (i : ι), f i a)
have cons : ⨅ (i : ι), f i a + ∑ a ∈ s, f i a = HAdd.hAdd (α := ℝ≥0∞) (⨅ (i : ι), f i a) (⨅ (i : ι), ∑ a ∈ s, f i a)
Tactic: simp only [Finset.sum_cons, ← ih]
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
⊢ ⨅ (i : ι), f i a + ∑ a ∈ s, f i a = HAdd.hAdd (α := ℝ≥0∞) (⨅ (i : ι), f i a) (⨅ (i : ι), ∑ a ∈ s, f i a)
have cons : ∀ (i j : ι), ∃ (k : ι), f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
Tactic: refine (iInf_add_iInf fun i j => ?_).symm
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
i j : ι
⊢ ∃ (k : ι), f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
have cons : ∀ (k : ι) (hk : ∀ a_1 ∈ Finset.cons a s ha, f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1),
  f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
Tactic: refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (hypothesis)
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
i j k : ι
hk : ∀ a_1 ∈ Finset.cons a s ha, f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1
⊢ f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
have hk₁ : (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ x ∈ s, f k x ≤ f i x ∧ f k x ≤ f j x
Tactic: rw [Finset.forall_mem_cons] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
s : Finset α
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
⊢ Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
have empty : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ ∅, f i a) (∑ a ∈ ∅, ⨅ (i : ι), f i a)
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp only [Finset.sum_empty, ciInf_const]
  | cons a s ha ih =>
    simp only [Finset.sum_cons, ← ih]
    refine (iInf_add_iInf fun i j => ?_).symm
    refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
    rw [Finset.forall_mem_cons] at hk
    exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
s : Finset α
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
empty : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ ∅, f i a) (∑ a ∈ ∅, ⨅ (i : ι), f i a)
⊢ Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
have cons : ∀ (a : α) (s : Finset α) (ha : a ∉ s) (ih : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)),
  Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ Finset.cons a s ha, f i a) (∑ a ∈ Finset.cons a s ha, ⨅ (i : ι), f i a)
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp only [Finset.sum_empty, ciInf_const]
  | cons a s ha ih =>
    simp only [Finset.sum_cons, ← ih]
    refine (iInf_add_iInf fun i j => ?_).symm
    refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
    rw [Finset.forall_mem_cons] at hk
    exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ENNReal.toNNReal (∑ a ∈ s, f a) = ∑ a ∈ s, (f a).toNNReal
have rw : ∀ x ∈ s, f x = (↑(f x).toNNReal : ℝ≥0∞)
Tactic: rw [← coe_inj, coe_toNNReal, coe_finsetSum, sum_congr rfl]
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
rw : ∀ x ∈ s, f x = (↑(f x).toNNReal : ℝ≥0∞)
⊢ ENNReal.toNNReal (∑ a ∈ s, f a) = ∑ a ∈ s, (f a).toNNReal
have rw₁ : Ne (α := ℝ≥0∞) (∑ a ∈ s, f a) ∞
Tactic: rw [← coe_inj, coe_toNNReal, coe_finsetSum, sum_congr rfl]
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ENNReal.toReal (∑ a ∈ s, f a) = ∑ a ∈ s, (f a).toReal
have rw : Eq (α := ℝ) (∑ i ∈ s, (↑(f i).toNNReal : ℝ)) (∑ a ∈ s, (f a).toReal)
Tactic: rw [ENNReal.toReal, toNNReal_sum hf, NNReal.coe_sum]
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i)
have simp_rw : Real.toNNReal (∑ i ∈ s, f i) = ∑ a ∈ s, (f a).toNNReal
Tactic: simp_rw [ENNReal.ofReal, ← coe_finsetSum, coe_inj]
-- Lean 4 proof step from Mathlib.Data.ENNReal.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
f g : α → ℝ≥0∞
a : α
s_1 : Finset α
h : a ∉ s_1
hs : s_1.Nonempty
ih : ∀ (Hlt : ∀ i ∈ s_1, f i < g i), LT.lt (α := ℝ≥0∞) (∑ i ∈ s_1, f i) (∑ i ∈ s_1, g i)
Hlt : ∀ i ∈ cons a s_1 h, f i < g i
⊢ LT.lt (α := ℝ≥0∞) (∑ i ∈ cons a s_1 h, f i) (∑ i ∈ cons a s_1 h, g i)
have cons : ∀ (Hlt : f a < g a ∧ ∀ x ∈ s_1, f x < g x), f a + ∑ i ∈ s_1, f i < g a + ∑ i ∈ s_1, g i
Tactic: simp only [Finset.sum_cons, forall_mem_cons] at Hlt ⊢
Cleared hypotheses: Hlt