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 α
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
⊢ Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L

Tactic:
hf.map g hg.continuous

Premises used: Topology.IsInducing.continuous, Multipliable.map
-- 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
⊢ Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L

Tactic:
exact hf.map g hg.continuous

Premises used: Topology.IsInducing.continuous, Multipliable.map
-- 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
pos :
  ∀ (hL : L.NeBot),
    Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
      (∏'[L] (i : β), (g : (a : α) → γ) (f i))
neg :
  ∀ (hL : ¬L.NeBot),
    Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
      (∏'[L] (i : β), (g : (a : α) → γ) (f i))
⊢ Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[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_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
hL : L.NeBot
⊢ Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[L] (i : β), (g : (a : α) → γ) (f i))

Tactic:
⟨_, hf.map_tprod g hg.continuous⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, Topology.IsInducing.continuous, Multipliable.map_tprod
-- 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
hL : L.NeBot
⊢ Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[L] (i : β), (g : (a : α) → γ) (f i))

Tactic:
exact ⟨_, hf.map_tprod g hg.continuous⟩
-- 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
hL : ¬L.NeBot
pos :
  ∀ (hfs : Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ (g : (a : α) → γ) (f x))),
    Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
      (∏'[L] (i : β), (g : (a : α) → γ) (f i))
neg :
  ∀ (hfs : ¬Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ (g : (a : α) → γ) (f x))),
    Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
      (∏'[L] (i : β), (g : (a : α) → γ) (f i))
⊢ Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[L] (i : β), (g : (a : α) → γ) (f i))

Tactic:
by_cases hfs : (mulSupport fun x ↦ g (f x)).Finite

Premises used: Set.Finite, Function.mulSupport, DFunLike.coe
-- 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
hL : ¬L.NeBot
hfs : Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ (g : (a : α) → γ) (f x))
⊢ Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[L] (i : β), (g : (a : α) → γ) (f i))

Tactic:
simp [tprod_bot hL, finprod_eq_prod _ hfs, ← _root_.map_prod]

Premises used: map_prod, tprod_bot, finprod_eq_prod
-- 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
hL : ¬L.NeBot
hfs : ¬Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ (g : (a : α) → γ) (f x))
⊢ Eq.{u_3 + 1} (α := γ) ((g : (a : α) → γ) 1 : γ) (∏'[L] (i : β), (g : (a : α) → γ) (f i) : γ)

Tactic:
simp [tprod_bot hL, finprod_of_infinite_mulSupport hfs]

Premises used: finprod_of_infinite_mulSupport, 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 β
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
hL : ¬L.NeBot
hfs : ¬Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_3} (M := γ) fun (x : β) ↦ (g : (a : α) → γ) (f x))
⊢ Membership.mem (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑g : (a : α) → γ))
    (∏'[L] (i : β), (g : (a : α) → γ) (f i))

Tactic:
exact ⟨1, by simp [tprod_bot hL, finprod_of_infinite_mulSupport hfs]⟩
-- 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 : β → α
hgf : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
a : α
ha : Eq.{u_3 + 1} (α := γ) ((g : (a : α) → γ) a : γ) (∏'[L] (i : β), (g : (a : α) → γ) (f i) : γ)
h : HasProd f a L
⊢ Multipliable f L

Tactic:
use a
-- 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 : β → α
hgf : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
a : α
ha : Eq.{u_3 + 1} (α := γ) ((g : (a : α) → γ) a : γ) (∏'[L] (i : β), (g : (a : α) → γ) (f i) : γ)
⊢ HasProd.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) (∏'[L] (b : β), ((⇑g : (a : α) → γ) ∘ f) b) L

Tactic:
have := hgf.hasProd
-- 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 : β → α
hgf : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
a : α
ha : Eq.{u_3 + 1} (α := γ) ((g : (a : α) → γ) a : γ) (∏'[L] (i : β), (g : (a : α) → γ) (f i) : γ)
this : HasProd.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) (∏'[L] (b : β), ((⇑g : (a : α) → γ) ∘ f) b) L
⊢ HasProd.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f : β → γ) ((g : (a : α) → γ) a : γ) L

Tactic:
simp_rw [comp_apply, ← ha] at this

Premises used: Function.comp_apply
-- 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 : β → α
hgf : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
a : α
ha : Eq.{u_3 + 1} (α := γ) ((g : (a : α) → γ) a : γ) (∏'[L] (i : β), (g : (a : α) → γ) (f i) : γ)
this : HasProd.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f : β → γ) ((g : (a : α) → γ) a : γ) L
⊢ HasProd f a L

Tactic:
(hg.hasProd_iff f a).mp this

Premises used: Topology.IsInducing.hasProd_iff, Iff.mp
-- 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 : β → α
hgf : Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L
a : α
ha : Eq.{u_3 + 1} (α := γ) ((g : (a : α) → γ) a : γ) (∏'[L] (i : β), (g : (a : α) → γ) (f i) : γ)
this : HasProd.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f : β → γ) ((g : (a : α) → γ) a : γ) L
⊢ HasProd f a L

Tactic:
exact (hg.hasProd_iff f a).mp this

Premises used: Topology.IsInducing.hasProd_iff, Iff.mp
-- 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
inst_4 : EquivLike G α γ
inst_5 : MulEquivClass G α γ
g : G
hg : Continuous[inst_1, inst_3] (⇑g : (a : α) → γ)
hg' : Continuous[inst_3, inst_1] (EquivLike.inv g)
⊢ Multipliable.{u_3, u_2} (α := γ) ((⇑g : (a : α) → γ) ∘ f) L ↔ Multipliable f L

Tactic:
Multipliable.map_iff_of_leftInverse g (g : α ≃* γ).symm hg hg' (EquivLike.left_inv g)

Premises used: Multipliable.map_iff_of_leftInverse, MulEquiv.symm, MulEquivClass.toMulEquiv, EquivLike.left_inv
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
α' : Type u_4
inst_2 : CommMonoid α'
inst_3 : TopologicalSpace α'
e : α' → α
hes : Surjective e
f : β → α
g : γ → α'
he : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a
⊢ Multipliable f ↔ Multipliable g

Tactic:
hes.exists.trans <| exists_congr <| @he

Premises used: Function.Surjective.exists, Multipliable, exists_congr, Iff.trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f g : β → α
a b : α
L : SummationFilter β
inst_2 : ContinuousMul α
hf : Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
hg : Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, g b) L.filter (𝓝 b)
simp_rw : Tendsto (fun (s : Finset β) ↦ HMul.hMul (α := α) (∏ x ∈ s, f x) (∏ x ∈ s, g x)) L.filter (𝓝 (a * b))
⊢ Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b * g b) L.filter (𝓝 (a * b))

Tactic:
simp_rw [prod_mul_distrib]

Premises used: Finset.prod_mul_distrib
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f g : β → α
a b : α
L : SummationFilter β
inst_2 : ContinuousMul α
hf : Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
hg : Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, g b) L.filter (𝓝 b)
⊢ Tendsto (fun (s : Finset β) ↦ HMul.hMul (α := α) (∏ x ∈ s, f x) (∏ x ∈ s, g x)) L.filter (𝓝 (a * b))

Tactic:
hf.mul hg

Premises used: Filter.Tendsto.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f g : β → α
a b : α
L : SummationFilter β
inst_2 : ContinuousMul α
hf : Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
hg : Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, g b) L.filter (𝓝 b)
⊢ Tendsto (fun (s : Finset β) ↦ HMul.hMul (α := α) (∏ x ∈ s, f x) (∏ x ∈ s, g x)) L.filter (𝓝 (a * b))

Tactic:
exact hf.mul hg

Premises used: Filter.Tendsto.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f g : β → α
L : SummationFilter β
inst_2 : ContinuousMul α
hf : Multipliable f L
hg : Multipliable g L
⊢ Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ f b * g b) L

Tactic:
(hf.hasProd.mul hg.hasProd).multipliable

Premises used: Multipliable.hasProd, HasProd.mul, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst_2 : ContinuousMul α
hf : HasProd f a L
⊢ HasProd (fun (x : β) ↦ HPow.hPow (β := ℕ) (f x) 0) (HPow.hPow (β := ℕ) a 0) L

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst_2 : ContinuousMul α
hf : HasProd f a L
n : ℕ
hn : HasProd (fun (x : β) ↦ f x ^ n) (a ^ n) L
⊢ HasProd (fun (x : β) ↦ f x ^ (n + 1)) (a ^ (n + 1)) L

Tactic:
simpa [pow_succ] using hn.mul hf

Premises used: pow_succ, HasProd.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst_2 : ContinuousMul α
hf : HasProd f a L
n : ℕ
zero : HasProd (fun (x : β) ↦ HPow.hPow (β := ℕ) (f x) 0) (HPow.hPow (β := ℕ) a 0) L
succ : ∀ (n : ℕ) (hn : HasProd (fun (x : β) ↦ f x ^ n) (a ^ n) L), HasProd (fun (x : β) ↦ f x ^ (n + 1)) (a ^ (n + 1)) L
⊢ HasProd (fun (x : β) ↦ f x ^ n) (a ^ n) L

Tactic:
induction n with
  | zero => simp
  | succ n hn => simpa [pow_succ] using hn.mul hf

Premises used: pow_succ
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : ContinuousMul α
hf : Multipliable f L
n : ℕ
⊢ Multipliable.{u_1, u_2} (α := α) (fun (x : β) ↦ f x ^ n) L

Tactic:
(hf.hasProd.pow n).multipliable

Premises used: Multipliable.hasProd, HasProd.multipliable, HasProd.pow
-- 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 : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ (∀ (i : γ), Membership.mem (γ := Finset γ) ∅ i → HasProd (f i) (a i) L) →
    HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ ∏ i ∈ ∅, f i b) (∏ i ∈ ∅, a i) L

Tactic:
simp
-- 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 : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
simp :
  ∀ (a_1 : γ) (s : Finset γ),
    a_1 ∉ s →
      ((∀ i ∈ s, HasProd (f i) (a i) L) → HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L) →
        HasProd (f a_1) (a a_1) L →
          (∀ a_5 ∈ s, HasProd (f a_5) (a a_5) L) →
            HasProd (fun (b : β) ↦ f a_1 b * ∏ i ∈ s, f i b) (a a_1 * ∏ i ∈ s, a i) L
⊢ ∀ (a_1 : γ) (s : Finset γ),
    a_1 ∉ s →
      ((∀ i ∈ s, HasProd (f i) (a i) L) → HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L) →
        (∀ i ∈ insert a_1 s, HasProd (f i) (a i) L) →
          HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ ∏ i ∈ insert a_1 s, f i b) (∏ i ∈ insert a_1 s, a i) L

Tactic:
simp +contextual only [mem_insert, forall_eq_or_imp, not_false_iff,
      prod_insert, and_imp]

Premises used: Finset.prod_insert, and_imp, Finset.mem_insert, forall_eq_or_imp, not_false_iff
-- 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 : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ ∀ (a_1 : γ) (s : Finset γ),
    a_1 ∉ s →
      ((∀ i ∈ s, HasProd (f i) (a i) L) → HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L) →
        HasProd (f a_1) (a a_1) L →
          (∀ a_5 ∈ s, HasProd (f a_5) (a a_5) L) →
            HasProd (fun (b : β) ↦ f a_1 b * ∏ i ∈ s, f i b) (a a_1 * ∏ i ∈ s, a i) L

Tactic:
fun x s _ IH hx h ↦ hx.mul (IH h)

Premises used: HasProd.mul
-- 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 : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ ∀ (a_1 : γ) (s : Finset γ),
    a_1 ∉ s →
      ((∀ i ∈ s, HasProd (f i) (a i) L) → HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L) →
        HasProd (f a_1) (a a_1) L →
          (∀ a_5 ∈ s, HasProd (f a_5) (a a_5) L) →
            HasProd (fun (b : β) ↦ f a_1 b * ∏ i ∈ s, f i b) (a a_1 * ∏ i ∈ s, a i) L

Tactic:
exact fun x s _ IH hx h ↦ hx.mul (IH h)
-- 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 : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ (∀ i ∈ s, HasProd (f i) (a i) L) → HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L

Tactic:
exact Finset.induction_on s (by simp) <| by
    simp +contextual only [mem_insert, forall_eq_or_imp, not_false_iff,
      prod_insert, and_imp]
    exact fun x s _ IH hx h ↦ hx.mul (IH h)
-- 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 : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ (∀ i ∈ s, HasProd (f i) (a i) L) → HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L

Tactic:
classical
  exact Finset.induction_on s (by simp) <| by
    simp +contextual only [mem_insert, forall_eq_or_imp, not_false_iff,
      prod_insert, and_imp]
    exact fun x s _ IH hx h ↦ hx.mul (IH h)
-- 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 : ContinuousMul α
f : γ → β → α
s : Finset γ
hf : ∀ i ∈ s, Multipliable (f i) L
⊢ Multipliable.{u_1, u_2} (α := α) (fun (b : β) ↦ ∏ i ∈ s, f i b) L

Tactic:
(hasProd_prod fun i hi ↦ (hf i hi).hasProd).multipliable

Premises used: hasProd_prod, Multipliable.hasProd, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a b : α
inst_2 : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a
hb : HasProd (β := (↑t : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ t)) b
rw : ∀ (ha : HasProd (s.mulIndicator f) a) (hb : HasProd (t.mulIndicator f) b), HasProd ((s ∪ t).mulIndicator f) (a * b)
⊢ HasProd (β := (↑(s ∪ t) : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s ∪ t)) (a * b)

Tactic:
rw [hasProd_subtype_iff_mulIndicator] at *

Premises used: hasProd_subtype_iff_mulIndicator
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a b : α
inst_2 : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (s.mulIndicator f) a
hb : HasProd (t.mulIndicator f) b
rw : HasProd (fun (a : β) ↦ s.mulIndicator f a * t.mulIndicator f a) (a * b)
⊢ HasProd ((s ∪ t).mulIndicator f) (a * b)

Tactic:
rw [Set.mulIndicator_union_of_disjoint hs]

Premises used: Set.mulIndicator_union_of_disjoint
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a b : α
inst_2 : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (s.mulIndicator f) a
hb : HasProd (t.mulIndicator f) b
⊢ HasProd (fun (a : β) ↦ s.mulIndicator f a * t.mulIndicator f a) (a * b)

Tactic:
ha.mul hb

Premises used: HasProd.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a b : α
inst_2 : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (s.mulIndicator f) a
hb : HasProd (t.mulIndicator f) b
⊢ HasProd (fun (a : β) ↦ s.mulIndicator f a * t.mulIndicator f a) (a * b)

Tactic:
exact ha.mul hb

Premises used: HasProd.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
inst_2 : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s : Set ι).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd (β := (↑(t i) : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ t i)) (a i)
simp_rw :
  ∀ (hf : ∀ i ∈ s, HasProd ((t i).mulIndicator f) (a i)), HasProd (Set.mulIndicator (⋃ i ∈ s, t i) f) (∏ i ∈ s, a i)
⊢ HasProd (β := (↑(⋃ i ∈ s, t i) : Type u_2))
    (f ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) (⋃ i ∈ s, t i) x)) (∏ i ∈ s, a i)

Tactic:
simp_rw [hasProd_subtype_iff_mulIndicator] at *

Premises used: hasProd_subtype_iff_mulIndicator
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
inst_2 : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s : Set ι).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd ((t i).mulIndicator f) (a i)
rw : HasProd.{u_1, u_2} (α := α) (fun (a : β) ↦ ∏ i ∈ s, (t i).mulIndicator f a) (∏ i ∈ s, a i)
⊢ HasProd (Set.mulIndicator (⋃ i ∈ s, t i) f) (∏ i ∈ s, a i)

Tactic:
rw [Finset.mulIndicator_biUnion _ _ hs]

Premises used: Finset.mulIndicator_biUnion
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
inst_2 : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s : Set ι).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd ((t i).mulIndicator f) (a i)
⊢ HasProd.{u_1, u_2} (α := α) (fun (a : β) ↦ ∏ i ∈ s, (t i).mulIndicator f a) (∏ i ∈ s, a i)

Tactic:
hasProd_prod hf

Premises used: hasProd_prod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
inst_2 : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s : Set ι).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd ((t i).mulIndicator f) (a i)
⊢ HasProd.{u_1, u_2} (α := α) (fun (a : β) ↦ ∏ i ∈ s, (t i).mulIndicator f a) (∏ i ∈ s, a i)

Tactic:
exact hasProd_prod hf

Premises used: hasProd_prod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a b : α
inst_2 : ContinuousMul α
s t : Set β
hs : IsCompl s t
ha : HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a
hb : HasProd (β := (↑t : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ t)) b
⊢ HasProd f (a * b)

Tactic:
simpa [← hs.compl_eq] using
    (hasProd_subtype_iff_mulIndicator.1 ha).mul (hasProd_subtype_iff_mulIndicator.1 hb)

Premises used: hasProd_subtype_iff_mulIndicator, IsCompl.compl_eq, HasProd.mul, Iff.mp