awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : L.LeAtTop
s : Finset β
hf : mulSupport f ⊆ (↑s : Set β)
rw : Eq.{u_1 + 1} (α := α) (∏ᶠ (b : β), f b) (∏ b ∈ s, f b)
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), f b) (∏ b ∈ s, f b)
have rw₁ : Eq.{u_1 + 1} (α := α) (∏ i ∈ s, f i) (∏ b ∈ s, f b)
Tactic: rw [tprod_eq_finprod (s.finite_toSet.subset hf), finprod_eq_prod_of_mulSupport_subset _ 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 β
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (x : β), 1) 1
have rw : Eq.{u_1 + 1} (α := α)
  (if h : Multipliable.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) L then
    if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) h
  else 1)
  1
Tactic: rw [tprod_def, dif_pos multipliable_one, mulSupport_fun_one, Set.empty_inter,
    Set.mulIndicator_one, finprod_one, eq_true_intro hasProd_one, if_true, ite_self]
-- 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 β
rw :
  Eq.{u_1 + 1} (α := α)
    (if h : Multipliable.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) L then
      if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun (x : β) ↦ 1)
      else
        if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
        else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) h
    else 1)
    1
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (x : β), 1) 1
have rw₁ : Eq.{u_1 + 1} (α := α)
  (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
    finprod (L.support.mulIndicator fun (x : β) ↦ 1)
  else
    if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
    else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) sorry)
  1
Tactic: rw [tprod_def, dif_pos multipliable_one, mulSupport_fun_one, Set.empty_inter,
    Set.mulIndicator_one, finprod_one, eq_true_intro hasProd_one, if_true, ite_self]
-- 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 β
rw :
  Eq.{u_1 + 1} (α := α)
    (if h : Multipliable.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) L then
      if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun (x : β) ↦ 1)
      else
        if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
        else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) h
    else 1)
    1
rw₁ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (x : β), 1) 1
have rw₂ : Eq.{u_1 + 1} (α := α)
  (if L.HasSupport ∧ (∅ ∩ L.support).Finite then finprod (L.support.mulIndicator fun (x : β) ↦ 1)
  else
    if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
    else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) sorry)
  1
Tactic: rw [tprod_def, dif_pos multipliable_one, mulSupport_fun_one, Set.empty_inter,
    Set.mulIndicator_one, finprod_one, eq_true_intro hasProd_one, if_true, ite_self]
-- 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 β
rw :
  Eq.{u_1 + 1} (α := α)
    (if h : Multipliable.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) L then
      if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun (x : β) ↦ 1)
      else
        if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
        else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) h
    else 1)
    1
rw₁ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₂ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ (∅ ∩ L.support).Finite then finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (x : β), 1) 1
have rw₃ : Eq.{u_1 + 1} (α := α)
  (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then finprod (L.support.mulIndicator fun (x : β) ↦ 1)
  else
    if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
    else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) sorry)
  1
Tactic: rw [tprod_def, dif_pos multipliable_one, mulSupport_fun_one, Set.empty_inter,
    Set.mulIndicator_one, finprod_one, eq_true_intro hasProd_one, if_true, ite_self]
-- 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 β
rw :
  Eq.{u_1 + 1} (α := α)
    (if h : Multipliable.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) L then
      if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun (x : β) ↦ 1)
      else
        if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
        else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) h
    else 1)
    1
rw₁ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₂ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ (∅ ∩ L.support).Finite then finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₃ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (x : β), 1) 1
have rw₄ : Eq.{u_1 + 1} (α := α)
  (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then ∏ᶠ (x : β), 1
  else
    if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
    else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) sorry)
  1
Tactic: rw [tprod_def, dif_pos multipliable_one, mulSupport_fun_one, Set.empty_inter,
    Set.mulIndicator_one, finprod_one, eq_true_intro hasProd_one, if_true, ite_self]
-- 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 β
rw :
  Eq.{u_1 + 1} (α := α)
    (if h : Multipliable.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) L then
      if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun (x : β) ↦ 1)
      else
        if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
        else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) h
    else 1)
    1
rw₁ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₂ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ (∅ ∩ L.support).Finite then finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₃ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₄ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then ∏ᶠ (x : β), 1
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (x : β), 1) 1
have rw₅ : Eq.{u_1 + 1} (α := α)
  (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then 1
  else
    if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
    else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) sorry)
  1
Tactic: rw [tprod_def, dif_pos multipliable_one, mulSupport_fun_one, Set.empty_inter,
    Set.mulIndicator_one, finprod_one, eq_true_intro hasProd_one, if_true, ite_self]
-- 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 β
rw :
  Eq.{u_1 + 1} (α := α)
    (if h : Multipliable.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) L then
      if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun (x : β) ↦ 1)
      else
        if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
        else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) h
    else 1)
    1
rw₁ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₂ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ (∅ ∩ L.support).Finite then finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₃ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₄ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then ∏ᶠ (x : β), 1
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₅ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then 1
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (x : β), 1) 1
have rw₆ : Eq.{u_1 + 1} (α := α)
  (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then 1
  else if True then 1 else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) sorry)
  1
Tactic: rw [tprod_def, dif_pos multipliable_one, mulSupport_fun_one, Set.empty_inter,
    Set.mulIndicator_one, finprod_one, eq_true_intro hasProd_one, if_true, ite_self]
-- 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 β
rw :
  Eq.{u_1 + 1} (α := α)
    (if h : Multipliable.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) L then
      if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun (x : β) ↦ 1)
      else
        if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
        else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) h
    else 1)
    1
rw₁ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₂ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ (∅ ∩ L.support).Finite then finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₃ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₄ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then ∏ᶠ (x : β), 1
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₅ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then 1
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₆ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then 1
    else if True then 1 else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (x : β), 1) 1
have rw₇ : Eq.{u_1 + 1} (α := α) (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then 1 else 1) 1
Tactic: rw [tprod_def, dif_pos multipliable_one, mulSupport_fun_one, Set.empty_inter,
    Set.mulIndicator_one, finprod_one, eq_true_intro hasProd_one, if_true, ite_self]
-- 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 β
rw :
  Eq.{u_1 + 1} (α := α)
    (if h : Multipliable.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) L then
      if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
        finprod (L.support.mulIndicator fun (x : β) ↦ 1)
      else
        if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
        else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) h
    else 1)
    1
rw₁ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (x : β) ↦ 1) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₂ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ (∅ ∩ L.support).Finite then finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₃ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then finprod (L.support.mulIndicator fun (x : β) ↦ 1)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₄ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then ∏ᶠ (x : β), 1
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₅ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then 1
    else
      if HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₆ :
  Eq.{u_1 + 1} (α := α)
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then 1
    else if True then 1 else Exists.choose (p := fun (a : α) ↦ HasProd (fun (x : β) ↦ 1) a L) ⋯)
    1
rw₇ : Eq.{u_1 + 1} (α := α) (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) ∅ then 1 else 1) 1
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (x : β), 1) 1
have rw₈ : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rw [tprod_def, dif_pos multipliable_one, mulSupport_fun_one, Set.empty_inter,
    Set.mulIndicator_one, finprod_one, eq_true_intro hasProd_one, if_true, ite_self]
-- 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 β
inst_2 : L.LeAtTop
inst_3 : Fintype β
f : β → α
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), f b) (∏ b : β, f b)
have hf : ∀ b ∉ univ, f b = 1
Tactic: apply tprod_eq_prod
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
s : Finset β
L : SummationFilter β
inst_2 : L.LeAtTop
⊢ Eq.{u_1 + 1} (α := α) (∏ x ∈ s, f x) (∏'[L] (x : β), (↑s : Set β).mulIndicator f x)
have rw : Eq.{u_1 + 1} (α := α) (∏ x ∈ s, f x) (∏ b ∈ s, (↑s : Set β).mulIndicator f b)
Tactic: rw [tprod_eq_prod' (Set.mulSupport_mulIndicator_subset),
      Finset.prod_mulIndicator_subset _ Finset.Subset.rfl]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
s : Finset β
L : SummationFilter β
inst_2 : L.LeAtTop
rw : Eq.{u_1 + 1} (α := α) (∏ x ∈ s, f x) (∏ b ∈ s, (↑s : Set β).mulIndicator f b)
⊢ Eq.{u_1 + 1} (α := α) (∏ x ∈ s, f x) (∏'[L] (x : β), (↑s : Set β).mulIndicator f x)
have rw₁ : Eq.{u_1 + 1} (α := α) (∏ x ∈ s, f x) (∏ i ∈ s, f i)
Tactic: rw [tprod_eq_prod' (Set.mulSupport_mulIndicator_subset),
      Finset.prod_mulIndicator_subset _ Finset.Subset.rfl]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : Bool → α
⊢ ∏' (i : Bool), f i = f false * f true
have rw : ∏ b : Bool, f b = f false * f true
Tactic: rw [tprod_fintype, Fintype.prod_bool, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : Bool → α
rw : ∏ b : Bool, f b = f false * f true
⊢ ∏' (i : Bool), f i = f false * f true
have rw₁ : f true * f false = f false * f true
Tactic: rw [tprod_fintype, Fintype.prod_bool, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : Bool → α
rw : ∏ b : Bool, f b = f false * f true
rw₁ : f true * f false = f false * f true
⊢ ∏' (i : Bool), f i = f false * f true
have rw₂ : f false * f true = f false * f true
Tactic: rw [tprod_fintype, Fintype.prod_bool, mul_comm]
-- 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 β
inst_2 : L.LeAtTop
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
⊢ ∏'[L] (b : β), f b = f b
have rw : ∀ b_1 ∉ {b}, f b_1 = 1
Tactic: rw [tprod_eq_prod (s := {b}), prod_singleton]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
b : β
inst_2 : DecidablePred fun (x : β) ↦ x = b
a : β → α
L : SummationFilter β
inst_3 : L.LeAtTop
⊢ (∏'[L] (b' : β), if b' = b then a b' else 1) = a b
have rw : (if b = b then a b else 1) = a b
Tactic: rw [tprod_eq_mulSingle b]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
b : β
inst_2 : DecidablePred fun (x : β) ↦ x = b
a : β → α
L : SummationFilter β
inst_3 : L.LeAtTop
rw : (if b = b then a b else 1) = a b
⊢ (∏'[L] (b' : β), if b' = b then a b' else 1) = a b
have rw₁ : ∀ (b' : β), b' ≠ b → (if b' = b then a b' else 1) = 1
Tactic: rw [tprod_eq_mulSingle b]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Finset β
f : β → α
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : ↥s), f (↑x : β)) (∏ x ∈ s, f x)
have rw : Eq.{u_1 + 1} (α := α) (∏' (x : ↥s), f (↑x : β)) (∏ x ∈ s.attach, f (↑x : β))
Tactic: rw [← prod_attach]
-- 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
⊢ mulSupport f = g '' mulSupport (f ∘ g)
have rw : mulSupport f = g '' g ⁻¹' mulSupport f
Tactic: rw [mulSupport_comp_eq_preimage, Set.image_preimage_eq_iff.2 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
rw : mulSupport f = g '' g ⁻¹' mulSupport f
⊢ mulSupport f = g '' mulSupport (f ∘ g)
have rw₁ : mulSupport f = mulSupport f
Tactic: rw [mulSupport_comp_eq_preimage, Set.image_preimage_eq_iff.2 hf]
-- 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
⊢ Eq.{u_1 + 1} (α := α) (∏' (c : γ), f (g c)) (∏' (b : β), f b)
have this : mulSupport f = g '' mulSupport (f ∘ g)
Tactic: have : mulSupport f = g '' mulSupport (f ∘ g) := by
    rw [mulSupport_comp_eq_preimage, Set.image_preimage_eq_iff.2 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
this : mulSupport f = g '' mulSupport (f ∘ g)
⊢ Eq.{u_1 + 1} (α := α) (∏' (c : γ), f (g c)) (∏' (b : β), f b)
have rw : tprod (f ∘ g) = ∏' (b : β), f b
Tactic: rw [← Function.comp_def]
-- 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)
⊢ tprod (f ∘ g) = ∏' (b : β), f b
have pos : ∀ (hf_fin : (mulSupport f).Finite), tprod (f ∘ g) = ∏' (b : β), f b
Tactic: by_cases hf_fin : (mulSupport f).Finite
-- 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)
pos : ∀ (hf_fin : (mulSupport f).Finite), tprod (f ∘ g) = ∏' (b : β), f b
⊢ tprod (f ∘ g) = ∏' (b : β), f b
have neg : ∀ (hf_fin : ¬(mulSupport f).Finite), tprod (f ∘ g) = ∏' (b : β), f b
Tactic: by_cases hf_fin : (mulSupport f).Finite