awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Basic (goal)
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : 0 ≤ a
hb : 0 ≤ b
pos : p → 0 ≤ if p then a else b
⊢ 0 ≤ if p then a else b
have neg : ¬p → 0 ≤ if p then a else b
Tactic: by_cases p
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Basic (goal)
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ (if p then a else b) ≠ 0
have pos : p → (if p then a else b) ≠ 0
Tactic: by_cases p
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Basic (goal)
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
pos : p → (if p then a else b) ≠ 0
⊢ (if p then a else b) ≠ 0
have neg : ¬p → (if p then a else b) ≠ 0
Tactic: by_cases p
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Basic (goal)
Goal:
a : ℤ
ha : 0 < a
⊢ 0 < a / a
have rw : LT.lt (α := ℤ) 0 1
Tactic: rw [Int.ediv_self ha.ne']
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : DecidableEq β
b : β
a : α
⊢ HasProd (Pi.mulSingle (M := fun (a : β) ↦ α) b a) a
have h : ∀ (x : β), Pi.mulSingle (M := fun (a : β) ↦ α) b a x = if x = b then a else 1
Tactic: convert! hasProd_ite_eq (L := .unconditional β) b a
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : DecidableEq β
b : β
a : α
⊢ ∏' (b' : β), Pi.mulSingle (M := fun (a : β) ↦ α) b a b' = a
have rw : Pi.mulSingle (M := fun (a : β) ↦ α) b a b = a
Tactic: rw [tprod_eq_mulSingle b]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : DecidableEq β
b : β
a : α
rw : Pi.mulSingle (M := fun (a : β) ↦ α) b a b = a
⊢ ∏' (b' : β), Pi.mulSingle (M := fun (a : β) ↦ α) b a b' = a
have rw₁ : ∀ (b' : β), b' ≠ b → Eq.{u_1 + 1} (α := α) (Pi.mulSingle (M := fun (a : β) ↦ α) b a b' : α) (1 : α)
Tactic: rw [tprod_eq_mulSingle b]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
b : β
t : Set γ
f : β × γ → α
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑(SProd.sprod (α := Set β) {b} t) : Type (max u_3 u_2))), f (↑x : β × γ))
    (∏' (c : (↑t : Type u_3)), f (b, (↑c : γ)))
have rw : Eq.{u_1 + 1} (α := α) (∏' (x : (↑(Prod.mk b '' t) : Type (max u_3 u_2))), f (↑x : β × γ))
  (∏' (c : (↑t : Type u_3)), f (b, (↑c : γ)))
Tactic: rw [tprod_congr_set_coe _ Set.singleton_prod, tprod_image _ (Prod.mk_right_injective b).injOn]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
b : β
t : Set γ
f : β × γ → α
rw :
  Eq.{u_1 + 1} (α := α) (∏' (x : (↑(Prod.mk b '' t) : Type (max u_3 u_2))), f (↑x : β × γ))
    (∏' (c : (↑t : Type u_3)), f (b, (↑c : γ)))
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑(SProd.sprod (α := Set β) {b} t) : Type (max u_3 u_2))), f (↑x : β × γ))
    (∏' (c : (↑t : Type u_3)), f (b, (↑c : γ)))
have rw₁ : Eq.{u_1 + 1} (α := α) (∏' (x : (↑t : Type u_3)), f (b, (↑x : γ))) (∏' (c : (↑t : Type u_3)), f (b, (↑c : γ)))
Tactic: rw [tprod_congr_set_coe _ Set.singleton_prod, tprod_image _ (Prod.mk_right_injective b).injOn]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Set β
c : γ
f : β × γ → α
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑(SProd.sprod (β := Set γ) s {c}) : Type (max u_2 u_3))), f (↑x : β × γ))
    (∏' (b : (↑s : Type u_2)), f ((↑b : β), c))
have rw : Eq.{u_1 + 1} (α := α) (∏' (x : (↑((fun (a : β) ↦ (a, c)) '' s) : Type (max u_3 u_2))), f (↑x : β × γ))
  (∏' (b : (↑s : Type u_2)), f ((↑b : β), c))
Tactic: rw [tprod_congr_set_coe _ Set.prod_singleton, tprod_image _ (Prod.mk_left_injective c).injOn]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Set β
c : γ
f : β × γ → α
rw :
  Eq.{u_1 + 1} (α := α) (∏' (x : (↑((fun (a : β) ↦ (a, c)) '' s) : Type (max u_3 u_2))), f (↑x : β × γ))
    (∏' (b : (↑s : Type u_2)), f ((↑b : β), c))
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑(SProd.sprod (β := Set γ) s {c}) : Type (max u_2 u_3))), f (↑x : β × γ))
    (∏' (b : (↑s : Type u_2)), f ((↑b : β), c))
have rw₁ : Eq.{u_1 + 1} (α := α) (∏' (x : (↑s : Type u_2)), f ((↑x : β), c)) (∏' (b : (↑s : Type u_2)), f ((↑b : β), c))
Tactic: rw [tprod_congr_set_coe _ Set.prod_singleton, tprod_image _ (Prod.mk_left_injective c).injOn]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_4
β : Type u_5
M : Type u_6
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ Tendsto (α := Prod.{u_4, u_5} (Finset α) (Finset β))
    ((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘
      (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
    (Filter.map (α := Finset (α ⊕ β)) (⇑sumEquiv : (a : Finset (α ⊕ β)) → Finset α × Finset β) atTop) (𝓝 (a * b))
have rw : Tendsto
  ((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘ (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
  (SProd.sprod (α := Filter (Finset α)) (β := Filter (Finset β)) atTop atTop) (𝓝 (a * b))
Tactic: rw [Finset.sumEquiv.map_atTop, ← prod_atTop_atTop_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_4
β : Type u_5
M : Type u_6
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ Tendsto
    ((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘
      (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
    (SProd.sprod (α := Filter (Finset α)) (β := Filter (Finset β)) atTop atTop) (𝓝 (a * b))
have h : Eq (α := Prod.{u_4, u_5} (Finset α) (Finset β) → M)
  ((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘ (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
  ((fun (p : M × M) ↦ p.1 * p.2) ∘
    Prod.map (fun (s : Finset α) ↦ ∏ b ∈ s, (f ∘ Sum.inl) b) fun (s : Finset β) ↦ ∏ b ∈ s, (f ∘ Sum.inr) b)
Tactic: convert! (tendsto_mul.comp (nhds_prod_eq (x := a) (y := b) ▸ Tendsto.prodMap h₁ h₂))
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_4
β : Type u_5
M : Type u_6
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ Eq (α := Prod.{u_4, u_5} (Finset α) (Finset β) → M)
    ((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘
      (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
    ((fun (p : M × M) ↦ p.1 * p.2) ∘
      Prod.map (fun (s : Finset α) ↦ ∏ b ∈ s, (f ∘ Sum.inl) b) fun (s : Finset β) ↦ ∏ b ∈ s, (f ∘ Sum.inr) b)
have h : ∀ (s : Prod.{u_4, u_5} (Finset α) (Finset β)),
  Eq.{u_6 + 1} (α := M)
    (((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘
        (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
      s)
    (((fun (p : M × M) ↦ p.1 * p.2) ∘
        Prod.map (fun (s : Finset α) ↦ ∏ b ∈ s, (f ∘ Sum.inl) b) fun (s : Finset β) ↦ ∏ b ∈ s, (f ∘ Sum.inr) b)
      s)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (hypothesis)
Goal:
α : Type u_4
β : Type u_5
M : Type u_6
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ HasProd f (a * b)
have this : Tendsto (α := Prod.{u_4, u_5} (Finset α) (Finset β))
  ((fun (x : Finset (α ⊕ β)) ↦ ∏ b ∈ x, f b) ∘ (⇑(OrderIso.symm sumEquiv) : (a : Finset α × Finset β) → Finset (α ⊕ β)))
  (Filter.map (α := Finset (α ⊕ β)) (⇑sumEquiv : (a : Finset (α ⊕ β)) → Finset α × Finset β) atTop) (𝓝 (a * b))
Tactic: have : Tendsto ((∏ b ∈ ·, f b) ∘ sumEquiv.symm) (atTop.map sumEquiv) (nhds (a * b)) := by
    rw [Finset.sumEquiv.map_atTop, ← prod_atTop_atTop_eq]
    convert! (tendsto_mul.comp (nhds_prod_eq (x := a) (y := b) ▸ Tendsto.prodMap h₁ h₂))
    ext s
    simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
⊢ HasProd g a
have refine : ∀ (ib : Set α), ib ∈ 𝓝 a ∧ IsClosed[inst_1] ib → ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id ib
Tactic: refine (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
⊢ ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
have rcases : ∀ (u : Finset ((b : β) × γ b))
  (hu :
    ∀ b ≥ u,
      Membership.mem (γ := Set (Finset ((b : β) × γ b))) ((fun (s : Finset ((b : β) × γ b)) ↦ ∏ b ∈ s, f b) ⁻¹' s) b),
  ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
Tactic: rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
hu :
  ∀ b ≥ u,
    Membership.mem (γ := Set (Finset ((b : β) × γ b))) ((fun (s : Finset ((b : β) × γ b)) ↦ ∏ b ∈ s, f b) ⁻¹' s) b
⊢ ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
have right : ∀ x ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u), ∏ b ∈ x, g b ∈ id s
Tactic: use u.image Sigma.fst, trivial
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
hu :
  ∀ b ≥ u,
    Membership.mem (γ := Set (Finset ((b : β) × γ b))) ((fun (s : Finset ((b : β) × γ b)) ↦ ∏ b ∈ s, f b) ⁻¹' s) b
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
⊢ ∏ b ∈ bs, g b ∈ id s
have hu₁ : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
Tactic: simp only [Set.mem_preimage, Finset.le_iff_subset] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
⊢ Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ bs, f p) atTop
    (𝓝 (∏ b ∈ bs, g b))
have simp : Tendsto (β := α)
  (fun (t : Finset ((b : β) × γ b)) ↦
    ∏ a ∈ bs, ∏ s ∈ t.preimage (Sigma.mk (β := fun (a : β) ↦ γ a) a) sorry, f (Sigma.mk (β := fun (a : β) ↦ γ a) a s))
  atTop (𝓝 (∏ b ∈ bs, g b))
Tactic: simp only [← sigma_preimage_mk, prod_sigma]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
⊢ Tendsto (β := α)
    (fun (t : Finset ((b : β) × γ b)) ↦
      ∏ a ∈ bs, ∏ s ∈ t.preimage (Sigma.mk (β := fun (a : β) ↦ γ a) a) ⋯, f (Sigma.mk (β := fun (a : β) ↦ γ a) a s))
    atTop (𝓝 (∏ b ∈ bs, g b))
have refine : ∀ b ∈ bs,
  Tendsto
    (fun (t : Finset ((b : β) × γ b)) ↦
      ∏ s ∈ t.preimage (Sigma.mk (β := fun (a : β) ↦ γ a) b) sorry, f (Sigma.mk (β := fun (a : β) ↦ γ a) b s))
    atTop (𝓝 (g b))
Tactic: refine tendsto_finsetProd _ fun b _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
⊢ ∏ b ∈ bs, g b ∈ id s
have this : Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ bs, f p) atTop
  (𝓝 (∏ b ∈ bs, g b))
Tactic: have : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ bs, f p) atTop
      (𝓝 <| ∏ b ∈ bs, g b) := by
    simp only [← sigma_preimage_mk, prod_sigma]
    refine tendsto_finsetProd _ fun b _ ↦ ?_
    change
      Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
    exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst_1] s
u : Finset ((b : β) × γ b)
bs : Finset β
hbs : bs ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → ∏ b ∈ b, f b ∈ s
this :
  Tendsto (β := α) (fun (t : Finset ((b : β) × γ b)) ↦ ∏ p ∈ t with p.fst (β := fun (b : β) ↦ γ b) ∈ bs, f p) atTop
    (𝓝 (∏ b ∈ bs, g b))
⊢ ∏ b ∈ bs, g b ∈ id s
have right : ∀ (t : Finset ((b : β) × γ b)) (ht : t ≥ u) (x : (b : β) × γ b) (hx : x ∈ u),
  x ∈ {p ∈ t | p.fst (β := fun (b : β) ↦ γ b) ∈ bs}
Tactic: refine hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
⊢ HasProd g a
have refine : ∀ (ib : Set α), ib ∈ 𝓝 a ∧ IsClosed[inst_1] ib → ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id ib
Tactic: classical
  refine (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr ?_
  rintro s ⟨hs, hsc⟩
  rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩
  use u.image Sigma.fst, trivial
  intro bs hbs
  simp only [Set.mem_preimage, Finset.le_iff_subset] at hu
  have : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ bs, f p) atTop
      (𝓝 <| ∏ b ∈ bs, g b) := by
    simp only [← sigma_preimage_mk, prod_sigma]
    refine tendsto_finsetProd _ fun b _ ↦ ?_
    change
      Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
    exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
  refine hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ ?_⟩)
  exact mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
refine :
  ∀ (ib : Set α), ib ∈ 𝓝 a ∧ IsClosed[inst_1] ib → ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id ib
⊢ HasProd g a
have refine₁ : ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s), ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
Tactic: classical
  refine (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr ?_
  rintro s ⟨hs, hsc⟩
  rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩
  use u.image Sigma.fst, trivial
  intro bs hbs
  simp only [Set.mem_preimage, Finset.le_iff_subset] at hu
  have : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ bs, f p) atTop
      (𝓝 <| ∏ b ∈ bs, g b) := by
    simp only [← sigma_preimage_mk, prod_sigma]
    refine tendsto_finsetProd _ fun b _ ↦ ?_
    change
      Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
    exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
  refine hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ ?_⟩)
  exact mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
refine :
  ∀ (ib : Set α), ib ∈ 𝓝 a ∧ IsClosed[inst_1] ib → ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id ib
refine₁ :
  ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s),
    ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
⊢ HasProd g a
have refine₂ : ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s) (u : Finset ((b : β) × γ b))
  (hu :
    ∀ b ≥ u,
      Membership.mem (γ := Set (Finset ((b : β) × γ b))) ((fun (s : Finset ((b : β) × γ b)) ↦ ∏ b ∈ s, f b) ⁻¹' s) b),
  ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
Tactic: classical
  refine (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr ?_
  rintro s ⟨hs, hsc⟩
  rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩
  use u.image Sigma.fst, trivial
  intro bs hbs
  simp only [Set.mem_preimage, Finset.le_iff_subset] at hu
  have : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ bs, f p) atTop
      (𝓝 <| ∏ b ∈ bs, g b) := by
    simp only [← sigma_preimage_mk, prod_sigma]
    refine tendsto_finsetProd _ fun b _ ↦ ?_
    change
      Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
    exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
  refine hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ ?_⟩)
  exact mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun (c : γ b) ↦ f (Sigma.mk (β := fun (b : β) ↦ γ b) b c)) (g b)
refine :
  ∀ (ib : Set α), ib ∈ 𝓝 a ∧ IsClosed[inst_1] ib → ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id ib
refine₁ :
  ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s),
    ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
refine₂ :
  ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s) (u : Finset ((b : β) × γ b))
    (hu :
      ∀ b ≥ u,
        Membership.mem (γ := Set (Finset ((b : β) × γ b))) ((fun (s : Finset ((b : β) × γ b)) ↦ ∏ b ∈ s, f b) ⁻¹' s) b),
    ∃ (ia : Finset β), True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s
⊢ HasProd g a
have right : ∀ (s : Set α) (hs : s ∈ 𝓝 a) (hsc : IsClosed[inst_1] s) (u : Finset ((b : β) × γ b))
  (hu :
    ∀ b ≥ u,
      Membership.mem (γ := Set (Finset ((b : β) × γ b))) ((fun (s : Finset ((b : β) × γ b)) ↦ ∏ b ∈ s, f b) ⁻¹' s) b),
  ∀ x ∈ Set.Ici (image (Sigma.fst (β := fun (b : β) ↦ γ b)) u), ∏ b ∈ x, g b ∈ id s
Tactic: classical
  refine (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr ?_
  rintro s ⟨hs, hsc⟩
  rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩
  use u.image Sigma.fst, trivial
  intro bs hbs
  simp only [Set.mem_preimage, Finset.le_iff_subset] at hu
  have : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ bs, f p) atTop
      (𝓝 <| ∏ b ∈ bs, g b) := by
    simp only [← sigma_preimage_mk, prod_sigma]
    refine tendsto_finsetProd _ fun b _ ↦ ?_
    change
      Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
    exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
  refine hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ ?_⟩)
  exact mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩