awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h₂ : IsOpen (Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal))
⊢ (∀ 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₃ : (⊤, (↑a : EReal)).1 ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal)
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
h₂ : IsOpen (Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal))
h₃ : (⊤, (↑a : EReal)).1 ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal)
⊢ (∀ 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₄ : (⊤, (↑a : EReal)).2 ∈ Ioi (↑(a / 2) : EReal)
Tactic: split_ands
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p_in_prod : p ∈ Ioi (↑(2 * max (x + 1) 0 / a) : EReal) ×ˢ Ioi (↑(a / 2) : EReal)
⊢ (↑x : EReal) < p.1 * p.2
have p_in_prod₁ : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1 ∧ (↑(a / 2) : EReal) < p.2
Tactic: simp only [Set.mem_prod, Set.mem_Ioi] at p_in_prod
Cleared hypotheses: p_in_prod
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p_in_prod : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1 ∧ (↑(a / 2) : EReal) < p.2
⊢ (↑x : EReal) < p.1 * p.2
have p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
Tactic: rcases p_in_prod with ⟨p1_gt, p2_gt⟩
Cleared hypotheses: p_in_prod
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p_in_prod : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1 ∧ (↑(a / 2) : EReal) < p.2
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
⊢ (↑x : EReal) < p.1 * p.2
have p2_gt : (↑(a / 2) : EReal) < p.2
Tactic: rcases p_in_prod with ⟨p1_gt, p2_gt⟩
Cleared hypotheses: p_in_prod
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
⊢ 0 < p.1
have apply : 0 ≤ (↑(2 * max (x + 1) 0 / a) : EReal)
Tactic: apply lt_of_le_of_lt _ p1_gt
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
⊢ 0 ≤ (↑(2 * max (x + 1) 0 / a) : EReal)
have rw : 0 ≤ 2 * max (x + 1) 0 / a
Tactic: rw [EReal.coe_nonneg]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
⊢ 0 ≤ 2 * max (x + 1) 0 / a
have apply : 0 ≤ 2 * max (x + 1) 0
Tactic: apply mul_nonneg _ (le_of_lt (inv_pos_of_pos h))
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
⊢ (↑x : EReal) < p.1 * p.2
have p1_pos : 0 < p.1
Tactic: have p1_pos : 0 < p.1 := by
      apply lt_of_le_of_lt _ p1_gt
      rw [EReal.coe_nonneg]
      apply mul_nonneg _ (le_of_lt (inv_pos_of_pos h))
      simp only [Nat.ofNat_pos, mul_nonneg_iff_of_pos_left, le_max_iff, le_refl, or_true]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
⊢ 0 < (↑(a / 2) : EReal)
have rw : 0 < a / 2
Tactic: rw [EReal.coe_pos]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
⊢ 0 < a / 2
have linarith : a / 2 ≤ 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
linarith : a / 2 ≤ 0 → 2 / 2 = 1
⊢ 0 < a / 2
have linarith₁ : a / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
linarith : a / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : a / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 < a / 2
have linarith₂ : a / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
linarith : a / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : a / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : a / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < a / 2
have linarith₃ : a / 2 ≤ 0 → 0 - a + (1 * a - HMul.hMul (α := ℝ) 2 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
⊢ (↑x : EReal) < p.1 * p.2
have a2_pos : 0 < (↑(a / 2) : EReal)
Tactic: have a2_pos : 0 < ((a / 2 : ℝ) : EReal) := by rw [EReal.coe_pos]; linarith
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < (↑(a / 2) : EReal)
⊢ (↑x : EReal) < p.1 * p.2
have lock : (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal) ≤ p.1 * (↑(a / 2) : EReal)
Tactic: have lock := mul_le_mul_of_nonneg_right (le_of_lt p1_gt) (le_of_lt a2_pos)
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < (↑(a / 2) : EReal)
lock : (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal) ≤ p.1 * (↑(a / 2) : EReal)
⊢ (↑x : EReal) < p.1 * p.2
have key : p.1 * (↑(a / 2) : EReal) ≤ p.1 * p.2
Tactic: have key := mul_le_mul_of_nonneg_left (le_of_lt p2_gt) (le_of_lt p1_pos)
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < (↑(a / 2) : EReal)
lock : (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal) ≤ p.1 * (↑(a / 2) : EReal)
key : p.1 * (↑(a / 2) : EReal) ≤ p.1 * p.2
⊢ (↑x : EReal) < p.1 * p.2
have lock₁ : (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal) ≤ p.1 * p.2
Tactic: replace lock := le_trans lock key
Cleared hypotheses: lock
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < (↑(a / 2) : EReal)
key : p.1 * (↑(a / 2) : EReal) ≤ p.1 * p.2
lock : (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal) ≤ p.1 * p.2
⊢ (↑x : EReal) < p.1 * p.2
have apply : (↑x : EReal) < (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal)
Tactic: apply lt_of_lt_of_le _ lock
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : (↑(2 * max (x + 1) 0 / a) : EReal) < p.1
p2_gt : (↑(a / 2) : EReal) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < (↑(a / 2) : EReal)
key : p.1 * (↑(a / 2) : EReal) ≤ p.1 * p.2
lock : (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal) ≤ p.1 * p.2
⊢ (↑x : EReal) < (↑(2 * max (x + 1) 0 / a) : EReal) * (↑(a / 2) : EReal)
have rw : x < a / a * (2 / 2 * max (x + 1) 0)
Tactic: rw [← EReal.coe_mul, EReal.coe_lt_coe_iff, _root_.div_mul_div_comm, mul_comm,
      ← _root_.div_mul_div_comm, mul_div_right_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : a ≠ 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))
have inl : ∀ (a_neg : a < 0), ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))
Tactic: rcases lt_or_gt_of_ne h with a_neg | a_pos
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
a : ℝ
h : a ≠ 0
inl : ∀ (a_neg : a < 0), 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))
have inr : ∀ (a_pos : 0 < a), ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))
Tactic: rcases lt_or_gt_of_ne h with a_neg | a_pos
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
p : EReal × EReal
h₁ : p.1 ≠ 0 ∨ p.2 ≠ ⊥
h₂ : p.1 ≠ 0 ∨ p.2 ≠ ⊤
h₃ : p.1 ≠ ⊥ ∨ p.2 ≠ 0
h₄ : p.1 ≠ ⊤ ∨ p.2 ≠ 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) p
have rcases : ∀ (x y : EReal) (h₁ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊥) (h₂ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊤) (h₃ : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ 0)
  (h₄ : (x, y).1 ≠ ⊤ ∨ (x, y).2 ≠ 0), ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (x, y)
Tactic: rcases p with ⟨x, y⟩
Cleared hypotheses: p, h₁, h₂, h₃, h₄
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x y : EReal
h₁ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊥
h₂ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊤
h₃ : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ 0
h₄ : (x, y).1 ≠ ⊤ ∨ (x, y).2 ≠ 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (x, y)
have bot : ∀ (h₁ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊥) (h₂ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊤)
  (h₃ : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ 0) (h₄ : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ 0),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, y)
Tactic: induction x
Cleared hypotheses: x, h₁, h₂, h₃, h₄
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x y : EReal
h₁ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊥
h₂ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊤
h₃ : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ 0
h₄ : (x, y).1 ≠ ⊤ ∨ (x, y).2 ≠ 0
bot :
  ∀ (h₁ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊥) (h₂ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊤)
    (h₃ : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ 0) (h₄ : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ 0),
    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 ≠ 0 ∨ ((↑a : EReal), y).2 ≠ ⊥)
  (h₂ : ((↑a : EReal), y).1 ≠ 0 ∨ ((↑a : EReal), y).2 ≠ ⊤) (h₃ : ((↑a : EReal), y).1 ≠ ⊥ ∨ ((↑a : EReal), y).2 ≠ 0)
  (h₄ : ((↑a : EReal), y).1 ≠ ⊤ ∨ ((↑a : EReal), y).2 ≠ 0),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), y)
Tactic: induction x
Cleared hypotheses: x, h₁, h₂, h₃, h₄
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
x y : EReal
h₁ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊥
h₂ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊤
h₃ : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ 0
h₄ : (x, y).1 ≠ ⊤ ∨ (x, y).2 ≠ 0
bot :
  ∀ (h₁ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊥) (h₂ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊤)
    (h₃ : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ 0) (h₄ : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, y)
coe :
  ∀ (a : ℝ) (h₁ : ((↑a : EReal), y).1 ≠ 0 ∨ ((↑a : EReal), y).2 ≠ ⊥)
    (h₂ : ((↑a : EReal), y).1 ≠ 0 ∨ ((↑a : EReal), y).2 ≠ ⊤) (h₃ : ((↑a : EReal), y).1 ≠ ⊥ ∨ ((↑a : EReal), y).2 ≠ 0)
    (h₄ : ((↑a : EReal), y).1 ≠ ⊤ ∨ ((↑a : EReal), y).2 ≠ 0),
    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 0 ∨ (⊤, y).2 ≠ ⊥) (h₂ : Ne (α := EReal) (⊤, y).1 0 ∨ (⊤, y).2 ≠ ⊤)
  (h₃ : Ne (α := EReal) (⊤, y).1 ⊥ ∨ (⊤, y).2 ≠ 0) (h₄ : Ne (α := EReal) (⊤, y).1 ⊤ ∨ (⊤, y).2 ≠ 0),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, y)
Tactic: induction x
Cleared hypotheses: x, h₁, h₂, h₃, h₄
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
h₁ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊤
h₃ : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ 0
h₄ : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, y)
have bot : ∀ (h₁ : Ne (α := EReal) (⊥, ⊥).1 0 ∨ Ne (α := EReal) (⊥, ⊥).2 ⊥)
  (h₂ : Ne (α := EReal) (⊥, ⊥).1 0 ∨ Ne (α := EReal) (⊥, ⊥).2 ⊤)
  (h₃ : Ne (α := EReal) (⊥, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊥).2 0)
  (h₄ : Ne (α := EReal) (⊥, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊥).2 0),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, ⊥)
Tactic: induction y
Cleared hypotheses: y, h₁, h₂, h₃, h₄
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
h₁ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊤
h₃ : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ 0
h₄ : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ 0
bot :
  ∀ (h₁ : Ne (α := EReal) (⊥, ⊥).1 0 ∨ Ne (α := EReal) (⊥, ⊥).2 ⊥)
    (h₂ : Ne (α := EReal) (⊥, ⊥).1 0 ∨ Ne (α := EReal) (⊥, ⊥).2 ⊤)
    (h₃ : Ne (α := EReal) (⊥, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊥).2 0)
    (h₄ : Ne (α := EReal) (⊥, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊥).2 0),
    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 0 ∨ (⊥, (↑a : EReal)).2 ≠ ⊥)
  (h₂ : Ne (α := EReal) (⊥, (↑a : EReal)).1 0 ∨ (⊥, (↑a : EReal)).2 ≠ ⊤)
  (h₃ : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊥ ∨ (⊥, (↑a : EReal)).2 ≠ 0)
  (h₄ : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊤ ∨ (⊥, (↑a : EReal)).2 ≠ 0),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, (↑a : EReal))
Tactic: induction y
Cleared hypotheses: y, h₁, h₂, h₃, h₄
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
h₁ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊥, y).1 0 ∨ (⊥, y).2 ≠ ⊤
h₃ : Ne (α := EReal) (⊥, y).1 ⊥ ∨ (⊥, y).2 ≠ 0
h₄ : Ne (α := EReal) (⊥, y).1 ⊤ ∨ (⊥, y).2 ≠ 0
bot :
  ∀ (h₁ : Ne (α := EReal) (⊥, ⊥).1 0 ∨ Ne (α := EReal) (⊥, ⊥).2 ⊥)
    (h₂ : Ne (α := EReal) (⊥, ⊥).1 0 ∨ Ne (α := EReal) (⊥, ⊥).2 ⊤)
    (h₃ : Ne (α := EReal) (⊥, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊥).2 0)
    (h₄ : Ne (α := EReal) (⊥, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊥).2 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, ⊥)
bot₁ :
  ∀ (a : ℝ) (h₁ : Ne (α := EReal) (⊥, (↑a : EReal)).1 0 ∨ (⊥, (↑a : EReal)).2 ≠ ⊥)
    (h₂ : Ne (α := EReal) (⊥, (↑a : EReal)).1 0 ∨ (⊥, (↑a : EReal)).2 ≠ ⊤)
    (h₃ : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊥ ∨ (⊥, (↑a : EReal)).2 ≠ 0)
    (h₄ : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊤ ∨ (⊥, (↑a : EReal)).2 ≠ 0),
    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 0 ∨ Ne (α := EReal) (⊥, ⊤).2 ⊥)
  (h₂ : Ne (α := EReal) (⊥, ⊤).1 0 ∨ Ne (α := EReal) (⊥, ⊤).2 ⊤)
  (h₃ : Ne (α := EReal) (⊥, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊥, ⊤).2 0)
  (h₄ : Ne (α := EReal) (⊥, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊥, ⊤).2 0),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, ⊤)
Tactic: induction y
Cleared hypotheses: y, h₁, h₂, h₃, h₄
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
a : ℝ
h₁ : ((↑a : EReal), y).1 ≠ 0 ∨ ((↑a : EReal), y).2 ≠ ⊥
h₂ : ((↑a : EReal), y).1 ≠ 0 ∨ ((↑a : EReal), y).2 ≠ ⊤
h₃ : ((↑a : EReal), y).1 ≠ ⊥ ∨ ((↑a : EReal), y).2 ≠ 0
h₄ : ((↑a : EReal), y).1 ≠ ⊤ ∨ ((↑a : EReal), y).2 ≠ 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), y)
have coe : ∀ (h₁ : ((↑a : EReal), ⊥).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊥)
  (h₂ : ((↑a : EReal), ⊥).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊤)
  (h₃ : ((↑a : EReal), ⊥).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0)
  (h₄ : ((↑a : EReal), ⊥).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), ⊥)
Tactic: induction y
Cleared hypotheses: y, h₁, h₂, h₃, h₄
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
a : ℝ
h₁ : ((↑a : EReal), y).1 ≠ 0 ∨ ((↑a : EReal), y).2 ≠ ⊥
h₂ : ((↑a : EReal), y).1 ≠ 0 ∨ ((↑a : EReal), y).2 ≠ ⊤
h₃ : ((↑a : EReal), y).1 ≠ ⊥ ∨ ((↑a : EReal), y).2 ≠ 0
h₄ : ((↑a : EReal), y).1 ≠ ⊤ ∨ ((↑a : EReal), y).2 ≠ 0
coe :
  ∀ (h₁ : ((↑a : EReal), ⊥).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊥)
    (h₂ : ((↑a : EReal), ⊥).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊤)
    (h₃ : ((↑a : EReal), ⊥).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0)
    (h₄ : ((↑a : EReal), ⊥).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0),
    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 ≠ 0 ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊥)
  (h₂ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ 0 ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊤)
  (h₃ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊥ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ 0)
  (h₄ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊤ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ 0),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), (↑a_1 : EReal))
Tactic: induction y
Cleared hypotheses: y, h₁, h₂, h₃, h₄
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
a : ℝ
h₁ : ((↑a : EReal), y).1 ≠ 0 ∨ ((↑a : EReal), y).2 ≠ ⊥
h₂ : ((↑a : EReal), y).1 ≠ 0 ∨ ((↑a : EReal), y).2 ≠ ⊤
h₃ : ((↑a : EReal), y).1 ≠ ⊥ ∨ ((↑a : EReal), y).2 ≠ 0
h₄ : ((↑a : EReal), y).1 ≠ ⊤ ∨ ((↑a : EReal), y).2 ≠ 0
coe :
  ∀ (h₁ : ((↑a : EReal), ⊥).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊥)
    (h₂ : ((↑a : EReal), ⊥).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊤)
    (h₃ : ((↑a : EReal), ⊥).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0)
    (h₄ : ((↑a : EReal), ⊥).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), ⊥)
coe₁ :
  ∀ (a_1 : ℝ) (h₁ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ 0 ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊥)
    (h₂ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ 0 ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ ⊤)
    (h₃ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊥ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ 0)
    (h₄ : ((↑a : EReal), (↑a_1 : EReal)).1 ≠ ⊤ ∨ ((↑a : EReal), (↑a_1 : EReal)).2 ≠ 0),
    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 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊥)
  (h₂ : ((↑a : EReal), ⊤).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊤)
  (h₃ : ((↑a : EReal), ⊤).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 0)
  (h₄ : ((↑a : EReal), ⊤).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 0),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), ⊤)
Tactic: induction y
Cleared hypotheses: y, h₁, h₂, h₃, h₄
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
h₁ : Ne (α := EReal) (⊤, y).1 0 ∨ (⊤, y).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊤, y).1 0 ∨ (⊤, y).2 ≠ ⊤
h₃ : Ne (α := EReal) (⊤, y).1 ⊥ ∨ (⊤, y).2 ≠ 0
h₄ : Ne (α := EReal) (⊤, y).1 ⊤ ∨ (⊤, y).2 ≠ 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, y)
have top : ∀ (h₁ : Ne (α := EReal) (⊤, ⊥).1 0 ∨ Ne (α := EReal) (⊤, ⊥).2 ⊥)
  (h₂ : Ne (α := EReal) (⊤, ⊥).1 0 ∨ Ne (α := EReal) (⊤, ⊥).2 ⊤)
  (h₃ : Ne (α := EReal) (⊤, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊥).2 0)
  (h₄ : Ne (α := EReal) (⊤, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊥).2 0),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, ⊥)
Tactic: induction y
Cleared hypotheses: y, h₁, h₂, h₃, h₄
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
h₁ : Ne (α := EReal) (⊤, y).1 0 ∨ (⊤, y).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊤, y).1 0 ∨ (⊤, y).2 ≠ ⊤
h₃ : Ne (α := EReal) (⊤, y).1 ⊥ ∨ (⊤, y).2 ≠ 0
h₄ : Ne (α := EReal) (⊤, y).1 ⊤ ∨ (⊤, y).2 ≠ 0
top :
  ∀ (h₁ : Ne (α := EReal) (⊤, ⊥).1 0 ∨ Ne (α := EReal) (⊤, ⊥).2 ⊥)
    (h₂ : Ne (α := EReal) (⊤, ⊥).1 0 ∨ Ne (α := EReal) (⊤, ⊥).2 ⊤)
    (h₃ : Ne (α := EReal) (⊤, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊥).2 0)
    (h₄ : Ne (α := EReal) (⊤, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊥).2 0),
    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 0 ∨ (⊤, (↑a : EReal)).2 ≠ ⊥)
  (h₂ : Ne (α := EReal) (⊤, (↑a : EReal)).1 0 ∨ (⊤, (↑a : EReal)).2 ≠ ⊤)
  (h₃ : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊥ ∨ (⊤, (↑a : EReal)).2 ≠ 0)
  (h₄ : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊤ ∨ (⊤, (↑a : EReal)).2 ≠ 0),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))
Tactic: induction y
Cleared hypotheses: y, h₁, h₂, h₃, h₄
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (goal)
Goal:
y : EReal
h₁ : Ne (α := EReal) (⊤, y).1 0 ∨ (⊤, y).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊤, y).1 0 ∨ (⊤, y).2 ≠ ⊤
h₃ : Ne (α := EReal) (⊤, y).1 ⊥ ∨ (⊤, y).2 ≠ 0
h₄ : Ne (α := EReal) (⊤, y).1 ⊤ ∨ (⊤, y).2 ≠ 0
top :
  ∀ (h₁ : Ne (α := EReal) (⊤, ⊥).1 0 ∨ Ne (α := EReal) (⊤, ⊥).2 ⊥)
    (h₂ : Ne (α := EReal) (⊤, ⊥).1 0 ∨ Ne (α := EReal) (⊤, ⊥).2 ⊤)
    (h₃ : Ne (α := EReal) (⊤, ⊥).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊥).2 0)
    (h₄ : Ne (α := EReal) (⊤, ⊥).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊥).2 0),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, ⊥)
top₁ :
  ∀ (a : ℝ) (h₁ : Ne (α := EReal) (⊤, (↑a : EReal)).1 0 ∨ (⊤, (↑a : EReal)).2 ≠ ⊥)
    (h₂ : Ne (α := EReal) (⊤, (↑a : EReal)).1 0 ∨ (⊤, (↑a : EReal)).2 ≠ ⊤)
    (h₃ : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊥ ∨ (⊤, (↑a : EReal)).2 ≠ 0)
    (h₄ : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊤ ∨ (⊤, (↑a : EReal)).2 ≠ 0),
    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 0 ∨ Ne (α := EReal) (⊤, ⊤).2 ⊥)
  (h₂ : Ne (α := EReal) (⊤, ⊤).1 0 ∨ Ne (α := EReal) (⊤, ⊤).2 ⊤)
  (h₃ : Ne (α := EReal) (⊤, ⊤).1 ⊥ ∨ Ne (α := EReal) (⊤, ⊤).2 0)
  (h₄ : Ne (α := EReal) (⊤, ⊤).1 ⊤ ∨ Ne (α := EReal) (⊤, ⊤).2 0),
  ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, ⊤)
Tactic: induction y
Cleared hypotheses: y, h₁, h₂, h₃, h₄
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
a : ℝ
h₁ : Ne (α := EReal) (⊥, (↑a : EReal)).1 0 ∨ (⊥, (↑a : EReal)).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊥, (↑a : EReal)).1 0 ∨ (⊥, (↑a : EReal)).2 ≠ ⊤
h₃ : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊥ ∨ (⊥, (↑a : EReal)).2 ≠ 0
h₄ : Ne (α := EReal) (⊥, (↑a : EReal)).1 ⊤ ∨ (⊥, (↑a : EReal)).2 ≠ 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊥, (↑a : EReal))
have h₅ : ¬a = 0
Tactic: simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₃
Cleared hypotheses: h₃