awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
X : Type u_4
inst_4 : TopologicalSpace X
a : X
f : X → G₀
hf : ContinuousAt f a
m : ℤ
h : f a ≠ 0 ∨ 0 ≤ m
⊢ ContinuousAt.{u_4, u_3} (Y := G₀) (fun (x : X) ↦ f x ^ m) a

Tactic:
hf.zpow₀ m h

Premises used: ContinuousAt, Filter.Tendsto.zpow₀
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
X : Type u_4
inst_4 : TopologicalSpace X
a : X
s : Set X
f : X → G₀
hf : ContinuousWithinAt f s a
m : ℤ
h : f a ≠ 0 ∨ 0 ≤ m
⊢ ContinuousWithinAt.{u_4, u_3} (Y := G₀) (fun (x : X) ↦ f x ^ m) s a

Tactic:
hf.zpow₀ m h

Premises used: ContinuousWithinAt, Filter.Tendsto.zpow₀
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
X : Type u_4
inst_4 : TopologicalSpace X
s : Set X
f : X → G₀
hf : ContinuousOn f s
m : ℤ
h : ∀ a ∈ s, f a ≠ 0 ∨ 0 ≤ m
⊢ ContinuousOn.{u_4, u_3} (Y := G₀) (fun (x : X) ↦ f x ^ m) s

Tactic:
fun a ha => (hf a ha).zpow₀ m (h a ha)

Premises used: ContinuousOn, ContinuousWithinAt.zpow₀
-- Module: Mathlib.Topology.Algebra.GroupWithZero
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
inst_1 : TopologicalSpace G₀
inst_2 : ContinuousInv₀ G₀
inst_3 : ContinuousMul G₀
X : Type u_4
inst_4 : TopologicalSpace X
f : X → G₀
hf : Continuous[inst_4, inst_1] f
m : ℤ
h0 : ∀ (a : X), f a ≠ 0 ∨ 0 ≤ m
⊢ Continuous[inst_4, inst_1] fun (x : X) ↦ f x ^ m

Tactic:
continuous_iff_continuousAt.2 fun x => (hf.tendsto x).zpow₀ m (h0 x)

Premises used: Iff.mpr, Continuous.tendsto, Filter.Tendsto.zpow₀, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hs : ∀ a ∈ frontier s, f a = 1
hf : ContinuousOn f (closure[inst] s)
⊢ Continuous[inst, inst_1] (s.mulIndicator f)

Tactic:
continuous_piecewise hs hf continuousOn_const

Premises used: Set.mulIndicator, continuousOn_const, continuous_piecewise
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hs : ∀ a ∈ frontier s, f a = 1
hf : ContinuousOn f (closure[inst] s)
⊢ Continuous[inst, inst_1] (s.mulIndicator f)

Tactic:
exact continuous_piecewise hs hf continuousOn_const

Premises used: continuousOn_const, continuous_piecewise
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hs : ∀ a ∈ frontier s, f a = 1
hf : ContinuousOn f (closure[inst] s)
⊢ Continuous[inst, inst_1] (s.mulIndicator f)

Tactic:
classical exact continuous_piecewise hs hf continuousOn_const
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hs : ∀ a ∈ frontier s, f a = 1
hf : Continuous[inst, inst_1] f
⊢ Continuous[inst, inst_1] (s.mulIndicator f)

Tactic:
hf.piecewise hs continuous_const

Premises used: Set.mulIndicator, continuous_const, Continuous.piecewise
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hs : ∀ a ∈ frontier s, f a = 1
hf : Continuous[inst, inst_1] f
⊢ Continuous[inst, inst_1] (s.mulIndicator f)

Tactic:
exact hf.piecewise hs continuous_const

Premises used: continuous_const, Continuous.piecewise
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hs : ∀ a ∈ frontier s, f a = 1
hf : Continuous[inst, inst_1] f
⊢ Continuous[inst, inst_1] (s.mulIndicator f)

Tactic:
classical exact hf.piecewise hs continuous_const
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hf : ContinuousOn f (interior s)
x : α
hx : x ∉ frontier s
⊢ x ∈ interior s ∪ interior sᶜ

Tactic:
rw [← Set.mem_compl_iff, compl_frontier_eq_union_interior] at hx

Premises used: compl_frontier_eq_union_interior, Set.mem_compl_iff
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hf : ContinuousOn f (interior s)
x : α
hx : x ∈ interior s ∪ interior sᶜ
inl : ∀ (h : x ∈ interior s), ContinuousAt (s.mulIndicator f) x
inr : ∀ (h : x ∈ interior sᶜ), ContinuousAt (s.mulIndicator f) x
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
obtain h | h := hx
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hf : ContinuousOn f (interior s)
x : α
h rwa rwa₁ rwa₂ rwa₃ : x ∈ interior s
⊢ x ∈ interior (interior s)

Tactic:
rwa [interior_interior]

Premises used: interior_interior
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior s
⊢ interior s ∈ 𝓝 x

Tactic:
have hs : interior s ∈ 𝓝 x := mem_interior_iff_mem_nhds.mp (by rwa [interior_interior])
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior s
hs : interior s ∈ 𝓝 x
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
ContinuousAt.congr (hf.continuousAt hs) <| Filter.eventuallyEq_iff_exists_mem.mpr
      ⟨interior s, hs, Set.eqOn_mulIndicator.symm.mono interior_subset⟩

Premises used: Iff.mpr, interior_subset, ContinuousAt.congr, Set.eqOn_mulIndicator, And.intro, interior, Exists.intro, Filter.eventuallyEq_iff_exists_mem, Set.EqOn.symm, ContinuousOn.continuousAt, Set.EqOn.mono
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior s
hs : interior s ∈ 𝓝 x
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
exact ContinuousAt.congr (hf.continuousAt hs) <| Filter.eventuallyEq_iff_exists_mem.mpr
      ⟨interior s, hs, Set.eqOn_mulIndicator.symm.mono interior_subset⟩

Premises used: Iff.mpr, interior_subset, ContinuousAt.congr, Set.eqOn_mulIndicator, And.intro, interior, Exists.intro, Filter.eventuallyEq_iff_exists_mem, Set.EqOn.symm, ContinuousOn.continuousAt, Set.EqOn.mono
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior sᶜ
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
ContinuousAt.congr continuousAt_const <| Filter.eventuallyEq_iff_exists_mem.mpr
      ⟨sᶜ, mem_interior_iff_mem_nhds.mp h, Set.eqOn_mulIndicator'.symm⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, Compl.compl, ContinuousAt.congr, Set.eqOn_mulIndicator', continuousAt_const, And.intro, Exists.intro, Iff.mp, Filter.eventuallyEq_iff_exists_mem, Set.EqOn.symm
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior sᶜ
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
exact ContinuousAt.congr continuousAt_const <| Filter.eventuallyEq_iff_exists_mem.mpr
      ⟨sᶜ, mem_interior_iff_mem_nhds.mp h, Set.eqOn_mulIndicator'.symm⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, Compl.compl, ContinuousAt.congr, Set.eqOn_mulIndicator', continuousAt_const, And.intro, Exists.intro, Iff.mp, Filter.eventuallyEq_iff_exists_mem, Set.EqOn.symm
-- Module: Mathlib.Topology.Algebra.Indicator
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
inst_2 : One β
hs : IsClopen s
hf : Continuous[inst, inst_1] f
⊢ ∀ a ∈ frontier s, f a = 1

Tactic:
simp [isClopen_iff_frontier_eq_empty.mp hs]

Premises used: Iff.mp, isClopen_iff_frontier_eq_empty
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
⊢ HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L

Tactic:
simp [HasProd, tendsto_const_nhds]

Premises used: tendsto_const_nhds, HasProd, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : IsEmpty β
⊢ HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L

Tactic:
hasProd_one

Premises used: hasProd_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 β
⊢ HasProd f 1 L

Tactic:
convert! hasProd_one

Premises used: hasProd_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : Subsingleton α
⊢ HasProd.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) 1 L

Tactic:
hasProd_one

Premises used: hasProd_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : Subsingleton α
⊢ HasProd f 1 L

Tactic:
convert! hasProd_one

Premises used: hasProd_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
⊢ Multipliable.{u_1, u_2} (α := α) (fun (x : β) ↦ 1) L

Tactic:
hasProd_one.multipliable

Premises used: hasProd_one, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : IsEmpty β
⊢ Multipliable f L

Tactic:
hasProd_empty.multipliable

Premises used: HasProd.multipliable, hasProd_empty
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : Subsingleton α
⊢ Multipliable f L

Tactic:
HasProd.of_subsingleton_cod.multipliable

Premises used: HasProd.of_subsingleton_cod, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f g : β → α
L : SummationFilter β
hfg : ∀ (b : β), f b = g b
⊢ Multipliable f L ↔ Multipliable g L

Tactic:
iff_of_eq (congr_arg (Multipliable · L) <| funext hfg)

Premises used: Multipliable, congr_arg, funext, iff_of_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f g : β → α
L : SummationFilter β
hf : Multipliable f L
hfg : ∀ (b : β), f b = g b
⊢ Multipliable g L

Tactic:
(multipliable_congr hfg).mp hf

Premises used: multipliable_congr, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f g : β → α
a : α
L : SummationFilter β
hf : HasProd f a L
h : ∀ (x : β), g x = f x
⊢ HasProd g a L

Tactic:
(funext h : g = f) ▸ hf

Premises used: Eq.rec, funext, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
g : γ → α
h_eq :
  ∀ (u : Finset γ),
    ∃ (v : Finset β),
      ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset γ), u ⊆ u' ∧ Eq.{u_1 + 1} (α := α) (∏ x ∈ u', g x) (∏ b ∈ v', f b)
hf : HasProd g a
⊢ HasProd f a

Tactic:
le_trans (map_atTop_finsetProd_le_of_prod_eq h_eq) hf

Premises used: HasProd, Filter.Tendsto, Filter.map_atTop_finsetProd_le_of_prod_eq, le_trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
g : γ → α
h₁ :
  ∀ (u : Finset γ),
    ∃ (v : Finset β),
      ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset γ), u ⊆ u' ∧ Eq.{u_1 + 1} (α := α) (∏ x ∈ u', g x) (∏ b ∈ v', f b)
h₂ :
  ∀ (v : Finset β),
    ∃ (u : Finset γ),
      ∀ (u' : Finset γ), u ⊆ u' → ∃ (v' : Finset β), v ⊆ v' ∧ Eq.{u_1 + 1} (α := α) (∏ b ∈ v', f b) (∏ x ∈ u', g x)
⊢ HasProd f a ↔ HasProd g a

Tactic:
⟨HasProd.hasProd_of_prod_eq h₂, HasProd.hasProd_of_prod_eq h₁⟩

Premises used: HasProd.hasProd_of_prod_eq, Iff.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
g : γ → β
hg : Injective g
hf : ∀ x ∉ Set.range g, f x = 1
⊢ Multipliable (f ∘ g) ↔ Multipliable f

Tactic:
exists_congr fun _ ↦ hg.hasProd_iff hf

Premises used: Multipliable, exists_congr, Function.Injective.hasProd_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
rw : ∀ x ∉ Set.range g, extend g f 1 x = 1
⊢ HasProd (extend g f 1) a ↔ HasProd f a

Tactic:
rw [← hg.hasProd_iff, extend_comp hg]

Premises used: Function.extend_comp, Function.Injective.hasProd_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ ∀ x ∉ Set.range g, extend g f 1 x = 1

Tactic:
extend_apply' _ _

Premises used: Set.Mem, setOf, Function.extend_apply', Set.range
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ ∀ x ∉ Set.range g, extend g f 1 x = 1

Tactic:
exact extend_apply' _ _

Premises used: Function.extend_apply'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
g : β → γ
hg : Injective g
⊢ Multipliable (extend g f 1) ↔ Multipliable f

Tactic:
exists_congr fun _ ↦ hasProd_extend_one hg

Premises used: Multipliable, exists_congr, hasProd_extend_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
s : Set β
rw :
  HasProd (β := (↑s : Type u_2))
      (Set.mulIndicator (Set.range (ι := (↑s : Type u_2)) (Subtype.val (p := fun (x : β) ↦ x ∈ s))) f ∘
        Subtype.val (p := fun (x : β) ↦ x ∈ s))
      a ↔
    HasProd (s.mulIndicator f) a
rw₁ :
  HasProd (β := (↑s : Type u_2)) (s.mulIndicator f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a ↔
    HasProd (s.mulIndicator f) a
rw₂ rw₃ : HasProd (s.mulIndicator f) a ↔ HasProd (s.mulIndicator f) a
⊢ HasProd (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) a ↔ HasProd (s.mulIndicator f) a

Tactic:
rw [← Set.mulIndicator_range_comp, Subtype.range_coe,
    hasProd_subtype_iff_of_mulSupport_subset Set.mulSupport_mulIndicator_subset]

Premises used: Subtype.range_coe, Set.mulSupport_mulIndicator_subset, hasProd_subtype_iff_of_mulSupport_subset, Set.mulIndicator_range_comp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
s : Set β
⊢ Multipliable (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s)) ↔ Multipliable (s.mulIndicator f)

Tactic:
exists_congr fun _ ↦ hasProd_subtype_iff_mulIndicator

Premises used: hasProd_subtype_iff_mulIndicator, Multipliable, exists_congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
⊢ HasProd (β := (↑(mulSupport f) : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ mulSupport f)) a ↔ HasProd f a

Tactic:
hasProd_subtype_iff_of_mulSupport_subset <| Set.Subset.refl _

Premises used: Set.Subset.refl, hasProd_subtype_iff_of_mulSupport_subset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Finset β
f : β → α
⊢ Multipliable (β := (↑(↑s : Set β) : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ (↑s : Set β)))

Tactic:
(s.hasProd f).multipliable

Premises used: Set.Elem, SetLike.coe, Finset.hasProd, HasProd.multipliable, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Set β
hs : s.Finite
f : β → α
⊢ Multipliable (β := (↑(↑(hs.toFinset (s := s)) : Set β) : Type u_2))
    (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ (↑(hs.toFinset (s := s)) : Set β)))

Tactic:
have := hs.toFinset.multipliable f
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
s : Set β
hs : s.Finite
f : β → α
this :
  Multipliable (β := (↑(↑(hs.toFinset (s := s)) : Set β) : Type u_2))
    (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ (↑(hs.toFinset (s := s)) : Set β)))
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : Multipliable (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s))),
    Multipliable (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s))
⊢ Multipliable (β := (↑s : Type u_2)) (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ s))

Tactic:
rwa [hs.coe_toFinset] at this

Premises used: Set.Finite.coe_toFinset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : L.HasSupport
h : HasFiniteMulSupport f
hf : ∀ b ∉ Set.Finite.toFinset (s := mulSupport f) h, f b = 1
⊢ Multipliable f L

Tactic:
apply multipliable_of_ne_finset_one (s := h.toFinset)

Premises used: multipliable_of_ne_finset_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : L.HasSupport
h : HasFiniteMulSupport f
⊢ ∀ b ∉ Set.Finite.toFinset (s := mulSupport f) h, f b = 1

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : Finite β
inst_3 : L.HasSupport
f : β → α
⊢ Multipliable f L

Tactic:
multipliable_of_hasFiniteMulSupport <| Set.finite_univ.subset (Set.subset_univ _)

Premises used: Set.subset_univ, Set.Finite.subset, multipliable_of_hasFiniteMulSupport, Set.finite_univ
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
L : SummationFilter β
inst_2 : L.LeAtTop
⊢ ∀ b_1 ∉ {b}, f b_1 = 1

Tactic:
simpa [hf]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
L : SummationFilter β
inst_2 : L.LeAtTop
this : HasProd f (∏ b' ∈ {b}, f b') L
⊢ HasProd f (f b) L

Tactic:
simpa using this
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
inst_2 : Unique β
f : β → α
L : SummationFilter β
inst_3 : L.LeAtTop
⊢ HasProd f (f default) L

Tactic:
hasProd_single default (fun _ hb ↦ False.elim <| hb <| Unique.uniq ..) L

Premises used: Inhabited.default, False.elim, Unique.uniq, hasProd_single
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
m : β
f : β → α
⊢ HasProd (β := (↑{m} : Type u_2)) (Set.restrict (π := fun (a : β) ↦ α) {m} f) (f m)

Tactic:
hasProd_unique (Set.restrict {m} f)

Premises used: Set.restrict, hasProd_unique, Singleton.singleton, SummationFilter.unconditional
-- 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
⊢ HasProd (fun (b' : β) ↦ if b' = b then a else 1) (if b = b then a else 1) L

Tactic:
hasProd_single b (hf := fun b' hb' ↦ if_neg hb') (L := L)

Premises used: hasProd_single, if_neg
-- 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
h : a = if b = b then a else 1
⊢ HasProd (fun (b' : β) ↦ if b' = b then a else 1) a L

Tactic:
convert! hasProd_single b (hf := fun b' hb' ↦ if_neg hb') (L := L)

Premises used: hasProd_single, if_neg
-- 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
⊢ a = if b = b then a else 1

Tactic:
(if_pos rfl).symm

Premises used: if_pos, Eq.symm, rfl
-- 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
⊢ a = if b = b then a else 1

Tactic:
exact (if_pos rfl).symm

Premises used: if_pos, Eq.symm, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
e : γ ≃ β
⊢ ∀ x ∉ Set.range.{u_2, u_3 + 1} (ι := γ) (⇑e : (a : γ) → β), f x = 1

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
g : γ → β
hg : Injective g
⊢ HasProd (fun (x : (↑(Set.range g) : Type u_2)) ↦ f (↑x : β)) a ↔ HasProd (f ∘ g) a

Tactic:
(Equiv.ofInjective g hg).hasProd_iff.symm

Premises used: Equiv.hasProd_iff, Equiv.ofInjective, Iff.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
e : γ ≃ β
⊢ Multipliable (f ∘ (⇑e : (a : γ) → β)) ↔ Multipliable f

Tactic:
exists_congr fun _ ↦ e.hasProd_iff

Premises used: Equiv.hasProd_iff, Multipliable, exists_congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
a : α
g : γ → α
e : Equiv.{u_2 + 1, u_3 + 1} (↑(mulSupport f) : Type u_2) (↑(mulSupport g) : Type u_3)
he :
  ∀ (x : (↑(mulSupport f) : Type u_2)),
    g (↑((e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)) x) : γ) = f (↑x : β)
⊢ Eq (α := (↑(mulSupport f) : Type u_2) → α)
    (comp (β := (↑(mulSupport g) : Type u_3)) (g ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ mulSupport g))
      (⇑e : (a : (↑(mulSupport f) : Type u_2)) → (↑(mulSupport g) : Type u_3)))
    (f ∘ Subtype.val (p := fun (x : β) ↦ x ∈ mulSupport f))

Tactic:
have : (g ∘ (↑)) ∘ e = f ∘ (↑) := funext he