awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0
h : (↑a : ℝ≥0∞) ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ ∞
refine : ∀ᶠ (x : ℝ≥0∞ × ℝ≥0∞) in 𝓝 ((↑a : ℝ≥0∞), ∞), x.1 - x.2 = 0
⊢ Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) (𝓝 ((↑a : ℝ≥0∞), ∞)) (𝓝 0)

Tactic:
refine (tendsto_pure.2 ?_).mono_right (pure_le_nhds _)

Premises used: Iff.mpr, pure_le_nhds, Filter.tendsto_pure, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0
h : (↑a : ℝ≥0∞) ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ ∞
⊢ ∀ᶠ (x : ℝ≥0∞ × ℝ≥0∞) in 𝓝 ((↑a : ℝ≥0∞), ∞), x.1 - x.2 = 0

Tactic:
((gt_mem_nhds <| coe_lt_coe.2 <| lt_add_one a).prod_nhds
      (lt_mem_nhds <| @coe_lt_top (a + 1))).mono fun x hx =>
        tsub_eq_zero_iff_le.2 (hx.1.trans hx.2).le

Premises used: Iff.mpr, gt_mem_nhds, lt_add_one, ENNReal.coe_lt_coe, LT.lt.le, tsub_eq_zero_iff_le, Filter.Eventually.mono, And.right, And.left, LT.lt.trans, Filter.Eventually.prod_nhds, lt_mem_nhds, ENNReal.coe_lt_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0
h : (↑a : ℝ≥0∞) ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ ∞
⊢ ∀ᶠ (x : ℝ≥0∞ × ℝ≥0∞) in 𝓝 ((↑a : ℝ≥0∞), ∞), x.1 - x.2 = 0

Tactic:
exact ((gt_mem_nhds <| coe_lt_coe.2 <| lt_add_one a).prod_nhds
      (lt_mem_nhds <| @coe_lt_top (a + 1))).mono fun x hx =>
        tsub_eq_zero_iff_le.2 (hx.1.trans hx.2).le

Premises used: Iff.mpr, gt_mem_nhds, lt_add_one, ENNReal.coe_lt_coe, LT.lt.le, tsub_eq_zero_iff_le, Filter.Eventually.mono, And.right, And.left, LT.lt.trans, Filter.Eventually.prod_nhds, lt_mem_nhds, ENNReal.coe_lt_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ≥0
h : (↑a : ℝ≥0∞) ≠ ∞ ∨ (↑b : ℝ≥0∞) ≠ ∞
simp : Tendsto (fun (a : ℝ≥0 × ℝ≥0) ↦ a.1 - a.2) (𝓝 (a, b)) (𝓝 (a - b))
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) (𝓝 ((↑a : ℝ≥0∞), (↑b : ℝ≥0∞))) (𝓝 ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)))

Tactic:
simp only [nhds_coe_coe, tendsto_map'_iff, ← ENNReal.coe_sub, Function.comp_def, tendsto_coe]

Premises used: Filter.tendsto_map'_iff, ENNReal.tendsto_coe, Function.comp_def, ENNReal.coe_sub, ENNReal.nhds_coe_coe
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ≥0
h : (↑a : ℝ≥0∞) ≠ ∞ ∨ (↑b : ℝ≥0∞) ≠ ∞
⊢ Tendsto (fun (a : ℝ≥0 × ℝ≥0) ↦ a.1 - a.2) (𝓝 (a, b)) (𝓝 (a - b))

Tactic:
continuous_sub.tendsto (a, b)

Premises used: Prod.mk, Continuous.tendsto, ContinuousSub.continuous_sub
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ≥0
h : (↑a : ℝ≥0∞) ≠ ∞ ∨ (↑b : ℝ≥0∞) ≠ ∞
⊢ Tendsto (fun (a : ℝ≥0 × ℝ≥0) ↦ a.1 - a.2) (𝓝 (a, b)) (𝓝 (a - b))

Tactic:
exact continuous_sub.tendsto (a, b)

Premises used: Prod.mk, Continuous.tendsto, ContinuousSub.continuous_sub
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
ma mb : α → ℝ≥0∞
a b : ℝ≥0∞
hma : Tendsto ma f (𝓝 a)
hmb : Tendsto mb f (𝓝 b)
h : a ≠ ∞ ∨ b ≠ ∞
⊢ Tendsto (fun (a : α) ↦ ma a - mb a) f (𝓝 (a - b))

Tactic:
show Tendsto ((fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 - p.2) ∘ fun a => (ma a, mb a)) f (𝓝 (a - b)) from
    Tendsto.comp (ENNReal.tendsto_sub h) (hma.prodMk_nhds hmb)

Premises used: ENNReal.tendsto_sub, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b_1 : ℝ≥0∞
ha : a ≠ 0 ∨ b_1 ≠ ∞
hb_1 : b_1 ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
⊢ Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)

Tactic:
tendsto_nhds_top_iff_nnreal.2 fun n => ?_

Premises used: Iff.mpr, ENNReal.tendsto_nhds_top_iff_nnreal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b_1 : ℝ≥0∞
ha : a ≠ 0 ∨ b_1 ≠ ∞
hb_1 : b_1 ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
refine : ∀ (n : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) < a.1 * a.2
⊢ Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)

Tactic:
refine tendsto_nhds_top_iff_nnreal.2 fun n => ?_

Premises used: Iff.mpr, ENNReal.tendsto_nhds_top_iff_nnreal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b_1 : ℝ≥0∞
ha : a ≠ 0 ∨ b_1 ≠ ∞
hb_1 : b_1 ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
n : ℝ≥0
rcases :
  ∀ (ε : ℝ≥0) (hε : 0 < (↑ε : ℝ≥0∞)) (hεb : (↑ε : ℝ≥0∞) < b), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) < a.1 * a.2
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) < a.1 * a.2

Tactic:
rcases lt_iff_exists_nnreal_btwn.1 (pos_iff_ne_zero.2 hb) with ⟨ε, hε, hεb⟩

Premises used: Iff.mpr, ENNReal.lt_iff_exists_nnreal_btwn, Iff.mp, pos_iff_ne_zero
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b_1 : ℝ≥0∞
ha : a ≠ 0 ∨ b_1 ≠ ∞
hb_1 : b_1 ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < (↑ε : ℝ≥0∞)
hεb : (↑ε : ℝ≥0∞) < b
⊢ ∀ᶠ (c : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) / (↑ε : ℝ≥0∞) < c.1 ∧ (↑ε : ℝ≥0∞) < c.2

Tactic:
have : ∀ᶠ c : ℝ≥0∞ × ℝ≥0∞ in 𝓝 (∞, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2 :=
      (lt_mem_nhds <| div_lt_top coe_ne_top hε.ne').prod_nhds (lt_mem_nhds hεb)
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b_1 : ℝ≥0∞
ha : a ≠ 0 ∨ b_1 ≠ ∞
hb_1 : b_1 ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < (↑ε : ℝ≥0∞)
hεb : (↑ε : ℝ≥0∞) < b
this : ∀ᶠ (c : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) / (↑ε : ℝ≥0∞) < c.1 ∧ (↑ε : ℝ≥0∞) < c.2
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) < a.1 * a.2

Tactic:
this.mono fun c hc => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b_1 : ℝ≥0∞
ha : a ≠ 0 ∨ b_1 ≠ ∞
hb_1 : b_1 ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < (↑ε : ℝ≥0∞)
hεb : (↑ε : ℝ≥0∞) < b
this : ∀ᶠ (c : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) / (↑ε : ℝ≥0∞) < c.1 ∧ (↑ε : ℝ≥0∞) < c.2
refine : ∀ (c : ℝ≥0∞ × ℝ≥0∞) (hc : (↑n : ℝ≥0∞) / (↑ε : ℝ≥0∞) < c.1 ∧ (↑ε : ℝ≥0∞) < c.2), (↑n : ℝ≥0∞) < c.1 * c.2
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) < a.1 * a.2

Tactic:
refine this.mono fun c hc => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b_1 : ℝ≥0∞
ha : a ≠ 0 ∨ b_1 ≠ ∞
hb_1 : b_1 ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < (↑ε : ℝ≥0∞)
hεb : (↑ε : ℝ≥0∞) < b
this : ∀ᶠ (c : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) / (↑ε : ℝ≥0∞) < c.1 ∧ (↑ε : ℝ≥0∞) < c.2
c : ℝ≥0∞ × ℝ≥0∞
hc : (↑n : ℝ≥0∞) / (↑ε : ℝ≥0∞) < c.1 ∧ (↑ε : ℝ≥0∞) < c.2
⊢ (↑n : ℝ≥0∞) < c.1 * c.2

Tactic:
(ENNReal.div_mul_cancel hε.ne' coe_ne_top).symm.trans_lt (mul_lt_mul hc.1 hc.2)

Premises used: ENNReal.mul_lt_mul, ENNReal.div_mul_cancel, LT.lt.ne', And.right, And.left, Eq.trans_lt, Eq.symm, ENNReal.coe_ne_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b_1 : ℝ≥0∞
ha : a ≠ 0 ∨ b_1 ≠ ∞
hb_1 : b_1 ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < (↑ε : ℝ≥0∞)
hεb : (↑ε : ℝ≥0∞) < b
this : ∀ᶠ (c : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, b), (↑n : ℝ≥0∞) / (↑ε : ℝ≥0∞) < c.1 ∧ (↑ε : ℝ≥0∞) < c.2
c : ℝ≥0∞ × ℝ≥0∞
hc : (↑n : ℝ≥0∞) / (↑ε : ℝ≥0∞) < c.1 ∧ (↑ε : ℝ≥0∞) < c.2
⊢ (↑n : ℝ≥0∞) < c.1 * c.2

Tactic:
exact (ENNReal.div_mul_cancel hε.ne' coe_ne_top).symm.trans_lt (mul_lt_mul hc.1 hc.2)

Premises used: ENNReal.mul_lt_mul, ENNReal.div_mul_cancel, LT.lt.ne', And.right, And.left, Eq.trans_lt, Eq.symm, ENNReal.coe_ne_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ a ≠ ∞
⊢ ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)

Tactic:
have ht : ∀ b : ℝ≥0∞, b ≠ 0 →
      Tendsto (fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞) := fun b hb => by
    refine tendsto_nhds_top_iff_nnreal.2 fun n => ?_
    rcases lt_iff_exists_nnreal_btwn.1 (pos_iff_ne_zero.2 hb) with ⟨ε, hε, hεb⟩
    have : ∀ᶠ c : ℝ≥0∞ × ℝ≥0∞ in 𝓝 (∞, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2 :=
      (lt_mem_nhds <| div_lt_top coe_ne_top hε.ne').prod_nhds (lt_mem_nhds hεb)
    refine this.mono fun c hc => ?_
    exact (ENNReal.div_mul_cancel hε.ne' coe_ne_top).symm.trans_lt (mul_lt_mul hc.1 hc.2)
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
ha : Ne (α := ℝ≥0∞) ∞ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ Ne (α := ℝ≥0∞) ∞ ∞
⊢ ¬b = 0

Tactic:
simp only [ne_eq, or_false, not_true_eq_false] at hb

Premises used: not_true_eq_false, ne_eq, or_false
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
ha : Ne (α := ℝ≥0∞) ∞ 0 ∨ b ≠ ∞
hb : ¬b = 0
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 (∞ * b))

Tactic:
simp [ht b hb, top_mul hb]

Premises used: ENNReal.top_mul
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a_1 b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
a : ℝ≥0
ha : (↑a : ℝ≥0∞) ≠ 0 ∨ Ne (α := ℝ≥0∞) ∞ ∞
hb : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑a : ℝ≥0∞) ≠ ∞
⊢ ¬(↑a : ℝ≥0∞) = 0

Tactic:
simp only [ne_eq, or_false, not_true_eq_false] at ha

Premises used: not_true_eq_false, ne_eq, or_false
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a_1 b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
a : ℝ≥0
hb : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑a : ℝ≥0∞) ≠ ∞
ha : ¬(↑a : ℝ≥0∞) = 0
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 ((↑a : ℝ≥0∞), ∞)) (𝓝 ((↑a : ℝ≥0∞) * ∞))

Tactic:
simpa [Function.comp_def, mul_comm, mul_top ha]
        using (ht a ha).comp (continuous_swap.tendsto (ofNNReal a, ∞))

Premises used: ENNReal.ofNNReal, continuous_swap, Prod.mk, Continuous.tendsto, Function.comp_def, ENNReal.mul_top, mul_comm, Filter.Tendsto.comp, Top.top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a_1 b_1 : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
a b : ℝ≥0
ha : (↑a : ℝ≥0∞) ≠ 0 ∨ (↑b : ℝ≥0∞) ≠ ∞
hb : (↑b : ℝ≥0∞) ≠ 0 ∨ (↑a : ℝ≥0∞) ≠ ∞
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 ((↑a : ℝ≥0∞), (↑b : ℝ≥0∞))) (𝓝 ((↑a : ℝ≥0∞) * (↑b : ℝ≥0∞)))

Tactic:
simp only [nhds_coe_coe, ← coe_mul, tendsto_coe, tendsto_map'_iff, Function.comp_def,
        tendsto_mul]

Premises used: Filter.tendsto_map'_iff, ENNReal.coe_mul, ENNReal.tendsto_coe, Function.comp_def, tendsto_mul, ENNReal.nhds_coe_coe
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a_1 b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
a : ℝ≥0
ha : (↑a : ℝ≥0∞) ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ (↑a : ℝ≥0∞) ≠ ∞
coe :
  ∀ (ha : (↑a : ℝ≥0∞) ≠ 0 ∨ Ne (α := ℝ≥0∞) ∞ ∞) (hb : Ne (α := ℝ≥0∞) ∞ 0 ∨ (↑a : ℝ≥0∞) ≠ ∞),
    Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 ((↑a : ℝ≥0∞), ∞)) (𝓝 ((↑a : ℝ≥0∞) * ∞))
coe₁ :
  ∀ (b : ℝ≥0) (ha : (↑a : ℝ≥0∞) ≠ 0 ∨ (↑b : ℝ≥0∞) ≠ ∞) (hb : (↑b : ℝ≥0∞) ≠ 0 ∨ (↑a : ℝ≥0∞) ≠ ∞),
    Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 ((↑a : ℝ≥0∞), (↑b : ℝ≥0∞))) (𝓝 ((↑a : ℝ≥0∞) * (↑b : ℝ≥0∞)))
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 ((↑a : ℝ≥0∞), b)) (𝓝 ((↑a : ℝ≥0∞) * b))

Tactic:
induction b with
    | top =>
      simp only [ne_eq, or_false, not_true_eq_false] at ha
      simpa [Function.comp_def, mul_comm, mul_top ha]
        using (ht a ha).comp (continuous_swap.tendsto (ofNNReal a, ∞))
    | coe b =>
      simp only [nhds_coe_coe, ← coe_mul, tendsto_coe, tendsto_map'_iff, Function.comp_def,
        tendsto_mul]

Premises used: Filter.tendsto_map'_iff, not_true_eq_false, ne_eq, ENNReal.coe_mul, ENNReal.tendsto_coe, Function.comp_def, tendsto_mul, mul_comm, or_false, ENNReal.nhds_coe_coe
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ a ≠ ∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
top :
  ∀ (ha : Ne (α := ℝ≥0∞) ∞ 0 ∨ b ≠ ∞) (hb : b ≠ 0 ∨ Ne (α := ℝ≥0∞) ∞ ∞),
    Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 (∞ * b))
coe :
  ∀ (a : ℝ≥0) (ha : (↑a : ℝ≥0∞) ≠ 0 ∨ b ≠ ∞) (hb : b ≠ 0 ∨ (↑a : ℝ≥0∞) ≠ ∞),
    Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 ((↑a : ℝ≥0∞), b)) (𝓝 ((↑a : ℝ≥0∞) * b))
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

Tactic:
induction a with
  | top => simp only [ne_eq, or_false, not_true_eq_false] at hb; simp [ht b hb, top_mul hb]
  | coe a =>
    induction b with
    | top =>
      simp only [ne_eq, or_false, not_true_eq_false] at ha
      simpa [Function.comp_def, mul_comm, mul_top ha]
        using (ht a ha).comp (continuous_swap.tendsto (ofNNReal a, ∞))
    | coe b =>
      simp only [nhds_coe_coe, ← coe_mul, tendsto_coe, tendsto_map'_iff, Function.comp_def,
        tendsto_mul]

Premises used: Filter.tendsto_map'_iff, not_true_eq_false, ne_eq, ENNReal.coe_mul, ENNReal.tendsto_coe, Function.comp_def, tendsto_mul, mul_comm, or_false, ENNReal.nhds_coe_coe
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
ma mb : α → ℝ≥0∞
a b : ℝ≥0∞
hma : Tendsto ma f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ ∞
hmb : Tendsto mb f (𝓝 b)
hb : b ≠ 0 ∨ a ≠ ∞
⊢ Tendsto (fun (a : α) ↦ ma a * mb a) f (𝓝 (a * b))

Tactic:
show Tendsto ((fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 * p.2) ∘ fun a => (ma a, mb a)) f (𝓝 (a * b)) from
    Tendsto.comp (ENNReal.tendsto_mul ha hb) (hma.prodMk_nhds hmb)

Premises used: ENNReal.tendsto_mul, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : TopologicalSpace α
f g : α → ℝ≥0∞
s : Set α
hf : ContinuousOn f s
hg : ContinuousOn g s
h₁ : ∀ x ∈ s, f x ≠ 0 ∨ g x ≠ ∞
h₂ : ∀ x ∈ s, g x ≠ 0 ∨ f x ≠ ∞
⊢ ContinuousOn (Y := ℝ≥0∞) (fun (x : α) ↦ f x * g x) s

Tactic:
fun x hx =>
  ENNReal.Tendsto.mul (hf x hx) (h₁ x hx) (hg x hx) (h₂ x hx)

Premises used: ContinuousWithinAt, ENNReal.Tendsto.mul, ContinuousOn
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
inst : TopologicalSpace α
f g : α → ℝ≥0∞
hf : Continuous[inst, _] f
hg : Continuous[inst, _] g
h₁ : ∀ (x : α), f x ≠ 0 ∨ g x ≠ ∞
h₂ : ∀ (x : α), g x ≠ 0 ∨ f x ≠ ∞
⊢ Continuous[inst, _] fun (x : α) ↦ f x * g x

Tactic:
continuous_iff_continuousAt.2 fun x =>
    ENNReal.Tendsto.mul hf.continuousAt (h₁ x) hg.continuousAt (h₂ x)

Premises used: Iff.mpr, ENNReal.Tendsto.mul, Continuous.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ 0 ∨ a ≠ ∞
this : a = 0
⊢ Tendsto (fun (b : α) ↦ a * m b) f (𝓝 (a * b))

Tactic:
simp [this, tendsto_const_nhds]

Premises used: tendsto_const_nhds
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ ∞
⊢ Tendsto (fun (x : α) ↦ m x * b) f (𝓝 (a * b))

Tactic:
simpa only [mul_comm] using ENNReal.Tendsto.const_mul hm ha

Premises used: ENNReal.Tendsto.const_mul, mul_comm
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Tendsto (f i) x (𝓝 (a i))
h' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → a i ≠ ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ ∅, f c b) x (𝓝 (∏ c ∈ ∅, a c))

Tactic:
simp [tendsto_const_nhds]

Premises used: tendsto_const_nhds
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a_1 : ι
s : Finset ι
has : a_1 ∉ s
IH :
  ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
h : ∀ i ∈ Insert.insert a_1 s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ Insert.insert a_1 s, a i ≠ ∞
insert : Tendsto (fun (b : α) ↦ f a_1 b * ∏ c ∈ s, f c b) x (𝓝 (a a_1 * ∏ c ∈ s, a c))
⊢ Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ Insert.insert a_1 s, f c b) x (𝓝 (∏ c ∈ Insert.insert a_1 s, a c))

Tactic:
simp only [Finset.prod_insert has]

Premises used: Finset.prod_insert
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a_1 : ι
s : Finset ι
has : a_1 ∉ s
IH :
  ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
h : ∀ i ∈ Insert.insert a_1 s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ Insert.insert a_1 s, a i ≠ ∞
insert : a a_1 ≠ 0 ∨ Ne (α := ℝ≥0∞) (∏ c ∈ s, a c) ∞
insert₁ : Tendsto (β := ℝ≥0∞) (fun (a : α) ↦ ∏ c ∈ s, f c a) x (𝓝 (∏ c ∈ s, a c))
insert₂ : Ne (α := ℝ≥0∞) (∏ c ∈ s, a c) 0 ∨ a a_1 ≠ ∞
⊢ Tendsto (fun (b : α) ↦ f a_1 b * ∏ c ∈ s, f c b) x (𝓝 (a a_1 * ∏ c ∈ s, a c))

Tactic:
apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))

Premises used: ENNReal.Tendsto.mul, Finset.mem_insert_self
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a_1 : ι
s : Finset ι
has : a_1 ∉ s
IH :
  ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
h : ∀ i ∈ Insert.insert a_1 s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ Insert.insert a_1 s, a i ≠ ∞
insert : Ne (α := ℝ≥0∞) (∏ c ∈ s, a c) ∞
⊢ a a_1 ≠ 0 ∨ Ne (α := ℝ≥0∞) (∏ c ∈ s, a c) ∞

Tactic:
right
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a_1 : ι
s : Finset ι
has : a_1 ∉ s
IH :
  ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
h : ∀ i ∈ insert a_1 s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a_1 s, a i ≠ ∞
⊢ Ne (α := ℝ≥0∞) (∏ c ∈ s, a c) ∞

Tactic:
prod_ne_top fun i hi => h' _ (Finset.mem_insert_of_mem hi)

Premises used: ENNReal.prod_ne_top, Finset.mem_insert_of_mem
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a_1 : ι
s : Finset ι
has : a_1 ∉ s
IH :
  ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
h : ∀ i ∈ insert a_1 s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a_1 s, a i ≠ ∞
⊢ Ne (α := ℝ≥0∞) (∏ c ∈ s, a c) ∞

Tactic:
exact prod_ne_top fun i hi => h' _ (Finset.mem_insert_of_mem hi)

Premises used: ENNReal.prod_ne_top, Finset.mem_insert_of_mem
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a_1 : ι
s : Finset ι
has : a_1 ∉ s
IH :
  ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
h : ∀ i ∈ insert a_1 s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a_1 s, a i ≠ ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (a : α) ↦ ∏ c ∈ s, f c a) x (𝓝 (∏ c ∈ s, a c))

Tactic:
IH (fun i hi => h _ (Finset.mem_insert_of_mem hi)) fun i hi =>
        h' _ (Finset.mem_insert_of_mem hi)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a_1 : ι
s : Finset ι
has : a_1 ∉ s
IH :
  ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
h : ∀ i ∈ insert a_1 s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a_1 s, a i ≠ ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (a : α) ↦ ∏ c ∈ s, f c a) x (𝓝 (∏ c ∈ s, a c))

Tactic:
exact IH (fun i hi => h _ (Finset.mem_insert_of_mem hi)) fun i hi =>
        h' _ (Finset.mem_insert_of_mem hi)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a_1 : ι
s : Finset ι
has : a_1 ∉ s
IH :
  ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
h : ∀ i ∈ insert a_1 s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a_1 s, a i ≠ ∞
⊢ Ne (α := ℝ≥0∞) (∏ c ∈ s, a c) 0 ∨ a a_1 ≠ ∞

Tactic:
Or.inr (h' _ (Finset.mem_insert_self _ _))

Premises used: Finset.mem_insert_self, Or.inr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a_1 : ι
s : Finset ι
has : a_1 ∉ s
IH :
  ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
h : ∀ i ∈ insert a_1 s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a_1 s, a i ≠ ∞
⊢ Ne (α := ℝ≥0∞) (∏ c ∈ s, a c) 0 ∨ a a_1 ≠ ∞

Tactic:
exact Or.inr (h' _ (Finset.mem_insert_self _ _))

Premises used: Finset.mem_insert_self, Or.inr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
s : Finset ι
h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ s, a i ≠ ∞
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Tendsto (f i) x (𝓝 (a i)))
    (h' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ ∅, f c b) x (𝓝 (∏ c ∈ ∅, a c))
insert :
  ∀ (a_1 : ι) (s : Finset ι) (has : a_1 ∉ s)
    (IH :
      ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
        Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c)))
    (h : ∀ i ∈ Insert.insert a_1 s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ Insert.insert a_1 s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ Insert.insert a_1 s, f c b) x (𝓝 (∏ c ∈ Insert.insert a_1 s, a c))
⊢ Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))

Tactic:
induction s using Finset.induction with
  | empty => simp [tendsto_const_nhds]
  | insert _ _ has IH =>
    simp only [Finset.prod_insert has]
    apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))
    · right
      exact prod_ne_top fun i hi => h' _ (Finset.mem_insert_of_mem hi)
    · exact IH (fun i hi => h _ (Finset.mem_insert_of_mem hi)) fun i hi =>
        h' _ (Finset.mem_insert_of_mem hi)
    · exact Or.inr (h' _ (Finset.mem_insert_self _ _))

Premises used: ENNReal.Tendsto.mul, tendsto_const_nhds, Insert.insert, ENNReal.prod_ne_top, Or.inr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
s : Finset ι
h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ s, a i ≠ ∞
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Tendsto (f i) x (𝓝 (a i)))
    (h' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ ∅, f c b) x (𝓝 (∏ c ∈ ∅, a c))
insert :
  ∀ (a_1 : ι) (s : Finset ι) (has : a_1 ∉ s)
    (IH :
      ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
        Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c)))
    (h : ∀ i ∈ Insert.insert a_1 s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ Insert.insert a_1 s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ Insert.insert a_1 s, f c b) x (𝓝 (∏ c ∈ Insert.insert a_1 s, a c))
⊢ Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp [tendsto_const_nhds]
  | insert _ _ has IH =>
    simp only [Finset.prod_insert has]
    apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))
    · right
      exact prod_ne_top fun i hi => h' _ (Finset.mem_insert_of_mem hi)
    · exact IH (fun i hi => h _ (Finset.mem_insert_of_mem hi)) fun i hi =>
        h' _ (Finset.mem_insert_of_mem hi)
    · exact Or.inr (h' _ (Finset.mem_insert_self _ _))

Premises used: ENNReal.Tendsto.mul, tendsto_const_nhds, Insert.insert, ENNReal.prod_ne_top, Or.inr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ≥0∞
h : a ≠ ∞ ∨ b ≠ 0
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ a * x) b

Tactic:
Tendsto.const_mul tendsto_id h.symm

Premises used: ContinuousAt, Filter.tendsto_id, ENNReal.Tendsto.const_mul, Or.symm
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ≥0∞
h : a ≠ ∞ ∨ b ≠ 0
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ x * a) b

Tactic:
Tendsto.mul_const tendsto_id h.symm

Premises used: ENNReal.Tendsto.mul_const, ContinuousAt, Filter.tendsto_id, Or.symm
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ a * x

Tactic:
continuous_iff_continuousAt.2 fun _ => ENNReal.continuousAt_const_mul (Or.inl ha)

Premises used: Iff.mpr, ENNReal.continuousAt_const_mul, Or.inl, continuous_iff_continuousAt