case empty
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
s : Finset ι
h✝ : ∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a i))
h'✝ : ∀ (i : ι), i ∈ s → a i ≠ ⊤
h : ∀ (i : ι), i ∈ ∅ → Tendsto (f i) x (𝓝 (a i))
h' : ∀ (i : ι), i ∈ ∅ → a i ≠ ⊤
⊢ Tendsto (fun b => ∏ c in ∅, f c b) x (𝓝 (∏ c in ∅, a c))

case insert
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝¹ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a✝ : ι → ℝ≥0∞
s✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ s✝ → Tendsto (f i) x (𝓝 (a✝ i))
h'✝ : ∀ (i : ι), i ∈ s✝ → a✝ i ≠ ⊤
a : ι
s : Finset ι
has : ¬a ∈ s
IH :
  (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a✝ i))) →
    (∀ (i : ι), i ∈ s → a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c in s, f c b) x (𝓝 (∏ c in s, a✝ c))
h : ∀ (i : ι), i ∈ insert a s → Tendsto (f i) x (𝓝 (a✝ i))
h' : ∀ (i : ι), i ∈ insert a s → a✝ i ≠ ⊤
⊢ Tendsto (fun b => ∏ c in insert a s, f c b) x (𝓝 (∏ c in insert a s, a✝ c))
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
s : Finset ι
h : ∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a i))
h' : ∀ (i : ι), i ∈ s → a i ≠ ⊤
⊢ Tendsto (fun b => ∏ c in s, f c b) x (𝓝 (∏ c in s, a c))
induction' s using Finset.induction with a s has IH
case insert
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝¹ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a✝ : ι → ℝ≥0∞
s✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ s✝ → Tendsto (f i) x (𝓝 (a✝ i))
h'✝ : ∀ (i : ι), i ∈ s✝ → a✝ i ≠ ⊤
a : ι
s : Finset ι
has : ¬a ∈ s
IH :
  (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a✝ i))) →
    (∀ (i : ι), i ∈ s → a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c in s, f c b) x (𝓝 (∏ c in s, a✝ c))
h : ∀ (i : ι), i ∈ insert a s → Tendsto (f i) x (𝓝 (a✝ i))
h' : ∀ (i : ι), i ∈ insert a s → a✝ i ≠ ⊤
⊢ Tendsto (fun b => f a b * ∏ c in s, f c b) x (𝓝 (a✝ a * ∏ c in s, a✝ c))
case insert
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝¹ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a✝ : ι → ℝ≥0∞
s✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ s✝ → Tendsto (f i) x (𝓝 (a✝ i))
h'✝ : ∀ (i : ι), i ∈ s✝ → a✝ i ≠ ⊤
a : ι
s : Finset ι
has : ¬a ∈ s
IH :
  (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a✝ i))) →
    (∀ (i : ι), i ∈ s → a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c in s, f c b) x (𝓝 (∏ c in s, a✝ c))
h : ∀ (i : ι), i ∈ insert a s → Tendsto (f i) x (𝓝 (a✝ i))
h' : ∀ (i : ι), i ∈ insert a s → a✝ i ≠ ⊤
⊢ Tendsto (fun b => ∏ c in insert a s, f c b) x (𝓝 (∏ c in insert a s, a✝ c))
simp only [Finset.prod_insert has]
case insert.ha
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝¹ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a✝ : ι → ℝ≥0∞
s✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ s✝ → Tendsto (f i) x (𝓝 (a✝ i))
h'✝ : ∀ (i : ι), i ∈ s✝ → a✝ i ≠ ⊤
a : ι
s : Finset ι
has : ¬a ∈ s
IH :
  (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a✝ i))) →
    (∀ (i : ι), i ∈ s → a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c in s, f c b) x (𝓝 (∏ c in s, a✝ c))
h : ∀ (i : ι), i ∈ insert a s → Tendsto (f i) x (𝓝 (a✝ i))
h' : ∀ (i : ι), i ∈ insert a s → a✝ i ≠ ⊤
⊢ a✝ a ≠ 0 ∨ ∏ c in s, a✝ c ≠ ⊤

case insert.hmb
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝¹ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a✝ : ι → ℝ≥0∞
s✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ s✝ → Tendsto (f i) x (𝓝 (a✝ i))
h'✝ : ∀ (i : ι), i ∈ s✝ → a✝ i ≠ ⊤
a : ι
s : Finset ι
has : ¬a ∈ s
IH :
  (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a✝ i))) →
    (∀ (i : ι), i ∈ s → a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c in s, f c b) x (𝓝 (∏ c in s, a✝ c))
h : ∀ (i : ι), i ∈ insert a s → Tendsto (f i) x (𝓝 (a✝ i))
h' : ∀ (i : ι), i ∈ insert a s → a✝ i ≠ ⊤
⊢ Tendsto (fun a => ∏ c in s, f c a) x (𝓝 (∏ c in s, a✝ c))

case insert.hb
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝¹ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a✝ : ι → ℝ≥0∞
s✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ s✝ → Tendsto (f i) x (𝓝 (a✝ i))
h'✝ : ∀ (i : ι), i ∈ s✝ → a✝ i ≠ ⊤
a : ι
s : Finset ι
has : ¬a ∈ s
IH :
  (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a✝ i))) →
    (∀ (i : ι), i ∈ s → a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c in s, f c b) x (𝓝 (∏ c in s, a✝ c))
h : ∀ (i : ι), i ∈ insert a s → Tendsto (f i) x (𝓝 (a✝ i))
h' : ∀ (i : ι), i ∈ insert a s → a✝ i ≠ ⊤
⊢ ∏ c in s, a✝ c ≠ 0 ∨ a✝ a ≠ ⊤
case insert
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝¹ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a✝ : ι → ℝ≥0∞
s✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ s✝ → Tendsto (f i) x (𝓝 (a✝ i))
h'✝ : ∀ (i : ι), i ∈ s✝ → a✝ i ≠ ⊤
a : ι
s : Finset ι
has : ¬a ∈ s
IH :
  (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a✝ i))) →
    (∀ (i : ι), i ∈ s → a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c in s, f c b) x (𝓝 (∏ c in s, a✝ c))
h : ∀ (i : ι), i ∈ insert a s → Tendsto (f i) x (𝓝 (a✝ i))
h' : ∀ (i : ι), i ∈ insert a s → a✝ i ≠ ⊤
⊢ Tendsto (fun b => f a b * ∏ c in s, f c b) x (𝓝 (a✝ a * ∏ c in s, a✝ c))
apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))
no goals
case empty
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
s : Finset ι
h✝ : ∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a i))
h'✝ : ∀ (i : ι), i ∈ s → a i ≠ ⊤
h : ∀ (i : ι), i ∈ ∅ → Tendsto (f i) x (𝓝 (a i))
h' : ∀ (i : ι), i ∈ ∅ → a i ≠ ⊤
⊢ Tendsto (fun b => ∏ c in ∅, f c b) x (𝓝 (∏ c in ∅, a c))
simp [tendsto_const_nhds]
case insert.ha.h
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝¹ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a✝ : ι → ℝ≥0∞
s✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ s✝ → Tendsto (f i) x (𝓝 (a✝ i))
h'✝ : ∀ (i : ι), i ∈ s✝ → a✝ i ≠ ⊤
a : ι
s : Finset ι
has : ¬a ∈ s
IH :
  (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a✝ i))) →
    (∀ (i : ι), i ∈ s → a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c in s, f c b) x (𝓝 (∏ c in s, a✝ c))
h : ∀ (i : ι), i ∈ insert a s → Tendsto (f i) x (𝓝 (a✝ i))
h' : ∀ (i : ι), i ∈ insert a s → a✝ i ≠ ⊤
⊢ ∏ c in s, a✝ c ≠ ⊤
case insert.ha
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝¹ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a✝ : ι → ℝ≥0∞
s✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ s✝ → Tendsto (f i) x (𝓝 (a✝ i))
h'✝ : ∀ (i : ι), i ∈ s✝ → a✝ i ≠ ⊤
a : ι
s : Finset ι
has : ¬a ∈ s
IH :
  (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a✝ i))) →
    (∀ (i : ι), i ∈ s → a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c in s, f c b) x (𝓝 (∏ c in s, a✝ c))
h : ∀ (i : ι), i ∈ insert a s → Tendsto (f i) x (𝓝 (a✝ i))
h' : ∀ (i : ι), i ∈ insert a s → a✝ i ≠ ⊤
⊢ a✝ a ≠ 0 ∨ ∏ c in s, a✝ c ≠ ⊤
right
no goals
case insert.ha.h
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝¹ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a✝ : ι → ℝ≥0∞
s✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ s✝ → Tendsto (f i) x (𝓝 (a✝ i))
h'✝ : ∀ (i : ι), i ∈ s✝ → a✝ i ≠ ⊤
a : ι
s : Finset ι
has : ¬a ∈ s
IH :
  (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a✝ i))) →
    (∀ (i : ι), i ∈ s → a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c in s, f c b) x (𝓝 (∏ c in s, a✝ c))
h : ∀ (i : ι), i ∈ insert a s → Tendsto (f i) x (𝓝 (a✝ i))
h' : ∀ (i : ι), i ∈ insert a s → a✝ i ≠ ⊤
⊢ ∏ c in s, a✝ c ≠ ⊤
exact (prod_lt_top fun i hi => h' _ (Finset.mem_insert_of_mem hi)).ne
no goals
case insert.hmb
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝¹ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a✝ : ι → ℝ≥0∞
s✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ s✝ → Tendsto (f i) x (𝓝 (a✝ i))
h'✝ : ∀ (i : ι), i ∈ s✝ → a✝ i ≠ ⊤
a : ι
s : Finset ι
has : ¬a ∈ s
IH :
  (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a✝ i))) →
    (∀ (i : ι), i ∈ s → a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c in s, f c b) x (𝓝 (∏ c in s, a✝ c))
h : ∀ (i : ι), i ∈ insert a s → Tendsto (f i) x (𝓝 (a✝ i))
h' : ∀ (i : ι), i ∈ insert a s → a✝ i ≠ ⊤
⊢ Tendsto (fun a => ∏ c in s, f c a) x (𝓝 (∏ c in s, a✝ c))
exact IH (fun i hi => h _ (Finset.mem_insert_of_mem hi)) fun i hi =>
  h' _ (Finset.mem_insert_of_mem hi)
no goals
case insert.hb
α : Type u_2
β : Type ?u.99181
γ : Type ?u.99184
a✝¹ b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
ι : Type u_1
f : ι → α → ℝ≥0∞
x : Filter α
a✝ : ι → ℝ≥0∞
s✝ : Finset ι
h✝ : ∀ (i : ι), i ∈ s✝ → Tendsto (f i) x (𝓝 (a✝ i))
h'✝ : ∀ (i : ι), i ∈ s✝ → a✝ i ≠ ⊤
a : ι
s : Finset ι
has : ¬a ∈ s
IH :
  (∀ (i : ι), i ∈ s → Tendsto (f i) x (𝓝 (a✝ i))) →
    (∀ (i : ι), i ∈ s → a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c in s, f c b) x (𝓝 (∏ c in s, a✝ c))
h : ∀ (i : ι), i ∈ insert a s → Tendsto (f i) x (𝓝 (a✝ i))
h' : ∀ (i : ι), i ∈ insert a s → a✝ i ≠ ⊤
⊢ ∏ c in s, a✝ c ≠ 0 ∨ a✝ a ≠ ⊤
exact Or.inr (h' _ (Finset.mem_insert_self _ _))