awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
⊢ (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (b : β) ↦ f b)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ⋯) =
    ∏ᶠ (b : β), f b
have rw : (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (b : β), f b
  else
    if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
    else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) sorry) =
  ∏ᶠ (b : β), f b
Tactic: rw [L.support_eq_univ, Set.inter_univ, Set.mulIndicator_univ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
⊢ (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (b : β), f b
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ⋯) =
    ∏ᶠ (b : β), f b
have pos : ∀ (hf : (mulSupport f).Finite),
  (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (b : β), f b
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) sorry) =
    ∏ᶠ (b : β), f b
Tactic: by_cases hf : (mulSupport f).Finite
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
pos :
  ∀ (hf : (mulSupport f).Finite),
    (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (b : β), f b
      else
        if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
        else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ⋯) =
      ∏ᶠ (b : β), f b
⊢ (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (b : β), f b
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ⋯) =
    ∏ᶠ (b : β), f b
have neg : ∀ (hf : ¬(mulSupport f).Finite),
  (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (b : β), f b
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) sorry) =
    ∏ᶠ (b : β), f b
Tactic: by_cases hf : (mulSupport f).Finite
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : (mulSupport f).Finite
⊢ (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (b : β), f b
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ⋯) =
    ∏ᶠ (b : β), f b
have pos : L.HasSupport ∧ True
Tactic: rw [eq_true_intro hf, if_pos]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : (mulSupport f).Finite
⊢ L.HasSupport ∧ True
have pos : L.HasSupport
Tactic: simp only [and_true]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : ¬(mulSupport f).Finite
⊢ ¬(L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b))
have tauto : L.HasSupport → Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : ¬(mulSupport f).Finite
⊢ (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (b : β), f b
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ⋯) =
    ∏ᶠ (b : β), f b
have neg : (if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
  else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) sorry) =
  ∏ᶠ (b : β), f b
Tactic: rwa [if_neg (by tauto), if_pos (hasProd_bot hL _ _), finprod_of_infinite_mulSupport]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : ¬(mulSupport f).Finite
neg :
  (if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
    else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ⋯) =
    ∏ᶠ (b : β), f b
⊢ (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (b : β), f b
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ⋯) =
    ∏ᶠ (b : β), f b
have neg₁ : Eq.{u_1 + 1} (α := α) 1 (∏ᶠ (b : β), f b)
Tactic: rwa [if_neg (by tauto), if_pos (hasProd_bot hL _ _), finprod_of_infinite_mulSupport]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : ¬(mulSupport f).Finite
neg :
  (if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
    else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ⋯) =
    ∏ᶠ (b : β), f b
neg₁ : Eq.{u_1 + 1} (α := α) 1 (∏ᶠ (b : β), f b)
⊢ (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (b : β), f b
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ⋯) =
    ∏ᶠ (b : β), f b
have neg₂ : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rwa [if_neg (by tauto), if_pos (hasProd_bot hL _ _), finprod_of_infinite_mulSupport]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : ¬(mulSupport f).Finite
neg :
  (if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
    else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ⋯) =
    ∏ᶠ (b : β), f b
neg₁ : Eq.{u_1 + 1} (α := α) 1 (∏ᶠ (b : β), f b)
neg₂ : Eq.{u_1 + 1} (α := α) 1 1
⊢ (if L.HasSupport ∧ Set.Finite.{u_2} (α := β) (mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) then ∏ᶠ (b : β), f b
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ⋯) =
    ∏ᶠ (b : β), f b
have neg₃ : (mulSupport f).Infinite
Tactic: rwa [if_neg (by tauto), if_pos (hasProd_bot hL _ _), finprod_of_infinite_mulSupport]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst_2 : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
⊢ HasProd (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasProd f a L
have simp : Tendsto (fun (x : Finset β) ↦ ∏ x ∈ x.preimage g sorry, f (g x)) L.filter (𝓝 a) ↔
  Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
Tactic: simp only [HasProd, SummationFilter.comap_filter, tendsto_map'_iff, comp_apply,
    Embedding.coeFn_mk, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst_2 : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
⊢ Tendsto (fun (x : Finset β) ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) L.filter (𝓝 a) ↔
    Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
have refine : EventuallyEq.{u_2, u_1} (β := α) L.filter (fun (x : Finset β) ↦ ∏ x ∈ x.preimage g sorry, f (g x)) fun (s : Finset β) ↦
  ∏ b ∈ s, f b
Tactic: refine tendsto_congr' ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst_2 : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
⊢ EventuallyEq.{u_2, u_1} (β := α) L.filter (fun (x : Finset β) ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) fun (s : Finset β) ↦
    ∏ b ∈ s, f b
have h : ∀ (s : Finset β) (hs : (↑s : Set β) ⊆ L.support), Eq.{u_1 + 1} (α := α) (∏ x ∈ s.preimage g sorry, f (g x)) (∏ b ∈ s, f b)
Tactic: filter_upwards [L.eventually_le_support] with s hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
inst_2 : L.HasSupport
g : γ → β
hg : Injective g
hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1
s : Finset β
hs : (↑s : Set β) ⊆ L.support
⊢ Eq.{u_1 + 1} (α := α) (∏ x ∈ s.preimage g ⋯, f (g x)) (∏ b ∈ s, f b)
have h : ∀ x ∈ s, x ∉ Set.range g → f x = 1
Tactic: rw [s.prod_preimage]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ HasProd (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasProd f a L
have simp : Tendsto (fun (x : Finset β) ↦ ∏ x ∈ x.preimage g sorry, f (g x)) L.filter (𝓝 a) ↔
  Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
Tactic: simp only [HasProd, SummationFilter.comap_filter, tendsto_map'_iff, comp_apply,
    Embedding.coeFn_mk, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ Tendsto (fun (x : Finset β) ↦ ∏ x ∈ x.preimage g ⋯, f (g x)) L.filter (𝓝 a) ↔
    Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
have refine : ∀ (s : Finset β), Eq.{u_1 + 1} (α := α) (∏ x ∈ s.preimage g sorry, f (g x)) (∏ b ∈ s, f b)
Tactic: refine tendsto_congr fun s ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
s : Finset β
⊢ Eq.{u_1 + 1} (α := α) (∏ x ∈ s.preimage g ⋯, f (g x)) (∏ b ∈ s, f b)
have hg₁ : ∀ x ∈ s, x ∉ Set.range g → f x = 1
Tactic: rw [s.prod_preimage]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ HasProd (f ∘ g) a ↔ HasProd f a
have rw : HasProd (f ∘ g) a ↔ HasProd (f ∘ g) a ((unconditional β).comap { toFun := g, inj' := hg })
Tactic: rw [← hg.hasProd_comap_iff hf, SummationFilter.comap_unconditional]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
rw : HasProd (f ∘ g) a ↔ HasProd (f ∘ g) a ((unconditional β).comap { toFun := g, inj' := hg })
⊢ HasProd (f ∘ g) a ↔ HasProd f a
have rw₁ : HasProd (f ∘ g) a ↔ HasProd (f ∘ g) a
Tactic: rw [← hg.hasProd_comap_iff hf, SummationFilter.comap_unconditional]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
⊢ HasProd f (∏ b ∈ L.support.toFinset, f b) L
have h : ∀ᶠ (x' : Finset β) in L.filter, Eq.{u_1 + 1} (α := α) (∏ b ∈ x', f b) (∏ b ∈ L.support.toFinset, f b)
Tactic: apply tendsto_nhds_of_eventually_eq
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
⊢ ∀ᶠ (x' : Finset β) in L.filter, Eq.{u_1 + 1} (α := α) (∏ b ∈ x', f b) (∏ b ∈ L.support.toFinset, f b)
have h1 : ⋂ b ∈ L.support, {s : Finset β | b ∈ s} ∈ L.filter
Tactic: have h1 : ⋂ b ∈ L.support, {s | b ∈ s} ∈ L.filter :=
    (L.filter.biInter_mem L.support.toFinite).mpr (by tauto)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s : Finset β | b ∈ s} ∈ L.filter
⊢ ∀ᶠ (x' : Finset β) in L.filter, Eq.{u_1 + 1} (α := α) (∏ b ∈ x', f b) (∏ b ∈ L.support.toFinset, f b)
have h2 : ⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s} ∈ L.filter
Tactic: have h2 : ⋂ b ∈ L.supportᶜ, {s | b ∉ s} ∈ L.filter :=
    (L.filter.biInter_mem L.supportᶜ.toFinite).mpr
      (fun b hb ↦ (L.eventually_mem_or_not_mem b).resolve_left hb)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s : Finset β | b ∈ s} ∈ L.filter
h2 : ⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s} ∈ L.filter
⊢ ∀ᶠ (x' : Finset β) in L.filter, Eq.{u_1 + 1} (α := α) (∏ b ∈ x', f b) (∏ b ∈ L.support.toFinset, f b)
have h : ∀ (s : Finset β) (hs : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ L.support, {s : Finset β | b ∈ s}) s)
  (hs' : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s}) s),
  Eq.{u_1 + 1} (α := α) (∏ b ∈ s, f b) (∏ b ∈ L.support.toFinset, f b)
Tactic: filter_upwards [h1, h2] with s hs hs'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s : Finset β | b ∈ s} ∈ L.filter
h2 : ⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s} ∈ L.filter
s : Finset β
hs : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ L.support, {s : Finset β | b ∈ s}) s
hs' : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s}) s
⊢ Eq.{u_1 + 1} (α := α) (∏ b ∈ s, f b) (∏ b ∈ L.support.toFinset, f b)
have h : s = L.support.toFinset
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s : Finset β | b ∈ s} ∈ L.filter
h2 : ⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s} ∈ L.filter
s : Finset β
hs : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ L.support, {s : Finset β | b ∈ s}) s
hs' : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s}) s
⊢ s = L.support.toFinset
have hs₁ : ∀ (i : β) (i_1 : i ∈ L.support), i ∈ s
Tactic: simp only [Set.mem_iInter, Set.mem_setOf_eq, Set.mem_compl_iff] at hs hs'
Cleared hypotheses: hs, hs'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Fintype β
f : β → α
L : SummationFilter β
inst_3 : L.HasSupport
inst_4 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ L.support, {s : Finset β | b ∈ s} ∈ L.filter
h2 : ⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s} ∈ L.filter
s : Finset β
hs : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ L.support, {s : Finset β | b ∈ s}) s
hs' : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ L.supportᶜ, {s : Finset β | b ∉ s}) s
hs₁ : ∀ (i : β) (i_1 : i ∈ L.support), i ∈ s
⊢ s = L.support.toFinset
have hs'₁ : ∀ (i : β) (i_1 : i ∉ L.support), i ∉ s
Tactic: simp only [Set.mem_iInter, Set.mem_setOf_eq, Set.mem_compl_iff] at hs hs'
Cleared hypotheses: hs, hs'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : β) ↦ x ∈ L.support
⊢ HasProd f (∏ b ∈ ((↑s : Set β) ∩ L.support).toFinset, f b) L
have h : ∀ᶠ (x' : Finset β) in L.filter, Eq.{u_1 + 1} (α := α) (∏ b ∈ x', f b) (∏ b ∈ ((↑s : Set β) ∩ L.support).toFinset, f b)
Tactic: apply tendsto_nhds_of_eventually_eq
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : β) ↦ x ∈ L.support
⊢ ∀ᶠ (x' : Finset β) in L.filter, Eq.{u_1 + 1} (α := α) (∏ b ∈ x', f b) (∏ b ∈ ((↑s : Set β) ∩ L.support).toFinset, f b)
have h1 : ⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s} ∈ L.filter
Tactic: have h1 : ⋂ b ∈ (↑s ∩ L.support), {s | b ∈ s} ∈ L.filter :=
    (L.filter.biInter_mem (Set.toFinite _)).mpr (fun b hb ↦ hb.2)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s} ∈ L.filter
⊢ ∀ᶠ (x' : Finset β) in L.filter, Eq.{u_1 + 1} (α := α) (∏ b ∈ x', f b) (∏ b ∈ ((↑s : Set β) ∩ L.support).toFinset, f b)
have h : ∀ (t : Finset β) (ht : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s}) t)
  (ht' : (↑t : Set β) ⊆ L.support),
  Eq.{u_1 + 1} (α := α) (∏ b ∈ t, f b) (∏ b ∈ ((↑s : Set β) ∩ L.support).toFinset, f b)
Tactic: filter_upwards [h1, L.eventually_le_support] with t ht ht'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s} ∈ L.filter
t : Finset β
ht : Membership.mem (γ := Set (Finset β)) (⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s}) t
ht' : (↑t : Set β) ⊆ L.support
⊢ Eq.{u_1 + 1} (α := α) (∏ b ∈ t, f b) (∏ b ∈ ((↑s : Set β) ∩ L.support).toFinset, f b)
have ht₁ : ∀ (i : β) (i_1 : i ∈ (↑s : Set β) ∩ L.support), Membership.mem (γ := Set (Finset β)) {s : Finset β | i ∈ s} t
Tactic: simp only [Set.mem_iInter] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s} ∈ L.filter
t : Finset β
ht' : (↑t : Set β) ⊆ L.support
ht : ∀ (i : β) (i_1 : i ∈ (↑s : Set β) ∩ L.support), Membership.mem (γ := Set (Finset β)) {s : Finset β | i ∈ s} t
⊢ Eq.{u_1 + 1} (α := α) (∏ b ∈ t, f b) (∏ b ∈ ((↑s : Set β) ∩ L.support).toFinset, f b)
have h : ∀ a ∈ t, a ∉ ((↑s : Set β) ∩ L.support).toFinset → f a = 1
Tactic: apply Finset.prod_congr_of_eq_on_inter
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s} ∈ L.filter
t : Finset β
ht' : (↑t : Set β) ⊆ L.support
ht : ∀ (i : β) (i_1 : i ∈ (↑s : Set β) ∩ L.support), Membership.mem (γ := Set (Finset β)) {s : Finset β | i ∈ s} t
h : ∀ a ∈ t, a ∉ ((↑s : Set β) ∩ L.support).toFinset → f a = 1
⊢ Eq.{u_1 + 1} (α := α) (∏ b ∈ t, f b) (∏ b ∈ ((↑s : Set β) ∩ L.support).toFinset, f b)
have h₁ : ∀ a ∈ ((↑s : Set β) ∩ L.support).toFinset, a ∉ t → f a = 1
Tactic: apply Finset.prod_congr_of_eq_on_inter
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst_2 : L.HasSupport
inst_3 : DecidablePred fun (x : β) ↦ x ∈ L.support
h1 : ⋂ b ∈ (↑s : Set β) ∩ L.support, {s : Finset β | b ∈ s} ∈ L.filter
t : Finset β
ht' : (↑t : Set β) ⊆ L.support
ht : ∀ (i : β) (i_1 : i ∈ (↑s : Set β) ∩ L.support), Membership.mem (γ := Set (Finset β)) {s : Finset β | i ∈ s} t
h : ∀ a ∈ t, a ∉ ((↑s : Set β) ∩ L.support).toFinset → f a = 1
h₁ : ∀ a ∈ ((↑s : Set β) ∩ L.support).toFinset, a ∉ t → f a = 1
⊢ Eq.{u_1 + 1} (α := α) (∏ b ∈ t, f b) (∏ b ∈ ((↑s : Set β) ∩ L.support).toFinset, f b)
have h₂ : ∀ a ∈ t, a ∈ ((↑s : Set β) ∩ L.support).toFinset → f a = f a
Tactic: apply Finset.prod_congr_of_eq_on_inter
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
⊢ HasProd f (∏'[L] (b : β), f b) L
have rw : HasProd f
  (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
    finprod (L.support.mulIndicator fun (b : β) ↦ f b)
  else
    if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
    else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha)
  L
Tactic: rw [tprod_def, dif_pos ha]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
⊢ HasProd f
    (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (b : β) ↦ f b)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ha)
    L
have pos : ∀ (h : L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite),
  HasProd f (finprod (L.support.mulIndicator fun (b : β) ↦ f b)) L
Tactic: split_ifs with h h'