awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h0 : c ≠ 0
hinf : c ≠ ∞
⊢ a * c < b * c ↔ a < b

Tactic:
(mul_left_strictMono h0 hinf).lt_iff_lt

Premises used: StrictMono.lt_iff_lt, ENNReal.mul_left_strictMono
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * b = a ↔ b = 1

Tactic:
simpa using ENNReal.mul_right_inj ha₀ ha (c := 1)

Premises used: ENNReal.mul_right_inj
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb : b ≠ ∞
⊢ a * b = b ↔ a = 1

Tactic:
simpa using ENNReal.mul_left_inj hb₀ hb (b := 1)

Premises used: ENNReal.mul_left_inj
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
⊢ 0 < a → ∀ (n : ℕ), 0 < a ^ n

Tactic:
CanonicallyOrderedAdd.pow_pos

Premises used: CanonicallyOrderedAdd.pow_pos
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
⊢ a ≠ 0 → ∀ (n : ℕ), a ^ n ≠ 0

Tactic:
simpa only [pos_iff_ne_zero] using ENNReal.pow_pos

Premises used: ENNReal.pow_pos, pos_iff_ne_zero
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
⊢ ¬a < 0

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
⊢ a ≠ ∞ → a + b ≤ a + c → b ≤ c

Tactic:
WithTop.le_of_add_le_add_left

Premises used: WithTop.le_of_add_le_add_left, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
⊢ a ≠ ∞ → b + a ≤ c + a → b ≤ c

Tactic:
WithTop.le_of_add_le_add_right

Premises used: WithTop.le_of_add_le_add_right, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
⊢ a ≠ ∞ → b < c → a + b < a + c

Tactic:
WithTop.add_lt_add_left

Premises used: ENNReal, WithTop.add_lt_add_left
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
⊢ a ≠ ∞ → b < c → b + a < c + a

Tactic:
WithTop.add_lt_add_right

Premises used: WithTop.add_lt_add_right, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
⊢ a ≠ ∞ → (a + b ≤ a + c ↔ b ≤ c)

Tactic:
WithTop.add_le_add_iff_left

Premises used: ENNReal, WithTop.add_le_add_iff_left
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
⊢ a ≠ ∞ → (b + a ≤ c + a ↔ b ≤ c)

Tactic:
WithTop.add_le_add_iff_right

Premises used: ENNReal, WithTop.add_le_add_iff_right
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
⊢ a ≠ ∞ → (a + b < a + c ↔ b < c)

Tactic:
WithTop.add_lt_add_iff_left

Premises used: ENNReal, WithTop.add_lt_add_iff_left
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
⊢ a ≠ ∞ → (b + a < c + a ↔ b < c)

Tactic:
WithTop.add_lt_add_iff_right

Premises used: WithTop.add_lt_add_iff_right, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c d : ℝ≥0∞
⊢ a ≠ ∞ → a ≤ b → c < d → a + c < b + d

Tactic:
WithTop.add_lt_add_of_le_of_lt

Premises used: ENNReal, WithTop.add_lt_add_of_le_of_lt
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c d : ℝ≥0∞
⊢ c ≠ ∞ → a < b → c ≤ d → a + c < b + d

Tactic:
WithTop.add_lt_add_of_lt_of_le

Premises used: WithTop.add_lt_add_of_lt_of_le, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ AddLeftReflectLT ℝ≥0∞

Tactic:
WithTop.addLeftReflectLT

Premises used: WithTop.addLeftReflectLT, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
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
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hb : a < a + b), a < a + b
⊢ a < a + b

Tactic:
rwa [← pos_iff_ne_zero, ← ENNReal.add_lt_add_iff_left ha, add_zero] at hb

Premises used: ENNReal.add_lt_add_iff_left, add_zero, pos_iff_ne_zero
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
⊢ a + b = ∞ ↔ a = ∞ ∨ b = ∞

Tactic:
WithTop.add_eq_top

Premises used: WithTop.add_eq_top, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
⊢ a + b < ∞ ↔ a < ∞ ∧ b < ∞

Tactic:
WithTop.add_lt_top

Premises used: WithTop.add_lt_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
r₁ r₂ : ℝ≥0∞
h₁ : r₁ ≠ ∞
h₂ : r₂ ≠ ∞
⊢ r₁ ≠ ∞

Tactic:
h₁
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
r₁ r₂ : ℝ≥0∞
h₁ : r₁ ≠ ∞
h₂ : r₂ ≠ ∞
lift : ∀ (r₁ : ℝ≥0), ((↑r₁ : ℝ≥0∞) + r₂).toNNReal = (↑r₁ : ℝ≥0∞).toNNReal + r₂.toNNReal
⊢ (r₁ + r₂).toNNReal = r₁.toNNReal + r₂.toNNReal

Tactic:
lift r₁ to ℝ≥0 using h₁
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
r₂ : ℝ≥0∞
h₂ : r₂ ≠ ∞
r₁ : ℝ≥0
⊢ r₂ ≠ ∞

Tactic:
h₂
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
r₂ : ℝ≥0∞
h₂ : r₂ ≠ ∞
r₁ : ℝ≥0
lift : ∀ (r₂ : ℝ≥0), ((↑r₁ : ℝ≥0∞) + (↑r₂ : ℝ≥0∞)).toNNReal = (↑r₁ : ℝ≥0∞).toNNReal + (↑r₂ : ℝ≥0∞).toNNReal
⊢ ((↑r₁ : ℝ≥0∞) + r₂).toNNReal = (↑r₁ : ℝ≥0∞).toNNReal + r₂.toNNReal

Tactic:
lift r₂ to ℝ≥0 using h₂
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
r₁ r₂ : ℝ≥0
⊢ ((↑r₁ : ℝ≥0∞) + (↑r₂ : ℝ≥0∞)).toNNReal = (↑r₁ : ℝ≥0∞).toNNReal + (↑r₂ : ℝ≥0∞).toNNReal

Tactic:
rfl
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hle : a ≤ b + c
hb : b = ∞ → a = ∞
hc : c = ∞ → a = ∞
⊢ a.toReal ≤ b.toReal + c.toReal

Tactic:
le_trans (toReal_mono' hle ?_) toReal_add_le

Premises used: ENNReal.toReal_mono', ENNReal.toReal_add_le, le_trans
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hle : a ≤ b + c
hb : b = ∞ → a = ∞
hc : c = ∞ → a = ∞
refine : b + c = ∞ → a = ∞
⊢ a.toReal ≤ b.toReal + c.toReal

Tactic:
refine le_trans (toReal_mono' hle ?_) toReal_add_le

Premises used: ENNReal.toReal_mono', ENNReal.toReal_add_le, le_trans
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hle : a ≤ b + c
hb : b = ∞ → a = ∞
hc : c = ∞ → a = ∞
⊢ b + c = ∞ → a = ∞

Tactic:
simpa only [add_eq_top, or_imp] using And.intro hb hc

Premises used: ENNReal.add_eq_top, or_imp, And.intro
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hle : a ≤ b + c
hb : b ≠ ∞
hc : c ≠ ∞
⊢ a.toReal ≤ b.toReal + c.toReal

Tactic:
toReal_le_add' hle (flip absurd hb) (flip absurd hc)

Premises used: flip, absurd, ENNReal.toReal_le_add'
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x : ℝ≥0∞
rw : ¬x ≠ ∞ ↔ x = ∞
rw₁ rw₂ : x = ∞ ↔ x = ∞
⊢ ¬x < ∞ ↔ x = ∞

Tactic:
rw [lt_top_iff_ne_top, Classical.not_not]

Premises used: Classical.not_not, lt_top_iff_ne_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
⊢ a + b ≠ ∞ ↔ a ≠ ∞ ∧ b ≠ ∞

Tactic:
simpa only [lt_top_iff_ne_top] using add_lt_top

Premises used: lt_top_iff_ne_top, ENNReal.add_lt_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
⊢ a + b ≠ ∞

Tactic:
ENNReal.add_ne_top.2 ⟨ha, hb⟩

Premises used: Iff.mpr, And.intro, ENNReal.add_ne_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
⊢ a * ⊤ = if a = 0 then 0 else ⊤

Tactic:
WithTop.mul_top' a

Premises used: WithTop.mul_top'
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
⊢ a * ∞ = if a = 0 then 0 else ∞

Tactic:
convert! WithTop.mul_top' a

Premises used: WithTop.mul_top'
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
h : a ≠ 0
⊢ a * ∞ = ∞

Tactic:
WithTop.mul_top h

Premises used: WithTop.mul_top, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
⊢ ⊤ * a = if a = 0 then 0 else ⊤

Tactic:
WithTop.top_mul' a

Premises used: WithTop.top_mul'
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
⊢ ∞ * a = if a = 0 then 0 else ∞

Tactic:
convert! WithTop.top_mul' a

Premises used: WithTop.top_mul'
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
h : a ≠ 0
⊢ ∞ * a = ∞

Tactic:
WithTop.top_mul h

Premises used: WithTop.top_mul, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
⊢ HMul.hMul (α := ℝ≥0∞) ∞ ∞ = ∞

Tactic:
WithTop.top_mul_top

Premises used: WithTop.top_mul_top, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
⊢ a * b = ∞ ↔ a ≠ 0 ∧ b = ∞ ∨ a = ∞ ∧ b ≠ 0

Tactic:
WithTop.mul_eq_top_iff

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.mul_eq_top_iff
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
⊢ a < ∞ → b < ∞ → a * b < ∞

Tactic:
WithTop.mul_lt_top

Premises used: WithTop.mul_lt_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
⊢ a ≠ ∞ → b ≠ ∞ → a * b ≠ ∞

Tactic:
WithTop.mul_ne_top

Premises used: WithTop.mul_ne_top, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
h : a * b ≠ ∞
hb : b ≠ 0
⊢ a < ∞

Tactic:
lt_top_iff_ne_top.2 fun ha => h <| mul_eq_top.2 (Or.inr ⟨ha, hb⟩)

Premises used: Iff.mpr, lt_top_iff_ne_top, ENNReal.mul_eq_top, And.intro, Or.inr
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
h : a * b ≠ ∞
ha : a ≠ 0
rwa rwa₁ rwa₂ rwa₃ : a * b ≠ ∞
⊢ b * a ≠ ∞

Tactic:
rwa [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
mp : a * b < ∞ → a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0
mpr : a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0 → a * b < ∞
⊢ a * b < ∞ ↔ a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0

Tactic:
constructor
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
h : a * b < ∞
mp : ¬b = 0 → ¬a = 0 → a < ∞ ∧ b < ∞
⊢ a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0

Tactic:
rw [← or_assoc, or_iff_not_imp_right, or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right, or_assoc
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
h : a * b < ∞
hb : ¬b = 0
ha : ¬a = 0
⊢ a < ∞ ∧ b < ∞

Tactic:
⟨lt_top_of_mul_ne_top_left h.ne hb, lt_top_of_mul_ne_top_right h.ne ha⟩

Premises used: ENNReal.lt_top_of_mul_ne_top_left, And.intro, ENNReal.lt_top_of_mul_ne_top_right, LT.lt.ne
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
h : a * b < ∞
hb : ¬b = 0
ha : ¬a = 0
⊢ a < ∞ ∧ b < ∞

Tactic:
exact ⟨lt_top_of_mul_ne_top_left h.ne hb, lt_top_of_mul_ne_top_right h.ne ha⟩
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
ha : a < ∞
hb : b < ∞
⊢ a * b < ∞

Tactic:
mul_lt_top ha hb

Premises used: ENNReal.mul_lt_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
ha : a < ∞
hb : b < ∞
⊢ a * b < ∞

Tactic:
exact mul_lt_top ha hb

Premises used: ENNReal.mul_lt_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
b : ℝ≥0∞
⊢ 0 * b < ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
⊢ a * 0 < ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
rw : a = 0 → a < ∞
⊢ a * a < ∞ ↔ a < ∞

Tactic:
rw [ENNReal.mul_lt_top_iff, and_self, or_self, or_iff_left_iff_imp]

Premises used: or_iff_left_iff_imp, and_self, ENNReal.mul_lt_top_iff, or_self
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
⊢ LT.lt (α := ℝ≥0∞) 0 ∞

Tactic:
zero_lt_top

Premises used: ENNReal.zero_lt_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
⊢ LT.lt (α := ℝ≥0∞) 0 ∞

Tactic:
exact zero_lt_top

Premises used: ENNReal.zero_lt_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b

Tactic:
CanonicallyOrderedAdd.mul_pos

Premises used: CanonicallyOrderedAdd.mul_pos
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
ha : a ≠ 0
hb : b ≠ 0
⊢ 0 < a * b

Tactic:
mul_pos_iff.2 ⟨pos_iff_ne_zero.2 ha, pos_iff_ne_zero.2 hb⟩

Premises used: Iff.mpr, And.intro, pos_iff_ne_zero, ENNReal.mul_pos_iff
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (α := ℝ≥0∞) ∞ n = ∞

Tactic:
WithTop.top_pow hn

Premises used: ENNReal, WithTop.top_pow
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
n : ℕ
⊢ a ^ n = ∞ ↔ a = ∞ ∧ n ≠ 0

Tactic:
WithTop.pow_eq_top_iff

Premises used: WithTop.pow_eq_top_iff, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
n : ℕ
⊢ a ^ n ≠ ∞ ↔ a ≠ ∞ ∨ n = 0

Tactic:
WithTop.pow_ne_top_iff

Premises used: ENNReal, WithTop.pow_ne_top_iff
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
n : ℕ
⊢ a ^ n < ∞ ↔ a < ∞ ∨ n = 0

Tactic:
WithTop.pow_lt_top_iff

Premises used: WithTop.pow_lt_top_iff
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
n : ℕ
ha : a ^ n = ∞
⊢ a = ∞

Tactic:
WithTop.eq_top_of_pow n ha

Premises used: ENNReal, WithTop.eq_top_of_pow
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
n : ℕ
ha : a ≠ ∞
⊢ a ^ n ≠ ∞

Tactic:
WithTop.pow_ne_top ha

Premises used: ENNReal, WithTop.pow_ne_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
n : ℕ
ha : a < ∞
⊢ a ^ n < ∞

Tactic:
WithTop.pow_lt_top ha

Premises used: WithTop.pow_lt_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c d : ℝ≥0∞
ac : a < c
bd : b < d
⊢ a + b < c + d

Tactic:
WithTop.add_lt_add ac bd

Premises used: WithTop.add_lt_add
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
⊢ AddLECancellable a ↔ a ≠ ∞

Tactic:
WithTop.addLECancellable_iff_ne_top

Premises used: ENNReal, WithTop.addLECancellable_iff_ne_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
h : a ≠ ∞
⊢ AddLECancellable a

Tactic:
addLECancellable_iff_ne.mpr h

Premises used: Iff.mpr, ENNReal.addLECancellable_iff_ne
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
h : a < ∞
⊢ AddLECancellable a

Tactic:
cancel_of_ne h.ne

Premises used: ENNReal.cancel_of_ne, LT.lt.ne
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
h : a < b
⊢ AddLECancellable a

Tactic:
cancel_of_ne h.ne_top

Premises used: LT.lt.ne_top, ENNReal.cancel_of_ne
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0
⊢ AddLECancellable (↑a : ℝ≥0∞)

Tactic:
cancel_of_ne coe_ne_top

Premises used: ENNReal.cancel_of_ne, ENNReal.coe_ne_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : a ≠ ∞
⊢ a + b = a + c ↔ b = c

Tactic:
(cancel_of_ne h).inj

Premises used: AddLECancellable.inj, ENNReal.cancel_of_ne
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : a ≠ ∞
⊢ b + a = c + a ↔ b = c

Tactic:
(cancel_of_ne h).inj_left

Premises used: ENNReal.cancel_of_ne, AddLECancellable.inj_left
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
⊢ a - b = sInf {d : ℝ≥0∞ | a ≤ d + b}

Tactic:
le_antisymm (le_sInf fun _ h => tsub_le_iff_right.mpr h) <| sInf_le <| mem_setOf.2 le_tsub_add

Premises used: Iff.mpr, tsub_le_iff_right, Set.mem_setOf, le_antisymm, sInf_le, le_sInf, le_tsub_add
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
r p : ℝ≥0
⊢ (↑(r - p) : ℝ≥0∞) = (↑r : ℝ≥0∞) - (↑p : ℝ≥0∞)

Tactic:
WithTop.coe_sub

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.coe_sub
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
r : ℝ≥0
⊢ ∞ - (↑r : ℝ≥0∞) = ∞

Tactic:
rfl

Premises used: WithTop.sub, rfl
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
⊢ a ≠ ∞

Tactic:
ha
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
lift : ∀ (a : ℝ≥0), ∞ - (↑a : ℝ≥0∞) = ∞
⊢ ∞ - a = ∞

Tactic:
lift a to ℝ≥0 using ha
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0
⊢ ∞ - (↑a : ℝ≥0∞) = ∞

Tactic:
top_sub_coe

Premises used: ENNReal.top_sub_coe
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0
⊢ ∞ - (↑a : ℝ≥0∞) = ∞

Tactic:
exact top_sub_coe

Premises used: ENNReal.top_sub_coe
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
⊢ a - ∞ = 0

Tactic:
WithTop.sub_top

Premises used: ENNReal.ofNNReal, WithTop.some, ENNReal, WithTop.sub_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
⊢ a - b = ∞ ↔ a = ∞ ∧ b ≠ ∞

Tactic:
WithTop.sub_eq_top_iff

Premises used: WithTop.sub_eq_top_iff, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
⊢ a - b ≠ ∞ ↔ a ≠ ∞ ∨ b = ∞

Tactic:
WithTop.sub_ne_top_iff

Premises used: WithTop.sub_ne_top_iff, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
⊢ a - b ≠ ∞

Tactic:
mt sub_eq_top_iff.mp <| mt And.left ha

Premises used: mt, ENNReal.sub_eq_top_iff, And.left, Iff.mp
-- Module: Mathlib.Data.ENNReal.Operations
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∞)
rw₄ rw₅ : HSub.hSub (α := ℝ≥0∞) (↑m : ℝ≥0∞) (↑n : ℝ≥0∞) = HSub.hSub (α := ℝ≥0∞) (↑m : ℝ≥0∞) (↑n : ℝ≥0∞)
⊢ (↑(m - n) : ℝ≥0∞) = HSub.hSub (α := ℝ≥0∞) (↑m : ℝ≥0∞) (↑n : ℝ≥0∞)

Tactic:
rw [← coe_natCast, Nat.cast_tsub, coe_sub, coe_natCast, coe_natCast]

Premises used: ENNReal.coe_sub, Nat.cast_tsub, ENNReal.coe_natCast
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hb : b ≠ ∞
⊢ a = c + b → a - b = c

Tactic:
(cancel_of_ne hb).tsub_eq_of_eq_add

Premises used: ENNReal.cancel_of_ne, AddLECancellable.tsub_eq_of_eq_add
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
ha : a ≠ ∞
⊢ a = c + b → a - b = c

Tactic:
(cancel_of_ne ha).tsub_eq_of_eq_add'

Premises used: ENNReal.cancel_of_ne, AddLECancellable.tsub_eq_of_eq_add'
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hc : c ≠ ∞
⊢ a + c = b → a = b - c

Tactic:
(cancel_of_ne hc).eq_tsub_of_add_eq

Premises used: AddLECancellable.eq_tsub_of_add_eq, ENNReal.cancel_of_ne
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hb : b ≠ ∞
⊢ a + c = b → a = b - c

Tactic:
(cancel_of_ne hb).eq_tsub_of_add_eq'

Premises used: ENNReal.cancel_of_ne, AddLECancellable.eq_tsub_of_add_eq'
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hb : b ≠ ∞
⊢ a = b + c → a - b = c

Tactic:
(cancel_of_ne hb).tsub_eq_of_eq_add_rev

Premises used: ENNReal.cancel_of_ne, AddLECancellable.tsub_eq_of_eq_add_rev
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
ha : a ≠ ∞
⊢ a = b + c → a - b = c

Tactic:
(cancel_of_ne ha).tsub_eq_of_eq_add_rev'

Premises used: AddLECancellable.tsub_eq_of_eq_add_rev', ENNReal.cancel_of_ne
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
⊢ a + b - a = b

Tactic:
simp [ha]
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
hb : b ≠ ∞
⊢ a + b - b = a

Tactic:
simp [hb]
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
pos : ∀ (c_top : c = ∞), a - b + c = a + c - b
neg : ∀ (c_top : ¬c = ∞), a - b + c = a + c - b
⊢ a - b + c = a + c - b

Tactic:
by_cases c_top : c = ∞
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
c_top : c = ∞
⊢ a - b + c = a + c - b

Tactic:
simpa [c_top, eqComm]

Premises used: eqComm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
c_top : ¬c = ∞
⊢ a - b + c = a + c - b

Tactic:
ENNReal.eq_sub_of_add_eq b_ne_top ?_

Premises used: ENNReal.eq_sub_of_add_eq
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
c_top : ¬c = ∞
neg : a - b + c + b = a + c
⊢ a - b + c = a + c - b

Tactic:
refine ENNReal.eq_sub_of_add_eq b_ne_top ?_

Premises used: ENNReal.eq_sub_of_add_eq
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
c_top : ¬c = ∞
neg : a - b + (b + c) = a + c
⊢ a - b + c + b = a + c

Tactic:
simp only [add_assoc, add_comm c b]

Premises used: add_assoc, add_comm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
c_top : ¬c = ∞
⊢ a - b + (b + c) = a + c

Tactic:
simpa only [← add_assoc] using (add_left_inj c_top).mpr <| tsub_add_cancel_of_le hab

Premises used: Iff.mpr, add_assoc, tsub_add_cancel_of_le, ENNReal.add_left_inj
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hc : c ≠ ∞
⊢ c ≠ ∞

Tactic:
hc
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hc : c ≠ ∞
lift : ∀ (c : ℝ≥0), a + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = a - b
⊢ a + c - (b + c) = a - b

Tactic:
lift c to ℝ≥0 using hc
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
c : ℝ≥0
top : ∞ + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = ∞ - b
coe : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞) + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = (↑x : ℝ≥0∞) - b
⊢ a + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = a - b

Tactic:
cases a
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
b : ℝ≥0∞
c : ℝ≥0
top : ∞ + (↑c : ℝ≥0∞) - (∞ + (↑c : ℝ≥0∞)) = HSub.hSub (α := ℝ≥0∞) ∞ ∞
top₁ : ∀ (x : ℝ≥0), ∞ + (↑c : ℝ≥0∞) - ((↑x : ℝ≥0∞) + (↑c : ℝ≥0∞)) = ∞ - (↑x : ℝ≥0∞)
⊢ ∞ + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = ∞ - b

Tactic:
cases b
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
b : ℝ≥0∞
c x : ℝ≥0
coe : (↑x : ℝ≥0∞) + (↑c : ℝ≥0∞) - (∞ + (↑c : ℝ≥0∞)) = (↑x : ℝ≥0∞) - ∞
coe₁ : ∀ (x_1 : ℝ≥0), (↑x : ℝ≥0∞) + (↑c : ℝ≥0∞) - ((↑x_1 : ℝ≥0∞) + (↑c : ℝ≥0∞)) = (↑x : ℝ≥0∞) - (↑x_1 : ℝ≥0∞)
⊢ (↑x : ℝ≥0∞) + (↑c : ℝ≥0∞) - (b + (↑c : ℝ≥0∞)) = (↑x : ℝ≥0∞) - b

Tactic:
cases b
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
c : ℝ≥0
⊢ ∞ + (↑c : ℝ≥0∞) - (∞ + (↑c : ℝ≥0∞)) = HSub.hSub (α := ℝ≥0∞) ∞ ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
c x : ℝ≥0
⊢ ∞ + (↑c : ℝ≥0∞) - ((↑x : ℝ≥0∞) + (↑c : ℝ≥0∞)) = ∞ - (↑x : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
c x : ℝ≥0
⊢ (↑x : ℝ≥0∞) + (↑c : ℝ≥0∞) - (∞ + (↑c : ℝ≥0∞)) = (↑x : ℝ≥0∞) - ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
c x x_1 : ℝ≥0
coe : x + c - (x_1 + c) = x - x_1
⊢ (↑x : ℝ≥0∞) + (↑c : ℝ≥0∞) - ((↑x_1 : ℝ≥0∞) + (↑c : ℝ≥0∞)) = (↑x : ℝ≥0∞) - (↑x_1 : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
c x x_1 : ℝ≥0
coe coe₁ : x - x_1 = x - x_1
⊢ x + c - (x_1 + c) = x - x_1

Tactic:
rw [add_tsub_add_eq_tsub_right]

Premises used: add_tsub_add_eq_tsub_right
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hc : c ≠ ∞
simp_rw : a + c - (b + c) = a - b
⊢ c + a - (c + b) = a - b

Tactic:
simp_rw [add_comm c]

Premises used: add_comm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hc : c ≠ ∞
⊢ a + c - (b + c) = a - b

Tactic:
ENNReal.add_sub_add_eq_sub_right hc

Premises used: ENNReal.add_sub_add_eq_sub_right
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hc : c ≠ ∞
⊢ a + c - (b + c) = a - b

Tactic:
exact ENNReal.add_sub_add_eq_sub_right hc

Premises used: ENNReal.add_sub_add_eq_sub_right
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : a ≠ ∞ ∨ b ≠ ∞
inl : ∀ (h : a ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ ∞), a - ∞ < c → a < ∞ + c
inr : ∀ (hb : b ≠ ∞), a - b < c → a < b + c
⊢ a - b < c → a < b + c

Tactic:
obtain rfl | hb := eq_or_ne b ∞

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a c : ℝ≥0∞
h : a ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ ∞
inl : a - ∞ < c → a ≠ ∞
⊢ a - ∞ < c → a < ∞ + c

Tactic:
rw [top_add, lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top, top_add
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a c : ℝ≥0∞
h : a ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ ∞
⊢ a - ∞ < c → a ≠ ∞

Tactic:
fun _ => h.resolve_right (Classical.not_not.2 rfl)

Premises used: Iff.mpr, Classical.not_not, Or.resolve_right, rfl
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a c : ℝ≥0∞
h : a ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ ∞
⊢ a - ∞ < c → a ≠ ∞

Tactic:
exact fun _ => h.resolve_right (Classical.not_not.2 rfl)

Premises used: Iff.mpr, Classical.not_not, Or.resolve_right, rfl
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : a ≠ ∞ ∨ b ≠ ∞
hb : b ≠ ∞
⊢ a - b < c → a < b + c

Tactic:
(cancel_of_ne hb).lt_add_of_tsub_lt_left

Premises used: ENNReal.cancel_of_ne, AddLECancellable.lt_add_of_tsub_lt_left
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : a ≠ ∞ ∨ b ≠ ∞
hb : b ≠ ∞
⊢ a - b < c → a < b + c

Tactic:
exact (cancel_of_ne hb).lt_add_of_tsub_lt_left

Premises used: ENNReal.cancel_of_ne, AddLECancellable.lt_add_of_tsub_lt_left
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : a ≠ ∞ ∨ c ≠ ∞
⊢ a - c < b → a < b + c

Tactic:
add_comm c b ▸ ENNReal.lt_add_of_sub_lt_left h

Premises used: ENNReal.lt_add_of_sub_lt_left, Eq.rec, add_comm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
ha : a ≠ ∞
⊢ a + b ≤ c → b ≤ c - a

Tactic:
(cancel_of_ne ha).le_tsub_of_add_le_left

Premises used: ENNReal.cancel_of_ne, AddLECancellable.le_tsub_of_add_le_left
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hb : b ≠ ∞
⊢ a + b ≤ c → a ≤ c - b

Tactic:
(cancel_of_ne hb).le_tsub_of_add_le_right

Premises used: ENNReal.cancel_of_ne, AddLECancellable.le_tsub_of_add_le_right
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hac : c ≤ a
h : a < b + c
⊢ a - c < b

Tactic:
((cancel_of_lt' <| hac.trans_lt h).tsub_lt_iff_right hac).mpr h

Premises used: Iff.mpr, LE.le.trans_lt, AddLECancellable.tsub_lt_iff_right, ENNReal.cancel_of_lt'
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hb : b ≠ ∞
hab : b ≤ a
⊢ a - b < c ↔ a < c + b

Tactic:
(cancel_of_ne hb).tsub_lt_iff_right hab

Premises used: ENNReal.cancel_of_ne, AddLECancellable.tsub_lt_iff_right