Theorem: ENat.tendsto_mul (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Tactic:
clear n ι β s α
State after:
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

State before:
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Tactic:
wlog h : b ≤ a with h'
State after:
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h' : ∀ {a b : ℕ∞}, a ≠ 0 ∨ b ≠ ⊤ → b ≠ 0 ∨ a ≠ ⊤ → b ≤ a → Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
h : ¬b ≤ a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : b ≤ a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

State before:
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : b ≤ a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Tactic:
obtain (rfl | ha') := eq_or_ne a ⊤
State after:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 (⊤ * b))

case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : b ≤ a
ha' : a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

State before:
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : b ≤ a
ha' : a ≠ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Tactic:
lift a to ℕ using ha'
State after:
case inr.intro
b : ℕ∞
a : ℕ
ha : ↑a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ↑a ≠ ⊤
h : b ≤ ↑a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, b)) (𝓝 (↑a * b))

State before:
case inr.intro
b : ℕ∞
a : ℕ
ha : ↑a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ↑a ≠ ⊤
h : b ≤ ↑a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, b)) (𝓝 (↑a * b))
Tactic:
lift b to ℕ using (h.trans_lt (WithTop.coe_lt_top a)).ne
State after:
case inr.intro.intro
a b : ℕ
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ↑a ≠ ⊤
h : ↑b ≤ ↑a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, ↑b)) (𝓝 (↑a * ↑b))

State before:
case inr.intro.intro
a b : ℕ
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ↑a ≠ ⊤
h : ↑b ≤ ↑a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (↑a, ↑b)) (𝓝 (↑a * ↑b))
Tactic:
rw [← Nat.cast_mul, nhds_cast_cast, nhds_cast_eq]
State after:
case inr.intro.intro
a b : ℕ
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ↑a ≠ ⊤
h : ↑b ≤ ↑a
⊢ Tendsto (fun p => p.1 * p.2) (𝓟 {(↑a, ↑b)}) (𝓟 {↑(a * b)})

State before:
case inr.intro.intro
a b : ℕ
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ↑a ≠ ⊤
h : ↑b ≤ ↑a
⊢ Tendsto (fun p => p.1 * p.2) (𝓟 {(↑a, ↑b)}) (𝓟 {↑(a * b)})
Tactic:
simp
State after:
no goals

State before:
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h' : ∀ {a b : ℕ∞}, a ≠ 0 ∨ b ≠ ⊤ → b ≠ 0 ∨ a ≠ ⊤ → b ≤ a → Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
h : ¬b ≤ a
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Tactic:
specialize h' hb ha (not_le.1 h).le
State after:
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : ¬b ≤ a
h' : Tendsto (fun p => p.1 * p.2) (𝓝 (b, a)) (𝓝 (b * a))
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

State before:
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : ¬b ≤ a
h' : Tendsto (fun p => p.1 * p.2) (𝓝 (b, a)) (𝓝 (b * a))
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
Tactic:
rw [nhds_swap a b, mul_comm, tendsto_map'_iff]
State after:
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : ¬b ≤ a
h' : Tendsto (fun p => p.1 * p.2) (𝓝 (b, a)) (𝓝 (b * a))
⊢ Tendsto ((fun p => p.1 * p.2) ∘ Prod.swap) (𝓝 (b, a)) (𝓝 (b * a))

State before:
case inr
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : ¬b ≤ a
h' : Tendsto (fun p => p.1 * p.2) (𝓝 (b, a)) (𝓝 (b * a))
⊢ Tendsto ((fun p => p.1 * p.2) ∘ Prod.swap) (𝓝 (b, a)) (𝓝 (b * a))
Tactic:
convert h'
State after:
case h.e'_3.h
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : ¬b ≤ a
h' : Tendsto (fun p => p.1 * p.2) (𝓝 (b, a)) (𝓝 (b * a))
x✝ : ℕ∞ × ℕ∞
⊢ ((fun p => p.1 * p.2) ∘ Prod.swap) x✝ = x✝.1 * x✝.2

State before:
case h.e'_3.h
a b : ℕ∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ a ≠ ⊤
h : ¬b ≤ a
h' : Tendsto (fun p => p.1 * p.2) (𝓝 (b, a)) (𝓝 (b * a))
x✝ : ℕ∞ × ℕ∞
⊢ ((fun p => p.1 * p.2) ∘ Prod.swap) x✝ = x✝.1 * x✝.2
Tactic:
simp [mul_comm]
State after:
no goals

State before:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
⊢ Tendsto (fun p => p.1 * p.2) (𝓝 (⊤, b)) (𝓝 (⊤ * b))
Tactic:
rw [top_mul (by simpa using hb), tendsto_nhds_top_iff]
State after:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
⊢ ∀ (x : ℕ), ∀ᶠ (a : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < a.1 * a.2

State before:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
⊢ ∀ (x : ℕ), ∀ᶠ (a : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < a.1 * a.2
Tactic:
intro x
State after:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
⊢ ∀ᶠ (a : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < a.1 * a.2

State before:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hforall : ∀ᶠ (c : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < c.1 ∧ 0 < c.2
⊢ ∀ᶠ (a : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < a.1 * a.2
Tactic:
refine hforall.mono ?_
State after:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hforall : ∀ᶠ (c : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < c.1 ∧ 0 < c.2
⊢ ∀ (x_1 : ℕ∞ × ℕ∞), ↑x < x_1.1 ∧ 0 < x_1.2 → ↑x < x_1.1 * x_1.2

State before:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hforall : ∀ᶠ (c : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < c.1 ∧ 0 < c.2
⊢ ∀ (x_1 : ℕ∞ × ℕ∞), ↑x < x_1.1 ∧ 0 < x_1.2 → ↑x < x_1.1 * x_1.2
Tactic:
simp only [and_imp, Prod.forall, ← ENat.one_le_iff_pos]
State after:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hforall : ∀ᶠ (c : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < c.1 ∧ 0 < c.2
⊢ ∀ (a b : ℕ∞), ↑x < a → 1 ≤ b → ↑x < a * b

State before:
case inl
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hforall : ∀ᶠ (c : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < c.1 ∧ 0 < c.2
⊢ ∀ (a b : ℕ∞), ↑x < a → 1 ≤ b → ↑x < a * b
Tactic:
exact fun y z hy hz ↦ hy.trans_le <| le_mul_of_one_le_right' hz
State after:
no goals

State before:
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
⊢ b ≠ 0
Tactic:
simpa using hb
State after:
no goals

State before:
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
⊢ ∀ᶠ (c : ℕ∞ × ℕ∞) in 𝓝 (⊤, b), ↑x < c.1 ∧ 0 < c.2
Tactic:
refine (lt_mem_nhds (show (x : ℕ∞) < ⊤ from WithTop.coe_lt_top x)).prod_nhds ?_
State after:
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 b, 0 < y

State before:
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 b, 0 < y
Tactic:
obtain (rfl | hbne) := eq_or_ne b ⊤
State after:
case inl
x : ℕ
ha hb : ⊤ ≠ 0 ∨ ⊤ ≠ ⊤
h : ⊤ ≤ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 ⊤, 0 < y

case inr
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hbne : b ≠ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 b, 0 < y

State before:
case inr
b : ℕ∞
ha : ⊤ ≠ 0 ∨ b ≠ ⊤
hb : b ≠ 0 ∨ ⊤ ≠ ⊤
h : b ≤ ⊤
x : ℕ
hbne : b ≠ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 b, 0 < y
Tactic:
lift b to ℕ using hbne
State after:
case inr.intro
x b : ℕ
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ⊤ ≠ ⊤
h : ↑b ≤ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 ↑b, 0 < y

State before:
case inr.intro
x b : ℕ
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ⊤ ≠ ⊤
h : ↑b ≤ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 ↑b, 0 < y
Tactic:
rw [nhds_cast_eq, principal_singleton, eventually_pure, Nat.cast_pos,
  ← Nat.ne_zero_iff_zero_lt]
State after:
case inr.intro
x b : ℕ
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ⊤ ≠ ⊤
h : ↑b ≤ ⊤
⊢ b ≠ 0

State before:
case inr.intro
x b : ℕ
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑b ≠ 0 ∨ ⊤ ≠ ⊤
h : ↑b ≤ ⊤
⊢ b ≠ 0
Tactic:
simpa using hb
State after:
no goals

State before:
case inl
x : ℕ
ha hb : ⊤ ≠ 0 ∨ ⊤ ≠ ⊤
h : ⊤ ≤ ⊤
⊢ ∀ᶠ (y : ℕ∞) in 𝓝 ⊤, 0 < y
Tactic:
apply lt_mem_nhds (by simp)
State after:
no goals

State before:
x : ℕ
ha hb : ⊤ ≠ 0 ∨ ⊤ ≠ ⊤
h : ⊤ ≤ ⊤
⊢ 0 < ⊤
Tactic:
simp
State after:
no goals