awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
rcases :
  ∀ (s : Finset α) (hs : ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e),
    Membership.mem (γ := Filter α) cofinite (f ⁻¹' e)
⊢ Membership.mem (γ := Filter α) cofinite (f ⁻¹' e)

Tactic:
rcases hf.vanishing he with ⟨s, hs⟩

Premises used: Multipliable.vanishing
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
s : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
⊢ Membership.mem (γ := Filter α) cofinite (f ⁻¹' e)

Tactic:
s.eventually_cofinite_notMem.mono fun x hx ↦ ?_

Premises used: Set.Mem, Filter.Eventually, setOf, Finset.eventually_cofinite_notMem, Filter.Eventually.mono, Set.preimage
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
s : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
refine : ∀ (x : α) (hx : x ∉ s), f x ∈ e
⊢ Membership.mem (γ := Filter α) cofinite (f ⁻¹' e)

Tactic:
refine s.eventually_cofinite_notMem.mono fun x hx ↦ ?_

Premises used: Finset.eventually_cofinite_notMem, Filter.Eventually.mono
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
s : Finset α
hs : ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
x : α
hx : x ∉ s
⊢ f x ∈ e

Tactic:
simpa using hs {x} (disjoint_singleton_left.2 hx)

Premises used: Iff.mpr, Finset.disjoint_singleton_left, Singleton.singleton
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_5
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : DiscreteTopology α
β : Type u_6
f : β → α
h : Multipliable f
⊢ HasFiniteMulSupport f

Tactic:
haveI : IsTopologicalGroup α := ⟨⟩
  h.tendsto_cofinite_one (discreteTopology_iff_singleton_mem_nhds.mp ‹_› 1)

Premises used: Set.Mem, Multipliable.tendsto_cofinite_one, setOf, IsTopologicalGroup.mk, Set.Finite, discreteTopology_iff_singleton_mem_nhds, Set.preimage, Set.singleton, Iff.mp, Function.mulSupport, Function.HasFiniteMulSupport, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
inst_3 : FirstCountableTopology G
inst_4 : T1Space G
hf : Multipliable f
⊢ (mulSupport f).Countable

Tactic:
simpa only [ker_nhds] using hf.tendsto_cofinite_one.countable_compl_preimage_ker

Premises used: Multipliable.tendsto_cofinite_one, Filter.Tendsto.countable_compl_preimage_ker, ker_nhds
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : Infinite β
inst_4 : T2Space G
a : G
⊢ (Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ a) ↔ a = 1

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : Infinite β
inst_4 : T2Space G
a : G
refine_1 : ∀ (h : Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ a), a = 1
refine_2 : a = 1 → Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ a
⊢ (Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ a) ↔ a = 1

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : Infinite β
inst_4 : T2Space G
a : G
h : Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ a
refine_1 : ∀ (ha : ¬a = 1), False
⊢ a = 1

Tactic:
by_contra ha
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : Infinite β
inst_4 : T2Space G
a : G
h : Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ a
ha : ¬a = 1
⊢ Membership.mem (γ := Filter G) (𝓝 1) {a}ᶜ

Tactic:
have : {a}ᶜ ∈ 𝓝 1 := compl_singleton_mem_nhds (Ne.symm ha)
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : Infinite β
inst_4 : T2Space G
a : G
h : Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ a
ha : ¬a = 1
this : Membership.mem (γ := Filter G) (𝓝 1) {a}ᶜ
⊢ Finite β

Tactic:
simpa [← Set.finite_univ_iff] using h.tendsto_cofinite_one this

Premises used: Multipliable.tendsto_cofinite_one, Set.finite_univ_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : Infinite β
inst_4 : T2Space G
a : G
h : Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ a
ha : ¬a = 1
this : Membership.mem (γ := Filter G) (𝓝 1) {a}ᶜ
⊢ Finite β

Tactic:
have : Finite β := by
      simpa [← Set.finite_univ_iff] using h.tendsto_cofinite_one this
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : Infinite β
inst_4 : T2Space G
a : G
h : Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ a
ha : ¬a = 1
this_1 : Membership.mem (γ := Filter G) (𝓝 1) {a}ᶜ
this : Finite β
⊢ False

Tactic:
not_finite β

Premises used: not_finite
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : Infinite β
inst_4 : T2Space G
a : G
h : Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ a
ha : ¬a = 1
this_1 : Membership.mem (γ := Filter G) (𝓝 1) {a}ᶜ
this : Finite β
⊢ False

Tactic:
exact not_finite β

Premises used: not_finite
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : Infinite β
inst_4 : T2Space G
⊢ Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ 1

Tactic:
multipliable_one

Premises used: multipliable_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : Infinite β
inst_4 : T2Space G
⊢ Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ 1

Tactic:
exact multipliable_one

Premises used: multipliable_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
a : G
inl : ∀ (hβ : Finite β), ∏' (x : β), a = a ^ Nat.card β
inr : ∀ (hβ : Infinite β), ∏' (x : β), a = a ^ Nat.card β
⊢ ∏' (x : β), a = a ^ Nat.card β

Tactic:
rcases finite_or_infinite β with hβ | hβ

Premises used: finite_or_infinite
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
a : G
hβ : Finite β
this : Fintype β := Fintype.ofFinite β
inl : ∏ b : β, a = a ^ Nat.card β
⊢ ∏' (x : β), a = a ^ Nat.card β

Tactic:
rw [tprod_eq_prod (s := univ) (fun x hx ↦ (hx (mem_univ x)).elim)]

Premises used: Finset.mem_univ, False.elim, tprod_eq_prod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
a : G
hβ : Finite β
this : Fintype β := Fintype.ofFinite β
⊢ ∏ b : β, a = a ^ Nat.card β

Tactic:
simp only [prod_const, Nat.card_eq_fintype_card, Fintype.card]

Premises used: Fintype.card, Finset.prod_const, Nat.card_eq_fintype_card
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
a : G
hβ : Infinite β
inr : Eq.{u_4 + 1} (α := G) (∏' (x : β), a) 1
⊢ ∏' (x : β), a = a ^ Nat.card β

Tactic:
simp only [Nat.card_eq_zero_of_infinite, pow_zero]

Premises used: Nat.card_eq_zero_of_infinite, pow_zero
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
a : G
hβ : Infinite β
inr : Eq.{u_4 + 1} (α := G) (∏' (x : β), 1) 1
inr₁ : ∀ (ha : a ≠ 1), Eq.{u_4 + 1} (α := G) (∏' (x : β), a) 1
⊢ Eq.{u_4 + 1} (α := G) (∏' (x : β), a) 1

Tactic:
rcases eq_or_ne a 1 with rfl | ha

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
hβ : Infinite β
⊢ Eq.{u_4 + 1} (α := G) (∏' (x : β), 1) 1

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
a : G
hβ : Infinite β
ha : a ≠ 1
inr : ¬Multipliable.{u_4, u_2} (α := G) fun (b : β) ↦ a
⊢ Eq.{u_4 + 1} (α := G) (∏' (x : β), a) 1

Tactic:
apply tprod_eq_one_of_not_multipliable

Premises used: tprod_eq_one_of_not_multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
β : Type u_2
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
a : G
hβ : Infinite β
ha : a ≠ 1
⊢ ¬Multipliable.{u_4, u_2} (α := G) fun (b : β) ↦ a

Tactic:
simpa [multipliable_const_iff] using ha

Premises used: multipliable_const_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
⊢ HasProd g (c * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i))

Tactic:
(Tendsto.mul_const ((∏ i ∈ s, g i) / ∏ i ∈ s, f i) hc).congr' ?_

Premises used: HasProd, Filter.Tendsto.mul_const, HDiv.hDiv, Finset.prod, Filter.Tendsto.congr'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
refine :
  EventuallyEq.{u_1, u_4} (β := K) (SummationFilter.unconditional α).filter
    (fun (x : Finset α) ↦ (∏ b ∈ x, f b) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i)) fun (s : Finset α) ↦
    ∏ b ∈ s, g b
⊢ HasProd g (c * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i))

Tactic:
refine (Tendsto.mul_const ((∏ i ∈ s, g i) / ∏ i ∈ s, f i) hc).congr' ?_

Premises used: Filter.Tendsto.mul_const, HDiv.hDiv, Finset.prod, Filter.Tendsto.congr'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
h : ∀ (t : Finset α) (ht : s ≤ t), (∏ b ∈ t, f b) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i) = ∏ b ∈ t, g b
⊢ EventuallyEq.{u_1, u_4} (β := K) (SummationFilter.unconditional α).filter
    (fun (x : Finset α) ↦ (∏ b ∈ x, f b) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i)) fun (s : Finset α) ↦
    ∏ b ∈ s, g b

Tactic:
filter_upwards [eventually_ge_atTop s] with t ht

Premises used: Filter.eventually_ge_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ≤ t
rw : (∏ x ∈ s, f x) * (t \ s).prod g * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i)
| (∏ i ∈ t, f i) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i)

Tactic:
rw [← union_sdiff_of_subset ht, prod_union disjoint_sdiff,
      prod_congr rfl fun i hi ↦ hs' i (mem_sdiff.mp hi).2]

Premises used: Finset.prod_union, Finset.prod_congr, Finset.disjoint_sdiff, Finset.mem_sdiff, And.right, Iff.mp, Finset.union_sdiff_of_subset, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ≤ t
conv_lhs :
  (∏ i ∈ t, f i) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i) =
    HMul.hMul (α := K) (∏ i ∈ s, f i) (∏ i ∈ t \ s, g i) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i)
conv_lhs₁ :
  (∏ x ∈ s, f x) * (t \ s).prod g * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i) =
    HMul.hMul (α := K) (∏ i ∈ s, f i) (∏ i ∈ t \ s, g i) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i)
⊢ (∏ i ∈ t, f i) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i) =
    HMul.hMul (α := K) (∏ i ∈ s, f i) (∏ i ∈ t \ s, g i) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i)

Tactic:
conv_lhs => rw [← union_sdiff_of_subset ht, prod_union disjoint_sdiff,
      prod_congr rfl fun i hi ↦ hs' i (mem_sdiff.mp hi).2]

Premises used: Finset.prod_union, Finset.prod_congr, Finset.disjoint_sdiff, Finset.mem_sdiff, And.right, Iff.mp, Finset.union_sdiff_of_subset, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ≤ t
rw : Ne.{u_4 + 1} (α := K) (∏ i ∈ s, f i) 0
⊢ HMul.hMul (α := K) (∏ i ∈ s, f i) (∏ i ∈ t \ s, g i) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i) =
    HMul.hMul (α := K) (∏ i ∈ s, g i) (∏ i ∈ t \ s, g i)

Tactic:
rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self, one_mul, mul_comm]

Premises used: mul_div_assoc, div_mul_eq_mul_div, mul_comm, one_mul, div_self
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ≤ t
⊢ Ne.{u_4 + 1} (α := K) (∏ i ∈ s, f i) 0

Tactic:
prod_ne_zero_iff.mpr hs

Premises used: Iff.mpr, Finset.prod_ne_zero_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ≤ t
⊢ Ne.{u_4 + 1} (α := K) (∏ i ∈ s, f i) 0

Tactic:
exact prod_ne_zero_iff.mpr hs

Premises used: Iff.mpr, Finset.prod_ne_zero_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ≤ t
rw : Eq.{u_4 + 1} (α := K) (∏ x ∈ s ∪ t \ s, g x) (∏ i ∈ t, g i)
rw₁ rw₂ : Eq.{u_4 + 1} (α := K) (∏ x ∈ t, g x) (∏ i ∈ t, g i)
⊢ HMul.hMul (α := K) (∏ i ∈ s, g i) (∏ i ∈ t \ s, g i) = ∏ i ∈ t, g i

Tactic:
rw [← prod_union disjoint_sdiff, union_sdiff_of_subset ht]

Premises used: Finset.prod_union, Finset.disjoint_sdiff, Finset.union_sdiff_of_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ≤ t
calc :
  (∏ i ∈ t, f i) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i) =
    HMul.hMul (α := K) (∏ i ∈ s, f i) (∏ i ∈ t \ s, g i) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i)
calc₁ :
  HMul.hMul (α := K) (∏ i ∈ s, f i) (∏ i ∈ t \ s, g i) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i) =
    HMul.hMul (α := K) (∏ i ∈ s, g i) (∏ i ∈ t \ s, g i)
calc₂ : HMul.hMul (α := K) (∏ i ∈ s, g i) (∏ i ∈ t \ s, g i) = ∏ i ∈ t, g i
⊢ (∏ b ∈ t, f b) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i) = ∏ b ∈ t, g b

Tactic:
calc (∏ i ∈ t, f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)
  _ = ((∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) * _ := by
    conv_lhs => rw [← union_sdiff_of_subset ht, prod_union disjoint_sdiff,
      prod_congr rfl fun i hi ↦ hs' i (mem_sdiff.mp hi).2]
  _ = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i := by
    rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self, one_mul, mul_comm]
    exact prod_ne_zero_iff.mpr hs
  _ = ∏ i ∈ t, g i := by
    rw [← prod_union disjoint_sdiff, union_sdiff_of_subset ht]

Premises used: HMul.hMul, HDiv.hDiv, Finset.prod, SDiff.sdiff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
refine :
  EventuallyEq.{u_1, u_4} (β := K) (SummationFilter.unconditional α).filter
    (fun (x : Finset α) ↦ (∏ b ∈ x, f b) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i)) fun (s : Finset α) ↦
    ∏ b ∈ s, g b
h : ∀ (t : Finset α) (ht : s ≤ t), (∏ b ∈ t, f b) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i) = ∏ b ∈ t, g b
⊢ HasProd g (c * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i))

Tactic:
classical
  refine (Tendsto.mul_const ((∏ i ∈ s, g i) / ∏ i ∈ s, f i) hc).congr' ?_
  filter_upwards [eventually_ge_atTop s] with t ht
  calc (∏ i ∈ t, f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)
  _ = ((∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) * _ := by
    conv_lhs => rw [← union_sdiff_of_subset ht, prod_union disjoint_sdiff,
      prod_congr rfl fun i hi ↦ hs' i (mem_sdiff.mp hi).2]
  _ = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i := by
    rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self, one_mul, mul_comm]
    exact prod_ne_zero_iff.mpr hs
  _ = ∏ i ∈ t, g i := by
    rw [← prod_union disjoint_sdiff, union_sdiff_of_subset ht]

Premises used: Filter.Tendsto.mul_const, HDiv.hDiv, Finset.prod, Filter.eventually_ge_atTop, Filter.Tendsto.congr'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
inst_3 : T2Space K
hc : Multipliable f
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
⊢ ∏' (i : α), g i = (∏' (i : α), f i) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i)

Tactic:
(hc.hasProd.congr_cofinite₀ hs hs').tprod_eq

Premises used: HasProd.congr_cofinite₀, HasProd.tprod_eq, Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
hf : Multipliable f
hf' : ∀ (a : α), f a ≠ 0
hfg : ∀ᶠ (a : α) in cofinite, f a = g a
obtain : ∀ (c : K) (hc : HasProd f c), Multipliable g
⊢ Multipliable g

Tactic:
obtain ⟨c, hc⟩ := hf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
hf' : ∀ (a : α), f a ≠ 0
hfg : ∀ᶠ (a : α) in cofinite, f a = g a
c : K
hc : HasProd f c
⊢ ∀ i ∉ Set.Finite.toFinset (s := {x : α | (fun (a : α) ↦ f a = g a) x}ᶜ) hfg, f i = g i

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
hf' : ∀ (a : α), f a ≠ 0
hfg : ∀ᶠ (a : α) in cofinite, f a = g a
c : K
hc : HasProd f c
obtain : ∀ (s : Finset α) (hs : ∀ i ∉ s, f i = g i), Multipliable g
⊢ Multipliable g

Tactic:
obtain ⟨s, hs⟩ : ∃ s : Finset α, ∀ i ∉ s, f i = g i := ⟨hfg.toFinset, by simp⟩

Premises used: Finset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
hf' : ∀ (a : α), f a ≠ 0
hfg : ∀ᶠ (a : α) in cofinite, f a = g a
c : K
hc : HasProd f c
s : Finset α
hs : ∀ i ∉ s, f i = g i
⊢ Multipliable g

Tactic:
(hc.congr_cofinite₀ (fun a _ ↦ hf' a) hs).multipliable

Premises used: HasProd.congr_cofinite₀, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
hf' : ∀ (a : α), f a ≠ 0
hfg : ∀ᶠ (a : α) in cofinite, f a = g a
c : K
hc : HasProd f c
s : Finset α
hs : ∀ i ∉ s, f i = g i
⊢ Multipliable g

Tactic:
exact (hc.congr_cofinite₀ (fun a _ ↦ hf' a) hs).multipliable

Premises used: HasProd.congr_cofinite₀, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
K : Type u_4
inst : CommGroupWithZero K
inst_1 : TopologicalSpace K
inst_2 : SeparatelyContinuousMul K
f g : α → K
hf : Multipliable f
hf' : ∀ (a : α), f a ≠ 0
hfg : ∀ᶠ (a : α) in cofinite, f a = g a
obtain : ∀ (c : K) (hc : HasProd f c), Multipliable g
obtain₁ : ∀ (c : K) (hc : HasProd f c) (s : Finset α) (hs : ∀ i ∉ s, f i = g i), Multipliable g
⊢ Multipliable g

Tactic:
classical
  obtain ⟨c, hc⟩ := hf
  obtain ⟨s, hs⟩ : ∃ s : Finset α, ∀ i ∉ s, f i = g i := ⟨hfg.toFinset, by simp⟩
  exact (hc.congr_cofinite₀ (fun a _ ↦ hf' a) hs).multipliable

Premises used: Finset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
L : SummationFilter β
f : β → α
a : α
⊢ HasSum (α := UniformSpace.Completion α) ((⇑toCompl : (a : α) → UniformSpace.Completion α) ∘ f)
      (↑a : UniformSpace.Completion α) L ↔
    HasSum f a L

Tactic:
(isDenseInducing_toCompl α).hasSum_iff f a

Premises used: UniformSpace.Completion.coe', IsDenseInducing.toIsInducing, SeparationQuotient.mk, Topology.IsInducing.hasSum_iff, UniformSpace.Completion.isDenseInducing_toCompl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
L : SummationFilter β
f : β → α
⊢ Summable f L ↔
    Summable (α := UniformSpace.Completion α) ((⇑toCompl : (a : α) → UniformSpace.Completion α) ∘ f) L ∧
      Membership.mem (γ := Set (UniformSpace.Completion α))
        (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
        (∑'[L] (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))

Tactic:
(isDenseInducing_toCompl α).summable_iff_tsum_comp_mem_range f

Premises used: IsDenseInducing.toIsInducing, Topology.IsInducing.summable_iff_tsum_comp_mem_range, UniformSpace.Completion.isDenseInducing_toCompl