awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞)
rw₂ : (↑(↑m : ℝ≥0) : ℝ≥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∞) - (↑(↑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∞)
rw₂ : (↑(↑m : ℝ≥0) : ℝ≥0∞) - (↑(↑n : ℝ≥0) : ℝ≥0∞) = HSub.hSub (α := ℝ≥0∞) (↑m : ℝ≥0∞) (↑n : ℝ≥0∞)
rw₃ : (↑m : ℝ≥0∞) - (↑(↑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∞) = 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:
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
⊢ a - b + c = a + c - b
have pos : ∀ (c_top : c = ∞), a - b + c = a + c - b
Tactic: by_cases c_top : c = ∞
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
pos : ∀ (c_top : c = ∞), a - b + c = a + c - b
⊢ a - b + c = a + c - b
have neg : ∀ (c_top : ¬c = ∞), a - b + c = a + c - b
Tactic: by_cases c_top : c = ∞
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
c_top : ¬c = ∞
⊢ a - b + c = a + c - b
have neg : a - b + c + b = a + c
Tactic: refine ENNReal.eq_sub_of_add_eq b_ne_top ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
c_top : ¬c = ∞
⊢ a - b + c + b = a + c
have neg : a - b + (b + c) = a + c
Tactic: simp only [add_assoc, add_comm c b]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
hc : c ≠ ∞
⊢ a + c - (b + c) = a - b
have lift : ∀ (c : ℝ≥0), a + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = a - b
Tactic: lift c to ℝ≥0 using hc
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b : ℝ≥0∞
c : ℝ≥0
⊢ a + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = a - b
have top : ∞ + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = ∞ - b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b : ℝ≥0∞
c : ℝ≥0
top : ∞ + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = ∞ - b
⊢ a + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = a - b
have coe : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞) + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = (↑x : ℝ≥0∞) - b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
b : ℝ≥0∞
c : ℝ≥0
⊢ ∞ + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = ∞ - b
have top : ∞ + (↑c : ℝ≥0∞) - (∞ + (↑c : ℝ≥0∞)) = HSub.hSub (α := ℝ≥0∞) ∞ ∞
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
b : ℝ≥0∞
c : ℝ≥0
top : ∞ + (↑c : ℝ≥0∞) - (∞ + (↑c : ℝ≥0∞)) = HSub.hSub (α := ℝ≥0∞) ∞ ∞
⊢ ∞ + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = ∞ - b
have top₁ : ∀ (x : ℝ≥0), ∞ + (↑c : ℝ≥0∞) - ((↑x : ℝ≥0∞) + (↑c : ℝ≥0∞)) = ∞ - (↑x : ℝ≥0∞)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
b : ℝ≥0∞
c x : ℝ≥0
⊢ (↑x : ℝ≥0∞) + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = (↑x : ℝ≥0∞) - b
have coe : (↑x : ℝ≥0∞) + (↑c : ℝ≥0∞) - (∞ + (↑c : ℝ≥0∞)) = (↑x : ℝ≥0∞) - ∞
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
b : ℝ≥0∞
c x : ℝ≥0
coe : (↑x : ℝ≥0∞) + (↑c : ℝ≥0∞) - (∞ + (↑c : ℝ≥0∞)) = (↑x : ℝ≥0∞) - ∞
⊢ (↑x : ℝ≥0∞) + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = (↑x : ℝ≥0∞) - b
have coe₁ : ∀ (x_1 : ℝ≥0), (↑x : ℝ≥0∞) + (↑c : ℝ≥0∞) - ((↑x_1 : ℝ≥0∞) + (↑c : ℝ≥0∞)) = (↑x : ℝ≥0∞) - (↑x_1 : ℝ≥0∞)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
c x x_1 : ℝ≥0
⊢ (↑x : ℝ≥0∞) + (↑c : ℝ≥0∞) - ((↑x_1 : ℝ≥0∞) + (↑c : ℝ≥0∞)) = (↑x : ℝ≥0∞) - (↑x_1 : ℝ≥0∞)
have coe : x + c - (x_1 + c) = x - x_1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
c x x_1 : ℝ≥0
⊢ x + c - (x_1 + c) = x - x_1
have coe : x - x_1 = x - x_1
Tactic: rw [add_tsub_add_eq_tsub_right]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
hc : c ≠ ∞
⊢ c + a - (c + b) = a - b
have simp_rw : a + c - (b + c) = a - b
Tactic: simp_rw [add_comm c]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
h : a ≠ ∞ ∨ b ≠ ∞
⊢ a - b < c → a < b + c
have inl : ∀ (h : a ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ ∞), a - ∞ < c → a < ∞ + c
Tactic: obtain rfl | hb := eq_or_ne b ∞
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
h : a ≠ ∞ ∨ b ≠ ∞
inl : ∀ (h : a ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ ∞), a - ∞ < c → a < ∞ + c
⊢ a - b < c → a < b + c
have inr : ∀ (hb : b ≠ ∞), a - b < c → a < b + c
Tactic: obtain rfl | hb := eq_or_ne b ∞
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a c : ℝ≥0∞
h : a ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ ∞
⊢ a - ∞ < c → a < ∞ + c
have inl : a - ∞ < c → a ≠ ∞
Tactic: rw [top_add, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
⊢ (a - b) * c = a * c - b * c
have inl : ∀ (hab : a ≤ b), (a - b) * c = a * c - b * c
Tactic: rcases le_or_gt a b with hab | hab
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
inl : ∀ (hab : a ≤ b), (a - b) * c = a * c - b * c
⊢ (a - b) * c = a * c - b * c
have inr : ∀ (hab : b < a), (a - b) * c = a * c - b * c
Tactic: rcases le_or_gt a b with hab | hab
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : b < a
⊢ (a - b) * c = a * c - b * c
have inr : ∀ (h : LT.lt (α := ℝ≥0∞) 0 0 → 0 < a → c ≠ ∞) (hab : 0 < a), (a - 0) * c = a * c - 0 * c
Tactic: rcases eq_zero_or_pos b with (rfl | hb)
Cleared hypotheses: b, h, hab
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : b < a
inr : ∀ (h : LT.lt (α := ℝ≥0∞) 0 0 → 0 < a → c ≠ ∞) (hab : 0 < a), (a - 0) * c = a * c - 0 * c
⊢ (a - b) * c = a * c - b * c
have inr₁ : ∀ (hb : 0 < b), (a - b) * c = a * c - b * c
Tactic: rcases eq_zero_or_pos b with (rfl | hb)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
h : 0 < c → c < b → a ≠ ∞
⊢ a * (b - c) = a * b - a * c
have simp : (b - c) * a = b * a - c * a
Tactic: simp only [mul_comm a]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b : ℝ≥0∞
hb : b ≠ ∞
⊢ a.toReal - b.toReal ≤ (a - b).toReal
have lift : ∀ (b : ℝ≥0), a.toReal - (↑b : ℝ≥0∞).toReal ≤ (a - (↑b : ℝ≥0∞)).toReal
Tactic: lift b to ℝ≥0 using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a : ℝ≥0∞
b : ℝ≥0
⊢ a.toReal - (↑b : ℝ≥0∞).toReal ≤ (a - (↑b : ℝ≥0∞)).toReal
have top : ENNReal.toReal ∞ - (↑b : ℝ≥0∞).toReal ≤ (∞ - (↑b : ℝ≥0∞)).toReal
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a : ℝ≥0∞
b : ℝ≥0
top : ENNReal.toReal ∞ - (↑b : ℝ≥0∞).toReal ≤ (∞ - (↑b : ℝ≥0∞)).toReal
⊢ a.toReal - (↑b : ℝ≥0∞).toReal ≤ (a - (↑b : ℝ≥0∞)).toReal
have coe : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞).toReal - (↑b : ℝ≥0∞).toReal ≤ ((↑x : ℝ≥0∞) - (↑b : ℝ≥0∞)).toReal
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
b x : ℝ≥0
⊢ (↑x : ℝ≥0∞).toReal - (↑b : ℝ≥0∞).toReal ≤ ((↑x : ℝ≥0∞) - (↑b : ℝ≥0∞)).toReal
have coe : (↑x : ℝ) - (↑b : ℝ) ≤ max ((↑x : ℝ) - (↑b : ℝ)) 0
Tactic: simp only [← coe_sub, NNReal.sub_def, Real.coe_toNNReal', coe_toReal]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b : ℝ≥0∞
hb : b ≠ ∞
⊢ (a - b).toNNReal = a.toNNReal - b.toNNReal
have lift : ∀ (b : ℝ≥0), (a - (↑b : ℝ≥0∞)).toNNReal = a.toNNReal - (↑b : ℝ≥0∞).toNNReal
Tactic: lift b to ℝ≥0 using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a : ℝ≥0∞
b : ℝ≥0
⊢ (a - (↑b : ℝ≥0∞)).toNNReal = a.toNNReal - (↑b : ℝ≥0∞).toNNReal
have top : (∞ - (↑b : ℝ≥0∞)).toNNReal = ENNReal.toNNReal ∞ - (↑b : ℝ≥0∞).toNNReal
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a : ℝ≥0∞
b : ℝ≥0
top : (∞ - (↑b : ℝ≥0∞)).toNNReal = ENNReal.toNNReal ∞ - (↑b : ℝ≥0∞).toNNReal
⊢ (a - (↑b : ℝ≥0∞)).toNNReal = a.toNNReal - (↑b : ℝ≥0∞).toNNReal
have coe : ∀ (x : ℝ≥0), ((↑x : ℝ≥0∞) - (↑b : ℝ≥0∞)).toNNReal = (↑x : ℝ≥0∞).toNNReal - (↑b : ℝ≥0∞).toNNReal
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
p q : ℝ
hq : 0 ≤ q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
have inl : ∀ (h : p ≤ q), ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
Tactic: obtain h | h := le_total p q
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
p q : ℝ
hq : 0 ≤ q
inl : ∀ (h : p ≤ q), ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
have inr : ∀ (h : q ≤ p), ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
Tactic: obtain h | h := le_total p q
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
p q : ℝ
hq : 0 ≤ q
h : p ≤ q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
have inl : 0 = ENNReal.ofReal p - ENNReal.ofReal q
Tactic: rw [ofReal_of_nonpos (sub_nonpos_of_le h), tsub_eq_zero_of_le (ofReal_le_ofReal h)]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
p q : ℝ
hq : 0 ≤ q
h : p ≤ q
inl : 0 = ENNReal.ofReal p - ENNReal.ofReal q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
have inl₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [ofReal_of_nonpos (sub_nonpos_of_le h), tsub_eq_zero_of_le (ofReal_le_ofReal h)]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
have inr : ENNReal.ofReal (p - q) + ENNReal.ofReal q = ENNReal.ofReal p
Tactic: refine ENNReal.eq_sub_of_add_eq ofReal_ne_top ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal (p - q) + ENNReal.ofReal q = ENNReal.ofReal p
have inr : ENNReal.ofReal (p - q + q) = ENNReal.ofReal p
Tactic: rw [← ofReal_add (sub_nonneg_of_le h) hq, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
inr : ENNReal.ofReal (p - q + q) = ENNReal.ofReal p
⊢ ENNReal.ofReal (p - q) + ENNReal.ofReal q = ENNReal.ofReal p
have inr₁ : ENNReal.ofReal p = ENNReal.ofReal p
Tactic: rw [← ofReal_add (sub_nonneg_of_le h) hq, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (hypothesis)
Goal:
a b c : ℝ≥0∞
ha : a ≠ ∞
h : b ≤ a
⊢ a - c - (a - b) = b - c
have hb : b ≠ ∞
Tactic: have hb : b ≠ ∞ := ne_top_of_le_ne_top ha h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b c : ℝ≥0∞
ha : a ≠ ∞
h : b ≤ a
hb : b ≠ ∞
⊢ a - c - (a - b) = b - c
have lift : ∀ (a : ℝ≥0) (h : b ≤ (↑a : ℝ≥0∞)), (↑a : ℝ≥0∞) - c - ((↑a : ℝ≥0∞) - b) = b - c
Tactic: lift a to ℝ≥0 using ha
Cleared hypotheses: a, ha, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
b c : ℝ≥0∞
hb : b ≠ ∞
a : ℝ≥0
h : b ≤ (↑a : ℝ≥0∞)
⊢ (↑a : ℝ≥0∞) - c - ((↑a : ℝ≥0∞) - b) = b - c
have lift : ∀ (b : ℝ≥0) (h : (↑b : ℝ≥0∞) ≤ (↑a : ℝ≥0∞)), (↑a : ℝ≥0∞) - c - ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)) = (↑b : ℝ≥0∞) - c
Tactic: lift b to ℝ≥0 using hb
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
c : ℝ≥0∞
a b : ℝ≥0
h : (↑b : ℝ≥0∞) ≤ (↑a : ℝ≥0∞)
⊢ (↑a : ℝ≥0∞) - c - ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)) = (↑b : ℝ≥0∞) - c
have top : (↑a : ℝ≥0∞) - ∞ - ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)) = (↑b : ℝ≥0∞) - ∞
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
c : ℝ≥0∞
a b : ℝ≥0
h : (↑b : ℝ≥0∞) ≤ (↑a : ℝ≥0∞)
top : (↑a : ℝ≥0∞) - ∞ - ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)) = (↑b : ℝ≥0∞) - ∞
⊢ (↑a : ℝ≥0∞) - c - ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)) = (↑b : ℝ≥0∞) - c
have coe : ∀ (x : ℝ≥0), (↑a : ℝ≥0∞) - (↑x : ℝ≥0∞) - ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)) = (↑b : ℝ≥0∞) - (↑x : ℝ≥0∞)
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b : ℝ≥0
h : (↑b : ℝ≥0∞) ≤ (↑a : ℝ≥0∞)
x : ℝ≥0
⊢ (↑a : ℝ≥0∞) - (↑x : ℝ≥0∞) - ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)) = (↑b : ℝ≥0∞) - (↑x : ℝ≥0∞)
have coe : a - x - (a - b) = b - x
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a b : ℝ≥0
h : (↑b : ℝ≥0∞) ≤ (↑a : ℝ≥0∞)
x : ℝ≥0
⊢ a - x - (a - b) = b - x
have coe : b ≤ a
Tactic: rw [tsub_tsub_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ (iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal
have inl : IsEmpty ι → (iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
inl : IsEmpty ι → (iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal
⊢ (iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal
have inr : Nonempty ι → (iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h : IsEmpty ι
⊢ (iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal
have inl : ENNReal.toNNReal ∞ = ⨅ (i : ι), (f i).toNNReal
Tactic: rw [iInf_of_empty, toNNReal_top, NNReal.iInf_empty]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h : IsEmpty ι
inl : ENNReal.toNNReal ∞ = ⨅ (i : ι), (f i).toNNReal
⊢ (iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal
have inl₁ : Eq (α := ℝ≥0) 0 (⨅ (i : ι), (f i).toNNReal)
Tactic: rw [iInf_of_empty, toNNReal_top, NNReal.iInf_empty]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h : IsEmpty ι
inl : ENNReal.toNNReal ∞ = ⨅ (i : ι), (f i).toNNReal
inl₁ : Eq (α := ℝ≥0) 0 (⨅ (i : ι), (f i).toNNReal)
⊢ (iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal
have inl₂ : Eq (α := ℝ≥0) 0 0
Tactic: rw [iInf_of_empty, toNNReal_top, NNReal.iInf_empty]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h : Nonempty ι
⊢ (iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal
have inr : ∀ (f : (i : ι) → ℝ≥0),
  ENNReal.toNNReal (⨅ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨅ (i : ι), ENNReal.toNNReal ((fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) i)
Tactic: lift f to ι → ℝ≥0 using hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
h : Nonempty ι
f : (i : ι) → ℝ≥0
inr inr₁ : ENNReal.toNNReal (⨅ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨅ (i : ι), (↑(f i) : ℝ≥0∞).toNNReal
⊢ ENNReal.toNNReal (⨅ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨅ (i : ι), ENNReal.toNNReal ((fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) i)
have inr₂ : (↑(iInf f) : ℝ≥0∞).toNNReal = ⨅ (i : ι), (↑(f i) : ℝ≥0∞).toNNReal
Tactic: simp_rw [← coe_iInf, toNNReal_coe]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (hypothesis)
Goal:
s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ∞
⊢ (sInf s).toNNReal = sInf (ENNReal.toNNReal '' s)
have hf : ∀ (i : { x : ℝ≥0∞ // x ∈ s }), (↑i : ℝ≥0∞) ≠ ∞
Tactic: have hf : ∀ i, ((↑) : s → ℝ≥0∞) i ≠ ∞ := fun ⟨r, rs⟩ => hs r rs
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
⊢ ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)
have inl : ∀ (i : ι) (hi : f i ≤ 0), ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)
Tactic: obtain ⟨i, hi⟩ | h := em (∃ i, f i ≤ 0)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
inl : ∀ (i : ι) (hi : f i ≤ 0), ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)
⊢ ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)
have inr : ∀ (h : ¬∃ (i : ι), f i ≤ 0), ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)
Tactic: obtain ⟨i, hi⟩ | h := em (∃ i, f i ≤ 0)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
i : ι
hi : f i ≤ 0
⊢ ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)
have inl : ENNReal.ofReal (⨅ (i : ι), f i) = ⊥
Tactic: rw [iInf_eq_bot.2 fun _ _ ↦ ⟨i, by simpa [ofReal_of_nonpos hi]⟩]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (hypothesis)
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ¬∃ (i : ι), f i ≤ 0
⊢ ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)
have h₁ : ∀ (i : ι), 0 ≤ f i
Tactic: replace h i : 0 ≤ f i := le_of_not_ge fun hi ↦ h ⟨i, hi⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
⊢ ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)
have inr : ∀ (a : ℝ≥0∞), a ≤ ENNReal.ofReal (⨅ (i : ι), f i) ↔ a ≤ ⨅ (i : ι), ENNReal.ofReal (f i)
Tactic: refine eq_of_forall_le_iff fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
⊢ a ≤ ENNReal.ofReal (⨅ (i : ι), f i) ↔ a ≤ ⨅ (i : ι), ENNReal.ofReal (f i)
have inr : ∞ ≤ ENNReal.ofReal (⨅ (i : ι), f i) ↔ LE.le (α := ℝ≥0∞) ∞ (⨅ (i : ι), ENNReal.ofReal (f i))
Tactic: obtain rfl | ha := eq_or_ne a ∞
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
inr : ∞ ≤ ENNReal.ofReal (⨅ (i : ι), f i) ↔ LE.le (α := ℝ≥0∞) ∞ (⨅ (i : ι), ENNReal.ofReal (f i))
⊢ a ≤ ENNReal.ofReal (⨅ (i : ι), f i) ↔ a ≤ ⨅ (i : ι), ENNReal.ofReal (f i)
have inr₁ : ∀ (ha : a ≠ ∞), a ≤ ENNReal.ofReal (⨅ (i : ι), f i) ↔ a ≤ ⨅ (i : ι), ENNReal.ofReal (f i)
Tactic: obtain rfl | ha := eq_or_ne a ∞
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ a ≤ ENNReal.ofReal (⨅ (i : ι), f i) ↔ a ≤ ⨅ (i : ι), ENNReal.ofReal (f i)
have inr : (∀ (i : ι), a.toReal ≤ f i) ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)
Tactic: rw [le_iInf_iff, le_ofReal_iff_toReal_le ha, le_ciInf_iff ⟨0, by simpa [mem_lowerBounds]⟩]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
inr : (∀ (i : ι), a.toReal ≤ f i) ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)
⊢ a ≤ ENNReal.ofReal (⨅ (i : ι), f i) ↔ a ≤ ⨅ (i : ι), ENNReal.ofReal (f i)
have inr₁ : LE.le (α := ℝ) 0 (⨅ (i : ι), f i)
Tactic: rw [le_iInf_iff, le_ofReal_iff_toReal_le ha, le_ciInf_iff ⟨0, by simpa [mem_lowerBounds]⟩]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ a - ⨅ (i : ι), f i = ⨆ (i : ι), a - f i
have refine : ∀ (c : ℝ≥0∞), a - ⨅ (i : ι), f i ≤ c ↔ ⨆ (i : ι), a - f i ≤ c
Tactic: refine eq_of_forall_ge_iff fun c => ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a c : ℝ≥0∞
⊢ a - ⨅ (i : ι), f i ≤ c ↔ ⨆ (i : ι), a - f i ≤ c
have rw : a ≤ ⨅ (i : ι), f i + c ↔ ⨆ (i : ι), a - f i ≤ c
Tactic: rw [tsub_le_iff_right, add_comm, iInf_add]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ a + iInf f = ⨅ (b : ι), a + f b
have rw : Eq (α := ℝ≥0∞) (⨅ (i : ι), f i + a) (⨅ (b : ι), a + f b)
Tactic: rw [add_comm, iInf_add]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f k + g k ≤ f i + g j
⊢ ⨅ (a : ι), ⨅ (a' : ι), f a + g a' = iInf f + iInf g
have simp_rw : Eq (α := ℝ≥0∞) (⨅ (a : ι), ⨅ (a' : ι), f a + g a') (⨅ (i : ι), f i + iInf g)
Tactic: simp_rw [iInf_add, add_iInf]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Type u_2
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ f _k + g _k ≤ f i + g j
have h₁ : f _k ≤ f i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Type u_2
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
h₁ : f _k ≤ f i
⊢ f _k + g _k ≤ f i + g j
have h₂ : g _k ≤ g j
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a : ℝ≥0∞
s : Set ℝ≥0∞
⊢ a + sInf s = ⨅ b ∈ s, a + b
have rw : a + ⨅ a ∈ s, a = ⨅ b ∈ s, a + b
Tactic: rw [sInf_eq_iInf, add_iInf₂]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a : ℝ≥0∞
s : Set ℝ≥0∞
rw : a + ⨅ a ∈ s, a = ⨅ b ∈ s, a + b
⊢ a + sInf s = ⨅ b ∈ s, a + b
have rw₁ : Eq (α := ℝ≥0∞) (⨅ i ∈ s, a + i) (⨅ b ∈ s, a + b)
Tactic: rw [sInf_eq_iInf, add_iInf₂]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
κ : Sort u_2
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ iInf f + iInf g
have simp_rw : a ≤ ⨅ (i : ι), ⨅ (b : κ), f i + g b
Tactic: simp_rw [iInf_add, add_iInf]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
a : ℝ≥0∞
κ : Sort u_2
q₁ : ι → Sort u_3
q₂ : κ → Sort u_4
f : (i : ι) → q₁ i → ℝ≥0∞
g : (k : κ) → q₂ k → ℝ≥0∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ HAdd.hAdd (α := ℝ≥0∞) (⨅ (i : ι), ⨅ (qi : q₁ i), f i qi) (⨅ (k : κ), ⨅ (qk : q₂ k), g k qk)
have simp_rw : a ≤ ⨅ (i : ι), ⨅ (j : q₁ i), ⨅ (i_1 : κ), ⨅ (j_1 : q₂ i_1), f i j + g i_1 j_1
Tactic: simp_rw [iInf₂_add, add_iInf₂]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a : ℝ≥0∞
⊢ ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b = a
have refine : ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b ≤ a
Tactic: refine le_antisymm ?_ (le_iInf₂ fun b hb ↦ hb.le)
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a : ℝ≥0∞
⊢ ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b ≤ a
have refine : ∀ (c : ℝ≥0∞) (hac : a < c), ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b < c
Tactic: refine le_of_forall_gt fun c hac ↦ ?_
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
a c : ℝ≥0∞
hac : a < c
⊢ ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b < c
have obtain : ∀ (d : ℝ≥0∞) (had : a < d) (hdc : d < c), ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b < c
Tactic: obtain ⟨d, had, hdc⟩ := exists_between hac
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
x y z : ℝ≥0∞
h : y + z < x
⊢ ∃ y' > y, ∃ z' > z, y' + z' < x
have contrapose! : ∀ (h : ∀ (y' : ℝ≥0∞) (_ : y' > y) (z' : ℝ≥0∞) (_ : z' > z), x ≤ y' + z'), x ≤ y + z
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ (iSup f).toNNReal = ⨆ (i : ι), (f i).toNNReal
have lift : ∀ (f : (i : ι) → ℝ≥0),
  ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), ENNReal.toNNReal ((fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) i)
Tactic: lift f to ι → ℝ≥0 using hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Data.ENNReal.Operations (goal)
Goal:
ι : Sort u_1
f : (i : ι) → ℝ≥0
⊢ ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), ENNReal.toNNReal ((fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) i)
have simp_rw : ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i
Tactic: simp_rw [toNNReal_coe]