ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>φ : (i : ι) → β i →+ γ<VAR>f : Π₀ (i : ι), β i<GOAL>(DFinsupp.sumAddHom φ) f = f.sum fun x => ⇑(φ x)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>AddCommMonoid γ<VAR>S : Type u_1<VAR>SetLike S γ<VAR>AddSubmonoidClass S γ<VAR>s : S<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i →+ γ<VAR>h : ∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ s<GOAL>(DFinsupp.sumAddHom g) f ∈ s
<VAR>ι : Type u<VAR>γ : Type w<VAR>DecidableEq ι<VAR>AddCommMonoid γ<VAR>S : ι → AddSubmonoid γ<GOAL>iSup S = AddMonoidHom.mrange (DFinsupp.sumAddHom fun i => (S i).subtype)
<VAR>ι : Type u<VAR>γ : Type w<VAR>DecidableEq ι<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>AddCommMonoid γ<VAR>S : ι → AddSubmonoid γ<GOAL>⨆ i, ⨆ (_ : p i), S i = AddMonoidHom.mrange ((DFinsupp.sumAddHom fun i => (S i).subtype).comp (DFinsupp.filterAddMonoidHom (fun i => ↥(S i)) p))
<VAR>ι : Type u<VAR>γ : Type w<VAR>DecidableEq ι<VAR>AddCommMonoid γ<VAR>S : ι → AddSubmonoid γ<VAR>x : γ<GOAL>x ∈ iSup S ↔ ∃ f, (DFinsupp.sumAddHom fun i => (S i).subtype) f = x
<VAR>ι : Type u<VAR>γ : Type w<VAR>DecidableEq ι<VAR>AddCommMonoid γ<VAR>S : ι → AddSubmonoid γ<VAR>(i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)<VAR>x : γ<GOAL>x ∈ iSup S ↔ ∃ f, (f.sum fun i xi => ↑xi) = x
<VAR>ι : Type u<VAR>γ : Type w<VAR>DecidableEq ι<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>AddCommMonoid γ<VAR>S : ι → AddSubmonoid γ<VAR>x : γ<GOAL>x ∈ ⨆ i, ⨆ (_ : p i), S i ↔ ∃ f, (DFinsupp.sumAddHom fun i => (S i).subtype) (DFinsupp.filter p f) = x
<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>β₁ : ι₁ → Type u_1<VAR>β₂ : ι₂ → Type u_2<VAR>γ : Type u_3<VAR>DecidableEq ι₁<VAR>DecidableEq ι₂<VAR>(i : ι₁) → AddZeroClass (β₁ i)<VAR>(i : ι₂) → AddZeroClass (β₂ i)<VAR>AddCommMonoid γ<VAR>f₁ : Π₀ (i : ι₁), β₁ i<VAR>f₂ : Π₀ (i : ι₂), β₂ i<VAR>h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ<GOAL>(DFinsupp.sumAddHom fun i₂ => (DFinsupp.sumAddHom fun i₁ => h i₁ i₂) f₁) f₂ = (DFinsupp.sumAddHom fun i₁ => (DFinsupp.sumAddHom fun i₂ => (h i₁ i₂).flip) f₂) f₁
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>AddCommMonoid γ<VAR>φ : (i : ι) → β i →+ γ<GOAL>DFinsupp.liftAddHom φ = DFinsupp.sumAddHom φ
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>AddCommMonoid γ<VAR>F : (Π₀ (i : ι), β i) →+ γ<VAR>i : ι<GOAL>DFinsupp.liftAddHom.symm F i = F.comp (DFinsupp.singleAddHom β i)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddCommMonoid (β i)<GOAL>DFinsupp.liftAddHom (DFinsupp.singleAddHom β) = AddMonoidHom.id (Π₀ (i : ι), β i)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>AddCommMonoid γ<VAR>f : (i : ι) → β i →+ γ<VAR>i : ι<VAR>x : β i<GOAL>(DFinsupp.liftAddHom f) (DFinsupp.single i x) = (f i) x
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>AddCommMonoid γ<VAR>f : (i : ι) → β i →+ γ<VAR>i : ι<GOAL>(DFinsupp.liftAddHom f).comp (DFinsupp.singleAddHom β i) = f i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>δ : Type u_1<VAR>(i : ι) → AddZeroClass (β i)<VAR>AddCommMonoid γ<VAR>AddCommMonoid δ<VAR>g : γ →+ δ<VAR>f : (i : ι) → β i →+ γ<GOAL>g.comp (DFinsupp.liftAddHom f) = DFinsupp.liftAddHom fun a => g.comp (f a)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>AddCommMonoid γ<GOAL>(DFinsupp.sumAddHom fun i => 0) = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (β i)<VAR>AddCommMonoid γ<VAR>g h : (i : ι) → β i →+ γ<GOAL>(DFinsupp.sumAddHom fun i => g i + h i) = DFinsupp.sumAddHom g + DFinsupp.sumAddHom h
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddCommMonoid (β i)<GOAL>DFinsupp.sumAddHom (DFinsupp.singleAddHom β) = AddMonoidHom.id (Π₀ (i : ι), β i)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>δ : Type u_1<VAR>(i : ι) → AddZeroClass (β i)<VAR>AddCommMonoid γ<VAR>AddCommMonoid δ<VAR>g : γ →+ δ<VAR>f : (i : ι) → β i →+ γ<GOAL>g.comp (DFinsupp.sumAddHom f) = DFinsupp.sumAddHom fun a => g.comp (f a)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddGroup (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommGroup γ<VAR>f g : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂<GOAL>(f - g).sum h = f.sum h - g.sum h
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>γ : Type w<VAR>α : Type x<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>s : Finset α<VAR>g : α → Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_zero : ∀ (i : ι), h i 0 = 0<VAR>h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂<GOAL>∑ i ∈ s, (g i).sum h = (∑ i ∈ s, g i).sum h
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>γ : Type w<VAR>α : Type x<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>CommMonoid γ<VAR>s : Finset α<VAR>g : α → Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_zero : ∀ (i : ι), h i 0 = 1<VAR>h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂<GOAL>∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>ι₁ : Type u₁<VAR>DecidableEq ι₁<VAR>β₁ : ι₁ → Type v₁<VAR>(i₁ : ι₁) → Zero (β₁ i₁)<VAR>(i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>f : Π₀ (i₁ : ι₁), β₁ i₁<VAR>g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_zero : ∀ (i : ι), h i 0 = 0<VAR>h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂<GOAL>(f.sum g).sum h = f.sum fun i b => (g i b).sum h
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>ι₁ : Type u₁<VAR>DecidableEq ι₁<VAR>β₁ : ι₁ → Type v₁<VAR>(i₁ : ι₁) → Zero (β₁ i₁)<VAR>(i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>CommMonoid γ<VAR>f : Π₀ (i₁ : ι₁), β₁ i₁<VAR>g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_zero : ∀ (i : ι), h i 0 = 1<VAR>h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂<GOAL>(f.sum g).prod h = f.prod fun i b => (g i b).prod h
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<GOAL>f.sum DFinsupp.single = f
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>CommMonoid γ<VAR>v : Π₀ (i : ι), β i<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>h : (i : ι) → β i → γ<VAR>hp : ∀ x ∈ v.support, p x<GOAL>((DFinsupp.subtypeDomain p v).prod fun i b => h (↑i) b) = v.prod h
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddCommMonoid γ<VAR>v : Π₀ (i : ι), β i<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>h : (i : ι) → β i → γ<VAR>hp : ∀ x ∈ v.support, p x<GOAL>((DFinsupp.subtypeDomain p v).sum fun i b => h (↑i) b) = v.sum h
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>(i : ι) → AddCommMonoid (β i)<VAR>s : Finset γ<VAR>h : γ → Π₀ (i : ι), β i<VAR>p : ι → Prop<VAR>DecidablePred p<GOAL>DFinsupp.subtypeDomain p (∑ c ∈ s, h c) = ∑ c ∈ s, DFinsupp.subtypeDomain p (h c)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>δ : γ → Type x<VAR>DecidableEq γ<VAR>(c : γ) → Zero (δ c)<VAR>(c : γ) → (x : δ c) → Decidable (x ≠ 0)<VAR>(i : ι) → AddCommMonoid (β i)<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>s : Π₀ (c : γ), δ c<VAR>h : (c : γ) → δ c → Π₀ (i : ι), β i<GOAL>DFinsupp.subtypeDomain p (s.sum h) = s.sum fun c d => DFinsupp.subtypeDomain p (h c d)
<VAR>ι : Type u<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>(i : ι) → AddZeroClass (β₁ i)<VAR>(i : ι) → AddZeroClass (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y<VAR>g₁ g₂ : Π₀ (i : ι), β₁ i<GOAL>DFinsupp.mapRange f hf (g₁ + g₂) = DFinsupp.mapRange f hf g₁ + DFinsupp.mapRange f hf g₂
<VAR>ι : Type u<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>(i : ι) → AddZeroClass (β₁ i)<VAR>(i : ι) → AddZeroClass (β₂ i)<VAR>f : (i : ι) → β₁ i →+ β₂ i<VAR>x : Π₀ (i : ι), β₁ i<GOAL>(DFinsupp.mapRange.addMonoidHom f) x = DFinsupp.mapRange (fun i x => (f i) x) ⋯ x
<VAR>ι : Type u<VAR>β₂ : ι → Type v₂<VAR>(i : ι) → AddZeroClass (β₂ i)<GOAL>(DFinsupp.mapRange.addMonoidHom fun i => AddMonoidHom.id (β₂ i)) = AddMonoidHom.id (Π₀ (i : ι), β₂ i)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>(i : ι) → AddZeroClass (β i)<VAR>(i : ι) → AddZeroClass (β₁ i)<VAR>(i : ι) → AddZeroClass (β₂ i)<VAR>f : (i : ι) → β₁ i →+ β₂ i<VAR>f₂ : (i : ι) → β i →+ β₁ i<GOAL>(DFinsupp.mapRange.addMonoidHom fun i => (f i).comp (f₂ i)) = (DFinsupp.mapRange.addMonoidHom f).comp (DFinsupp.mapRange.addMonoidHom f₂)
<VAR>ι : Type u<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>(i : ι) → AddZeroClass (β₁ i)<VAR>(i : ι) → AddZeroClass (β₂ i)<VAR>e : (i : ι) → β₁ i ≃+ β₂ i<VAR>x : Π₀ (i : ι), β₁ i<GOAL>(DFinsupp.mapRange.addEquiv e) x = DFinsupp.mapRange (fun i x => (e i) x) ⋯ x
<VAR>ι : Type u<VAR>β₁ : ι → Type v₁<VAR>(i : ι) → AddZeroClass (β₁ i)<GOAL>(DFinsupp.mapRange.addEquiv fun i => AddEquiv.refl (β₁ i)) = AddEquiv.refl (Π₀ (i : ι), β₁ i)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>(i : ι) → AddZeroClass (β i)<VAR>(i : ι) → AddZeroClass (β₁ i)<VAR>(i : ι) → AddZeroClass (β₂ i)<VAR>f : (i : ι) → β i ≃+ β₁ i<VAR>f₂ : (i : ι) → β₁ i ≃+ β₂ i<GOAL>(DFinsupp.mapRange.addEquiv fun i => (f i).trans (f₂ i)) = (DFinsupp.mapRange.addEquiv f).trans (DFinsupp.mapRange.addEquiv f₂)
<VAR>ι : Type u<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>(i : ι) → AddZeroClass (β₁ i)<VAR>(i : ι) → AddZeroClass (β₂ i)<VAR>e : (i : ι) → β₁ i ≃+ β₂ i<GOAL>(DFinsupp.mapRange.addEquiv e).symm = DFinsupp.mapRange.addEquiv fun i => (e i).symm
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>R : Type u_1<VAR>S : Type u_2<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddMonoid R<VAR>AddCommMonoid S<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i → R →+ S<GOAL>⇑(f.sum g) = f.sum fun a b => ⇑(g a b)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>R : Type u_1<VAR>S : Type u_2<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>Monoid R<VAR>CommMonoid S<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i → R →* S<GOAL>⇑(f.prod g) = f.prod fun a b => ⇑(g a b)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>R : Type u_1<VAR>S : Type u_2<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>AddMonoid R<VAR>AddCommMonoid S<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i → R →+ S<VAR>r : R<GOAL>(f.sum g) r = f.sum fun a b => (g a b) r
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>R : Type u_1<VAR>S : Type u_2<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>Monoid R<VAR>CommMonoid S<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i → R →* S<VAR>r : R<GOAL>(f.prod g) r = f.prod fun a b => (g a b) r
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>R : Type u_1<VAR>S : Type u_2<VAR>AddCommMonoid R<VAR>AddCommMonoid S<VAR>(i : ι) → AddZeroClass (β i)<VAR>h : R →+ S<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i →+ R<GOAL>h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun i => h.comp (g i)) f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>R : Type u_1<VAR>S : Type u_2<VAR>AddZeroClass R<VAR>AddCommMonoid S<VAR>(i : ι) → AddZeroClass (β i)<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i →+ R →+ S<VAR>r : R<GOAL>((DFinsupp.sumAddHom g) f) r = (DFinsupp.sumAddHom fun i => (AddMonoidHom.eval r).comp (g i)) f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>R : Type u_1<VAR>S : Type u_2<VAR>AddZeroClass R<VAR>AddCommMonoid S<VAR>(i : ι) → AddZeroClass (β i)<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i →+ R →+ S<GOAL>⇑((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun i => (AddMonoidHom.coeFn R S).comp (g i)) f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>R : Type u_1<VAR>S : Type u_2<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>(i : ι) → AddZeroClass (β i)<VAR>h : R →+* S<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i →+ R<GOAL>h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun i => h.toAddMonoidHom.comp (g i)) f
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>DecidableEq ι<VAR>R : Type u_1<VAR>S : Type u_2<VAR>AddCommMonoid R<VAR>AddCommMonoid S<VAR>(i : ι) → AddZeroClass (β i)<VAR>h : R ≃+ S<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i →+ R<GOAL>h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun i => h.toAddMonoidHom.comp (g i)) f
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>i : ι<VAR>Infinite (π i)<VAR>(i : ι) → Zero (π i)<GOAL>Infinite (Π₀ (i : ι), π i)
<VAR>z : ℂ<GOAL>IsCauSeq abs fun n => ∑ m ∈ Finset.range n, Complex.abs (z ^ m / ↑m.factorial)
<VAR>z : ℂ<GOAL>IsCauSeq ⇑Complex.abs fun n => ∑ m ∈ Finset.range n, z ^ m / ↑m.factorial
<VAR>x y : ℂ<GOAL>Complex.exp (x + y) = Complex.exp x * Complex.exp y
<VAR>l : List ℂ<GOAL>Complex.exp l.sum = (List.map Complex.exp l).prod
<VAR>s : Multiset ℂ<GOAL>Complex.exp s.sum = (Multiset.map Complex.exp s).prod
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℂ<GOAL>Complex.exp (∑ x ∈ s, f x) = ∏ x ∈ s, Complex.exp (f x)
<VAR>x : ℂ<VAR>n : ℕ<GOAL>Complex.exp (n • x) = Complex.exp x ^ n
<VAR>x : ℂ<VAR>n : ℕ<GOAL>Complex.exp (↑n * x) = Complex.exp x ^ n
<VAR>x : ℂ<GOAL>Complex.exp x ≠ 0
<VAR>x : ℂ<GOAL>Complex.exp (-x) = (Complex.exp x)⁻¹
<VAR>x y : ℂ<GOAL>Complex.exp (x - y) = Complex.exp x / Complex.exp y
<VAR>z : ℂ<VAR>n : ℤ<GOAL>Complex.exp (↑n * z) = Complex.exp z ^ n
<VAR>x : ℂ<GOAL>Complex.exp ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.exp x)
<VAR>x : ℝ<GOAL>↑(Complex.exp ↑x).re = Complex.exp ↑x
<VAR>x : ℝ<GOAL>↑(Real.exp x) = Complex.exp ↑x
<VAR>x : ℝ<GOAL>(Complex.exp ↑x).im = 0
<VAR>x : ℝ<GOAL>(Complex.exp ↑x).re = Real.exp x
<VAR>x : ℂ<GOAL>2 * Complex.sinh x = Complex.exp x - Complex.exp (-x)
<VAR>x : ℂ<GOAL>2 * Complex.cosh x = Complex.exp x + Complex.exp (-x)
<VAR>x : ℂ<GOAL>Complex.sinh (-x) = -Complex.sinh x
<VAR>a b c d : ℂ<GOAL>(a - b) * (c + d) + (a + b) * (c - d) = 2 * (a * c - b * d)
<VAR>x y : ℂ<GOAL>Complex.sinh (x + y) = Complex.sinh x * Complex.cosh y + Complex.cosh x * Complex.sinh y
<VAR>x : ℂ<GOAL>Complex.cosh (-x) = Complex.cosh x
<VAR>a b c d : ℂ<GOAL>(a + b) * (c + d) + (a - b) * (c - d) = 2 * (a * c + b * d)
<VAR>x y : ℂ<GOAL>Complex.cosh (x + y) = Complex.cosh x * Complex.cosh y + Complex.sinh x * Complex.sinh y
<VAR>x y : ℂ<GOAL>Complex.sinh (x - y) = Complex.sinh x * Complex.cosh y - Complex.cosh x * Complex.sinh y
<VAR>x y : ℂ<GOAL>Complex.cosh (x - y) = Complex.cosh x * Complex.cosh y - Complex.sinh x * Complex.sinh y
<VAR>x : ℂ<GOAL>Complex.sinh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.sinh x)
<VAR>x : ℝ<GOAL>↑(Complex.sinh ↑x).re = Complex.sinh ↑x
<VAR>x : ℝ<GOAL>↑(Real.sinh x) = Complex.sinh ↑x
<VAR>x : ℝ<GOAL>(Complex.sinh ↑x).im = 0
<VAR>x : ℝ<GOAL>(Complex.sinh ↑x).re = Real.sinh x
<VAR>x : ℂ<GOAL>Complex.cosh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.cosh x)
<VAR>x : ℝ<GOAL>↑(Complex.cosh ↑x).re = Complex.cosh ↑x
<VAR>x : ℝ<GOAL>↑(Real.cosh x) = Complex.cosh ↑x
<VAR>x : ℝ<GOAL>(Complex.cosh ↑x).im = 0
<VAR>x : ℝ<GOAL>(Complex.cosh ↑x).re = Real.cosh x
<VAR>x : ℂ<GOAL>Complex.tanh x = Complex.sinh x / Complex.cosh x
<VAR>x : ℂ<GOAL>Complex.tanh (-x) = -Complex.tanh x
<VAR>x : ℂ<GOAL>Complex.tanh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.tanh x)
<VAR>x : ℝ<GOAL>↑(Complex.tanh ↑x).re = Complex.tanh ↑x
<VAR>x : ℝ<GOAL>↑(Real.tanh x) = Complex.tanh ↑x
<VAR>x : ℝ<GOAL>(Complex.tanh ↑x).im = 0
<VAR>x : ℝ<GOAL>(Complex.tanh ↑x).re = Real.tanh x
<VAR>x : ℂ<GOAL>Complex.cosh x + Complex.sinh x = Complex.exp x
<VAR>x : ℂ<GOAL>Complex.sinh x + Complex.cosh x = Complex.exp x
<VAR>x : ℂ<GOAL>Complex.exp x - Complex.cosh x = Complex.sinh x
<VAR>x : ℂ<GOAL>Complex.exp x - Complex.sinh x = Complex.cosh x
<VAR>x : ℂ<GOAL>Complex.cosh x - Complex.sinh x = Complex.exp (-x)
<VAR>x : ℂ<GOAL>Complex.sinh x - Complex.cosh x = -Complex.exp (-x)
<VAR>x : ℂ<GOAL>Complex.cosh x ^ 2 - Complex.sinh x ^ 2 = 1
<VAR>x : ℂ<GOAL>Complex.cosh x ^ 2 = Complex.sinh x ^ 2 + 1
<VAR>x : ℂ<GOAL>Complex.sinh x ^ 2 = Complex.cosh x ^ 2 - 1
<VAR>x : ℂ<GOAL>Complex.cosh (2 * x) = Complex.cosh x ^ 2 + Complex.sinh x ^ 2
<VAR>x : ℂ<GOAL>Complex.sinh (2 * x) = 2 * Complex.sinh x * Complex.cosh x
<VAR>x : ℂ<GOAL>Complex.cosh (3 * x) = 4 * Complex.cosh x ^ 3 - 3 * Complex.cosh x
<VAR>x : ℂ<GOAL>Complex.sinh (3 * x) = 4 * Complex.sinh x ^ 3 + 3 * Complex.sinh x
<VAR>x : ℂ<GOAL>Complex.sin (-x) = -Complex.sin x
<VAR>x : ℂ<GOAL>2 * Complex.sin x = (Complex.exp (-x * Complex.I) - Complex.exp (x * Complex.I)) * Complex.I
<VAR>x : ℂ<GOAL>2 * Complex.cos x = Complex.exp (x * Complex.I) + Complex.exp (-x * Complex.I)
<VAR>x : ℂ<GOAL>Complex.sinh (x * Complex.I) = Complex.sin x * Complex.I
<VAR>x : ℂ<GOAL>Complex.cosh (x * Complex.I) = Complex.cos x
<VAR>x : ℂ<GOAL>Complex.tanh (x * Complex.I) = Complex.tan x * Complex.I
<VAR>x : ℂ<GOAL>Complex.cos (x * Complex.I) = Complex.cosh x
<VAR>x : ℂ<GOAL>Complex.sin (x * Complex.I) = Complex.sinh x * Complex.I
<VAR>x : ℂ<GOAL>Complex.tan (x * Complex.I) = Complex.tanh x * Complex.I
<VAR>x y : ℂ<GOAL>Complex.sin (x + y) = Complex.sin x * Complex.cos y + Complex.cos x * Complex.sin y
<VAR>x : ℂ<GOAL>Complex.cos (-x) = Complex.cos x
<VAR>a b c d : ℂ<GOAL>(a + b) * (c + d) - (b - a) * (d - c) * -1 = 2 * (a * c + b * d)
<VAR>x y : ℂ<GOAL>Complex.cos (x + y) = Complex.cos x * Complex.cos y - Complex.sin x * Complex.sin y
<VAR>x y : ℂ<GOAL>Complex.sin (x - y) = Complex.sin x * Complex.cos y - Complex.cos x * Complex.sin y
<VAR>x y : ℂ<GOAL>Complex.cos (x - y) = Complex.cos x * Complex.cos y + Complex.sin x * Complex.sin y
<VAR>x y : ℂ<GOAL>Complex.sin (x + y * Complex.I) = Complex.sin x * Complex.cosh y + Complex.cos x * Complex.sinh y * Complex.I
<VAR>z : ℂ<GOAL>Complex.sin z = Complex.sin ↑z.re * Complex.cosh ↑z.im + Complex.cos ↑z.re * Complex.sinh ↑z.im * Complex.I
<VAR>x y : ℂ<GOAL>Complex.cos (x + y * Complex.I) = Complex.cos x * Complex.cosh y - Complex.sin x * Complex.sinh y * Complex.I
<VAR>z : ℂ<GOAL>Complex.cos z = Complex.cos ↑z.re * Complex.cosh ↑z.im - Complex.sin ↑z.re * Complex.sinh ↑z.im * Complex.I
<VAR>x y : ℂ<GOAL>Complex.sin x - Complex.sin y = 2 * Complex.sin ((x - y) / 2) * Complex.cos ((x + y) / 2)
<VAR>x y : ℂ<GOAL>Complex.cos x - Complex.cos y = -2 * Complex.sin ((x + y) / 2) * Complex.sin ((x - y) / 2)
<VAR>x y : ℂ<GOAL>Complex.sin x + Complex.sin y = 2 * Complex.sin ((x + y) / 2) * Complex.cos ((x - y) / 2)
<VAR>x y : ℂ<GOAL>Complex.cos x + Complex.cos y = 2 * Complex.cos ((x + y) / 2) * Complex.cos ((x - y) / 2)
<VAR>x : ℂ<GOAL>Complex.sin ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.sin x)
<VAR>x : ℝ<GOAL>↑(Complex.sin ↑x).re = Complex.sin ↑x
<VAR>x : ℝ<GOAL>↑(Real.sin x) = Complex.sin ↑x
<VAR>x : ℝ<GOAL>(Complex.sin ↑x).im = 0
<VAR>x : ℝ<GOAL>(Complex.sin ↑x).re = Real.sin x
<VAR>x : ℂ<GOAL>Complex.cos ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.cos x)
<VAR>x : ℝ<GOAL>↑(Complex.cos ↑x).re = Complex.cos ↑x
<VAR>x : ℝ<GOAL>↑(Real.cos x) = Complex.cos ↑x
<VAR>x : ℝ<GOAL>(Complex.cos ↑x).im = 0
<VAR>x : ℝ<GOAL>(Complex.cos ↑x).re = Real.cos x
<VAR>x : ℂ<GOAL>Complex.tan x = Complex.sin x / Complex.cos x
<VAR>x : ℂ<GOAL>x.cot = Complex.cos x / Complex.sin x
<VAR>x : ℂ<VAR>hx : Complex.cos x ≠ 0<GOAL>Complex.tan x * Complex.cos x = Complex.sin x
<VAR>x : ℂ<GOAL>Complex.tan (-x) = -Complex.tan x
<VAR>x : ℂ<GOAL>Complex.tan ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.tan x)
<VAR>x : ℂ<GOAL>((starRingEnd ℂ) x).cot = (starRingEnd ℂ) x.cot
<VAR>x : ℝ<GOAL>↑(Complex.tan ↑x).re = Complex.tan ↑x
<VAR>x : ℝ<GOAL>↑(↑x).cot.re = (↑x).cot
<VAR>x : ℝ<GOAL>↑(Real.tan x) = Complex.tan ↑x
<VAR>x : ℝ<GOAL>↑x.cot = (↑x).cot
<VAR>x : ℝ<GOAL>(Complex.tan ↑x).im = 0
<VAR>x : ℝ<GOAL>(Complex.tan ↑x).re = Real.tan x
<VAR>x : ℂ<GOAL>Complex.cos x + Complex.sin x * Complex.I = Complex.exp (x * Complex.I)
<VAR>x : ℂ<GOAL>Complex.cos x - Complex.sin x * Complex.I = Complex.exp (-x * Complex.I)
<VAR>x : ℂ<GOAL>Complex.sin x ^ 2 + Complex.cos x ^ 2 = 1
<VAR>x : ℂ<GOAL>Complex.cos x ^ 2 + Complex.sin x ^ 2 = 1
<VAR>x : ℂ<GOAL>Complex.cos (2 * x) = Complex.cos x ^ 2 - Complex.sin x ^ 2
<VAR>x : ℂ<GOAL>Complex.cos (2 * x) = 2 * Complex.cos x ^ 2 - 1
<VAR>x : ℂ<GOAL>Complex.sin (2 * x) = 2 * Complex.sin x * Complex.cos x
<VAR>x : ℂ<GOAL>Complex.cos x ^ 2 = 1 / 2 + Complex.cos (2 * x) / 2
<VAR>x : ℂ<GOAL>Complex.cos x ^ 2 = 1 - Complex.sin x ^ 2
<VAR>x : ℂ<GOAL>Complex.sin x ^ 2 = 1 - Complex.cos x ^ 2
<VAR>x : ℂ<VAR>hx : Complex.cos x ≠ 0<GOAL>(1 + Complex.tan x ^ 2)⁻¹ = Complex.cos x ^ 2
<VAR>x : ℂ<VAR>hx : Complex.cos x ≠ 0<GOAL>Complex.tan x ^ 2 / (1 + Complex.tan x ^ 2) = Complex.sin x ^ 2
<VAR>x : ℂ<GOAL>Complex.cos (3 * x) = 4 * Complex.cos x ^ 3 - 3 * Complex.cos x
<VAR>x : ℂ<GOAL>Complex.sin (3 * x) = 3 * Complex.sin x - 4 * Complex.sin x ^ 3
<VAR>x : ℂ<GOAL>Complex.exp (x * Complex.I) = Complex.cos x + Complex.sin x * Complex.I
<VAR>x y : ℂ<GOAL>Complex.exp (x + y * Complex.I) = Complex.exp x * (Complex.cos y + Complex.sin y * Complex.I)
<VAR>x : ℂ<GOAL>Complex.exp x = Complex.exp ↑x.re * (Complex.cos ↑x.im + Complex.sin ↑x.im * Complex.I)
<VAR>x : ℂ<GOAL>(Complex.exp x).re = Real.exp x.re * Real.cos x.im
<VAR>x : ℂ<GOAL>(Complex.exp x).im = Real.exp x.re * Real.sin x.im
<VAR>x : ℝ<GOAL>(Complex.exp (↑x * Complex.I)).re = Real.cos x
<VAR>x : ℝ<GOAL>(Complex.exp (↑x * Complex.I)).im = Real.sin x
<VAR>n : ℕ<VAR>z : ℂ<GOAL>(Complex.cos z + Complex.sin z * Complex.I) ^ n = Complex.cos (↑n * z) + Complex.sin (↑n * z) * Complex.I
<VAR>x y : ℝ<GOAL>Real.exp (x + y) = Real.exp x * Real.exp y
<VAR>l : List ℝ<GOAL>Real.exp l.sum = (List.map Real.exp l).prod
<VAR>s : Multiset ℝ<GOAL>Real.exp s.sum = (Multiset.map Real.exp s).prod
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<GOAL>Real.exp (∑ x ∈ s, f x) = ∏ x ∈ s, Real.exp (f x)
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.exp (n • x) = Real.exp x ^ n
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.exp (↑n * x) = Real.exp x ^ n
<VAR>x : ℝ<GOAL>Real.exp x ≠ 0
<VAR>x : ℝ<GOAL>Real.exp (-x) = (Real.exp x)⁻¹
<VAR>x y : ℝ<GOAL>Real.exp (x - y) = Real.exp x / Real.exp y
<VAR>x : ℝ<GOAL>Real.sin (-x) = -Real.sin x
<VAR>x y : ℝ<GOAL>Real.sin (x + y) = Real.sin x * Real.cos y + Real.cos x * Real.sin y
<VAR>x : ℝ<GOAL>Real.cos (-x) = Real.cos x
<VAR>x : ℝ<GOAL>Real.cos |x| = Real.cos x
<VAR>x y : ℝ<GOAL>Real.cos (x + y) = Real.cos x * Real.cos y - Real.sin x * Real.sin y
<VAR>x y : ℝ<GOAL>Real.sin (x - y) = Real.sin x * Real.cos y - Real.cos x * Real.sin y
<VAR>x y : ℝ<GOAL>Real.cos (x - y) = Real.cos x * Real.cos y + Real.sin x * Real.sin y
<VAR>x y : ℝ<GOAL>Real.sin x - Real.sin y = 2 * Real.sin ((x - y) / 2) * Real.cos ((x + y) / 2)
<VAR>x y : ℝ<GOAL>Real.cos x - Real.cos y = -2 * Real.sin ((x + y) / 2) * Real.sin ((x - y) / 2)
<VAR>x y : ℝ<GOAL>Real.cos x + Real.cos y = 2 * Real.cos ((x + y) / 2) * Real.cos ((x - y) / 2)
<VAR>x : ℝ<GOAL>Real.tan x = Real.sin x / Real.cos x
<VAR>x : ℝ<GOAL>x.cot = Real.cos x / Real.sin x
<VAR>x : ℝ<VAR>hx : Real.cos x ≠ 0<GOAL>Real.tan x * Real.cos x = Real.sin x
<VAR>x : ℝ<GOAL>Real.tan (-x) = -Real.tan x
<VAR>x : ℝ<GOAL>Real.sin x ^ 2 + Real.cos x ^ 2 = 1
<VAR>x : ℝ<GOAL>Real.cos x ^ 2 + Real.sin x ^ 2 = 1
<VAR>x : ℝ<GOAL>Real.sin x ^ 2 ≤ 1
<VAR>x : ℝ<GOAL>Real.cos x ^ 2 ≤ 1
<VAR>x : ℝ<GOAL>|Real.sin x| ≤ 1
<VAR>x : ℝ<GOAL>|Real.cos x| ≤ 1
<VAR>x : ℝ<GOAL>Real.sin x ≤ 1
<VAR>x : ℝ<GOAL>Real.cos x ≤ 1
<VAR>x : ℝ<GOAL>-1 ≤ Real.sin x
<VAR>x : ℝ<GOAL>-1 ≤ Real.cos x
<VAR>x : ℝ<GOAL>Real.cos (2 * x) = 2 * Real.cos x ^ 2 - 1
<VAR>x : ℝ<GOAL>Real.cos (2 * x) = Real.cos x ^ 2 - Real.sin x ^ 2
<VAR>x : ℝ<GOAL>Real.sin (2 * x) = 2 * Real.sin x * Real.cos x
<VAR>x : ℝ<GOAL>Real.cos x ^ 2 = 1 / 2 + Real.cos (2 * x) / 2
<VAR>x : ℝ<GOAL>Real.cos x ^ 2 = 1 - Real.sin x ^ 2