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 α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : (mulSupport f).Finite
⊢ (mulSupport (f ∘ g)).Finite

Tactic:
have hfg_fin : (mulSupport (f ∘ g)).Finite := hf_fin.preimage hg.injOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : (mulSupport f).Finite
hfg_fin : (mulSupport (f ∘ g)).Finite
⊢ Injective g

Tactic:
hg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : (mulSupport f).Finite
hfg_fin : (mulSupport (f ∘ g)).Finite
pos :
  ∀ (g : γ ↪ β) (hf : mulSupport f ⊆ Set.range.{u_2, u_3 + 1} (ι := γ) (⇑g : (a : γ) → β))
    (this : mulSupport f = Set.image.{u_3, u_2} (α := γ) (⇑g : (a : γ) → β) (mulSupport (f ∘ (⇑g : (a : γ) → β))))
    (hfg_fin : Set.Finite.{u_3} (α := γ) (mulSupport (f ∘ (⇑g : (a : γ) → β)))),
    tprod (f ∘ (⇑g : (a : γ) → β)) = ∏' (b : β), f b
⊢ tprod (f ∘ g) = ∏' (b : β), f b

Tactic:
lift g to γ ↪ β using hg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
hf_fin : (mulSupport f).Finite
g : γ ↪ β
hf : mulSupport f ⊆ Set.range.{u_2, u_3 + 1} (ι := γ) (⇑g : (a : γ) → β)
this : mulSupport f = Set.image.{u_3, u_2} (α := γ) (⇑g : (a : γ) → β) (mulSupport (f ∘ (⇑g : (a : γ) → β)))
hfg_fin : Set.Finite.{u_3} (α := γ) (mulSupport (f ∘ (⇑g : (a : γ) → β)))
pos :
  Eq.{u_1 + 1} (α := α) (∏ x ∈ Finset.map g (hfg_fin.toFinset (s := mulSupport (f ∘ (⇑g : (a : γ) → β)))), f x)
    (∏ x ∈ hf_fin.toFinset (s := mulSupport f), f x)
⊢ tprod (f ∘ (⇑g : (a : γ) → β)) = ∏' (b : β), f b

Tactic:
simp_rw [tprod_eq_prod' hf_fin.coe_toFinset.ge, tprod_eq_prod' hfg_fin.coe_toFinset.ge,
      comp_apply, ← Finset.prod_map]

Premises used: Eq.ge, Set.Finite.coe_toFinset, tprod_eq_prod', Function.comp_apply, Finset.prod_map
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
hf_fin : (mulSupport f).Finite
g : γ ↪ β
hf : mulSupport f ⊆ Set.range.{u_2, u_3 + 1} (ι := γ) (⇑g : (a : γ) → β)
this : mulSupport f = Set.image.{u_3, u_2} (α := γ) (⇑g : (a : γ) → β) (mulSupport (f ∘ (⇑g : (a : γ) → β)))
hfg_fin : Set.Finite.{u_3} (α := γ) (mulSupport (f ∘ (⇑g : (a : γ) → β)))
⊢ Eq.{u_1 + 1} (α := α) (∏ x ∈ Finset.map g (hfg_fin.toFinset (s := mulSupport (f ∘ (⇑g : (a : γ) → β)))), f x)
    (∏ x ∈ hf_fin.toFinset (s := mulSupport f), f x)

Tactic:
Finset.prod_congr (Finset.coe_injective ?_) fun _ _ ↦ rfl

Premises used: Finset.prod_congr, Finset.coe_injective, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
hf_fin : (mulSupport f).Finite
g : γ ↪ β
hf : mulSupport f ⊆ Set.range.{u_2, u_3 + 1} (ι := γ) (⇑g : (a : γ) → β)
this : mulSupport f = Set.image.{u_3, u_2} (α := γ) (⇑g : (a : γ) → β) (mulSupport (f ∘ (⇑g : (a : γ) → β)))
hfg_fin : Set.Finite.{u_3} (α := γ) (mulSupport (f ∘ (⇑g : (a : γ) → β)))
pos :
  (↑(Finset.map g (hfg_fin.toFinset (s := mulSupport (f ∘ (⇑g : (a : γ) → β))))) : Set β) =
    (↑(hf_fin.toFinset (s := mulSupport f)) : Set β)
⊢ Eq.{u_1 + 1} (α := α) (∏ x ∈ Finset.map g (hfg_fin.toFinset (s := mulSupport (f ∘ (⇑g : (a : γ) → β)))), f x)
    (∏ x ∈ hf_fin.toFinset (s := mulSupport f), f x)

Tactic:
refine Finset.prod_congr (Finset.coe_injective ?_) fun _ _ ↦ rfl

Premises used: Finset.prod_congr, Finset.coe_injective, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
hf_fin : (mulSupport f).Finite
g : γ ↪ β
hf : mulSupport f ⊆ Set.range.{u_2, u_3 + 1} (ι := γ) (⇑g : (a : γ) → β)
this : mulSupport f = Set.image.{u_3, u_2} (α := γ) (⇑g : (a : γ) → β) (mulSupport (f ∘ (⇑g : (a : γ) → β)))
hfg_fin : Set.Finite.{u_3} (α := γ) (mulSupport (f ∘ (⇑g : (a : γ) → β)))
⊢ (↑(Finset.map g (hfg_fin.toFinset (s := mulSupport (f ∘ (⇑g : (a : γ) → β))))) : Set β) =
    (↑(hf_fin.toFinset (s := mulSupport f)) : Set β)

Tactic:
simp [this]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
rwa : ∀ (hf_fin : ¬(g '' mulSupport (f ∘ g)).Finite), ¬(mulSupport (f ∘ g)).Finite
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hf_fin : ¬(mulSupport (f ∘ g)).Finite), ¬(mulSupport (f ∘ g)).Finite
⊢ ¬(mulSupport (f ∘ g)).Finite

Tactic:
rwa [this, Set.finite_image_iff hg.injOn] at hf_fin

Premises used: Function.Injective.injOn, Set.finite_image_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
⊢ ¬(mulSupport (f ∘ g)).Finite

Tactic:
have hf_fin' : ¬ Set.Finite (mulSupport (f ∘ g)) := by
      rwa [this, Set.finite_image_iff hg.injOn] at hf_fin
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
hf_fin' : ¬(mulSupport (f ∘ g)).Finite
⊢ (unconditional β).HasSupport

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
hf_fin' : ¬(mulSupport (f ∘ g)).Finite
⊢ (unconditional γ).HasSupport

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
hf_fin' : ¬(mulSupport (f ∘ g)).Finite
neg :
  Eq.{u_1 + 1} (α := α)
    (if h : ∃ (a : α), HasProd (f ∘ g) a then
      if HasProd (f ∘ g) 1 then 1 else Exists.choose (p := fun (a : α) ↦ HasProd (f ∘ g) a) ⋯
    else 1)
    (if h : ∃ (a : α), HasProd (fun (b : β) ↦ f b) a then
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a) ⋯
    else 1)
⊢ tprod (f ∘ g) = ∏' (b : β), f b

Tactic:
simp_rw [tprod_def, SummationFilter.support_eq_univ, Set.inter_univ,
      show (unconditional β).HasSupport by infer_instance,
      show (unconditional γ).HasSupport by infer_instance, true_and,
      if_neg hf_fin, if_neg hf_fin', Multipliable]

Premises used: SummationFilter.support_eq_univ, Set.inter_univ, Multipliable, tprod_def, if_neg, true_and, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
hf_fin' : ¬(mulSupport (f ∘ g)).Finite
⊢ Eq.{u_1 + 1} (α := α)
    (if h : ∃ (a : α), HasProd (f ∘ g) a then
      if HasProd (f ∘ g) 1 then 1 else Exists.choose (p := fun (a : α) ↦ HasProd (f ∘ g) a) ⋯
    else 1)
    (if h : ∃ (a : α), HasProd (fun (b : β) ↦ f b) a then
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a) ⋯
    else 1)

Tactic:
simp [hg.hasProd_iff (mulSupport_subset_iff'.1 hf)]

Premises used: Function.mulSupport_subset_iff', Iff.mp, Function.Injective.hasProd_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
have : mulSupport f = g '' mulSupport (f ∘ g)
have₁ : ∀ (this : mulSupport f = g '' mulSupport (f ∘ g)), Eq.{u_1 + 1} (α := α) (∏' (c : γ), f (g c)) (∏' (b : β), f b)
have₂ : mulSupport f = g '' mulSupport (f ∘ g)
have₃ have₄ :
  ∀ (this : mulSupport f = g '' mulSupport (f ∘ g)), Eq.{u_1 + 1} (α := α) (∏' (c : γ), f (g c)) (∏' (b : β), f b)
have₅ : ∀ (this : mulSupport f = g '' mulSupport (f ∘ g)), tprod (f ∘ g) = ∏' (b : β), f b
pos :
  ∀ (this : mulSupport f = g '' mulSupport (f ∘ g)) (hf_fin : (mulSupport f).Finite), tprod (f ∘ g) = ∏' (b : β), f b
neg neg₁ :
  ∀ (this : mulSupport f = g '' mulSupport (f ∘ g)) (hf_fin : ¬(mulSupport f).Finite), tprod (f ∘ g) = ∏' (b : β), f b
⊢ Eq.{u_1 + 1} (α := α) (∏' (c : γ), f (g c)) (∏' (b : β), f b)

Tactic:
classical
  have : mulSupport f = g '' mulSupport (f ∘ g) := by
    rw [mulSupport_comp_eq_preimage, Set.image_preimage_eq_iff.2 hf]
  rw [← Function.comp_def]
  by_cases hf_fin : (mulSupport f).Finite
  · have hfg_fin : (mulSupport (f ∘ g)).Finite := hf_fin.preimage hg.injOn
    lift g to γ ↪ β using hg
    simp_rw [tprod_eq_prod' hf_fin.coe_toFinset.ge, tprod_eq_prod' hfg_fin.coe_toFinset.ge,
      comp_apply, ← Finset.prod_map]
    refine Finset.prod_congr (Finset.coe_injective ?_) fun _ _ ↦ rfl
    simp [this]
  · have hf_fin' : ¬ Set.Finite (mulSupport (f ∘ g)) := by
      rwa [this, Set.finite_image_iff hg.injOn] at hf_fin
    simp_rw [tprod_def, SummationFilter.support_eq_univ, Set.inter_univ,
      show (unconditional β).HasSupport by infer_instance,
      show (unconditional γ).HasSupport by infer_instance, true_and,
      if_neg hf_fin, if_neg hf_fin', Multipliable]
    simp [hg.hasProd_iff (mulSupport_subset_iff'.1 hf)]

Premises used: SummationFilter.support_eq_univ, Set.inter_univ, Function.mulSupport_subset_iff', Set.Finite, Finset.prod_congr, Multipliable, Finset.coe_injective, Function.comp_def, Iff.mp, Function.mulSupport, Function.Injective.hasProd_iff, tprod_def, Function.comp_apply, Finset.prod_map, rfl, true_and, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
e : γ ≃ β
f : β → α
⊢ mulSupport f ⊆ Set.range.{u_2, u_3 + 1} (ι := γ) (⇑e : (a : γ) → β)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : TopologicalSpace α
β : Type u_4
inst_2 : InvolutiveNeg β
f : β → α
⊢ Eq.{u_1 + 1} (α := α) (∏' (d : β), f (-d)) (∏' (d : β), f d)

Tactic:
(Equiv.neg β).tprod_eq f

Premises used: Equiv.neg, Equiv.tprod_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst_2 : SetLike S α
inst_3 : SubmonoidClass S α
h_closed : IsClosed[inst_1] (↑s : Set α)
f : ι → α
h : ∀ (i : ι), f i ∈ s
pos : ∀ (hf : Multipliable f), ∏' (i : ι), f i ∈ s
neg : ∀ (hf : ¬Multipliable f), ∏' (i : ι), f i ∈ s
⊢ ∏' (i : ι), f i ∈ s

Tactic:
by_cases hf : Multipliable f

Premises used: Multipliable, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst_2 : SetLike S α
inst_3 : SubmonoidClass S α
h_closed : IsClosed[inst_1] (↑s : Set α)
f : ι → α
h : ∀ (i : ι), f i ∈ s
hf : Multipliable f
⊢ ∏' (i : ι), f i ∈ s

Tactic:
h_closed.mem_of_tendsto hf.hasProd <| .of_forall fun _ => prod_mem fun i _ => h i

Premises used: IsClosed.mem_of_tendsto, Filter.Eventually.of_forall, Multipliable.hasProd, prod_mem
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst_2 : SetLike S α
inst_3 : SubmonoidClass S α
h_closed : IsClosed[inst_1] (↑s : Set α)
f : ι → α
h : ∀ (i : ι), f i ∈ s
hf : Multipliable f
⊢ ∏' (i : ι), f i ∈ s

Tactic:
exact h_closed.mem_of_tendsto hf.hasProd <| .of_forall fun _ => prod_mem fun i _ => h i

Premises used: IsClosed.mem_of_tendsto, Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst_2 : SetLike S α
inst_3 : SubmonoidClass S α
h_closed : IsClosed[inst_1] (↑s : Set α)
f : ι → α
h : ∀ (i : ι), f i ∈ s
hf : ¬Multipliable f
⊢ ∏' (i : ι), f i ∈ s

Tactic:
simp [tprod_eq_one_of_not_multipliable hf, one_mem]

Premises used: tprod_eq_one_of_not_multipliable, OneMemClass.one_mem
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
s : Set β
hs : mulSupport f ⊆ s
⊢ mulSupport f ⊆ Set.range (ι := { x : β // x ∈ s }) (Subtype.val (p := fun (x : β) ↦ x ∈ s))

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑(mulSupport f) : Type u_2)), f (↑x : β)) (∏' (x : β), f x)

Tactic:
tprod_subtype_eq_of_mulSupport_subset Set.Subset.rfl

Premises used: Set.Subset.rfl, tprod_subtype_eq_of_mulSupport_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Set β
f : β → α
rw : ∀ (b : (↑s : Type u_2)), f (↑b : β) = s.mulIndicator f (↑b : β)
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑s : Type u_2)), f (↑x : β)) (∏' (x : β), s.mulIndicator f x)

Tactic:
rw [← tprod_subtype_eq_of_mulSupport_subset Set.mulSupport_mulIndicator_subset, tprod_congr]

Premises used: tprod_congr, tprod_subtype_eq_of_mulSupport_subset, Set.mulSupport_mulIndicator_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Set β
f : β → α
⊢ ∀ (b : (↑s : Type u_2)), f (↑b : β) = s.mulIndicator f (↑b : β)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑Set.univ : Type u_2)), f (↑x : β)) (∏' (x : β), f x)

Tactic:
tprod_subtype_eq_of_mulSupport_subset <| Set.subset_univ _

Premises used: Set.subset_univ, tprod_subtype_eq_of_mulSupport_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
g : γ → β
f : β → α
s : Set γ
hg : Set.InjOn g s
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑(g '' s) : Type u_2)), f (↑x : β)) (∏' (x : (↑s : Type u_3)), f (g (↑x : γ)))

Tactic:
((Equiv.Set.imageOfInjOn _ _ hg).tprod_eq fun x ↦ f x).symm

Premises used: Equiv.Set.imageOfInjOn, Equiv.tprod_eq, Eq.symm, Subtype.val
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
g : γ → β
f : β → α
hg : Injective g
rw : Eq.{u_1 + 1} (α := α) (∏' (x : (↑Set.univ : Type u_3)), f (g (↑x : γ))) (∏' (x : γ), f (g x))
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑(Set.range g) : Type u_2)), f (↑x : β)) (∏' (x : γ), f (g x))

Tactic:
rw [← Set.image_univ, tprod_image f hg.injOn]

Premises used: Set.image_univ, tprod_image, Function.Injective.injOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
g : γ → β
f : β → α
hg : Injective g
simp_rw : Eq.{u_1 + 1} (α := α) (∏' (x : (↑Set.univ : Type u_3)), (f ∘ g) (↑x : γ)) (∏' (x : γ), (f ∘ g) x)
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑Set.univ : Type u_3)), f (g (↑x : γ))) (∏' (x : γ), f (g x))

Tactic:
simp_rw [← comp_apply (g := g), tprod_univ (f ∘ g)]

Premises used: Function.comp, tprod_univ, Function.comp_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
s t : Set β
hf₀ : ∀ b ∈ t, f b = 1
b : (↑s : Type u_2)
hb : b ∉ Set.range (ι := (↑(s \ t) : Type u_2)) (Set.inclusion (s := s \ t) (t := s) ⋯)
⊢ (↑b : β) ∈ t

Tactic:
simpa using hb
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
s : Set β
b : β
hf₀ : f b = 1
⊢ Eq.{u_1 + 1} (α := α) (∏' (a : (↑s : Type u_2)), f (↑a : β)) (∏' (a : (↑(s \ {b}) : Type u_2)), f (↑a : β))

Tactic:
tprod_setElem_eq_tprod_setElem_diff s {b} fun _ ha ↦ ha ▸ hf₀

Premises used: Eq.rec, tprod_setElem_eq_tprod_setElem_diff, Singleton.singleton, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
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 : γ)
rw :
  Eq.{u_1 + 1} (α := α) (∏' (c : (↑(mulSupport g) : Type u_3)), f (i c))
    (∏' (x : (↑(mulSupport g) : Type u_3)), g (↑x : γ))
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : β), f x) (∏' (y : γ), g y)

Tactic:
rw [← tprod_subtype_mulSupport g, ← hi.tprod_eq hf]

Premises used: tprod_subtype_mulSupport, Function.Injective.tprod_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
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 : γ)
⊢ Eq.{u_1 + 1} (α := α) (∏' (c : (↑(mulSupport g) : Type u_3)), f (i c))
    (∏' (x : (↑(mulSupport g) : Type u_3)), g (↑x : γ))

Tactic:
simp only [hfg]
-- 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 : β)
⊢ mulSupport g ⊆
    Set.range.{u_3, u_2 + 1} (ι := (↑(mulSupport f) : Type u_2))
      (comp (β := { x : γ // x ∈ mulSupport g }) (Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g))
        (⇑e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
P : Prop
inst_2 : Decidable P
x : β → ¬P → α
pos :
  ∀ (hP : P),
    Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), if h : P then 1 else x b h) (if h : P then 1 else ∏'[L] (b : β), x b h)
neg :
  ∀ (hP : ¬P),
    Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), if h : P then 1 else x b h) (if h : P then 1 else ∏'[L] (b : β), x b h)
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), if h : P then 1 else x b h) (if h : P then 1 else ∏'[L] (b : β), x b h)

Tactic:
by_cases hP : P
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
P : Prop
inst_2 : Decidable P
x : β → ¬P → α
hP : P
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), if h : P then 1 else x b h) (if h : P then 1 else ∏'[L] (b : β), x b h)

Tactic:
simp [hP]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
P : Prop
inst_2 : Decidable P
x : β → ¬P → α
hP : ¬P
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), if h : P then 1 else x b h) (if h : P then 1 else ∏'[L] (b : β), x b h)

Tactic:
simp [hP]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
P : Prop
inst_2 : Decidable P
x : β → P → α
pos :
  ∀ (hP : P),
    Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), if h : P then x b h else 1) (if h : P then ∏'[L] (b : β), x b h else 1)
neg :
  ∀ (hP : ¬P),
    Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), if h : P then x b h else 1) (if h : P then ∏'[L] (b : β), x b h else 1)
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), if h : P then x b h else 1) (if h : P then ∏'[L] (b : β), x b h else 1)

Tactic:
by_cases hP : P
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
P : Prop
inst_2 : Decidable P
x : β → P → α
hP : P
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), if h : P then x b h else 1) (if h : P then ∏'[L] (b : β), x b h else 1)

Tactic:
simp [hP]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
P : Prop
inst_2 : Decidable P
x : β → P → α
hP : ¬P
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), if h : P then x b h else 1) (if h : P then ∏'[L] (b : β), x b h else 1)

Tactic:
simp [hP]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
γ : Type u_4
g : γ → β
hg : Injective g
f : γ → α
⊢ mulSupport (extend g f 1) ⊆ Set.range g

Tactic:
have : mulSupport (extend g f 1) ⊆ Set.range g := mulSupport_subset_iff'.2 <| extend_apply' _ _
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
γ : Type u_4
g : γ → β
hg : Injective g
f : γ → α
this : mulSupport (extend g f 1) ⊆ Set.range g
simp_rw : Eq.{u_1 + 1} (α := α) (∏' (c : γ), extend g f 1 (g c)) (∏' (x : γ), f x)
⊢ Eq.{u_1 + 1} (α := α) (∏' (y : β), extend g f 1 y) (∏' (x : γ), f x)

Tactic:
simp_rw [← hg.tprod_eq this, hg.extend_apply]

Premises used: Function.Injective.tprod_eq, Function.Injective.extend_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
f : β → α
i : β
hi : Membership.mem (γ := Set β) (⋃ (d : γ), s d) i
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
obtain : ∀ (j : γ) (hj : i ∈ s j), ∏' (d : γ), (s d).mulIndicator f i = f i
⊢ ∏' (d : γ), (s d).mulIndicator f i = f i

Tactic:
obtain ⟨j, hj⟩ := Set.mem_iUnion.mp hi

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
f : β → α
i : β
hi : Membership.mem (γ := Set β) (⋃ (d : γ), s d) i
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
j : γ
hj : i ∈ s j
rw : ∏' (x : (↑{j} : Type u_3)), (s (↑x : γ)).mulIndicator f i = f i
rw₁ : Subset (α := Set γ) (mulSupport.{u_3, u_1} (M := α) fun (d : γ) ↦ (s d).mulIndicator f i) {j}
⊢ ∏' (d : γ), (s d).mulIndicator f i = f i

Tactic:
rw [← tprod_subtype_eq_of_mulSupport_subset (s := {j})]

Premises used: tprod_subtype_eq_of_mulSupport_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
f : β → α
i : β
hi : Membership.mem (γ := Set β) (⋃ (d : γ), s d) i
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
j : γ
hj : i ∈ s j
⊢ ∏' (x : (↑{j} : Type u_3)), (s (↑x : γ)).mulIndicator f i = f i

Tactic:
aesop