awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, (↑a : EReal)), a.1 + a.2 < (↑x : EReal)
have refine : ∀ (r : ℝ) (x : EReal × EReal) (h : x.1 < (↑(r - (a + 1)) : EReal) ∧ x.2 < (↑(a + 1) : EReal)), x.1 + x.2 < (↑r : EReal)
Tactic: refine fun r ↦ ((gt_mem_nhds (bot_lt_coe (r - (a + 1)))).prod_nhds
    (gt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| lt_add_one _)).mono fun _ h ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, ⊥)
have simp : ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ⊥), a.1 + a.2 < (↑x : EReal)
Tactic: simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ⊥), a.1 + a.2 < (↑x : EReal)
have refine : ∀ (r : ℝ) (x : EReal × EReal) (h : x.1 < (↑0 : EReal) ∧ x.2 < (↑r : EReal)), x.1 + x.2 < (↑r : EReal)
Tactic: refine fun r ↦ ((gt_mem_nhds (bot_lt_coe 0)).prod_nhds
    (gt_mem_nhds <| bot_lt_coe r)).mono fun _ h ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
p : EReal × EReal
h : p.1 ≠ ⊤ ∨ p.2 ≠ ⊥
h' : p.1 ≠ ⊥ ∨ p.2 ≠ ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) p
have rcases : ∀ (x y : EReal) (h : (x, y).1 ≠ ⊤ ∨ (x, y).2 ≠ ⊥) (h' : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ ⊤),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (x, y)
Tactic: rcases p with ⟨x, y⟩
Cleared hypotheses: p, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x y : EReal
h : (x, y).1 ≠ ⊤ ∨ (x, y).2 ≠ ⊥
h' : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (x, y)
have bot : ∀ (h : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ ⊥) (h' : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ ⊤),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, y)
Tactic: induction x
Cleared hypotheses: x, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x y : EReal
h : (x, y).1 ≠ ⊤ ∨ (x, y).2 ≠ ⊥
h' : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ ⊤
bot :
  ∀ (h : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ ⊥) (h' : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, y)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (x, y)
have coe : ∀ (a : ℝ) (h : ((↑a : EReal), y).1 ≠ ⊤ ∨ ((↑a : EReal), y).2 ≠ ⊥)
  (h' : ((↑a : EReal), y).1 ≠ ⊥ ∨ ((↑a : EReal), y).2 ≠ ⊤),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), y)
Tactic: induction x
Cleared hypotheses: x, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x y : EReal
h : (x, y).1 ≠ ⊤ ∨ (x, y).2 ≠ ⊥
h' : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ ⊤
bot :
  ∀ (h : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ ⊥) (h' : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, y)
coe :
  ∀ (a : ℝ) (h : ((↑a : EReal), y).1 ≠ ⊤ ∨ ((↑a : EReal), y).2 ≠ ⊥)
    (h' : ((↑a : EReal), y).1 ≠ ⊥ ∨ ((↑a : EReal), y).2 ≠ ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), y)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (x, y)
have top : ∀ (h : Ne (α := EReal) (⊤, y).1 ⊤ ∨ (⊤, y).2 ≠ ⊥) (h' : Ne (α := EReal) (⊤, y).1 ⊥ ∨ (⊤, y).2 ≠ ⊤),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, y)
Tactic: induction x
Cleared hypotheses: x, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
h : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ ⊥
h' : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, y)
have bot : ∀ (h : Ne (α := EReal) (⊥, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊥).2 ⊥)
  (h' : Ne (α := EReal) (⊥, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊥).2 ⊤),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, ⊥)
Tactic: induction y
Cleared hypotheses: y, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
h : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ ⊥
h' : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ ⊤
bot :
  ∀ (h : Ne (α := EReal) (⊥, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊥).2 ⊥)
    (h' : Ne (α := EReal) (⊥, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊥).2 ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, ⊥)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, y)
have bot₁ : ∀ (a : ℝ) (h : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊤ ∨ (⊥, (↑a : EReal)).2 ≠ ⊥)
  (h' : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊥ ∨ (⊥, (↑a : EReal)).2 ≠ ⊤),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, (↑a : EReal))
Tactic: induction y
Cleared hypotheses: y, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
h : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ ⊥
h' : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ ⊤
bot :
  ∀ (h : Ne (α := EReal) (⊥, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊥).2 ⊥)
    (h' : Ne (α := EReal) (⊥, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊥).2 ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, ⊥)
bot₁ :
  ∀ (a : ℝ) (h : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊤ ∨ (⊥, (↑a : EReal)).2 ≠ ⊥)
    (h' : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊥ ∨ (⊥, (↑a : EReal)).2 ≠ ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, (↑a : EReal))
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, y)
have bot₂ : ∀ (h : Ne (α := EReal) (⊥, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊤).2 ⊥)
  (h' : Ne (α := EReal) (⊥, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊤).2 ⊤),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊥, ⊤)
Tactic: induction y
Cleared hypotheses: y, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
a : ℝ
h : ((↑a : EReal), y).1 ≠ ⊤ ∨ ((↑a : EReal), y).2 ≠ ⊥
h' : ((↑a : EReal), y).1 ≠ ⊥ ∨ ((↑a : EReal), y).2 ≠ ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), y)
have coe : ∀ (h : ((↑a : EReal), ⊥).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊥)
  (h' : ((↑a : EReal), ⊥).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊤),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), ⊥)
Tactic: induction y
Cleared hypotheses: y, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
a : ℝ
h : ((↑a : EReal), y).1 ≠ ⊤ ∨ ((↑a : EReal), y).2 ≠ ⊥
h' : ((↑a : EReal), y).1 ≠ ⊥ ∨ ((↑a : EReal), y).2 ≠ ⊤
coe :
  ∀ (h : ((↑a : EReal), ⊥).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊥)
    (h' : ((↑a : EReal), ⊥).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), ⊥)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), y)
have coe₁ : ∀ (a_1 : ℝ) (h : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊤ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊥)
  (h' : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊥ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊤),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), (↑a_1 : EReal))
Tactic: induction y
Cleared hypotheses: y, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
a : ℝ
h : ((↑a : EReal), y).1 ≠ ⊤ ∨ ((↑a : EReal), y).2 ≠ ⊥
h' : ((↑a : EReal), y).1 ≠ ⊥ ∨ ((↑a : EReal), y).2 ≠ ⊤
coe :
  ∀ (h : ((↑a : EReal), ⊥).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊥)
    (h' : ((↑a : EReal), ⊥).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), ⊥)
coe₁ :
  ∀ (a_1 : ℝ) (h : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊤ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊥)
    (h' : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊥ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), (↑a_1 : EReal))
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), y)
have coe₂ : ∀ (h : ((↑a : EReal), ⊤).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊥)
  (h' : ((↑a : EReal), ⊤).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊤),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), ⊤)
Tactic: induction y
Cleared hypotheses: y, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
h : Ne (α := EReal) (⊤, y).1 ⊤ ∨ (⊤, y).2 ≠ ⊥
h' : Ne (α := EReal) (⊤, y).1 ⊥ ∨ (⊤, y).2 ≠ ⊤
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, y)
have top : ∀ (h : Ne (α := EReal) (⊤, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊥).2 ⊥)
  (h' : Ne (α := EReal) (⊤, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊥).2 ⊤),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, ⊥)
Tactic: induction y
Cleared hypotheses: y, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
h : Ne (α := EReal) (⊤, y).1 ⊤ ∨ (⊤, y).2 ≠ ⊥
h' : Ne (α := EReal) (⊤, y).1 ⊥ ∨ (⊤, y).2 ≠ ⊤
top :
  ∀ (h : Ne (α := EReal) (⊤, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊥).2 ⊥)
    (h' : Ne (α := EReal) (⊤, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊥).2 ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, ⊥)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, y)
have top₁ : ∀ (a : ℝ) (h : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊤ ∨ (⊤, (↑a : EReal)).2 ≠ ⊥)
  (h' : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊥ ∨ (⊤, (↑a : EReal)).2 ≠ ⊤),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, (↑a : EReal))
Tactic: induction y
Cleared hypotheses: y, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
h : Ne (α := EReal) (⊤, y).1 ⊤ ∨ (⊤, y).2 ≠ ⊥
h' : Ne (α := EReal) (⊤, y).1 ⊥ ∨ (⊤, y).2 ≠ ⊤
top :
  ∀ (h : Ne (α := EReal) (⊤, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊥).2 ⊥)
    (h' : Ne (α := EReal) (⊤, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊥).2 ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, ⊥)
top₁ :
  ∀ (a : ℝ) (h : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊤ ∨ (⊤, (↑a : EReal)).2 ≠ ⊥)
    (h' : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊥ ∨ (⊤, (↑a : EReal)).2 ≠ ⊤),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, (↑a : EReal))
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, y)
have top₂ : ∀ (h : Ne (α := EReal) (⊤, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊤).2 ⊥)
  (h' : Ne (α := EReal) (⊤, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊤).2 ⊤),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, ⊤)
Tactic: induction y
Cleared hypotheses: y, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal × EReal
y : EReal
⊢ (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
      (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y
have pos : ∀ (hx₁ : x.1 = ⊥),
  (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
      (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y
Tactic: by_cases hx₁ : x.1 = ⊥
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal × EReal
y : EReal
pos :
  ∀ (hx₁ : x.1 = ⊥),
    (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
      ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
        (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y
⊢ (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
      (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y
have neg : ∀ (hx₁ : ¬x.1 = ⊥),
  (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
      (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y
Tactic: by_cases hx₁ : x.1 = ⊥
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
⊢ (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
      (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y
have pos : ∀ (hx₂ : x.2 = ⊥),
  (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
      (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y
Tactic: by_cases hx₂ : x.2 = ⊥
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
pos :
  ∀ (hx₂ : x.2 = ⊥),
    (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
      ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
        (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y
⊢ (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
      (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y
have neg : ∀ (hx₂ : ¬x.2 = ⊥),
  (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x,
      (fun (x1 : EReal × EReal) (x2 : EReal) ↦ (fun (p : EReal × EReal) ↦ p.1 + p.2) x1 > x2) x' y
Tactic: by_cases hx₂ : x.2 = ⊥
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (b, a)
have h₁ : ∀ (x : EReal × EReal), x.1 * x.2 = ((fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ Prod.swap) x
Tactic: convert! h.comp continuous_swap.continuousAt (x := (b, a))
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
⊢ Eq (α := (p : EReal × EReal) → EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2)
    ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2))
have h₁ : ∀ (p : EReal × EReal),
  p.1 * p.2 = ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2)) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (-a, b)
have this : Eq (α := (p : EReal × EReal) → EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2)
  ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2))
Tactic: have : (fun p : EReal × EReal ↦ p.1 * p.2) = (fun x : EReal ↦ -x)
      ∘ (fun p : EReal × EReal ↦ p.1 * p.2) ∘ (fun p : EReal × EReal ↦ (-p.1, p.2)) := by
    ext p
    simp
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
this :
  Eq (α := (p : EReal × EReal) → EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2)
    ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2))
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (-a, b)
have rw : ContinuousAt (Y := EReal)
  ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2)) (-a, b)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a b : EReal
h : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (a, b)
this :
  Eq (α := (p : EReal × EReal) → EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2)
    ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2))
⊢ ContinuousAt (Y := EReal)
    ((fun (x : EReal) ↦ -x) ∘ (fun (p : EReal × EReal) ↦ p.1 * p.2) ∘ fun (p : EReal × EReal) ↦ (-p.1, p.2)) (-a, b)
have apply : ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (Prod.map (fun (a : EReal) ↦ -a) id (-a, b))
Tactic: apply ContinuousAt.comp (Continuous.continuousAt continuous_neg)
    <| ContinuousAt.comp _ (ContinuousAt.prodMap (Continuous.continuousAt continuous_neg)
      (Continuous.continuousAt continuous_id))
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, ⊤)
have simp : ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), (↑x : EReal) < a.1 * a.2
Tactic: simp only [ContinuousAt, EReal.top_mul_top, EReal.tendsto_nhds_top_iff_real]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : ℝ
⊢ ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), (↑x : EReal) < a.1 * a.2
have rw : ∃ (t : Set (EReal × EReal)), (∀ y ∈ t, (↑x : EReal) < y.1 * y.2) ∧ IsOpen t ∧ (⊤, ⊤) ∈ t
Tactic: rw [_root_.eventually_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : ℝ
⊢ ∃ (t : Set (EReal × EReal)), (∀ y ∈ t, (↑x : EReal) < y.1 * y.2) ∧ IsOpen t ∧ (⊤, ⊤) ∈ t
have h : (∀ y ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1), (↑x : EReal) < y.1 * y.2) ∧
  IsOpen (SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)) ∧
    (⊤, ⊤) ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)
Tactic: use (Set.Ioi ((max x 0) : EReal)) ×ˢ (Set.Ioi 1)
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : ℝ
⊢ (∀ y ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1), (↑x : EReal) < y.1 * y.2) ∧
    IsOpen (SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)) ∧
      (⊤, ⊤) ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)
have h : ∀ y ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1), (↑x : EReal) < y.1 * y.2
Tactic: split_ands
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : ℝ
h : ∀ y ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1), (↑x : EReal) < y.1 * y.2
⊢ (∀ y ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1), (↑x : EReal) < y.1 * y.2) ∧
    IsOpen (SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)) ∧
      (⊤, ⊤) ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)
have h₁ : IsOpen (SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1))
Tactic: split_ands
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : ℝ
h : ∀ y ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1), (↑x : EReal) < y.1 * y.2
h₁ : IsOpen (SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1))
⊢ (∀ y ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1), (↑x : EReal) < y.1 * y.2) ∧
    IsOpen (SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)) ∧
      (⊤, ⊤) ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)
have h₂ : (⊤, ⊤).1 ∈ Ioi (max (↑x : EReal) 0)
Tactic: split_ands
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x : ℝ
h : ∀ y ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1), (↑x : EReal) < y.1 * y.2
h₁ : IsOpen (SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1))
h₂ : (⊤, ⊤).1 ∈ Ioi (max (↑x : EReal) 0)
⊢ (∀ y ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1), (↑x : EReal) < y.1 * y.2) ∧
    IsOpen (SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)) ∧
      (⊤, ⊤) ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)
have h₃ : Membership.mem (γ := Set EReal) (Ioi 1) (⊤, ⊤).2
Tactic: split_ands
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
x : ℝ
p : EReal × EReal
p_in_prod : p ∈ SProd.sprod (β := Set EReal) (Ioi (max (↑x : EReal) 0)) (Ioi 1)
⊢ (↑x : EReal) < p.1 * p.2
have p_in_prod₁ : ((↑x : EReal) < p.1 ∧ 0 < p.1) ∧ 1 < p.2
Tactic: simp only [Set.mem_prod, Set.mem_Ioi, max_lt_iff] at p_in_prod
Cleared hypotheses: p_in_prod
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
x : ℝ
p : EReal × EReal
p_in_prod : ((↑x : EReal) < p.1 ∧ 0 < p.1) ∧ 1 < p.2
⊢ (↑x : EReal) < p.1 * p.2
have p2_gt_1 : 1 < p.2
Tactic: rcases p_in_prod with ⟨⟨p1_gt_x, p1_pos⟩, p2_gt_1⟩
Cleared hypotheses: p_in_prod
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
x : ℝ
p : EReal × EReal
p_in_prod : ((↑x : EReal) < p.1 ∧ 0 < p.1) ∧ 1 < p.2
p2_gt_1 : 1 < p.2
⊢ (↑x : EReal) < p.1 * p.2
have p1_gt_x : (↑x : EReal) < p.1
Tactic: rcases p_in_prod with ⟨⟨p1_gt_x, p1_pos⟩, p2_gt_1⟩
Cleared hypotheses: p_in_prod
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
x : ℝ
p : EReal × EReal
p_in_prod : ((↑x : EReal) < p.1 ∧ 0 < p.1) ∧ 1 < p.2
p2_gt_1 : 1 < p.2
p1_gt_x : (↑x : EReal) < p.1
⊢ (↑x : EReal) < p.1 * p.2
have p1_pos : 0 < p.1
Tactic: rcases p_in_prod with ⟨⟨p1_gt_x, p1_pos⟩, p2_gt_1⟩
Cleared hypotheses: p_in_prod
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : (↑x : EReal) < p.1
p1_pos : 0 < p.1
⊢ (↑x : EReal) < p.1 * p.2
have this : p.1 * 1 ≤ p.1 * p.2
Tactic: have := mul_le_mul_of_nonneg_left (le_of_lt p2_gt_1) (le_of_lt p1_pos)
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : (↑x : EReal) < p.1
p1_pos : 0 < p.1
this : p.1 * 1 ≤ p.1 * p.2
⊢ (↑x : EReal) < p.1 * p.2
have this₁ : p.1 ≤ p.1 * p.2
Tactic: rw [mul_one p.1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))
have simp : ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, (↑a : EReal)), (↑x : EReal) < a.1 * a.2
Tactic: simp only [ContinuousAt, EReal.top_mul_coe_of_pos h, EReal.tendsto_nhds_top_iff_real]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
x : ℝ
⊢ ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, (↑a : EReal)), (↑x : EReal) < a.1 * a.2
have rw : ∃ (t : Set (EReal × EReal)), (∀ y ∈ t, (↑x : EReal) < y.1 * y.2) ∧ IsOpen t ∧ (⊤, (↑a : EReal)) ∈ t
Tactic: rw [_root_.eventually_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
x : ℝ
⊢ ∃ (t : Set (EReal × EReal)), (∀ y ∈ t, (↑x : EReal) < y.1 * y.2) ∧ IsOpen t ∧ (⊤, (↑a : EReal)) ∈ t
have h₁ : (∀ y ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal), (↑x : EReal) < y.1 * y.2) ∧
  IsOpen (Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal)) ∧
    (⊤, (↑a : EReal)) ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal)
Tactic: use (Set.Ioi ((2 * (max (x + 1) 0) / a : ℝ) : EReal)) ×ˢ (Set.Ioi ((a / 2 : ℝ) : EReal))
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
x : ℝ
⊢ (∀ y ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal), (↑x : EReal) < y.1 * y.2) ∧
    IsOpen (Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal)) ∧
      (⊤, (↑a : EReal)) ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal)
have h₁ : ∀ y ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal), (↑x : EReal) < y.1 * y.2
Tactic: split_ands
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
x : ℝ
h₁ : ∀ y ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal), (↑x : EReal) < y.1 * y.2
⊢ (∀ y ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal), (↑x : EReal) < y.1 * y.2) ∧
    IsOpen (Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal)) ∧
      (⊤, (↑a : EReal)) ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal)
have h₂ : IsOpen (Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal))
Tactic: split_ands