awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a b : α
inst_2 : ContinuousMul α
s : Set β
ha : HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a
hb : HasProd (β := (↑sᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ sᶜ)) b
⊢ HasProd f (a * b)

Tactic:
ha.mul_isCompl isCompl_compl hb

Premises used: HasProd.mul_isCompl, isCompl_compl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
inst_2 : ContinuousMul α
s : Set β
hs : Multipliable (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s))
hsc : Multipliable (β := (↑sᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ sᶜ))
⊢ Multipliable f

Tactic:
(hs.hasProd.mul_compl hsc.hasProd).multipliable

Premises used: Multipliable.hasProd, HasProd.multipliable, HasProd.mul_compl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a b : α
inst_2 : ContinuousMul α
s : Set β
ha : HasProd (β := (↑sᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ sᶜ)) a
hb : HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) b
⊢ HasProd f (a * b)

Tactic:
ha.mul_isCompl isCompl_compl.symm hb

Premises used: HasProd.mul_isCompl, isCompl_compl, IsCompl.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
inst_2 : ContinuousMul α
s : Set β
hs : Multipliable (β := (↑sᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ sᶜ))
hsc : Multipliable (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s))
⊢ Multipliable f

Tactic:
(hs.hasProd.compl_mul hsc.hasProd).multipliable

Premises used: Multipliable.hasProd, HasProd.compl_mul, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update (β := fun (a : β) ↦ α) f b x) a' L
b' : β
pos : ∀ (hb' : b' = b), f b' * x = update (β := fun (a : β) ↦ α) f b x b' * f b
neg : ∀ (hb' : ¬b' = b), f b' * 1 = update (β := fun (a : β) ↦ α) f b x b' * 1
⊢ (f b' * if b' = b then x else 1) = update (β := fun (a : β) ↦ α) f b x b' * if b' = b then f b else 1

Tactic:
split_ifs with hb'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update (β := fun (a : β) ↦ α) f b x) a' L
b' : β
hb' : b' = b
⊢ f b' * x = update (β := fun (a : β) ↦ α) f b x b' * f b

Tactic:
simpa only [Function.update_apply, hb', eq_self_iff_true] using mul_comm (f b) x

Premises used: Function.update_apply, mul_comm, eq_self_iff_true
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update (β := fun (a : β) ↦ α) f b x) a' L
b' : β
hb' : ¬b' = b
⊢ f b' * 1 = update (β := fun (a : β) ↦ α) f b x b' * 1

Tactic:
simp only [Function.update_apply, hb', if_false]

Premises used: if_false, Function.update_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update (β := fun (a : β) ↦ α) f b x) a' L
⊢ ∀ (b' : β), (f b' * if b' = b then x else 1) = update (β := fun (a : β) ↦ α) f b x b' * if b' = b then f b else 1

Tactic:
have : ∀ b', f b' * ite (b' = b) x 1 = update f b x b' * ite (b' = b) (f b) 1 := by
    intro b'
    split_ifs with hb'
    · simpa only [Function.update_apply, hb', eq_self_iff_true] using mul_comm (f b) x
    · simp only [Function.update_apply, hb', if_false]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update (β := fun (a : β) ↦ α) f b x) a' L
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update (β := fun (a : β) ↦ α) f b x b' * if b' = b then f b else 1
⊢ HasProd (fun (b_1 : β) ↦ f b_1 * if b_1 = b then x else 1) (a * x) L

Tactic:
have h := hf.mul (hasProd_ite_eq b x L)
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update (β := fun (a : β) ↦ α) f b x) a' L
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update (β := fun (a : β) ↦ α) f b x b' * if b' = b then f b else 1
h : HasProd (fun (b_1 : β) ↦ f b_1 * if b_1 = b then x else 1) (a * x) L
⊢ HasProd (fun (b_1 : β) ↦ update (β := fun (a : β) ↦ α) f b x b_1 * if b_1 = b then f b else 1) (a * x) L

Tactic:
simp_rw [this] at h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update (β := fun (a : β) ↦ α) f b x) a' L
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update (β := fun (a : β) ↦ α) f b x b' * if b' = b then f b else 1
h : HasProd (fun (b_1 : β) ↦ update (β := fun (a : β) ↦ α) f b x b_1 * if b_1 = b then f b else 1) (a * x) L
⊢ a * x = a' * f b

Tactic:
HasProd.unique h (hf'.mul (hasProd_ite_eq b (f b) L))

Premises used: HasProd.unique, hasProd_ite_eq, HasProd.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update (β := fun (a : β) ↦ α) f b x) a' L
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update (β := fun (a : β) ↦ α) f b x b' * if b' = b then f b else 1
h : HasProd (fun (b_1 : β) ↦ update (β := fun (a : β) ↦ α) f b x b_1 * if b_1 = b then f b else 1) (a * x) L
⊢ a * x = a' * f b

Tactic:
exact HasProd.unique h (hf'.mul (hasProd_ite_eq b (f b) L))

Premises used: HasProd.unique, hasProd_ite_eq, HasProd.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a : α
hf : HasProd f a L
b : β
a' : α
hf' : HasProd (fun (n : β) ↦ if n = b then 1 else f n) a' L
⊢ a = a' * f b

Tactic:
(mul_one a).symm.trans (hf.update' b 1 ?_)

Premises used: HasProd.update', mul_one, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a : α
hf : HasProd f a L
b : β
a' : α
hf' : HasProd (fun (n : β) ↦ if n = b then 1 else f n) a' L
refine : HasProd (update (β := fun (a : β) ↦ α) f b 1) a' L
⊢ a = a' * f b

Tactic:
refine (mul_one a).symm.trans (hf.update' b 1 ?_)

Premises used: HasProd.update', mul_one, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a : α
hf : HasProd f a L
b : β
a' : α
hf' : HasProd (fun (n : β) ↦ if n = b then 1 else f n) a' L
⊢ HasProd (fun (n : β) ↦ if n = b then 1 else f n) a' L

Tactic:
hf'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a : α
hf : HasProd f a L
b : β
a' : α
hf' : HasProd (fun (n : β) ↦ if n = b then 1 else f n) a' L
h : ∀ (x : β), update (β := fun (a : β) ↦ α) f b 1 x = if x = b then 1 else f x
⊢ HasProd (update (β := fun (a : β) ↦ α) f b 1) a' L

Tactic:
convert! hf'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
β : Type u_2
L : SummationFilter β
inst : L.LeAtTop
inst_1 : L.NeBot
α : Type u_4
inst_2 : TopologicalSpace α
inst_3 : CommMonoid α
inst_4 : T2Space α
inst_5 : ContinuousMul α
inst_6 : DecidableEq β
f : β → α
a : α
hf : HasProd f a L
b : β
a' : α
hf' : HasProd (fun (n : β) ↦ if n = b then 1 else f n) a' L
x : β
⊢ update (β := fun (a : β) ↦ α) f b 1 x = if x = b then 1 else f x

Tactic:
apply update_apply

Premises used: Function.update_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
s t : Set β
h : s = t
rw rw₁ : Eq.{u_1 + 1} (α := α) (∏' (x : (↑t : Type u_2)), f (↑x : β)) (∏' (x : (↑t : Type u_2)), f (↑x : β))
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑s : Type u_2)), f (↑x : β)) (∏' (x : (↑t : Type u_2)), f (↑x : β))

Tactic:
rw [h]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
P Q : β → Prop
h : ∀ (x : β), P x ↔ Q x
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : { x : β // P x }), f (↑x : β)) (∏' (x : { x : β // Q x }), f (↑x : β))

Tactic:
tprod_congr_set_coe f <| Set.ext h

Premises used: Set.ext, Set.Mem, tprod_congr_set_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : L.LeAtTop
hf : HasFiniteMulSupport f
⊢ L.HasSupport

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : L.LeAtTop
hf : HasFiniteMulSupport f
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), f b) (∏ᶠ (b : β), f b)

Tactic:
simp [tprod_def, multipliable_of_hasFiniteMulSupport hf, show Set.Finite _ from hf,
    show L.HasSupport by infer_instance]

Premises used: multipliable_of_hasFiniteMulSupport, tprod_def
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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)
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (∏ i ∈ s, f i) (∏ b ∈ s, f b)
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), f b) (∏ b ∈ s, f b)

Tactic:
rw [tprod_eq_finprod (s.finite_toSet.subset hf), finprod_eq_prod_of_mulSupport_subset _ hf]

Premises used: Set.Finite.subset, tprod_eq_finprod, Finset.finite_toSet, finprod_eq_prod_of_mulSupport_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : L.LeAtTop
s : Finset β
hf : ∀ b ∉ s, f b = 1
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), f b) (∏ b ∈ s, f b)

Tactic:
tprod_eq_prod' <| mulSupport_subset_iff'.2 hf

Premises used: Iff.mpr, Function.mulSupport_subset_iff', tprod_eq_prod'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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
rw₈ rw₉ : Eq.{u_1 + 1} (α := α) 1 1
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (x : β), 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]

Premises used: if_true, multipliable_one, ite_self, eq_true_intro, dif_pos, Set.empty_inter, hasProd_one, tprod_def, Function.mulSupport_fun_one, finprod_one, Set.mulIndicator_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : IsEmpty β
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (x : β), 1) 1

Tactic:
tprod_one (L := L)

Premises used: tprod_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : IsEmpty β
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), f b) 1

Tactic:
convert! tprod_one (L := L)

Premises used: tprod_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f g : β → α
hfg : ∀ (b : β), f b = g b
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), f b) (∏'[L] (b : β), g b)

Tactic:
congr_arg (tprod · L) (funext hfg)

Premises used: congr_arg, funext, tprod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f g : β → γ → α
M : SummationFilter γ
hfg : ∀ (b : β) (c : γ), f b c = g b c
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), ∏'[M] (c : γ), f b c) (∏'[L] (b : β), ∏'[M] (c : γ), g b c)

Tactic:
tprod_congr fun b ↦ tprod_congr fun c ↦ hfg b c

Premises used: tprod_congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : L.LeAtTop
inst_3 : Fintype β
f : β → α
hf : ∀ b ∉ univ, f b = 1
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), f b) (∏ b : β, f b)

Tactic:
apply tprod_eq_prod

Premises used: tprod_eq_prod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : L.LeAtTop
inst_3 : Fintype β
f : β → α
⊢ ∀ b ∉ univ, f b = 1

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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)
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (∏ x ∈ s, f x) (∏ i ∈ s, f i)
⊢ Eq.{u_1 + 1} (α := α) (∏ x ∈ s, f x) (∏'[L] (x : β), (↑s : Set β).mulIndicator f x)

Tactic:
rw [tprod_eq_prod' (Set.mulSupport_mulIndicator_subset),
      Finset.prod_mulIndicator_subset _ Finset.Subset.rfl]

Premises used: Finset.prod_mulIndicator_subset, Finset.Subset.rfl, tprod_eq_prod', Set.mulSupport_mulIndicator_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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
rw₂ rw₃ : f false * f true = f false * f true
⊢ ∏' (i : Bool), f i = f false * f true

Tactic:
rw [tprod_fintype, Fintype.prod_bool, mul_comm]

Premises used: tprod_fintype, Fintype.prod_bool, mul_comm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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
rw : ∀ b_1 ∉ {b}, f b_1 = 1
⊢ ∏'[L] (b : β), f b = f b

Tactic:
rw [tprod_eq_prod (s := {b}), prod_singleton]

Premises used: Finset.prod_singleton, tprod_eq_prod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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
b' : β
hb' : b' ∉ {b}
⊢ b' ≠ b

Tactic:
simpa using hb'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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
⊢ ∀ b_1 ∉ {b}, f b_1 = 1

Tactic:
exact fun b' hb' ↦ hf b' (by simpa using hb')
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → γ → α
b : β
c : γ
hfb : ∀ (b' : β), b' ≠ b → f b' c = 1
hfc : ∀ (b' : β) (c' : γ), c' ≠ c → f b' c' = 1
⊢ ∏' (b' : β) (c' : γ), f b' c' = f b c

Tactic:
calc
    ∏' (b') (c'), f b' c' = ∏' b', f b' c := tprod_congr fun b' ↦ tprod_eq_mulSingle _ (hfc b')
    _ = f b c := tprod_eq_mulSingle _ hfb

Premises used: Trans.trans, tprod_congr, tprod_eq_mulSingle
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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
rw₁ : ∀ (b' : β), b' ≠ b → (if b' = b then a b' else 1) = 1
⊢ (∏'[L] (b' : β), if b' = b then a b' else 1) = a b

Tactic:
rw [tprod_eq_mulSingle b]

Premises used: tprod_eq_mulSingle
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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
⊢ (if b = b then a b else 1) = a b

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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
b' : β
hb' : b' ≠ b
⊢ (if b' = b then a b' else 1) = 1

Tactic:
simp [hb']
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Finset β
f : β → α
rw : Eq.{u_1 + 1} (α := α) (∏' (x : ↥s), f (↑x : β)) (∏ x ∈ s.attach, f (↑x : β))
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : ↥s), f (↑x : β)) (∏ x ∈ s, f x)

Tactic:
rw [← prod_attach]

Premises used: Finset.prod_attach
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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.attach, f (↑x : β))

Tactic:
tprod_fintype _

Premises used: Finset.univ, tprod_fintype, Finset.attach
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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.attach, f (↑x : β))

Tactic:
exact tprod_fintype _

Premises used: tprod_fintype
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Finset β
f : β → α
⊢ Eq.{u_1 + 1} (α := α) (∏' (x : (↑(↑s : Set β) : Type u_2)), f (↑x : β)) (∏ x ∈ s, f x)

Tactic:
simp [prod_attach]

Premises used: Finset.prod_attach
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
b : β
f : β → α
⊢ ∏' (x : (↑{b} : Type u_2)), f (↑x : β) = f b

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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
rw₁ rw₂ : mulSupport f = mulSupport f
⊢ mulSupport f = g '' mulSupport (f ∘ g)

Tactic:
rw [mulSupport_comp_eq_preimage, Set.image_preimage_eq_iff.2 hf]

Premises used: Iff.mpr, Function.mulSupport_comp_eq_preimage, Set.image_preimage_eq_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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)

Tactic:
have : mulSupport f = g '' mulSupport (f ∘ g) := by
    rw [mulSupport_comp_eq_preimage, Set.image_preimage_eq_iff.2 hf]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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)
rw : tprod (f ∘ g) = ∏' (b : β), f b
⊢ Eq.{u_1 + 1} (α := α) (∏' (c : γ), f (g c)) (∏' (b : β), f b)

Tactic:
rw [← Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
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
neg : ∀ (hf_fin : ¬(mulSupport f).Finite), tprod (f ∘ g) = ∏' (b : β), f b
⊢ tprod (f ∘ g) = ∏' (b : β), f b

Tactic:
by_cases hf_fin : (mulSupport f).Finite

Premises used: Set.Finite, Function.mulSupport