awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
g : γ → α
e : Equiv.{u_2 + 1, u_3 + 1} (↑(mulSupport f) : Type u_2) (↑(mulSupport g) : Type u_3)
he :
  ∀ (x : (↑(mulSupport f) : Type u_2)),
    g (↑((e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)) x) : γ) = f (↑x : β)
this :
  Eq (α := (↑(mulSupport f) : Type u_2) → α)
    (comp (β := (↑(mulSupport g) : Type u_3)) (g ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g))
      (⇑e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)))
    (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ mulSupport f))
rw : HasProd (β := (↑(mulSupport f) : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ mulSupport f)) a ↔ HasProd g a
rw₁ :
  HasProd.{u_1, u_2} (β := (↑(mulSupport f) : Type u_2))
      (comp (β := (↑(mulSupport g) : Type u_3)) (g ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g))
        (⇑e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)))
      a ↔
    HasProd g a
rw₂ :
  HasProd (β := (↑(mulSupport g) : Type u_3)) (g ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g)) a ↔ HasProd g a
rw₃ rw₄ : HasProd g a ↔ HasProd g a
⊢ HasProd f a ↔ HasProd g a

Tactic:
rw [← hasProd_subtype_mulSupport, ← this, e.hasProd_iff, hasProd_subtype_mulSupport]

Premises used: Equiv.hasProd_iff, hasProd_subtype_mulSupport
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
g : γ → α
i : (↑(mulSupport g) : Type u_3) → β
hi : Injective i
hf : mulSupport f ⊆ Set.range i
hfg : ∀ (x : (↑(mulSupport g) : Type u_3)), f (i x) = g (↑x : γ)
⊢ HasProd f a ↔ HasProd g a

Tactic:
Iff.symm <|
    Equiv.hasProd_iff_of_mulSupport
      (Equiv.ofBijective (fun x ↦ ⟨i x, fun hx ↦ x.coe_prop <| hfg x ▸ hx⟩)
        ⟨fun _ _ h ↦ hi <| Subtype.ext_iff.1 h, fun y ↦
          (hf y.coe_prop).imp fun _ hx ↦ Subtype.ext hx⟩)
      hfg

Premises used: Subtype.coe_prop, Eq.rec, Equiv.hasProd_iff_of_mulSupport, Exists.imp, Subtype.ext_iff, Subtype.mk, And.intro, Equiv.ofBijective, Iff.mp, Iff.symm, Subtype.ext
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
g : γ → α
e : Equiv.{u_2 + 1, u_3 + 1} (↑(mulSupport f) : Type u_2) (↑(mulSupport g) : Type u_3)
he :
  ∀ (x : (↑(mulSupport f) : Type u_2)),
    g (↑((e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)) x) : γ) = f (↑x : β)
⊢ Multipliable f ↔ Multipliable g

Tactic:
exists_congr fun _ ↦ e.hasProd_iff_of_mulSupport he

Premises used: Equiv.hasProd_iff_of_mulSupport, Multipliable, exists_congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
hf : HasProd f a L
G : Type u_4
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
g : G
hg : Continuous[inst_1, inst_3] (⇑g : (a : α) → γ)
⊢ Eq (α := Finset β → γ)
    (comp.{u_2 + 1, u_1 + 1, u_3 + 1} (β := α) (⇑g : (a : α) → γ) fun (s : Finset β) ↦ ∏ b ∈ s, f b)
    fun (s : Finset β) ↦ ∏ b ∈ s, ((⇑g : (a : α) → γ) ∘ f) b

Tactic:
have : (g ∘ fun s : Finset β ↦ ∏ b ∈ s, f b) = fun s : Finset β ↦ ∏ b ∈ s, (g ∘ f) b :=
    funext <| map_prod g _
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
hf : HasProd f a L
G : Type u_4
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
g : G
hg : Continuous[inst_1, inst_3] (⇑g : (a : α) → γ)
this :
  Eq (α := Finset β → γ)
    (comp.{u_2 + 1, u_1 + 1, u_3 + 1} (β := α) (⇑g : (a : α) → γ) fun (s : Finset β) ↦ ∏ b ∈ s, f b)
    fun (s : Finset β) ↦ ∏ b ∈ s, ((⇑g : (a : α) → γ) ∘ f) b
rw :
  Tendsto.{u_2, u_3} (β := γ)
    (comp.{u_2 + 1, u_1 + 1, u_3 + 1} (β := α) (⇑g : (a : α) → γ) fun (s : Finset β) ↦ ∏ b ∈ s, f b : Finset β → γ)
    L.filter (𝓝 ((g : (a : α) → γ) a) : Filter γ)
⊢ Tendsto.{u_2, u_3} (β := γ) (fun (s : Finset β) ↦ (∏ b ∈ s, ((⇑g : (a : α) → γ) ∘ f) b : γ)) L.filter
    (𝓝 ((g : (a : α) → γ) a) : Filter γ)

Tactic:
rw [← this]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
hf : HasProd f a L
G : Type u_4
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
g : G
hg : Continuous[inst_1, inst_3] (⇑g : (a : α) → γ)
this :
  Eq (α := Finset β → γ)
    (comp.{u_2 + 1, u_1 + 1, u_3 + 1} (β := α) (⇑g : (a : α) → γ) fun (s : Finset β) ↦ ∏ b ∈ s, f b)
    fun (s : Finset β) ↦ ∏ b ∈ s, ((⇑g : (a : α) → γ) ∘ f) b
⊢ Tendsto.{u_2, u_3} (β := γ)
    (comp.{u_2 + 1, u_1 + 1, u_3 + 1} (β := α) (⇑g : (a : α) → γ) fun (s : Finset β) ↦ ∏ b ∈ s, f b : Finset β → γ)
    L.filter (𝓝 ((g : (a : α) → γ) a) : Filter γ)

Tactic:
(hg.tendsto a).comp hf

Premises used: Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
hf : HasProd f a L
G : Type u_4
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
g : G
hg : Continuous[inst_1, inst_3] (⇑g : (a : α) → γ)
this :
  Eq (α := Finset β → γ)
    (comp.{u_2 + 1, u_1 + 1, u_3 + 1} (β := α) (⇑g : (a : α) → γ) fun (s : Finset β) ↦ ∏ b ∈ s, f b)
    fun (s : Finset β) ↦ ∏ b ∈ s, ((⇑g : (a : α) → γ) ∘ f) b
⊢ Tendsto.{u_2, u_3} (β := γ)
    (comp.{u_2 + 1, u_1 + 1, u_3 + 1} (β := α) (⇑g : (a : α) → γ) fun (s : Finset β) ↦ ∏ b ∈ s, f b : Finset β → γ)
    L.filter (𝓝 ((g : (a : α) → γ) a) : Filter γ)

Tactic:
exact (hg.tendsto a).comp hf

Premises used: Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
G : Type u_4
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
a : α
simp_rw :
  Tendsto.{u_2, u_3} (β := γ) (fun (s : Finset β) ↦ ((g : (a : α) → γ) (∏ x ∈ s, f x) : γ)) L.filter
      (𝓝 ((g : (a : α) → γ) a) : Filter γ) ↔
    Tendsto (fun (s : Finset β) ↦ ∏ x ∈ s, f x) L.filter (𝓝 a)
⊢ HasProd.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f : β → γ) ((g : (a : α) → γ) a : γ) L ↔ HasProd f a L

Tactic:
simp_rw [HasProd, comp_apply, ← _root_.map_prod]

Premises used: HasProd, map_prod, Function.comp_apply, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
G : Type u_4
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
a : α
⊢ Tendsto.{u_2, u_3} (β := γ) (fun (s : Finset β) ↦ ((g : (a : α) → γ) (∏ x ∈ s, f x) : γ)) L.filter
      (𝓝 ((g : (a : α) → γ) a) : Filter γ) ↔
    Tendsto (fun (s : Finset β) ↦ ∏ x ∈ s, f x) L.filter (𝓝 a)

Tactic:
hg.tendsto_nhds_iff.symm

Premises used: Topology.IsInducing.tendsto_nhds_iff, Iff.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
G : Type u_4
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
a : α
⊢ Tendsto.{u_2, u_3} (β := γ) (fun (s : Finset β) ↦ ((g : (a : α) → γ) (∏ x ∈ s, f x) : γ)) L.filter
      (𝓝 ((g : (a : α) → γ) a) : Filter γ) ↔
    Tendsto (fun (s : Finset β) ↦ ∏ x ∈ s, f x) L.filter (𝓝 a)

Tactic:
exact hg.tendsto_nhds_iff.symm

Premises used: Topology.IsInducing.tendsto_nhds_iff, Iff.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
hf : Multipliable f L
G : Type u_4
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
g : G
hg : Continuous[inst_1, inst_3] (⇑g : (a : α) → γ)
⊢ Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L

Tactic:
(hf.hasProd.map g hg).multipliable

Premises used: HasProd.map, Multipliable.hasProd, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
G : Type u_4
G' : Type u_5
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
inst_6 : FunLike G' γ α
inst_7 : MonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous[inst_1, inst_3] (⇑g : (a : α) → γ)
hg' : Continuous[inst_3, inst_1] (⇑g' : (a : γ) → α)
hinv : LeftInverse.{u_1 + 1, u_3 + 1} (α := α) (β := γ) (⇑g' : (a : γ) → α) (⇑g : (a : α) → γ)
h : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
⊢ Multipliable.{u_1, u_2} (α := α)
    (comp.{u_2 + 1, u_3 + 1, u_1 + 1} (β := γ) (⇑g' : (a : γ) → α) ((⇑g : (a : α) → γ) ∘ f)) L

Tactic:
have := h.map _ hg'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
G : Type u_4
G' : Type u_5
inst_4 : FunLike G α γ
inst_5 : MonoidHomClass G α γ
inst_6 : FunLike G' γ α
inst_7 : MonoidHomClass G' γ α
g : G
g' : G'
hg : Continuous[inst_1, inst_3] (⇑g : (a : α) → γ)
hg' : Continuous[inst_3, inst_1] (⇑g' : (a : γ) → α)
hinv : LeftInverse.{u_1 + 1, u_3 + 1} (α := α) (β := γ) (⇑g' : (a : γ) → α) (⇑g : (a : α) → γ)
h : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
this :
  Multipliable.{u_1, u_2} (α := α)
    (comp.{u_2 + 1, u_3 + 1, u_1 + 1} (β := γ) (⇑g' : (a : γ) → α) ((⇑g : (a : α) → γ) ∘ f)) L
rwa :
  ∀
    (this :
      Multipliable (α := α) (comp.{u_1 + 1, u_3 + 1, u_1 + 1} (β := γ) (⇑g' : (a : γ) → α) (⇑g : (a : α) → γ) ∘ f) L),
    Multipliable f L
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : Multipliable (id ∘ f) L), Multipliable f L
⊢ Multipliable f L

Tactic:
rwa [← Function.comp_assoc, hinv.id] at this

Premises used: Function.LeftInverse.id, Function.comp_assoc
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : L.NeBot
inst_3 : CommMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : T2Space γ
hf : Multipliable f L
G : Type u_4
inst_6 : FunLike G α γ
inst_7 : MonoidHomClass G α γ
g : G
hg : Continuous[inst_1, inst_4] (⇑g : (a : α) → γ)
⊢ Eq.{u_3 + 1} (α := γ) ((g : (a : α) → γ) (∏'[L] (i : β), f i) : γ) (∏'[L] (i : β), (g : (a : α) → γ) (f i) : γ)

Tactic:
(HasProd.tprod_eq (HasProd.map hf.hasProd g hg)).symm

Premises used: HasProd.map, HasProd.tprod_eq, Multipliable.hasProd, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
pos :
  ∀ (hL : L.NeBot),
    Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')
neg :
  ∀ (hL : ¬L.NeBot),
    Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')
⊢ Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')

Tactic:
by_cases hL : L.NeBot

Premises used: SummationFilter.NeBot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
pos :
  ∀ (h : Multipliable f L),
    Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')
neg :
  ∀ (h : ¬Multipliable f L),
    Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')
⊢ Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')

Tactic:
by_cases h : Multipliable f L

Premises used: Multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
h : Multipliable f L
⊢ Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')

Tactic:
h.map_tprod g hge.continuous

Premises used: Topology.IsClosedEmbedding.continuous, Multipliable.map_tprod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
h : Multipliable f L
⊢ Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')

Tactic:
exact h.map_tprod g hge.continuous

Premises used: Topology.IsClosedEmbedding.continuous, Multipliable.map_tprod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
h : ¬Multipliable f L
neg : ¬Multipliable.{u_6, u_4} (α := α') (fun (i : ι) ↦ (g : (a : α) → α') (f i)) L
⊢ Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')

Tactic:
rw [tprod_eq_one_of_not_multipliable h, tprod_eq_one_of_not_multipliable, map_one]

Premises used: tprod_eq_one_of_not_multipliable, map_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
h : ¬Multipliable f L
neg : ∀ (h : Multipliable.{u_6, u_4} (α := α') (fun (i : ι) ↦ (g : (a : α) → α') (f i)) L), Multipliable f L
⊢ ¬Multipliable.{u_6, u_4} (α := α') (fun (i : ι) ↦ (g : (a : α) → α') (f i)) L

Tactic:
contrapose h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
h : Multipliable.{u_6, u_4} (α := α') (fun (i : ι) ↦ (g : (a : α) → α') (f i)) L
⊢ ∃ (a : α'), Tendsto (fun (s : Finset ι) ↦ ∏ x ∈ s, (g : (a : α) → α') (f x)) L.filter (𝓝 a)

Tactic:
simp only [Multipliable, HasProd] at h ⊢

Premises used: HasProd, Multipliable, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
h : ∃ (a : α'), Tendsto (fun (s : Finset ι) ↦ ∏ x ∈ s, (g : (a : α) → α') (f x)) L.filter (𝓝 a)
neg :
  ∀ (b : α') (hb : Tendsto (fun (s : Finset ι) ↦ ∏ x ∈ s, (g : (a : α) → α') (f x)) L.filter (𝓝 b)),
    ∃ (a : α), Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
⊢ ∃ (a : α), Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)

Tactic:
obtain ⟨b, hb⟩ := h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
b : α'
hb : Tendsto (fun (s : Finset ι) ↦ ∏ x ∈ s, (g : (a : α) → α') (f x)) L.filter (𝓝 b)
⊢ ∀ (x : Finset ι),
    Membership.mem (γ := Set α') (Set.range.{u_6, u_5 + 1} (ι := α) (⇑g : (a : α) → α'))
      (∏ x ∈ x, (g : (a : α) → α') (f x))

Tactic:
simp [← _root_.map_prod]

Premises used: map_prod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
b : α'
hb : Tendsto (fun (s : Finset ι) ↦ ∏ x ∈ s, (g : (a : α) → α') (f x)) L.filter (𝓝 b)
neg : ∀ (a : α) (ha : (g : (a : α) → α') a = b), ∃ (a : α), Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
⊢ ∃ (a : α), Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)

Tactic:
obtain ⟨a, ha⟩ : b ∈ Set.range g :=
        hge.isClosed_range.mem_of_tendsto hb (.of_forall <| by simp [← _root_.map_prod])

Premises used: IsClosed.mem_of_tendsto, Filter.Eventually.of_forall, Set.range, DFunLike.coe, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
b : α'
hb : Tendsto (fun (s : Finset ι) ↦ ∏ x ∈ s, (g : (a : α) → α') (f x)) L.filter (𝓝 b)
a : α
ha : (g : (a : α) → α') a = b
h : Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
⊢ ∃ (a : α), Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)

Tactic:
use a
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : L.NeBot
b : α'
hb : Tendsto (fun (s : Finset ι) ↦ ∏ x ∈ s, (g : (a : α) → α') (f x)) L.filter (𝓝 b)
a : α
ha : (g : (a : α) → α') a = b
⊢ Tendsto (fun (s : Finset ι) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)

Tactic:
simp [hge.tendsto_nhds_iff, Function.comp_def, ha, hb]

Premises used: Function.comp_def, Topology.IsClosedEmbedding.tendsto_nhds_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst : CommMonoid α
inst_1 : CommMonoid α'
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace α'
inst_4 : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst_5 : FunLike G α α'
inst_6 : MonoidHomClass G α α'
hge : IsClosedEmbedding.{u_5, u_6} (X := α) (Y := α') (⇑g : (a : α) → α')
hL : ¬L.NeBot
⊢ Eq.{u_6 + 1} (α := α') ((g : (a : α) → α') (∏'[L] (i : ι), f i) : α') (∏'[L] (i : ι), (g : (a : α) → α') (f i) : α')

Tactic:
simpa [tprod_bot hL] using
      (MonoidHomClass.toMonoidHom g).map_finprod_of_injective hge.injective _

Premises used: MonoidHomClass.toMonoidHom, Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, MonoidHom.map_finprod_of_injective, tprod_bot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
G : Type u_4
f : β → α
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
inst_4 : T2Space γ
g : G
inst_5 : FunLike G α γ
inst_6 : MonoidHomClass G α γ
hg : Continuous[inst_1, inst_3] (⇑g : (a : α) → γ)
g' : γ → α
hg' : Continuous[inst_3, inst_1] g'
hgg' : LeftInverse g' (⇑g : (a : α) → γ)
⊢ Eq.{u_3 + 1} (α := γ) ((g : (a : α) → γ) (∏'[L] (b : β), f b) : γ) (∏'[L] (b : β), (g : (a : α) → γ) (f b) : γ)

Tactic:
(hgg'.isClosedEmbedding hg' hg).map_tprod _

Premises used: Topology.IsClosedEmbedding.map_tprod, Function.LeftInverse.isClosedEmbedding
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
inst_4 : T2Space γ
G : Type u_4
inst_5 : FunLike G α γ
inst_6 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
mp :
  Multipliable f L →
    Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L ∧
      Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
        (∏'[L] (i : β), (g : (a : α) → γ) (f i))
mpr :
  Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L ∧
      Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
        (∏'[L] (i : β), (g : (a : α) → γ) (f i)) →
    Multipliable f L
⊢ Multipliable f L ↔
    Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L ∧
      Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
        (∏'[L] (i : β), (g : (a : α) → γ) (f i))

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : CommMonoid γ
inst_3 : TopologicalSpace γ
inst_4 : T2Space γ
G : Type u_4
inst_5 : FunLike G α γ
inst_6 : MonoidHomClass G α γ
g : G
hg : IsInducing.{u_1, u_3} (X := α) (Y := γ) (⇑g : (a : α) → γ)
f : β → α
hf : Multipliable f L
mp : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
mp₁ :
  Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[L] (i : β), (g : (a : α) → γ) (f i))
⊢ Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L ∧
    Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
      (∏'[L] (i : β), (g : (a : α) → γ) (f i))

Tactic:
constructor