awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ HMul.hMul (α := α) (∏ x ∈ s, f x) (∏' (x : { x : β // x ∉ s }), f (↑x : β)) = ∏' (x : β), f x
have rw : HMul.hMul (α := α) (∏ x ∈ s, f x) (∏' (x : { x : β // x ∉ s }), f (↑x : β)) =
  HMul.hMul (α := α) (∏' (x : (↑(↑s : Set β) : Type u_2)), f (↑x : β))
    (∏' (x : (↑(↑s : Set β)ᶜ : Type u_2)), f (↑x : β))
Tactic: rw [← hf.tprod_subtype_mul_tprod_subtype_compl s]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : CommGroup α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ HMul.hMul (α := α) (∏ x ∈ s, f x) (∏' (x : { x : β // x ∉ s }), f (↑x : β)) =
    HMul.hMul (α := α) (∏' (x : (↑(↑s : Set β) : Type u_2)), f (↑x : β))
      (∏' (x : (↑(↑s : Set β)ᶜ : Type u_2)), f (↑x : β))
have simp : Eq.{u_1 + 1} (α := α) (∏' (x : { x : β // x ∉ s }), f (↑x : β)) (∏' (x : (↑(↑s : Set β)ᶜ : Type u_2)), f (↑x : β))
Tactic: simp only [Finset.tprod_subtype', mul_right_inj]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (hypothesis)
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
this : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
⊢ ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
have this₁ : IsUniformGroup G
Tactic: have : IsUniformGroup G := isUniformGroup_of_commGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
letI letI₁ letI₂ : ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
⊢ ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
have letI₃ : let this := IsTopologicalGroup.rightUniformSpace G;
∀ (this : IsUniformGroup G), ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
Tactic: classical
  letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
  have : IsUniformGroup G := isUniformGroup_of_commGroup
  exact cauchySeq_finset_iff_prod_vanishing.1 hf.hasProd.cauchySeq e he
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (hypothesis)
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
this : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
⊢ ∃ (s : Finset α), ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e
have this₁ : IsUniformGroup G
Tactic: have : IsUniformGroup G := isUniformGroup_of_commGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
letI letI₁ letI₂ : ∃ (s : Finset α), ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e
⊢ ∃ (s : Finset α), ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e
have letI₃ : let this := IsTopologicalGroup.rightUniformSpace G;
∀ (this : IsUniformGroup G),
  ∃ (s : Finset α), ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e
Tactic: classical
  letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
  have : IsUniformGroup G := isUniformGroup_of_commGroup
  exact cauchySeq_finset_iff_tprod_vanishing.1 hf.hasProd.cauchySeq e he
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
⊢ Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
have pos : ∀ (H : Multipliable f),
  Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
Tactic: by_cases H : Multipliable f
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
pos :
  ∀ (H : Multipliable f),
    Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
⊢ Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
have neg : ∀ (H : ¬Multipliable f),
  Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
Tactic: by_cases H : Multipliable f
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
⊢ Membership.mem (γ := Filter G) (Filter.map (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop) e
have pos : ∀ (s : Finset α) (hs : ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e),
  Membership.mem (γ := Filter G) (Filter.map (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop) e
Tactic: obtain ⟨s, hs⟩ := H.tprod_vanishing he
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : Membership.mem (γ := Filter G) (𝓝 1) e
s : Finset α
hs : ∀ (t : Set α), Disjoint t (↑s : Set α) → ∏' (b : (↑t : Type u_1)), f (↑b : α) ∈ e
⊢ Membership.mem (γ := Filter G) (Filter.map (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop) e
have pos : ∃ (a : Finset α), ∀ b ≥ a, ∏' (a : { x : α // x ∉ b }), f (↑a : α) ∈ e
Tactic: simp only [Filter.mem_map, mem_atTop_sets, Set.mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
H : ¬Multipliable f
⊢ Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
have neg : ∀ (x : Finset α), ¬Multipliable.{u_4, u_1} (α := G) fun (a : { x_1 : α // x_1 ∉ x }) ↦ f (↑a : α)
Tactic: refine tendsto_const_nhds.congr fun _ ↦ (tprod_eq_one_of_not_multipliable ?_).symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
⊢ Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
have pos : ∀ (H : Multipliable f),
  Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
Tactic: classical
  by_cases H : Multipliable f
  · intro e he
    obtain ⟨s, hs⟩ := H.tprod_vanishing he
    simp only [Filter.mem_map, mem_atTop_sets, Set.mem_preimage]
    exact ⟨s, fun t hts ↦ hs tᶜ <| Set.disjoint_left.mpr fun a ha has ↦ ha (hts has)⟩
  · refine tendsto_const_nhds.congr fun _ ↦ (tprod_eq_one_of_not_multipliable ?_).symm
    rwa [Finset.multipliable_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
Goal:
α : Type u_1
G : Type u_4
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : IsTopologicalGroup G
f : α → G
pos :
  ∀ (H : Multipliable f),
    Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
⊢ Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
have neg : ∀ (H : ¬Multipliable f),
  Tendsto.{u_1, u_4} (β := G) (fun (s : Finset α) ↦ ∏' (a : { x : α // x ∉ s }), f (↑a : α)) atTop (𝓝 1)
Tactic: classical
  by_cases H : Multipliable f
  · intro e he
    obtain ⟨s, hs⟩ := H.tprod_vanishing he
    simp only [Filter.mem_map, mem_atTop_sets, Set.mem_preimage]
    exact ⟨s, fun t hts ↦ hs tᶜ <| Set.disjoint_left.mpr fun a ha has ↦ ha (hts has)⟩
  · refine tendsto_const_nhds.congr fun _ ↦ (tprod_eq_one_of_not_multipliable ?_).symm
    rwa [Finset.multipliable_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ Membership.mem (γ := Filter α) cofinite (f ⁻¹' e)
have rcases : ∀ (s : Finset α) (hs : ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e),
  Membership.mem (γ := Filter α) cofinite (f ⁻¹' e)
Tactic: rcases hf.vanishing he with ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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)
have refine : ∀ (x : α) (hx : x ∉ s), f x ∈ e
Tactic: refine s.eventually_cofinite_notMem.mono fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
have refine_1 : ∀ (h : Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ a), a = 1
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ (Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ a) ↔ a = 1
have refine_2 : a = 1 → Multipliable.{u_4, u_2} (α := G) fun (x : β) ↦ a
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ a = 1
have refine_1 : ∀ (ha : ¬a = 1), False
Tactic: by_contra ha
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (hypothesis)
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
⊢ False
have this : Membership.mem (γ := Filter G) (𝓝 1) {a}ᶜ
Tactic: have : {a}ᶜ ∈ 𝓝 1 := compl_singleton_mem_nhds (Ne.symm ha)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (hypothesis)
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}ᶜ
⊢ False
have this₁ : Finite β
Tactic: have : Finite β := by
      simpa [← Set.finite_univ_iff] using h.tendsto_cofinite_one this
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ ∏' (x : β), a = a ^ Nat.card β
have inl : ∀ (hβ : Finite β), ∏' (x : β), a = a ^ Nat.card β
Tactic: rcases finite_or_infinite β with hβ | hβ
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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 β
⊢ ∏' (x : β), a = a ^ Nat.card β
have inr : ∀ (hβ : Infinite β), ∏' (x : β), a = a ^ Nat.card β
Tactic: rcases finite_or_infinite β with hβ | hβ
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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 β
⊢ ∏' (x : β), a = a ^ Nat.card β
have inl : ∏ b : β, a = a ^ Nat.card β
Tactic: rw [tprod_eq_prod (s := univ) (fun x hx ↦ (hx (mem_univ x)).elim)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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 β
⊢ ∏' (x : β), a = a ^ Nat.card β
have inr : Eq.{u_4 + 1} (α := G) (∏' (x : β), a) 1
Tactic: simp only [Nat.card_eq_zero_of_infinite, pow_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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 β
⊢ Eq.{u_4 + 1} (α := G) (∏' (x : β), a) 1
have inr : Eq.{u_4 + 1} (α := G) (∏' (x : β), 1) 1
Tactic: rcases eq_or_ne a 1 with rfl | ha
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ Eq.{u_4 + 1} (α := G) (∏' (x : β), a) 1
have inr₁ : ∀ (ha : a ≠ 1), Eq.{u_4 + 1} (α := G) (∏' (x : β), a) 1
Tactic: rcases eq_or_ne a 1 with rfl | ha
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ Eq.{u_4 + 1} (α := G) (∏' (x : β), a) 1
have inr : ¬Multipliable.{u_4, u_2} (α := G) fun (b : β) ↦ a
Tactic: apply tprod_eq_one_of_not_multipliable
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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))
have 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
Tactic: refine (Tendsto.mul_const ((∏ i ∈ s, g i) / ∏ i ∈ s, f i) hc).congr' ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ 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
have 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
Tactic: filter_upwards [eventually_ge_atTop s] with t ht
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
| (∏ i ∈ t, f i) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i)
have rw : (∏ x ∈ s, f x) * (t \ s).prod g * 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ (∏ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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)
⊢ (∏ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ 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)
have rw : Ne.{u_4 + 1} (α := K) (∏ i ∈ s, f i) 0
Tactic: rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self, one_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ HMul.hMul (α := K) (∏ i ∈ s, g i) (∏ i ∈ t \ s, g i) = ∏ i ∈ t, g i
have rw : Eq.{u_4 + 1} (α := K) (∏ x ∈ s ∪ t \ s, g x) (∏ i ∈ t, g i)
Tactic: rw [← prod_union disjoint_sdiff, union_sdiff_of_subset ht]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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)
⊢ HMul.hMul (α := K) (∏ i ∈ s, g i) (∏ i ∈ t \ s, g i) = ∏ i ∈ t, g i
have rw₁ : Eq.{u_4 + 1} (α := K) (∏ x ∈ t, g x) (∏ i ∈ t, g i)
Tactic: rw [← prod_union disjoint_sdiff, union_sdiff_of_subset ht]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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
⊢ (∏ b ∈ t, f b) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i) = ∏ b ∈ t, g b
have 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)
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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)
⊢ (∏ b ∈ t, f b) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i) = ∏ b ∈ t, g b
have 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)
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Group (goal)
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)
⊢ (∏ b ∈ t, f b) * HDiv.hDiv (α := K) (∏ i ∈ s, g i) (∏ i ∈ s, f i) = ∏ b ∈ t, g b
have calc₂ : HMul.hMul (α := K) (∏ i ∈ s, g i) (∏ i ∈ t \ s, g i) = ∏ i ∈ t, g i
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]