ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>AddCommMonoid γ<VAR>TopologicalSpace γ<VAR>hf : HasSum f a<VAR>G : Type u_5<VAR>FunLike G α γ<VAR>AddMonoidHomClass G α γ<VAR>g : G<VAR>hg : Continuous ⇑g<GOAL>HasSum (⇑g ∘ f) (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>CommMonoid γ<VAR>TopologicalSpace γ<VAR>hf : HasProd f a<VAR>G : Type u_5<VAR>FunLike G α γ<VAR>MonoidHomClass G α γ<VAR>g : G<VAR>hg : Continuous ⇑g<GOAL>HasProd (⇑g ∘ f) (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>CommMonoid γ<VAR>TopologicalSpace γ<VAR>G : Type u_5<VAR>FunLike G α γ<VAR>MonoidHomClass G α γ<VAR>g : G<VAR>hg : Inducing ⇑g<VAR>f : β → α<VAR>a : α<GOAL>HasProd (⇑g ∘ f) (g a) ↔ HasProd f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>AddCommMonoid γ<VAR>TopologicalSpace γ<VAR>G : Type u_5<VAR>FunLike G α γ<VAR>AddMonoidHomClass G α γ<VAR>g : G<VAR>hg : Inducing ⇑g<VAR>f : β → α<VAR>a : α<GOAL>HasSum (⇑g ∘ f) (g a) ↔ HasSum f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>CommMonoid γ<VAR>TopologicalSpace γ<VAR>hf : Multipliable f<VAR>G : Type u_5<VAR>FunLike G α γ<VAR>MonoidHomClass G α γ<VAR>g : G<VAR>hg : Continuous ⇑g<GOAL>Multipliable (⇑g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>AddCommMonoid γ<VAR>TopologicalSpace γ<VAR>hf : Summable f<VAR>G : Type u_5<VAR>FunLike G α γ<VAR>AddMonoidHomClass G α γ<VAR>g : G<VAR>hg : Continuous ⇑g<GOAL>Summable (⇑g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>AddCommMonoid γ<VAR>TopologicalSpace γ<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>FunLike G α γ<VAR>AddMonoidHomClass G α γ<VAR>FunLike G' γ α<VAR>AddMonoidHomClass G' γ α<VAR>g : G<VAR>g' : G'<VAR>hg : Continuous ⇑g<VAR>hg' : Continuous ⇑g'<VAR>hinv : Function.LeftInverse ⇑g' ⇑g<GOAL>Summable (⇑g ∘ f) ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>CommMonoid γ<VAR>TopologicalSpace γ<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>FunLike G α γ<VAR>MonoidHomClass G α γ<VAR>FunLike G' γ α<VAR>MonoidHomClass G' γ α<VAR>g : G<VAR>g' : G'<VAR>hg : Continuous ⇑g<VAR>hg' : Continuous ⇑g'<VAR>hinv : Function.LeftInverse ⇑g' ⇑g<GOAL>Multipliable (⇑g ∘ f) ↔ Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>AddCommMonoid γ<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>hf : Summable f<VAR>G : Type u_5<VAR>FunLike G α γ<VAR>AddMonoidHomClass G α γ<VAR>g : G<VAR>hg : Continuous ⇑g<GOAL>g (∑' (i : β), f i) = ∑' (i : β), g (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>CommMonoid γ<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>hf : Multipliable f<VAR>G : Type u_5<VAR>FunLike G α γ<VAR>MonoidHomClass G α γ<VAR>g : G<VAR>hg : Continuous ⇑g<GOAL>g (∏' (i : β), f i) = ∏' (i : β), g (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>AddCommMonoid γ<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>G : Type u_5<VAR>FunLike G α γ<VAR>AddMonoidHomClass G α γ<VAR>g : G<VAR>hg : Inducing ⇑g<VAR>f : β → α<GOAL>Summable f ↔ Summable (⇑g ∘ f) ∧ ∑' (i : β), g (f i) ∈ Set.range ⇑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>CommMonoid γ<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>G : Type u_5<VAR>FunLike G α γ<VAR>MonoidHomClass G α γ<VAR>g : G<VAR>hg : Inducing ⇑g<VAR>f : β → α<GOAL>Multipliable f ↔ Multipliable (⇑g ∘ f) ∧ ∏' (i : β), g (f i) ∈ Set.range ⇑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>CommMonoid γ<VAR>TopologicalSpace γ<VAR>G : Type u_5<VAR>EquivLike G α γ<VAR>MulEquivClass G α γ<VAR>g : G<VAR>hg : Continuous ⇑g<VAR>hg' : Continuous (EquivLike.inv g)<GOAL>Multipliable (⇑g ∘ f) ↔ Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>AddCommMonoid γ<VAR>TopologicalSpace γ<VAR>G : Type u_5<VAR>EquivLike G α γ<VAR>AddEquivClass G α γ<VAR>g : G<VAR>hg : Continuous ⇑g<VAR>hg' : Continuous (EquivLike.inv g)<GOAL>Summable (⇑g ∘ f) ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>α' : Type u_5<VAR>CommMonoid α'<VAR>TopologicalSpace α'<VAR>e : α' → α<VAR>hes : Function.Surjective e<VAR>f : β → α<VAR>g : γ → α'<VAR>he : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a<GOAL>Multipliable f ↔ Multipliable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>α' : Type u_5<VAR>AddCommMonoid α'<VAR>TopologicalSpace α'<VAR>e : α' → α<VAR>hes : Function.Surjective e<VAR>f : β → α<VAR>g : γ → α'<VAR>he : ∀ {a : α'}, HasSum f (e a) ↔ HasSum g a<GOAL>Summable f ↔ Summable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>ContinuousAdd α<VAR>hf : HasSum f a<VAR>hg : HasSum g b<GOAL>HasSum (fun b => f b + g b) (a + b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>ContinuousMul α<VAR>hf : HasProd f a<VAR>hg : HasProd g b<GOAL>HasProd (fun b => f b * g b) (a * b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f g : β → α<VAR>ContinuousMul α<VAR>hf : Multipliable f<VAR>hg : Multipliable g<GOAL>Multipliable fun b => f b * g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f g : β → α<VAR>ContinuousAdd α<VAR>hf : Summable f<VAR>hg : Summable g<GOAL>Summable fun b => f b + g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousMul α<VAR>f : γ → β → α<VAR>a : γ → α<VAR>s : Finset γ<GOAL>(∀ i ∈ s, HasProd (f i) (a i)) → HasProd (fun b => ∏ i ∈ s, f i b) (∏ i ∈ s, a i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousAdd α<VAR>f : γ → β → α<VAR>a : γ → α<VAR>s : Finset γ<GOAL>(∀ i ∈ s, HasSum (f i) (a i)) → HasSum (fun b => ∑ i ∈ s, f i b) (∑ i ∈ s, a i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousAdd α<VAR>f : γ → β → α<VAR>s : Finset γ<VAR>hf : ∀ i ∈ s, Summable (f i)<GOAL>Summable fun b => ∑ i ∈ s, f i b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>ContinuousMul α<VAR>f : γ → β → α<VAR>s : Finset γ<VAR>hf : ∀ i ∈ s, Multipliable (f i)<GOAL>Multipliable fun b => ∏ i ∈ s, f i b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a b : α<VAR>ContinuousAdd α<VAR>s t : Set β<VAR>hs : Disjoint s t<VAR>ha : HasSum (f ∘ Subtype.val) a<VAR>hb : HasSum (f ∘ Subtype.val) b<GOAL>HasSum (f ∘ Subtype.val) (a + b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a b : α<VAR>ContinuousMul α<VAR>s t : Set β<VAR>hs : Disjoint s t<VAR>ha : HasProd (f ∘ Subtype.val) a<VAR>hb : HasProd (f ∘ Subtype.val) b<GOAL>HasProd (f ∘ Subtype.val) (a * b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>ContinuousAdd α<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>t : ι → Set β<VAR>a : ι → α<VAR>hs : (↑s).Pairwise (Disjoint on t)<VAR>hf : ∀ i ∈ s, HasSum (f ∘ Subtype.val) (a i)<GOAL>HasSum (f ∘ Subtype.val) (∑ i ∈ s, a i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>ContinuousMul α<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>t : ι → Set β<VAR>a : ι → α<VAR>hs : (↑s).Pairwise (Disjoint on t)<VAR>hf : ∀ i ∈ s, HasProd (f ∘ Subtype.val) (a i)<GOAL>HasProd (f ∘ Subtype.val) (∏ i ∈ s, a i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a b : α<VAR>ContinuousMul α<VAR>s t : Set β<VAR>hs : IsCompl s t<VAR>ha : HasProd (f ∘ Subtype.val) a<VAR>hb : HasProd (f ∘ Subtype.val) b<GOAL>HasProd f (a * b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a b : α<VAR>ContinuousAdd α<VAR>s t : Set β<VAR>hs : IsCompl s t<VAR>ha : HasSum (f ∘ Subtype.val) a<VAR>hb : HasSum (f ∘ Subtype.val) b<GOAL>HasSum f (a + b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a b : α<VAR>ContinuousMul α<VAR>s : Set β<VAR>ha : HasProd (f ∘ Subtype.val) a<VAR>hb : HasProd (f ∘ Subtype.val) b<GOAL>HasProd f (a * b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a b : α<VAR>ContinuousAdd α<VAR>s : Set β<VAR>ha : HasSum (f ∘ Subtype.val) a<VAR>hb : HasSum (f ∘ Subtype.val) b<GOAL>HasSum f (a + b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>ContinuousAdd α<VAR>s : Set β<VAR>hs : Summable (f ∘ Subtype.val)<VAR>hsc : Summable (f ∘ Subtype.val)<GOAL>Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>ContinuousMul α<VAR>s : Set β<VAR>hs : Multipliable (f ∘ Subtype.val)<VAR>hsc : Multipliable (f ∘ Subtype.val)<GOAL>Multipliable f
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>TopologicalSpace α<VAR>CommMonoid α<VAR>T2Space α<VAR>ContinuousMul α<VAR>DecidableEq β<VAR>f : β → α<VAR>a a' : α<VAR>hf : HasProd f a<VAR>b : β<VAR>x : α<VAR>hf' : HasProd (Function.update f b x) a'<GOAL>a * x = a' * f b
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>TopologicalSpace α<VAR>AddCommMonoid α<VAR>T2Space α<VAR>ContinuousAdd α<VAR>DecidableEq β<VAR>f : β → α<VAR>a a' : α<VAR>hf : HasSum f a<VAR>b : β<VAR>x : α<VAR>hf' : HasSum (Function.update f b x) a'<GOAL>a + x = a' + f b
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>TopologicalSpace α<VAR>AddCommMonoid α<VAR>T2Space α<VAR>ContinuousAdd α<VAR>DecidableEq β<VAR>f : β → α<VAR>a : α<VAR>hf : HasSum f a<VAR>b : β<VAR>a' : α<VAR>hf' : HasSum (fun n => if n = b then 0 else f n) a'<GOAL>a = a' + f b
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>TopologicalSpace α<VAR>CommMonoid α<VAR>T2Space α<VAR>ContinuousMul α<VAR>DecidableEq β<VAR>f : β → α<VAR>a : α<VAR>hf : HasProd f a<VAR>b : β<VAR>a' : α<VAR>hf' : HasProd (fun n => if n = b then 1 else f n) a'<GOAL>a = a' * f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s t : Set β<VAR>h : s = t<GOAL>∑' (x : ↑s), f ↑x = ∑' (x : ↑t), f ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s t : Set β<VAR>h : s = t<GOAL>∏' (x : ↑s), f ↑x = ∏' (x : ↑t), f ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>P Q : β → Prop<VAR>h : ∀ (x : β), P x ↔ Q x<GOAL>∏' (x : { x // P x }), f ↑x = ∏' (x : { x // Q x }), f ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>P Q : β → Prop<VAR>h : ∀ (x : β), P x ↔ Q x<GOAL>∑' (x : { x // P x }), f ↑x = ∑' (x : { x // Q x }), f ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>hf : (Function.support f).Finite<GOAL>∑' (b : β), f b = ∑ᶠ (b : β), f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>hf : (Function.mulSupport f).Finite<GOAL>∏' (b : β), f b = ∏ᶠ (b : β), f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Finset β<VAR>hf : Function.mulSupport f ⊆ ↑s<GOAL>∏' (b : β), f b = ∏ b ∈ s, f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Finset β<VAR>hf : Function.support f ⊆ ↑s<GOAL>∑' (b : β), f b = ∑ b ∈ s, f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Finset β<VAR>hf : ∀ b ∉ s, f b = 1<GOAL>∏' (b : β), f b = ∏ b ∈ s, f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Finset β<VAR>hf : ∀ b ∉ s, f b = 0<GOAL>∑' (b : β), f b = ∑ b ∈ s, f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<GOAL>∏' (x : β), 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<GOAL>∑' (x : β), 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>IsEmpty β<GOAL>∑' (b : β), f b = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>IsEmpty β<GOAL>∏' (b : β), f b = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f g : β → α<VAR>hfg : ∀ (b : β), f b = g b<GOAL>∑' (b : β), f b = ∑' (b : β), g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f g : β → α<VAR>hfg : ∀ (b : β), f b = g b<GOAL>∏' (b : β), f b = ∏' (b : β), g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>Fintype β<VAR>f : β → α<GOAL>∑' (b : β), f b = ∑ b : β, f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>Fintype β<VAR>f : β → α<GOAL>∏' (b : β), f b = ∏ b : β, f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Finset β<GOAL>∏ x ∈ s, f x = ∏' (x : β), (↑s).mulIndicator f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Finset β<GOAL>∑ x ∈ s, f x = ∑' (x : β), (↑s).indicator f x
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : Bool → α<GOAL>∏' (i : Bool), f i = f false * f true
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : Bool → α<GOAL>∑' (i : Bool), f i = f false + f true
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>b : β<VAR>hf : ∀ (b' : β), b' ≠ b → f b' = 0<GOAL>∑' (b : β), f b = f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>b : β<VAR>hf : ∀ (b' : β), b' ≠ b → f b' = 1<GOAL>∏' (b : β), f b = f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → γ → α<VAR>b : β<VAR>c : γ<VAR>hfb : ∀ (b' : β), b' ≠ b → f b' c = 0<VAR>hfc : ∀ (b' : β) (c' : γ), c' ≠ c → f b' c' = 0<GOAL>∑' (b' : β) (c' : γ), f b' c' = f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → γ → α<VAR>b : β<VAR>c : γ<VAR>hfb : ∀ (b' : β), b' ≠ b → f b' c = 1<VAR>hfc : ∀ (b' : β) (c' : γ), c' ≠ c → f b' c' = 1<GOAL>∏' (b' : β) (c' : γ), f b' c' = f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>b : β<VAR>DecidablePred fun x => x = b<VAR>a : α<GOAL>(∑' (b' : β), if b' = b then a else 0) = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>b : β<VAR>DecidablePred fun x => x = b<VAR>a : α<GOAL>(∏' (b' : β), if b' = b then a else 1) = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>s : Finset β<VAR>f : β → α<GOAL>∑' (x : { x // x ∈ s }), f ↑x = ∑ x ∈ s, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>s : Finset β<VAR>f : β → α<GOAL>∏' (x : { x // x ∈ s }), f ↑x = ∏ x ∈ s, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>s : Finset β<VAR>f : β → α<GOAL>∑' (x : ↑↑s), f ↑x = ∑ x ∈ s, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>s : Finset β<VAR>f : β → α<GOAL>∏' (x : ↑↑s), f ↑x = ∏ x ∈ s, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>b : β<VAR>f : β → α<GOAL>∑' (x : ↑{b}), f ↑x = f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>b : β<VAR>f : β → α<GOAL>∏' (x : ↑{b}), f ↑x = f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>g : γ → β<VAR>hg : Function.Injective g<VAR>f : β → α<VAR>hf : Function.mulSupport f ⊆ Set.range g<GOAL>∏' (c : γ), f (g c) = ∏' (b : β), f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>g : γ → β<VAR>hg : Function.Injective g<VAR>f : β → α<VAR>hf : Function.support f ⊆ Set.range g<GOAL>∑' (c : γ), f (g c) = ∑' (b : β), f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>e : γ ≃ β<VAR>f : β → α<GOAL>∏' (c : γ), f (e c) = ∏' (b : β), f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>e : γ ≃ β<VAR>f : β → α<GOAL>∑' (c : γ), f (e c) = ∑' (b : β), f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Set β<VAR>hs : Function.mulSupport f ⊆ s<GOAL>∏' (x : ↑s), f ↑x = ∏' (x : β), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Set β<VAR>hs : Function.support f ⊆ s<GOAL>∑' (x : ↑s), f ↑x = ∑' (x : β), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<GOAL>∑' (x : ↑(Function.support f)), f ↑x = ∑' (x : β), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<GOAL>∏' (x : ↑(Function.mulSupport f)), f ↑x = ∏' (x : β), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>s : Set β<VAR>f : β → α<GOAL>∑' (x : ↑s), f ↑x = ∑' (x : β), s.indicator f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>s : Set β<VAR>f : β → α<GOAL>∏' (x : ↑s), f ↑x = ∏' (x : β), s.mulIndicator f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<GOAL>∑' (x : ↑Set.univ), f ↑x = ∑' (x : β), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<GOAL>∏' (x : ↑Set.univ), f ↑x = ∏' (x : β), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>g : γ → β<VAR>f : β → α<VAR>s : Set γ<VAR>hg : Set.InjOn g s<GOAL>∑' (x : ↑(g '' s)), f ↑x = ∑' (x : ↑s), f (g ↑x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>g : γ → β<VAR>f : β → α<VAR>s : Set γ<VAR>hg : Set.InjOn g s<GOAL>∏' (x : ↑(g '' s)), f ↑x = ∏' (x : ↑s), f (g ↑x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>g : γ → β<VAR>f : β → α<VAR>hg : Function.Injective g<GOAL>∑' (x : ↑(Set.range g)), f ↑x = ∑' (x : γ), f (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>g : γ → β<VAR>f : β → α<VAR>hg : Function.Injective g<GOAL>∏' (x : ↑(Set.range g)), f ↑x = ∏' (x : γ), f (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s t : Set β<VAR>hf₀ : ∀ b ∈ t, f b = 1<GOAL>∏' (a : ↑s), f ↑a = ∏' (a : ↑(s \ t)), f ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s t : Set β<VAR>hf₀ : ∀ b ∈ t, f b = 0<GOAL>∑' (a : ↑s), f ↑a = ∑' (a : ↑(s \ t)), f ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Set β<VAR>b : β<VAR>hf₀ : f b = 0<GOAL>∑' (a : ↑s), f ↑a = ∑' (a : ↑(s \ {b})), f ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>s : Set β<VAR>b : β<VAR>hf₀ : f b = 1<GOAL>∏' (a : ↑s), f ↑a = ∏' (a : ↑(s \ {b})), f ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>g : γ → α<VAR>i : ↑(Function.support g) → β<VAR>hi : Function.Injective i<VAR>hf : Function.support f ⊆ Set.range i<VAR>hfg : ∀ (x : ↑(Function.support g)), f (i x) = g ↑x<GOAL>∑' (x : β), f x = ∑' (y : γ), g y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>g : γ → α<VAR>i : ↑(Function.mulSupport g) → β<VAR>hi : Function.Injective i<VAR>hf : Function.mulSupport f ⊆ Set.range i<VAR>hfg : ∀ (x : ↑(Function.mulSupport g)), f (i x) = g ↑x<GOAL>∏' (x : β), f x = ∏' (y : γ), g y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>g : γ → α<VAR>e : ↑(Function.mulSupport f) ≃ ↑(Function.mulSupport g)<VAR>he : ∀ (x : ↑(Function.mulSupport f)), g ↑(e x) = f ↑x<GOAL>∏' (x : β), f x = ∏' (y : γ), g y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f : β → α<VAR>g : γ → α<VAR>e : ↑(Function.support f) ≃ ↑(Function.support g)<VAR>he : ∀ (x : ↑(Function.support f)), g ↑(e x) = f ↑x<GOAL>∑' (x : β), f x = ∑' (y : γ), g y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>P : Prop<VAR>Decidable P<VAR>x : β → ¬P → α<GOAL>(∏' (b : β), if h : P then 1 else x b h) = if h : P then 1 else ∏' (b : β), x b h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>P : Prop<VAR>Decidable P<VAR>x : β → ¬P → α<GOAL>(∑' (b : β), if h : P then 0 else x b h) = if h : P then 0 else ∑' (b : β), x b h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>P : Prop<VAR>Decidable P<VAR>x : β → P → α<GOAL>(∑' (b : β), if h : P then x b h else 0) = if h : P then ∑' (b : β), x b h else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>P : Prop<VAR>Decidable P<VAR>x : β → P → α<GOAL>(∏' (b : β), if h : P then x b h else 1) = if h : P then ∏' (b : β), x b h else 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>γ : Type u_5<VAR>g : γ → β<VAR>hg : Function.Injective g<VAR>f : γ → α<GOAL>∑' (y : β), Function.extend g f 0 y = ∑' (x : γ), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>γ : Type u_5<VAR>g : γ → β<VAR>hg : Function.Injective g<VAR>f : γ → α<GOAL>∏' (y : β), Function.extend g f 1 y = ∏' (x : γ), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>T2Space α<VAR>α' : Type u_5<VAR>CommMonoid α'<VAR>TopologicalSpace α'<VAR>e : α' → α<VAR>hes : Function.Surjective e<VAR>h1 : e 1 = 1<VAR>f : β → α<VAR>g : γ → α'<VAR>h : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a<GOAL>∏' (b : β), f b = e (∏' (c : γ), g c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>T2Space α<VAR>α' : Type u_5<VAR>AddCommMonoid α'<VAR>TopologicalSpace α'<VAR>e : α' → α<VAR>hes : Function.Surjective e<VAR>h1 : e 0 = 0<VAR>f : β → α<VAR>g : γ → α'<VAR>h : ∀ {a : α'}, HasSum f (e a) ↔ HasSum g a<GOAL>∑' (b : β), f b = e (∑' (c : γ), g c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>T2Space α<VAR>f : β → α<VAR>g : γ → α<VAR>h : ∀ {a : α}, HasProd f a ↔ HasProd g a<GOAL>∏' (b : β), f b = ∏' (c : γ), g c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>T2Space α<VAR>f : β → α<VAR>g : γ → α<VAR>h : ∀ {a : α}, HasSum f a ↔ HasSum g a<GOAL>∑' (b : β), f b = ∑' (c : γ), g c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>f g : β → α<VAR>T2Space α<VAR>ContinuousMul α<VAR>hf : Multipliable f<VAR>hg : Multipliable g<GOAL>∏' (b : β), f b * g b = (∏' (b : β), f b) * ∏' (b : β), g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>f g : β → α<VAR>T2Space α<VAR>ContinuousAdd α<VAR>hf : Summable f<VAR>hg : Summable g<GOAL>∑' (b : β), (f b + g b) = ∑' (b : β), f b + ∑' (b : β), g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>TopologicalSpace α<VAR>T2Space α<VAR>ContinuousMul α<VAR>f : γ → β → α<VAR>s : Finset γ<VAR>hf : ∀ i ∈ s, Multipliable (f i)<GOAL>∏' (b : β), ∏ i ∈ s, f i b = ∏ i ∈ s, ∏' (b : β), f i b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>T2Space α<VAR>ContinuousAdd α<VAR>f : γ → β → α<VAR>s : Finset γ<VAR>hf : ∀ i ∈ s, Summable (f i)<GOAL>∑' (b : β), ∑ i ∈ s, f i b = ∑ i ∈ s, ∑' (b : β), f i b