awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (hypothesis)
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
⊢ tprod (f ∘ g) = ∏' (b : β), f b
have hfg_fin : (mulSupport (f ∘ g)).Finite
Tactic: have hfg_fin : (mulSupport (f ∘ g)).Finite := hf_fin.preimage hg.injOn
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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
⊢ tprod (f ∘ g) = ∏' (b : β), f b
have 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
Tactic: lift g to γ ↪ β using hg
Cleared hypotheses: g, hg, hf, this, hfg_fin
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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 : γ) → β)))
⊢ tprod (f ∘ (⇑g : (a : γ) → β)) = ∏' (b : β), f b
have 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)
Tactic: simp_rw [tprod_eq_prod' hf_fin.coe_toFinset.ge, tprod_eq_prod' hfg_fin.coe_toFinset.ge,
      comp_apply, ← Finset.prod_map]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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)
have pos : (↑(Finset.map g (hfg_fin.toFinset (s := mulSupport (f ∘ (⇑g : (a : γ) → β))))) : Set β) =
  (↑(hf_fin.toFinset (s := mulSupport f)) : Set β)
Tactic: refine Finset.prod_congr (Finset.coe_injective ?_) fun _ _ ↦ rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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
have rwa : ∀ (hf_fin : ¬(g '' mulSupport (f ∘ g)).Finite), ¬(mulSupport (f ∘ g)).Finite
Tactic: rwa [this, Set.finite_image_iff hg.injOn] at hf_fin
Cleared hypotheses: hf_fin
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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
⊢ ¬(mulSupport (f ∘ g)).Finite
have rwa₁ : ∀ (hf_fin : ¬(mulSupport (f ∘ g)).Finite), ¬(mulSupport (f ∘ g)).Finite
Tactic: rwa [this, Set.finite_image_iff hg.injOn] at hf_fin
Cleared hypotheses: hf_fin
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (hypothesis)
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
⊢ tprod (f ∘ g) = ∏' (b : β), f b
have hf_fin' : ¬(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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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
⊢ tprod (f ∘ g) = ∏' (b : β), f b
have 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) sorry
  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) sorry
  else 1)
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := α) (∏' (c : γ), f (g c)) (∏' (b : β), f b)
have have : mulSupport f = g '' mulSupport (f ∘ g)
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)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := α) (∏' (c : γ), f (g c)) (∏' (b : β), f b)
have have₁ : ∀ (this : mulSupport f = g '' mulSupport (f ∘ g)), 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)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := α) (∏' (c : γ), f (g c)) (∏' (b : β), f b)
have have₅ : ∀ (this : mulSupport f = g '' mulSupport (f ∘ g)), tprod (f ∘ g) = ∏' (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)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := α) (∏' (c : γ), f (g c)) (∏' (b : β), f b)
have pos : ∀ (this : mulSupport f = g '' mulSupport (f ∘ g)) (hf_fin : (mulSupport f).Finite), tprod (f ∘ g) = ∏' (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)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := α) (∏' (c : γ), f (g c)) (∏' (b : β), f b)
have neg : ∀ (this : mulSupport f = g '' mulSupport (f ∘ g)) (hf_fin : ¬(mulSupport f).Finite), tprod (f ∘ g) = ∏' (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)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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
⊢ ∏' (i : ι), f i ∈ s
have pos : ∀ (hf : Multipliable f), ∏' (i : ι), f i ∈ s
Tactic: by_cases hf : Multipliable f
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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
⊢ ∏' (i : ι), f i ∈ s
have neg : ∀ (hf : ¬Multipliable f), ∏' (i : ι), f i ∈ s
Tactic: by_cases hf : Multipliable f
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Set β
f : β → α
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑s : Type u_2)), f (↑x : β)) (∏' (x : β), s.mulIndicator f x)
have rw : ∀ (b : (↑s : Type u_2)), f (↑b : β) = s.mulIndicator f (↑b : β)
Tactic: rw [← tprod_subtype_eq_of_mulSupport_subset Set.mulSupport_mulIndicator_subset, tprod_congr]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
g : γ → β
f : β → α
hg : Injective g
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑(Set.range g) : Type u_2)), f (↑x : β)) (∏' (x : γ), f (g x))
have rw : Eq.{u_1 + 1} (α := α) (∏' (x : (↑Set.univ : Type u_3)), f (g (↑x : γ))) (∏' (x : γ), f (g x))
Tactic: rw [← Set.image_univ, tprod_image f hg.injOn]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
g : γ → β
f : β → α
hg : Injective g
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑Set.univ : Type u_3)), f (g (↑x : γ))) (∏' (x : γ), f (g x))
have simp_rw : 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)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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} (α := α) (∏' (x : β), f x) (∏' (y : γ), g y)
have rw : Eq.{u_1 + 1} (α := α) (∏' (c : (↑(mulSupport g) : Type u_3)), f (i c))
  (∏' (x : (↑(mulSupport g) : Type u_3)), g (↑x : γ))
Tactic: rw [← tprod_subtype_mulSupport g, ← hi.tprod_eq hf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
P : Prop
inst_2 : Decidable P
x : β → ¬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)
have 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)
Tactic: by_cases hP : P
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hP : P
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
P : Prop
inst_2 : Decidable P
x : β → 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)
have 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)
Tactic: by_cases hP : P
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hP : P
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
γ : Type u_4
g : γ → β
hg : Injective g
f : γ → α
⊢ Eq.{u_1 + 1} (α := α) (∏' (y : β), extend g f 1 y) (∏' (x : γ), f x)
have this : mulSupport (extend g f 1) ⊆ Set.range g
Tactic: have : mulSupport (extend g f 1) ⊆ Set.range g := mulSupport_subset_iff'.2 <| extend_apply' _ _
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := α) (∏' (y : β), extend g f 1 y) (∏' (x : γ), f x)
have simp_rw : Eq.{u_1 + 1} (α := α) (∏' (c : γ), extend g f 1 (g c)) (∏' (x : γ), f x)
Tactic: simp_rw [← hg.tprod_eq this, hg.extend_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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)
⊢ ∏' (d : γ), (s d).mulIndicator f i = f i
have obtain : ∀ (j : γ) (hj : i ∈ s j), ∏' (d : γ), (s d).mulIndicator f i = f i
Tactic: obtain ⟨j, hj⟩ := Set.mem_iUnion.mp hi
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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
⊢ ∏' (d : γ), (s d).mulIndicator f i = f i
have rw : ∏' (x : (↑{j} : Type u_3)), (s (↑x : γ)).mulIndicator f i = f i
Tactic: rw [← tprod_subtype_eq_of_mulSupport_subset (s := {j})]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
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
⊢ ∏' (d : γ), (s d).mulIndicator f i = f i
have rw₁ : Subset (α := Set γ) (mulSupport.{u_3, u_1} (M := α) fun (d : γ) ↦ (s d).mulIndicator f i) {j}
Tactic: rw [← tprod_subtype_eq_of_mulSupport_subset (s := {j})]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
f : β → α
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
i : β
⊢ Set.mulIndicator (⋃ (d : γ), s d) f i = ∏' (d : γ), (s d).mulIndicator f i
have pos : ∀ (h₀ : Membership.mem (γ := Set β) (⋃ (d : γ), s d) i),
  Set.mulIndicator (⋃ (d : γ), s d) f i = ∏' (d : γ), (s d).mulIndicator f i
Tactic: by_cases h₀ : i ∈ ⋃ d, s d
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
f : β → α
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
i : β
pos :
  ∀ (h₀ : Membership.mem (γ := Set β) (⋃ (d : γ), s d) i),
    Set.mulIndicator (⋃ (d : γ), s d) f i = ∏' (d : γ), (s d).mulIndicator f i
⊢ Set.mulIndicator (⋃ (d : γ), s d) f i = ∏' (d : γ), (s d).mulIndicator f i
have neg : ∀ (h₀ : i ∉ ⋃ (d : γ), s d), Set.mulIndicator (⋃ (d : γ), s d) f i = ∏' (d : γ), (s d).mulIndicator f i
Tactic: by_cases h₀ : i ∈ ⋃ d, s d
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : γ → Set β
hs : Pairwise (Disjoint on s)
f : β → α
⊢ Set.mulIndicator (⋃ (d : γ), s d) f = fun (i : β) ↦ ∏' (d : γ), (s d).mulIndicator f i
have h : ∀ (i : β), Set.mulIndicator (⋃ (d : γ), s d) f i = ∏' (d : γ), (s d).mulIndicator f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : T2Space α
α' : Type u_4
inst_3 : CommMonoid α'
inst_4 : TopologicalSpace α'
e : α' → α
hes : Surjective e
h1 : e 1 = 1
f : β → α
g : γ → α'
h : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a
hg : ¬Multipliable g
⊢ ∏' (b : β), f b = e (∏' (c : γ), g c)
have hf : ¬Multipliable f
Tactic: have hf : ¬Multipliable f := mt (hes.multipliable_iff_of_hasProd_iff @h).1 hg
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : L.NeBot
hf : Multipliable f L
n : ℕ
⊢ ∏'[L] (b : β), f b ^ n = HPow.hPow (α := α) (∏'[L] (b : β), f b) n
have zero : ∏'[L] (b : β), HPow.hPow (β := ℕ) (f b) 0 = HPow.hPow (α := α) (β := ℕ) (∏'[L] (b : β), f b) 0
Tactic: induction n with
  | zero => simp
  | succ n hn => simp [pow_succ, (hf.pow n).tprod_mul hf, hn]
Cleared hypotheses: n