-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_mul (ha : a ≠ 0 ∨ b ≠ ∞) (hb : b ≠ 0 ∨ a ≠ ∞) :
    Tendsto (fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

Proof state:
case intro.intro
a b✝ : ℝ≥0∞
ha : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : b✝ ≠ 0 ∨ a ≠ ⊤
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < ↑ε
hεb : ↑ε < b
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, b), ↑n < a.1 * a.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)

Result:
case intro.intro
a b✝ : ℝ≥0∞
ha : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : b✝ ≠ 0 ∨ a ≠ ⊤
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < ↑ε
hεb : ↑ε < b
this : ∀ᶠ (c : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, b), ↑n < a.1 * a.2

Proof state:
case coe.top
a✝ b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 ⊤)
a : ℝ≥0
hb : ⊤ ≠ 0 ∨ ↑a ≠ ⊤
ha : ¬↑a = 0
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, ⊤)) (𝓝 (↑a * ⊤))

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

Result:
no goals

Proof state:
case coe
a✝ b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 ⊤)
a : ℝ≥0
ha : ↑a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ↑a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, b)) (𝓝 (↑a * 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]

Result:
no goals

Proof state:
a b✝ : ℝ≥0∞
ha : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : b✝ ≠ 0 ∨ a ≠ ⊤
b : ℝ≥0∞
hb : b ≠ 0
n : ℝ≥0
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, b), ↑n < a.1 * a.2

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

Result:
case intro.intro
a b✝ : ℝ≥0∞
ha : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : b✝ ≠ 0 ∨ a ≠ ⊤
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < ↑ε
hεb : ↑ε < b
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, b), ↑n < a.1 * a.2

Proof state:
a b✝ : ℝ≥0∞
ha : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : b✝ ≠ 0 ∨ a ≠ ⊤
b : ℝ≥0∞
hb : b ≠ 0
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 ⊤)

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

Result:
a b✝ : ℝ≥0∞
ha : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : b✝ ≠ 0 ∨ a ≠ ⊤
b : ℝ≥0∞
hb : b ≠ 0
n : ℝ≥0
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, b), ↑n < a.1 * a.2

Proof state:
case top
a b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 ⊤)
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : ¬b = 0
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 (⊤ * b))

Tactic:
simp [ht b hb, top_mul hb]

Result:
no goals

Proof state:
case top
a b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 ⊤)
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 (⊤ * b))

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

Result:
case top
a b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 ⊤)
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : ¬b = 0
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 (⊤ * b))

Proof state:
case intro.intro
a b✝ : ℝ≥0∞
ha : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : b✝ ≠ 0 ∨ a ≠ ⊤
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < ↑ε
hεb : ↑ε < b
this : ∀ᶠ (c : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2
⊢ ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, b), ↑n < a.1 * a.2

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

Result:
case intro.intro
a b✝ : ℝ≥0∞
ha : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : b✝ ≠ 0 ∨ a ≠ ⊤
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < ↑ε
hεb : ↑ε < b
this : ∀ᶠ (c : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2
c : ℝ≥0∞ × ℝ≥0∞
hc : ↑n / ↑ε < c.1 ∧ ↑ε < c.2
⊢ ↑n < c.1 * c.2

Proof state:
a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 ⊤)
⊢ Tendsto (fun p => 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]

Result:
no goals

Proof state:
case coe.top
a✝ b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 ⊤)
a : ℝ≥0
ha : ↑a ≠ 0 ∨ ⊤ ≠ ⊤
hb : ⊤ ≠ 0 ∨ ↑a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, ⊤)) (𝓝 (↑a * ⊤))

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

Result:
case coe.top
a✝ b : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 ⊤)
a : ℝ≥0
hb : ⊤ ≠ 0 ∨ ↑a ≠ ⊤
ha : ¬↑a = 0
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, ⊤)) (𝓝 (↑a * ⊤))

Proof state:
case coe.coe
a✝ b✝ : ℝ≥0∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 ⊤)
a b : ℝ≥0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ↑a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, ↑b)) (𝓝 (↑a * ↑b))

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

Result:
no goals

Proof state:
a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * 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)

Result:
a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 ⊤)
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

Proof state:
case intro.intro
a b✝ : ℝ≥0∞
ha : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : b✝ ≠ 0 ∨ a ≠ ⊤
b : ℝ≥0∞
hb : b ≠ 0
n ε : ℝ≥0
hε : 0 < ↑ε
hεb : ↑ε < b
this : ∀ᶠ (c : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2
c : ℝ≥0∞ × ℝ≥0∞
hc : ↑n / ↑ε < c.1 ∧ ↑ε < c.2
⊢ ↑n < 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)

Result:
no goals