awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ : α
inst_3 : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst_4 : DecidableEq β
a : α
b' : β
h : b' = b
⊢ a = (if b = b then a / f b else 1) * f b

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ : α
inst_3 : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst_4 : DecidableEq β
a : α
b' : β
h : ¬b' = b
⊢ Function.update (β := fun (a : β) ↦ α) f b a b' = (if b' = b then a / f b else 1) * f b'

Tactic:
simp only [h, update_of_ne, if_false, Ne, one_mul, not_false_iff]

Premises used: if_false, Ne, not_false_iff, one_mul, Function.update_of_ne
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
inst_3 : L.LeAtTop
hf : Multipliable f L
b : β
inst_4 : DecidableEq β
a : α
⊢ Multipliable (Function.update (β := fun (a : β) ↦ α) f b a) L

Tactic:
(hf.hasProd.update b a).multipliable

Premises used: Multipliable.hasProd, HasProd.multipliable, HasProd.update
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a₁
⊢ HasProd (β := (↑sᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ sᶜ)) a₂ ↔ HasProd f (a₁ * a₂)

Tactic:
⟨fun h ↦ hf.mul_compl h, fun h ↦ ?_⟩

Premises used: Iff.intro, HasProd.mul_compl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a₁
refine : ∀ (h : HasProd f (a₁ * a₂)), HasProd (β := (↑sᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ sᶜ)) a₂
⊢ HasProd (β := (↑sᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ sᶜ)) a₂ ↔ HasProd f (a₁ * a₂)

Tactic:
refine ⟨fun h ↦ hf.mul_compl h, fun h ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a₁
h : HasProd f (a₁ * a₂)
rw : ∀ (hf : HasProd (s.mulIndicator f) a₁) (h : HasProd f (a₁ * a₂)), HasProd (sᶜ.mulIndicator f) a₂
⊢ HasProd (β := (↑sᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ sᶜ)) a₂

Tactic:
rw [hasProd_subtype_iff_mulIndicator] at hf ⊢

Premises used: hasProd_subtype_iff_mulIndicator
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (s.mulIndicator f) a₁
h : HasProd f (a₁ * a₂)
rw : HasProd (f * (s.mulIndicator f)⁻¹) a₂
⊢ HasProd (sᶜ.mulIndicator f) a₂

Tactic:
rw [Set.mulIndicator_compl]

Premises used: Set.mulIndicator_compl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (s.mulIndicator f) a₁
h : HasProd f (a₁ * a₂)
⊢ HasProd (f * (s.mulIndicator f)⁻¹) a₂

Tactic:
simpa only [div_eq_mul_inv, mul_inv_cancel_comm] using h.div hf

Premises used: mul_inv_cancel_comm, HasProd.div, div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a₁
rw rw₁ : HasProd f a₂ ↔ HasProd f a₂
⊢ HasProd f (a₁ * (a₂ / a₁)) ↔ HasProd f a₂

Tactic:
rw [mul_div_cancel]

Premises used: mul_div_cancel
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a : α
s : Finset β
rw rw₁ : HasProd f (a * ∏ b ∈ s, f b) ↔ HasProd f (a * ∏ i ∈ s, f i)
⊢ HasProd f ((∏ b ∈ s, f b) * a) ↔ HasProd f (a * ∏ i ∈ s, f i)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a : α
s : Finset β
⊢ HasProd f a ↔ HasProd (fun (x : { x : β // x ∉ s }) ↦ f (↑x : β)) (a / ∏ i ∈ s, f i)

Tactic:
(s.hasProd f).hasProd_iff_compl

Premises used: Set.Mem, setOf, Set.Elem, SetLike.coe, HasProd.hasProd_iff_compl, Finset.hasProd, Not, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
s : Finset β
⊢ (Multipliable.{u_1, u_2} (α := α) fun (x : { x : β // x ∉ s }) ↦ f (↑x : β)) ↔ Multipliable f

Tactic:
(s.multipliable f).multipliable_compl_iff

Premises used: Finset.multipliable, Set.Mem, setOf, Multipliable.multipliable_compl_iff, Not
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
s : Set β
hs : s.Finite
⊢ Multipliable (β := (↑sᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ sᶜ)) ↔ Multipliable f

Tactic:
(hs.multipliable f).multipliable_compl_iff

Premises used: Set.Finite.multipliable, Multipliable.multipliable_compl_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a : α
inst_3 : L.LeAtTop
inst_4 : DecidableEq β
hf : HasProd f a L
b : β
⊢ HasProd (update (β := fun (a : β) ↦ α) f b 1) (1 / f b * a) L

Tactic:
hf.update b 1

Premises used: HasProd.update, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a : α
inst_3 : L.LeAtTop
inst_4 : DecidableEq β
hf : HasProd f a L
b : β
h : (fun (n : β) ↦ if n = b then 1 else f n) = update (β := fun (a : β) ↦ α) f b 1
h₁ : a / f b = 1 / f b * a
⊢ HasProd (fun (n : β) ↦ if n = b then 1 else f n) (a / f b) L

Tactic:
convert! hf.update b 1 using 1

Premises used: HasProd.update, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a : α
inst_3 : L.LeAtTop
inst_4 : DecidableEq β
hf : HasProd f a L
b : β
h : ∀ (n : β), (if n = b then 1 else f n) = update (β := fun (a : β) ↦ α) f b 1 n
⊢ (fun (n : β) ↦ if n = b then 1 else f n) = update (β := fun (a : β) ↦ α) f b 1

Tactic:
ext n
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a : α
inst_3 : L.LeAtTop
inst_4 : DecidableEq β
hf : HasProd f a L
b n : β
h h₁ : (if n = b then 1 else f n) = if n = b then 1 else f n
⊢ (if n = b then 1 else f n) = update (β := fun (a : β) ↦ α) f b 1 n

Tactic:
rw [Function.update_apply]

Premises used: Function.update_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
a : α
inst_3 : L.LeAtTop
inst_4 : DecidableEq β
hf : HasProd f a L
b : β
h : a / f b = 1 * a / f b
h₁ h₂ : a / f b = a / f b
⊢ a / f b = 1 / f b * a

Tactic:
rw [div_mul_eq_mul_div, one_mul]

Premises used: div_mul_eq_mul_div, one_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f g : β → α
hf : Multipliable f
hfg : f =ᶠ[cofinite] g
⊢ ∀ (b : (↑{x : β | (fun (x : β) ↦ f x = g x) x}ᶜᶜ : Type u_2)),
    (f ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f x = g x) x}ᶜᶜ x)) b =
      (g ∘ Subtype.val (p := fun (x : β) ↦ Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f x = g x) x}ᶜᶜ x)) b

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f g : β → α
hfg : f =ᶠ[cofinite] g
⊢ Multipliable f ↔ Multipliable g

Tactic:
⟨fun h ↦ h.congr_cofinite hfg, fun h ↦ h.congr_cofinite (hfg.mono fun _ h' ↦ h'.symm)⟩

Premises used: Multipliable.congr_cofinite, Filter.Eventually.mono, Iff.intro, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f₁ g₁ : ℕ → α
hf : Multipliable f₁
hfg : f₁ =ᶠ[atTop] g₁
⊢ Multipliable g₁

Tactic:
hf.congr_cofinite (Nat.cofinite_eq_atTop ▸ hfg)

Premises used: Multipliable.congr_cofinite, Eq.rec, Nat.cofinite_eq_atTop, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f₁ g₁ : ℕ → α
hfg : f₁ =ᶠ[atTop] g₁
⊢ Multipliable f₁ ↔ Multipliable g₁

Tactic:
multipliable_congr_cofinite (Nat.cofinite_eq_atTop ▸ hfg)

Premises used: Eq.rec, multipliable_congr_cofinite, Nat.cofinite_eq_atTop, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
inst_3 : T2Space α
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), (f b)⁻¹) (∏'[L] (b : β), f b)⁻¹

Tactic:
((Homeomorph.inv α).isClosedEmbedding.map_tprod f (g := MulEquiv.inv α)).symm

Premises used: Topology.IsClosedEmbedding.map_tprod, Homeomorph.inv, Homeomorph.isClosedEmbedding, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f g : β → α
inst_3 : T2Space α
inst_4 : L.NeBot
hf : Multipliable f L
hg : Multipliable g L
⊢ ∏'[L] (b : β), f b / g b = HDiv.hDiv (α := α) (∏'[L] (b : β), f b) (∏'[L] (b : β), g b)

Tactic:
(hf.hasProd.div hg.hasProd).tprod_eq

Premises used: HasProd.div, HasProd.tprod_eq, Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
inst_3 : T2Space α
s : Finset β
hf : Multipliable f
⊢ HMul.hMul (α := α) (∏ x ∈ s, f x) (∏' (x : (↑(↑s : Set β)ᶜ : Type u_2)), f (↑x : β)) = ∏' (x : β), f x

Tactic:
((s.hasProd f).mul_compl (s.multipliable_compl_iff.2 hf).hasProd).tprod_eq.symm

Premises used: Iff.mpr, Set.Mem, setOf, Set.Elem, HasProd.tprod_eq, Multipliable.hasProd, SetLike.coe, Finset.multipliable_compl_iff, Finset.hasProd, HasProd.mul_compl, Eq.symm, Not, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
inst_3 : T2Space α
inst_4 : DecidableEq β
hf : Multipliable f
b : β
rw : ∏' (n : β), f n = f b * ((∏' (b : β), f b) / f b)
⊢ ∏' (n : β), f n = f b * ∏' (n : β), if n = b then 1 else f n

Tactic:
rw [(hasProd_ite_div_hasProd hf.hasProd b).tprod_eq]

Premises used: HasProd.tprod_eq, Multipliable.hasProd, hasProd_ite_div_hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
inst_3 : T2Space α
inst_4 : DecidableEq β
hf : Multipliable f
b : β
⊢ ∏' (n : β), f n = f b * ((∏' (b : β), f b) / f b)

Tactic:
(mul_div_cancel _ _).symm

Premises used: mul_div_cancel, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalGroup α
f : β → α
inst_3 : T2Space α
inst_4 : DecidableEq β
hf : Multipliable f
b : β
⊢ ∏' (n : β), f n = f b * ((∏' (b : β), f b) / f b)

Tactic:
exact (mul_div_cancel _ _).symm

Premises used: mul_div_cancel, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommMonoid α
inst_2 : CompleteSpace α
f : β → α
⊢ Multipliable f ↔ CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∏ b ∈ s, f b

Tactic:
cauchy_map_iff_exists_tendsto.symm

Premises used: iInf, CauchySeq, cauchy_map_iff_exists_tendsto, HasProd, Multipliable, Filter.atTop, Iff.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommMonoid α
inst_2 : CompleteSpace α
f : β → α
⊢ Multipliable f ↔ CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∏ b ∈ s, f b

Tactic:
exact cauchy_map_iff_exists_tendsto.symm

Premises used: cauchy_map_iff_exists_tendsto, Iff.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommMonoid α
inst_2 : CompleteSpace α
f : β → α
⊢ Multipliable f ↔ CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∏ b ∈ s, f b

Tactic:
classical exact cauchy_map_iff_exists_tendsto.symm

Premises used: cauchy_map_iff_exists_tendsto, Iff.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
simp :
  Tendsto.{u_2, u_1} (β := α) (fun (x : Finset β × Finset β) ↦ HDiv.hDiv (α := α) (∏ b ∈ x.2, f b) (∏ b ∈ x.1, f b))
      atTop (𝓝 1) ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
⊢ (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∏ b ∈ s, f b) ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
simp only [CauchySeq, cauchy_map_iff, prod_atTop_atTop_eq,
    uniformity_eq_comap_nhds_one α, tendsto_comap_iff, Function.comp_def, atTop_neBot, true_and]

Premises used: CauchySeq, cauchy_map_iff, Filter.atTop_neBot, Filter.tendsto_comap_iff, Function.comp_def, Filter.prod_atTop_atTop_eq, uniformity_eq_comap_nhds_one, true_and
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
rw :
  (∀ (s : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) s →
        ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ s) ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : Finset β × Finset β) ↦ HDiv.hDiv (α := α) (∏ b ∈ x.2, f b) (∏ b ∈ x.1, f b))
      atTop (𝓝 1) ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
rw [tendsto_atTop']

Premises used: Filter.tendsto_atTop'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
mp :
  (∀ (s : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) s →
        ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ s) →
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
mpr :
  (∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e) →
    ∀ (s : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) s →
        ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ s
⊢ (∀ (s : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) s →
        ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ s) ↔
    ∀ (e : Set α),
      Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
h :
  ∀ (s : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) s →
      ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ s
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
mp :
  ∀ (s₁ s₂ : Finset β) (h : ∀ b ≥ (s₁, s₂), HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ e),
    ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
⊢ ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
obtain ⟨⟨s₁, s₂⟩, h⟩ := h e he
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
h_1 :
  ∀ (s : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) s →
      ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ s
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
s₁ s₂ : Finset β
h : ∀ b ≥ (s₁, s₂), HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ e
h₁ : ∀ (t : Finset β), Disjoint t (s₁ ∪ s₂) → ∏ b ∈ t, f b ∈ e
⊢ ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
use s₁ ∪ s₂
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
h_1 :
  ∀ (s : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) s →
      ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ s
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
s₁ s₂ : Finset β
h : ∀ b ≥ (s₁, s₂), HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ e
t : Finset β
ht : Disjoint t (s₁ ∪ s₂)
⊢ HDiv.hDiv (α := α) (∏ b ∈ (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).2, f b) (∏ b ∈ (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).1, f b) ∈ e

Tactic:
specialize h (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t) ⟨le_sup_left, le_sup_of_le_left le_sup_right⟩

Premises used: le_sup_left, le_sup_of_le_left, Prod.mk, le_sup_right, And.intro, Union.union
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
h_1 :
  ∀ (s : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) s →
      ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ s
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
s₁ s₂ t : Finset β
ht : Disjoint t (s₁ ∪ s₂)
h : HDiv.hDiv (α := α) (∏ b ∈ (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).2, f b) (∏ b ∈ (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).1, f b) ∈ e
⊢ ∏ b ∈ t, f b ∈ e

Tactic:
simpa only [Finset.prod_union ht.symm, mul_div_cancel_left] using h

Premises used: Finset.prod_union, Disjoint.symm, mul_div_cancel_left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
h :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
mpr :
  ∀ (d : Set α) (hd : Membership.mem (γ := Filter α) (𝓝 1) d) (hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e),
    ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ e
⊢ ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ e

Tactic:
rcases exists_nhds_split_inv he with ⟨d, hd, hde⟩

Premises used: exists_nhds_split_inv
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
h :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
d : Set α
hd : Membership.mem (γ := Filter α) (𝓝 1) d
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
mpr :
  ∀ (s : Finset β) (h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d),
    ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ e
⊢ ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ e

Tactic:
rcases h d hd with ⟨s, h⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
h_1 :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
d : Set α
hd : Membership.mem (γ := Filter α) (𝓝 1) d
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
h₁ : ∀ b ≥ (s, s), HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ e
⊢ ∃ (a : Finset β × Finset β), ∀ b ≥ a, HDiv.hDiv (α := α) (∏ b ∈ b.2, f b) (∏ b ∈ b.1, f b) ∈ e

Tactic:
use (s, s)

Premises used: Prod.mk
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
h_1 :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
d : Set α
hd : Membership.mem (γ := Filter α) (𝓝 1) d
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ≤ (t₁, t₂).1
ht₂ : (s, s).2 ≤ (t₁, t₂).2
rw :
  (∏ b ∈ t₂, f b) / HMul.hMul (α := α) (∏ x ∈ (t₁, t₂).1 \ (s, s).1, f x) (∏ x ∈ (s, s).1, f x) =
    HDiv.hDiv (α := α) (∏ b ∈ t₂ \ s, f b) (∏ b ∈ t₁ \ s, f b)
rw₁ :
  HMul.hMul (α := α) (∏ x ∈ (t₁, t₂).2 \ (s, s).2, f x) (∏ x ∈ (s, s).2, f x) /
      HMul.hMul (α := α) (∏ x ∈ (t₁, t₂).1 \ (s, s).1, f x) (∏ x ∈ (s, s).1, f x) =
    HDiv.hDiv (α := α) (∏ b ∈ t₂ \ s, f b) (∏ b ∈ t₁ \ s, f b)
rw₂ rw₃ :
  HDiv.hDiv (α := α) (∏ x ∈ (t₁, t₂).2 \ (s, s).2, f x) (∏ x ∈ (t₁, t₂).1 \ (s, s).1, f x) =
    HDiv.hDiv (α := α) (∏ b ∈ t₂ \ s, f b) (∏ b ∈ t₁ \ s, f b)
⊢ HDiv.hDiv (α := α) (∏ b ∈ t₂, f b) (∏ b ∈ t₁, f b) = HDiv.hDiv (α := α) (∏ b ∈ t₂ \ s, f b) (∏ b ∈ t₁ \ s, f b)

Tactic:
rw [← Finset.prod_sdiff ht₁, ← Finset.prod_sdiff ht₂, mul_div_mul_right_eq_div]

Premises used: mul_div_mul_right_eq_div, Finset.prod_sdiff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Group
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
f : β → α
h_1 :
  ∀ (e : Set α),
    Membership.mem (γ := Filter α) (𝓝 1) e → ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : Membership.mem (γ := Filter α) (𝓝 1) e
d : Set α
hd : Membership.mem (γ := Filter α) (𝓝 1) d
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ≤ (t₁, t₂).1
ht₂ : (s, s).2 ≤ (t₁, t₂).2
⊢ HDiv.hDiv (α := α) (∏ b ∈ t₂, f b) (∏ b ∈ t₁, f b) = HDiv.hDiv (α := α) (∏ b ∈ t₂ \ s, f b) (∏ b ∈ t₁ \ s, f b)

Tactic:
have : ((∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b) = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b := by
      rw [← Finset.prod_sdiff ht₁, ← Finset.prod_sdiff ht₂, mul_div_mul_right_eq_div]