awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
b_top : b ≠ ⊤
b0 : 0 < b
⊢ ∃ a' ∈ Ioo 0 a, c < a' * b
have inr : ∀ (a' : EReal) (ha' : c / b < a') (aa' : a' < a), ∃ a' ∈ Ioo 0 a, c < a' * b
Tactic: obtain ⟨a', ha', aa'⟩ := exists_between ((div_lt_iff b0 b_top).2 h)
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (hypothesis)
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ ∃ b' ∈ Ioo 0 b, c < a * b'
have hb : 0 < b
Tactic: have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
⊢ ∃ b' ∈ Ioo 0 b, c < a * b'
have simp_rw : ∀ (h : c < b * a), ∃ b' ∈ Ioo 0 b, c < b' * a
Tactic: simp_rw [mul_comm a] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c
have inl : ∀ (h₁ : Ne (α := EReal) ⊤ 0 ∨ b ≠ ⊤) (h₂ : Ne (α := EReal) ⊤ ⊤ ∨ 0 < b) (hc : ⊤ * b < c),
  ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo ⊤ ⊤) a' ∧ a' * b < c
Tactic: rcases eq_top_or_lt_top a with rfl | a_top
Cleared hypotheses: a, h₁, h₂, hc
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
inl :
  ∀ (h₁ : Ne (α := EReal) ⊤ 0 ∨ b ≠ ⊤) (h₂ : Ne (α := EReal) ⊤ ⊤ ∨ 0 < b) (hc : ⊤ * b < c),
    ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo ⊤ ⊤) a' ∧ a' * b < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c
have inr : ∀ (a_top : a < ⊤), ∃ a' ∈ Ioo a ⊤, a' * b < c
Tactic: rcases eq_top_or_lt_top a with rfl | a_top
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (hypothesis)
Goal:
b c : EReal
h₁ : Ne (α := EReal) ⊤ 0 ∨ b ≠ ⊤
h₂ : Ne (α := EReal) ⊤ ⊤ ∨ 0 < b
hc : ⊤ * b < c
⊢ ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo ⊤ ⊤) a' ∧ a' * b < c
have h₃ : 0 < b
Tactic: rw [ne_self_iff_false, false_or] at h₂
Cleared hypotheses: h₂, hc
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (hypothesis)
Goal:
b c : EReal
h₁ : Ne (α := EReal) ⊤ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ * b < c
⊢ ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo ⊤ ⊤) a' ∧ a' * b < c
have hc₁ : ⊤ < c
Tactic: rw [top_mul_of_pos h₂] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c
have inr : ∀ (b0 : b ≤ 0), ∃ a' ∈ Ioo a ⊤, a' * b < c
Tactic: rcases le_or_gt b 0 with b0 | b0
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
inr : ∀ (b0 : b ≤ 0), ∃ a' ∈ Ioo a ⊤, a' * b < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c
have inr₁ : ∀ (b0 : 0 < b), ∃ a' ∈ Ioo a ⊤, a' * b < c
Tactic: rcases le_or_gt b 0 with b0 | b0
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : b ≤ 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c
have inr : ∀ (a' : EReal) (aa' : a < a') (a_top' : a' < ⊤), ∃ a' ∈ Ioo a ⊤, a' * b < c
Tactic: obtain ⟨a', aa', a_top'⟩ := exists_between a_top
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c
have inr : ∀ (h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤) (h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤) (hc : a * ⊤ < c)
  (b0 : LT.lt (α := EReal) 0 ⊤), ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
Tactic: rcases eq_top_or_lt_top b with rfl | b_top
Cleared hypotheses: b, h₁, h₂, hc, b0
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
inr :
  ∀ (h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤) (h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤) (hc : a * ⊤ < c)
    (b0 : LT.lt (α := EReal) 0 ⊤), ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c
have inr₁ : ∀ (b_top : b < ⊤), ∃ a' ∈ Ioo a ⊤, a' * b < c
Tactic: rcases eq_top_or_lt_top b with rfl | b_top
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : a * ⊤ < c
b0 : LT.lt (α := EReal) 0 ⊤
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
have inr : ∀ (a0 : a < 0), ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
Tactic: rcases lt_trichotomy a 0 with a0 | rfl | a0
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : a * ⊤ < c
b0 : LT.lt (α := EReal) 0 ⊤
inr : ∀ (a0 : a < 0), ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
have inr₁ : ∀ (a_top : LT.lt (α := EReal) 0 ⊤) (h₁ : Ne (α := EReal) 0 0 ∨ Ne (α := EReal) ⊤ ⊤)
  (h₂ : Ne (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) 0 ⊤) (hc : HMul.hMul (α := EReal) 0 ⊤ < c),
  ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo 0 ⊤) a' ∧ a' * ⊤ < c
Tactic: rcases lt_trichotomy a 0 with a0 | rfl | a0
Cleared hypotheses: a, a_top, h₁, h₂, hc
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : a * ⊤ < c
b0 : LT.lt (α := EReal) 0 ⊤
inr : ∀ (a0 : a < 0), ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
inr₁ :
  ∀ (a_top : LT.lt (α := EReal) 0 ⊤) (h₁ : Ne (α := EReal) 0 0 ∨ Ne (α := EReal) ⊤ ⊤)
    (h₂ : Ne (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) 0 ⊤) (hc : HMul.hMul (α := EReal) 0 ⊤ < c),
    ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo 0 ⊤) a' ∧ a' * ⊤ < c
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
have inr₂ : ∀ (a0 : 0 < a), ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
Tactic: rcases lt_trichotomy a 0 with a0 | rfl | a0
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : a * ⊤ < c
b0 : LT.lt (α := EReal) 0 ⊤
a0 : a < 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
have inr : ∀ (a' : EReal) (aa' : a < a') (a0' : a' < 0), ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
Tactic: obtain ⟨a', aa', a0'⟩ := exists_between a0
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : a * ⊤ < c
b0 : LT.lt (α := EReal) 0 ⊤
a0 : a < 0
a' : EReal
aa' : a < a'
a0' : a' < 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
have inr : ∀ (hc : ⊥ < c) (b0 : LT.lt (α := EReal) 0 ⊤) (a0 : a < 0) (a' : EReal) (aa' : a < a') (a0' : a' < 0),
  ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
Tactic: rw [mul_top_of_neg a0] at hc
Cleared hypotheses: hc, b0, a0, a', aa', a0'
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (hypothesis)
Goal:
c : EReal
b0 : LT.lt (α := EReal) 0 ⊤
a_top : LT.lt (α := EReal) 0 ⊤
h₁ : Ne (α := EReal) 0 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : Ne (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : HMul.hMul (α := EReal) 0 ⊤ < c
⊢ ∃ (a' : EReal), Membership.mem (γ := Set EReal) (Ioo 0 ⊤) a' ∧ a' * ⊤ < c
have h₃ : False
Tactic: rw [ne_self_iff_false, ne_self_iff_false, false_or] at h₁
Cleared hypotheses: h₁, h₂, hc
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (hypothesis)
Goal:
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ Ne (α := EReal) ⊤ ⊤
h₂ : a ≠ ⊤ ∨ LT.lt (α := EReal) 0 ⊤
hc : a * ⊤ < c
b0 : LT.lt (α := EReal) 0 ⊤
a0 : 0 < a
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
have hc₁ : ⊤ < c
Tactic: rw [mul_top_of_pos a0] at hc
Cleared hypotheses: hc, b0, a0
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
b_top : b < ⊤
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c
have inr : ∀ (a' : EReal) (aa' : a < a') (hc' : a' < c / b), ∃ a' ∈ Ioo a ⊤, a' * b < c
Tactic: obtain ⟨a', aa', hc'⟩ := exists_between ((lt_div_iff b0 b_top.ne).2 hc)
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
hc : a * b < c
⊢ ∃ b' ∈ Ioo b ⊤, a * b' < c
have simp_rw : ∀ (hc : b * a < c), ∃ b' ∈ Ioo b ⊤, b' * a < c
Tactic: simp_rw [mul_comm a] at hc ⊢
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b
have refine : ∀ (d : EReal) (hd : a * b < d), c ≤ d
Tactic: refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd : a * b < d
⊢ c ≤ d
have obtain : ∀ (a' : EReal) (aa' : a' ∈ Ioo a ⊤) (hd : a' * b < d), c ≤ d
Tactic: obtain ⟨a', aa', hd⟩ := exists_mul_left_lt (h₁.imp_left ne_of_gt) h₂ hd
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (hypothesis)
Goal:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd_1 : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd : a' * b < d
⊢ c ≤ d
have h₃ : 0 < a' ∨ b ≠ ⊤
Tactic: replace h₁ : 0 < a' ∨ b ≠ ⊤ := h₁.imp_left fun a0 ↦ a0.trans (mem_Ioo.1 aa').1
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (hypothesis)
Goal:
a b c : EReal
h₂ : a ≠ ⊤ ∨ 0 < b
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd_1 : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
⊢ c ≤ d
have h₃ : a' ≠ ⊤ ∨ b ≠ 0
Tactic: replace h₂ : a' ≠ ⊤ ∨ b ≠ 0 := Or.inl (mem_Ioo.1 aa').2.ne
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : EReal
hd_1 : a * b < d
a' : EReal
aa' : a' ∈ Ioo a ⊤
hd : a' * b < d
h₁ : 0 < a' ∨ b ≠ ⊤
h₂ : a' ≠ ⊤ ∨ b ≠ 0
⊢ c ≤ d
have obtain : ∀ (b' : EReal) (bb' : b' ∈ Ioo b ⊤) (hd : a' * b' < d), c ≤ d
Tactic: obtain ⟨b', bb', hd⟩ := exists_mul_right_lt h₁ h₂ hd
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
⊢ a * b ≤ c
have refine : ∀ (d : EReal) (dab : d < a * b), d ≤ c
Tactic: refine le_of_forall_lt_imp_le_of_dense fun d dab ↦ ?_
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
⊢ d ≤ c
have inl : ∀ (d0 : d < 0), d ≤ c
Tactic: rcases lt_or_ge d 0 with d0 | d0
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
inl : ∀ (d0 : d < 0), d ≤ c
⊢ d ≤ c
have inr : ∀ (d0 : 0 ≤ d), d ≤ c
Tactic: rcases lt_or_ge d 0 with d0 | d0
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab : d < a * b
d0 : 0 ≤ d
⊢ d ≤ c
have inr : ∀ (a' : EReal) (aa' : a' ∈ Ioo 0 a) (dab : d < a' * b), d ≤ c
Tactic: obtain ⟨a', aa', dab⟩ := exists_lt_mul_left_of_nonneg ha d0 dab
-- Lean 4 proof step from Mathlib.Data.EReal.Inv (goal)
Goal:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ∈ Ioo 0 a, ∀ b' ∈ Ioo 0 b, a' * b' ≤ c
d : EReal
dab_1 : d < a * b
d0 : 0 ≤ d
a' : EReal
aa' : a' ∈ Ioo 0 a
dab : d < a' * b
⊢ d ≤ c
have inr : ∀ (b' : EReal) (bb' : b' ∈ Ioo 0 b) (dab : d < a' * b'), d ≤ c
Tactic: obtain ⟨b', bb', dab⟩ := exists_lt_mul_right_of_nonneg aa'.1.le d0 dab
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : x ≠ ⊥
⊢ ⊤ + x = ⊤
have bot : ∀ (h : Ne (α := EReal) ⊥ ⊥), HAdd.hAdd (α := EReal) ⊤ ⊥ = ⊤
Tactic: induction x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : x ≠ ⊥
bot : ∀ (h : Ne (α := EReal) ⊥ ⊥), HAdd.hAdd (α := EReal) ⊤ ⊥ = ⊤
⊢ ⊤ + x = ⊤
have coe : ∀ (a : ℝ) (h : (↑a : EReal) ≠ ⊥), ⊤ + (↑a : EReal) = ⊤
Tactic: induction x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : x ≠ ⊥
bot : ∀ (h : Ne (α := EReal) ⊥ ⊥), HAdd.hAdd (α := EReal) ⊤ ⊥ = ⊤
coe : ∀ (a : ℝ) (h : (↑a : EReal) ≠ ⊥), ⊤ + (↑a : EReal) = ⊤
⊢ ⊤ + x = ⊤
have top : ∀ (h : Ne (α := EReal) ⊤ ⊥), HAdd.hAdd (α := EReal) ⊤ ⊤ = ⊤
Tactic: induction x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
h : Ne (α := EReal) ⊥ ⊥
⊢ HAdd.hAdd (α := EReal) ⊤ ⊥ = ⊤
have bot : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
⊢ ⊤ + x = ⊤ ↔ x ≠ ⊥
have mp : ⊤ + x = ⊤ → x ≠ ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
mp : ⊤ + x = ⊤ → x ≠ ⊥
⊢ ⊤ + x = ⊤ ↔ x ≠ ⊥
have mpr : x ≠ ⊥ → ⊤ + x = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (hypothesis)
Goal:
h : HAdd.hAdd (α := EReal) ⊤ ⊥ = ⊤
⊢ False
have h₁ : Eq (α := EReal) ⊥ ⊤
Tactic: rw [add_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : x ≠ ⊥
⊢ ⊤ + x = ⊤
have mpr : ∀ (h : Ne (α := EReal) ⊥ ⊥), HAdd.hAdd (α := EReal) ⊤ ⊥ = ⊤
Tactic: cases x with
    | bot => contradiction
    | top => rfl
    | coe r => exact top_add_of_ne_bot h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : x ≠ ⊥
mpr : ∀ (h : Ne (α := EReal) ⊥ ⊥), HAdd.hAdd (α := EReal) ⊤ ⊥ = ⊤
⊢ ⊤ + x = ⊤
have mpr₁ : ∀ (h : Ne (α := EReal) ⊤ ⊥), HAdd.hAdd (α := EReal) ⊤ ⊤ = ⊤
Tactic: cases x with
    | bot => contradiction
    | top => rfl
    | coe r => exact top_add_of_ne_bot h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : x ≠ ⊥
mpr : ∀ (h : Ne (α := EReal) ⊥ ⊥), HAdd.hAdd (α := EReal) ⊤ ⊥ = ⊤
mpr₁ : ∀ (h : Ne (α := EReal) ⊤ ⊥), HAdd.hAdd (α := EReal) ⊤ ⊤ = ⊤
⊢ ⊤ + x = ⊤
have mpr₂ : ∀ (r : ℝ) (h : (↑r : EReal) ≠ ⊥), ⊤ + (↑r : EReal) = ⊤
Tactic: cases x with
    | bot => contradiction
    | top => rfl
    | coe r => exact top_add_of_ne_bot h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : x ≠ ⊥
⊢ x + ⊤ = ⊤
have rw : ⊤ + x = ⊤
Tactic: rw [add_comm, top_add_of_ne_bot h]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : x ≠ ⊥
rw : ⊤ + x = ⊤
⊢ x + ⊤ = ⊤
have rw₁ : Eq (α := EReal) ⊤ ⊤
Tactic: rw [add_comm, top_add_of_ne_bot h]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
⊢ x + ⊤ = ⊤ ↔ x ≠ ⊥
have rw : ⊤ + x = ⊤ ↔ x ≠ ⊥
Tactic: rw [add_comm, top_add_iff_ne_bot]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
rw : ⊤ + x = ⊤ ↔ x ≠ ⊥
⊢ x + ⊤ = ⊤ ↔ x ≠ ⊥
have rw₁ : x ≠ ⊥ ↔ x ≠ ⊥
Tactic: rw [add_comm, top_add_iff_ne_bot]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
hy : y ≠ ⊤
h'y : y ≠ ⊥
⊢ (x + y).toReal = x.toReal + y.toReal
have lift : ∀ (x : ℝ) (hx : (↑x : EReal) ≠ ⊤) (h'x : (↑x : EReal) ≠ ⊥), ((↑x : EReal) + y).toReal = (↑x : EReal).toReal + y.toReal
Tactic: lift x to ℝ using ⟨hx, h'x⟩
Cleared hypotheses: x, hx, h'x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : y ≠ ⊤
h'y : y ≠ ⊥
x : ℝ
hx : (↑x : EReal) ≠ ⊤
h'x : (↑x : EReal) ≠ ⊥
⊢ ((↑x : EReal) + y).toReal = (↑x : EReal).toReal + y.toReal
have lift : ∀ (y : ℝ) (hy : (↑y : EReal) ≠ ⊤) (h'y : (↑y : EReal) ≠ ⊥),
  ((↑x : EReal) + (↑y : EReal)).toReal = (↑x : EReal).toReal + (↑y : EReal).toReal
Tactic: lift y to ℝ using ⟨hy, h'y⟩
Cleared hypotheses: y, hy, h'y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x + y).toENNReal = x.toENNReal + y.toENNReal
have bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), (⊥ + y).toENNReal = toENNReal ⊥ + y.toENNReal
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), (⊥ + y).toENNReal = toENNReal ⊥ + y.toENNReal
⊢ (x + y).toENNReal = x.toENNReal + y.toENNReal
have coe : ∀ (a : ℝ) (hx : 0 ≤ (↑a : EReal)), ((↑a : EReal) + y).toENNReal = (↑a : EReal).toENNReal + y.toENNReal
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), (⊥ + y).toENNReal = toENNReal ⊥ + y.toENNReal
coe : ∀ (a : ℝ) (hx : 0 ≤ (↑a : EReal)), ((↑a : EReal) + y).toENNReal = (↑a : EReal).toENNReal + y.toENNReal
⊢ (x + y).toENNReal = x.toENNReal + y.toENNReal
have top : ∀ (hx : LE.le (α := EReal) 0 ⊤), (⊤ + y).toENNReal = toENNReal ⊤ + y.toENNReal
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊥
⊢ (⊥ + y).toENNReal = toENNReal ⊥ + y.toENNReal
have bot : ∀ (hy : LE.le (α := EReal) 0 ⊥), (HAdd.hAdd (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ + toENNReal ⊥
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊥
bot : ∀ (hy : LE.le (α := EReal) 0 ⊥), (HAdd.hAdd (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ + toENNReal ⊥
⊢ (⊥ + y).toENNReal = toENNReal ⊥ + y.toENNReal
have bot₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), (⊥ + (↑a : EReal)).toENNReal = toENNReal ⊥ + (↑a : EReal).toENNReal
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊥
bot : ∀ (hy : LE.le (α := EReal) 0 ⊥), (HAdd.hAdd (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ + toENNReal ⊥
bot₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), (⊥ + (↑a : EReal)).toENNReal = toENNReal ⊥ + (↑a : EReal).toENNReal
⊢ (⊥ + y).toENNReal = toENNReal ⊥ + y.toENNReal
have bot₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), (HAdd.hAdd (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ + toENNReal ⊤
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
a : ℝ
hx : 0 ≤ (↑a : EReal)
⊢ ((↑a : EReal) + y).toENNReal = (↑a : EReal).toENNReal + y.toENNReal
have coe : ∀ (hy : LE.le (α := EReal) 0 ⊥), ((↑a : EReal) + ⊥).toENNReal = (↑a : EReal).toENNReal + toENNReal ⊥
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
a : ℝ
hx : 0 ≤ (↑a : EReal)
coe : ∀ (hy : LE.le (α := EReal) 0 ⊥), ((↑a : EReal) + ⊥).toENNReal = (↑a : EReal).toENNReal + toENNReal ⊥
⊢ ((↑a : EReal) + y).toENNReal = (↑a : EReal).toENNReal + y.toENNReal
have coe₁ : ∀ (a_1 : ℝ) (hy : 0 ≤ (↑a_1 : EReal)),
  ((↑a : EReal) + (↑a_1 : EReal)).toENNReal = (↑a : EReal).toENNReal + (↑a_1 : EReal).toENNReal
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
a : ℝ
hx : 0 ≤ (↑a : EReal)
coe : ∀ (hy : LE.le (α := EReal) 0 ⊥), ((↑a : EReal) + ⊥).toENNReal = (↑a : EReal).toENNReal + toENNReal ⊥
coe₁ :
  ∀ (a_1 : ℝ) (hy : 0 ≤ (↑a_1 : EReal)),
    ((↑a : EReal) + (↑a_1 : EReal)).toENNReal = (↑a : EReal).toENNReal + (↑a_1 : EReal).toENNReal
⊢ ((↑a : EReal) + y).toENNReal = (↑a : EReal).toENNReal + y.toENNReal
have coe₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), ((↑a : EReal) + ⊤).toENNReal = (↑a : EReal).toENNReal + toENNReal ⊤
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊤
⊢ (⊤ + y).toENNReal = toENNReal ⊤ + y.toENNReal
have top : ∀ (hy : LE.le (α := EReal) 0 ⊥), (HAdd.hAdd (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ + toENNReal ⊥
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊤
top : ∀ (hy : LE.le (α := EReal) 0 ⊥), (HAdd.hAdd (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ + toENNReal ⊥
⊢ (⊤ + y).toENNReal = toENNReal ⊤ + y.toENNReal
have top₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), (⊤ + (↑a : EReal)).toENNReal = toENNReal ⊤ + (↑a : EReal).toENNReal
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
hx : LE.le (α := EReal) 0 ⊤
top : ∀ (hy : LE.le (α := EReal) 0 ⊥), (HAdd.hAdd (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ + toENNReal ⊥
top₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), (⊤ + (↑a : EReal)).toENNReal = toENNReal ⊤ + (↑a : EReal).toENNReal
⊢ (⊤ + y).toENNReal = toENNReal ⊤ + y.toENNReal
have top₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), (HAdd.hAdd (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ + toENNReal ⊤
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
hx : 0 ≤ (↑a : EReal)
a_1 : ℝ
hy : 0 ≤ (↑a_1 : EReal)
⊢ (↑(a + a_1) : EReal).toENNReal = (↑a : EReal).toENNReal + (↑a_1 : EReal).toENNReal
have coe : ENNReal.ofReal (a + a_1) = ENNReal.ofReal a + ENNReal.ofReal a_1
Tactic: simp_rw [real_coe_toENNReal]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
⊢ (x + y).toENNReal ≤ x.toENNReal + y.toENNReal
have bot : (⊥ + y).toENNReal ≤ toENNReal ⊥ + y.toENNReal
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
bot : (⊥ + y).toENNReal ≤ toENNReal ⊥ + y.toENNReal
⊢ (x + y).toENNReal ≤ x.toENNReal + y.toENNReal
have coe : ∀ (a : ℝ), ((↑a : EReal) + y).toENNReal ≤ (↑a : EReal).toENNReal + y.toENNReal
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
bot : (⊥ + y).toENNReal ≤ toENNReal ⊥ + y.toENNReal
coe : ∀ (a : ℝ), ((↑a : EReal) + y).toENNReal ≤ (↑a : EReal).toENNReal + y.toENNReal
⊢ (x + y).toENNReal ≤ x.toENNReal + y.toENNReal
have top : (⊤ + y).toENNReal ≤ toENNReal ⊤ + y.toENNReal
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
⊢ (⊥ + y).toENNReal ≤ toENNReal ⊥ + y.toENNReal
have bot : (HAdd.hAdd (α := EReal) ⊥ ⊥).toENNReal ≤ toENNReal ⊥ + toENNReal ⊥
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
bot : (HAdd.hAdd (α := EReal) ⊥ ⊥).toENNReal ≤ toENNReal ⊥ + toENNReal ⊥
⊢ (⊥ + y).toENNReal ≤ toENNReal ⊥ + y.toENNReal
have bot₁ : ∀ (a : ℝ), (⊥ + (↑a : EReal)).toENNReal ≤ toENNReal ⊥ + (↑a : EReal).toENNReal
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
bot : (HAdd.hAdd (α := EReal) ⊥ ⊥).toENNReal ≤ toENNReal ⊥ + toENNReal ⊥
bot₁ : ∀ (a : ℝ), (⊥ + (↑a : EReal)).toENNReal ≤ toENNReal ⊥ + (↑a : EReal).toENNReal
⊢ (⊥ + y).toENNReal ≤ toENNReal ⊥ + y.toENNReal
have bot₂ : (HAdd.hAdd (α := EReal) ⊥ ⊤).toENNReal ≤ toENNReal ⊥ + toENNReal ⊤
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
⊢ ((↑a : EReal) + y).toENNReal ≤ (↑a : EReal).toENNReal + y.toENNReal
have coe : ((↑a : EReal) + ⊥).toENNReal ≤ (↑a : EReal).toENNReal + toENNReal ⊥
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
coe : ((↑a : EReal) + ⊥).toENNReal ≤ (↑a : EReal).toENNReal + toENNReal ⊥
⊢ ((↑a : EReal) + y).toENNReal ≤ (↑a : EReal).toENNReal + y.toENNReal
have coe₁ : ∀ (a_1 : ℝ), ((↑a : EReal) + (↑a_1 : EReal)).toENNReal ≤ (↑a : EReal).toENNReal + (↑a_1 : EReal).toENNReal
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
coe : ((↑a : EReal) + ⊥).toENNReal ≤ (↑a : EReal).toENNReal + toENNReal ⊥
coe₁ : ∀ (a_1 : ℝ), ((↑a : EReal) + (↑a_1 : EReal)).toENNReal ≤ (↑a : EReal).toENNReal + (↑a_1 : EReal).toENNReal
⊢ ((↑a : EReal) + y).toENNReal ≤ (↑a : EReal).toENNReal + y.toENNReal
have coe₂ : ((↑a : EReal) + ⊤).toENNReal ≤ (↑a : EReal).toENNReal + toENNReal ⊤
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
⊢ (⊤ + y).toENNReal ≤ toENNReal ⊤ + y.toENNReal
have top : (HAdd.hAdd (α := EReal) ⊤ ⊥).toENNReal ≤ toENNReal ⊤ + toENNReal ⊥
Tactic: induction y
Cleared hypotheses: y