ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<GOAL>∀ (i₁ i₂ : Finset σ), i₁ ≠ i₂ → Disjoint (Finsupp.single (∑ i ∈ i₁, Finsupp.single i 1) 1).support (Finsupp.single (∑ i ∈ i₂, Finsupp.single i 1) 1).support
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<VAR>s t : Finset σ<VAR>hst : s ≠ t<GOAL>Disjoint (Finsupp.single (∑ i ∈ s, Finsupp.single i 1) 1).support (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<VAR>s t : Finset σ<VAR>hst : s ≠ t<GOAL>∀ ⦃a : σ →₀ ℕ⦄, a ∈ {∑ i ∈ s, Finsupp.single i 1} → a ∉ (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<VAR>s t : Finset σ<VAR>hst : s ≠ t<GOAL>∀ ⦃a : σ →₀ ℕ⦄, a ∈ {∑ i ∈ s, Finsupp.single i 1} → a ∉ {∑ i ∈ t, Finsupp.single i 1}
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<VAR>s t : Finset σ<VAR>hst : s ≠ t<GOAL>∀ ⦃a : σ →₀ ℕ⦄, a = ∑ i ∈ s, Finsupp.single i 1 → ¬a = ∑ i ∈ t, Finsupp.single i 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<VAR>s t : Finset σ<VAR>hst : s ≠ t<VAR>h : ∑ i ∈ t, Finsupp.single i 1 = ∑ i ∈ s, Finsupp.single i 1<VAR>this : (∑ i ∈ t, Finsupp.single i 1).support = (∑ i ∈ s, Finsupp.single i 1).support<GOAL>False
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<VAR>s t : Finset σ<VAR>hst : s ≠ t<VAR>h : ∑ i ∈ t, Finsupp.single i 1 = ∑ i ∈ s, Finsupp.single i 1<VAR>this : (t.biUnion fun i => (Finsupp.single i 1).support) = s.biUnion fun i => (Finsupp.single i 1).support<GOAL>False
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<VAR>s t : Finset σ<VAR>hst : s ≠ t<VAR>h : ∑ i ∈ t, Finsupp.single i 1 = ∑ i ∈ s, Finsupp.single i 1<VAR>this : (t.biUnion fun i => (Finsupp.single i 1).support) = (∑ i ∈ s, Finsupp.single i 1).support<GOAL>∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<VAR>s t : Finset σ<VAR>hst : s ≠ t<VAR>h : ∑ i ∈ t, Finsupp.single i 1 = ∑ i ∈ s, Finsupp.single i 1<VAR>this : (∑ i ∈ t, Finsupp.single i 1).support = (∑ i ∈ s, Finsupp.single i 1).support<GOAL>∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<GOAL>mgf X μ 0 = (μ Set.univ).toReal
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cocone F<VAR>X : C<VAR>h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones<VAR>s : Cocone F<VAR>s_pt : C<VAR>s_ι : F ⟶ (const J).obj s_pt<GOAL>h.hom.app s_pt { down := (h.inv.app s_pt s_ι).down } = s_ι
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<GOAL>TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), edist (f x) (F n x) < ε
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>P : ι → Ideal R<VAR>e : ι → ℕ<VAR>prime : ∀ i ∈ s, Prime (P i)<VAR>coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j<VAR>x : { x // x ∈ s } → R<GOAL>∃ y, ∀ (i : ι) (hi : i ∈ s), y - x ⟨i, hi⟩ ∈ P i ^ e i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>P : ι → Ideal R<VAR>e : ι → ℕ<VAR>prime : ∀ i ∈ s, Prime (P i)<VAR>coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j<VAR>x : { x // x ∈ s } → R<VAR>y : R<VAR>hy : ∀ (i : ι) (hi : i ∈ s), (Ideal.Quotient.mk (P i ^ e i)) y = (Ideal.Quotient.mk (P ↑⟨i, hi⟩ ^ e ↑⟨i, hi⟩)) (x ⟨i, hi⟩)<GOAL>∃ y, ∀ (i : ι) (hi : i ∈ s), y - x ⟨i, hi⟩ ∈ P i ^ e i
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u}<VAR>b : Ordinal.{max u v}<VAR>h : b ≤ lift.{v, u} a<GOAL>b.card ≤ Cardinal.lift.{v, u} a.card
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u}<VAR>b : Ordinal.{max u v}<VAR>h : b ≤ lift.{v, u} a<GOAL>b.card ≤ (lift.{v, u} a).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Set α<VAR>inst✝¹ : Fintype ↑s<VAR>inst✝ : Fintype ↑t<GOAL>s.toFinset ⊆ t.toFinset ↔ s ⊆ t
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o : Ordinal.{u}<VAR>hl : ∀ i ∈ ↑l, ord I i < o<VAR>f : LocallyConstant ↑C ℤ<GOAL>f ∈ eval C '' {m | m < l} ↔ f ∈ ⇑(πs C o) '' (eval (π C fun x => ord I x < o) '' {m | m < l})
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o : Ordinal.{u}<VAR>hl : ∀ i ∈ ↑l, ord I i < o<VAR>f : LocallyConstant ↑C ℤ<GOAL>(∃ x < l, eval C x = f) ↔ ∃ a < l, (πs C o) (eval (π C fun x => ord I x < o) a) = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o : Ordinal.{u}<VAR>hl : ∀ i ∈ ↑l, ord I i < o<VAR>f : LocallyConstant ↑C ℤ<GOAL>∀ (a : Products I), a < l ∧ eval C a = f ↔ a < l ∧ (πs C o) (eval (π C fun x => ord I x < o) a) = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o : Ordinal.{u}<VAR>hl : ∀ i ∈ ↑l, ord I i < o<VAR>f : LocallyConstant ↑C ℤ<VAR>m : Products I<GOAL>m < l ∧ eval C m = f ↔ m < l ∧ (πs C o) (eval (π C fun x => ord I x < o) m) = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o : Ordinal.{u}<VAR>hl : ∀ i ∈ ↑l, ord I i < o<VAR>f : LocallyConstant ↑C ℤ<VAR>m : Products I<GOAL>m < l → (eval C m = f ↔ (πs C o) (eval (π C fun x => ord I x < o) m) = f)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o : Ordinal.{u}<VAR>hl : ∀ i ∈ ↑l, ord I i < o<VAR>f : LocallyConstant ↑C ℤ<VAR>m : Products I<VAR>hm : m < l<GOAL>eval C m = f ↔ (πs C o) (eval (π C fun x => ord I x < o) m) = f
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>(Ioo a b).card = ↑b - ↑a - 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<GOAL>Tendsto (seminormFromConst_seq c f c) atTop (𝓝 (f c))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>hseq : seminormFromConst_seq c f c = fun _n => f c<GOAL>Tendsto (seminormFromConst_seq c f c) atTop (𝓝 (f c))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>hseq : seminormFromConst_seq c f c = fun _n => f c<GOAL>Tendsto (fun _n => f c) atTop (𝓝 (f c))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hIX : M.Basis I X<VAR>hJX : M.Basis J X<VAR>he : e ∈ I \ J<GOAL>∃ f ∈ J \ I, M.Basis (insert f (I \ {e})) X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hIX : M.Basis I X<VAR>hJX : M.Basis J X<VAR>he : e ∈ I \ J<VAR>y : α<VAR>hy : y ∈ J \ I<VAR>h : (M ↾ X).Base (insert y (I \ {e}))<GOAL>∃ f ∈ J \ I, M.Basis (insert f (I \ {e})) X
<VAR>a : ℝ<GOAL>closure {z | a < z.re} = {z | a ≤ z.re}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>A : ℝ<VAR>x : α<GOAL>|truncation f A x| ≤ |f x|
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>A : ℝ<VAR>x : α<GOAL>|if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |f x|
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasStrictTerminalObjects C<VAR>I : C<VAR>hI : IsTerminal I<VAR>A : C<VAR>f g : I ⟶ A<GOAL>f = g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasStrictTerminalObjects C<VAR>I : C<VAR>hI : IsTerminal I<VAR>A : C<VAR>f g : I ⟶ A<VAR>this : IsIso f<GOAL>f = g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasStrictTerminalObjects C<VAR>I : C<VAR>hI : IsTerminal I<VAR>A : C<VAR>f g : I ⟶ A<VAR>this✝ : IsIso f<VAR>this : IsIso g<GOAL>f = g
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>X✝ Y : C<VAR>α : F ⟶ G<VAR>x✝ : IsIso α<VAR>X : C<GOAL>(inv α).app X = inv (α.app X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>X✝ Y : C<VAR>α : F ⟶ G<VAR>x✝ : IsIso α<VAR>X : C<GOAL>α.app X ≫ (inv α).app X = 𝟙 (F.obj X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>X✝ Y : C<VAR>α : F ⟶ G<VAR>x✝ : IsIso α<VAR>X : C<GOAL>(α ≫ inv α).app X = 𝟙 (F.obj X)
<VAR>X : Type u_1<VAR>inst✝³ : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>s : Set 𝕜<VAR>inst✝¹ : Zero ↑s<VAR>h0 : ↑0 = 0<VAR>inst✝ : CompactSpace ↑s<GOAL>Dense ↑(adjoin 𝕜 {ContinuousMapZero.id h0})
<VAR>X : Type u_1<VAR>inst✝³ : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>s : Set 𝕜<VAR>inst✝¹ : Zero ↑s<VAR>h0 : ↑0 = 0<VAR>inst✝ : CompactSpace ↑s<VAR>h0' : 0 ∈ s<GOAL>Dense ↑(adjoin 𝕜 {ContinuousMapZero.id h0})
<VAR>X : Type u_1<VAR>inst✝³ : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>s : Set 𝕜<VAR>inst✝¹ : Zero ↑s<VAR>h0 : ↑0 = 0<VAR>inst✝ : CompactSpace ↑s<VAR>h0' : 0 ∈ s<GOAL>⇑toContinuousMapHom ⁻¹' ↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0'⟩)) = Set.univ
<VAR>X : Type u_1<VAR>inst✝³ : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>s : Set 𝕜<VAR>inst✝¹ : Zero ↑s<VAR>h0 : ↑0 = 0<VAR>inst✝ : CompactSpace ↑s<VAR>h0' : 0 ∈ s<VAR>f : C(↑s, 𝕜)₀<GOAL>f ∈ ⇑toContinuousMapHom ⁻¹' ↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0'⟩))
<VAR>X : Type u_1<VAR>inst✝³ : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>s : Set 𝕜<VAR>inst✝¹ : Zero ↑s<VAR>h0 : ↑0 = 0<VAR>inst✝ : CompactSpace ↑s<VAR>h0' : 0 ∈ s<VAR>f : C(↑s, 𝕜)₀<GOAL>f ⟨0, h0'⟩ = 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>x y : ZMod p<VAR>hy : y ≠ 0<VAR>hxy : x ^ 2 / y ^ 2 = -y ^ 2 / y ^ 2<GOAL>(x / y) ^ 2 = -1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommGroup α<GOAL>[].reverse.alternatingProd = [].alternatingProd ^ (-1) ^ ([].length + 1)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommGroup α<VAR>a : α<VAR>l : List α<GOAL>(a :: l).reverse.alternatingProd = (a :: l).alternatingProd ^ (-1) ^ ((a :: l).length + 1)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommGroup α<VAR>a : α<VAR>l : List α<GOAL>(l.alternatingProd ^ (-1) ^ l.length)⁻¹ * a ^ (-1) ^ l.length = (a / l.alternatingProd) ^ (-1) ^ l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NonAssocSemiring α<VAR>m n : ℕ<GOAL>↑(m * n) = ↑m * ↑n
<GOAL>MeasurePreserving (⇑measurableEquivPi) volume volume
<GOAL>volume = Measure.map (⇑measurableEquivPi.symm) volume
<GOAL>((Pi.basisFun ℝ (Fin 2)).map basisOneI.equivFun.toContinuousLinearEquiv.symm.toLinearEquiv).addHaar = volume
<VAR>z : ℂ<GOAL>Tendsto (fun n => ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))
<VAR>z : ℂ<VAR>A : Tendsto (fun n => ((↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))) atTop (𝓝 (Complex.sin (↑π * z)))<GOAL>Tendsto (fun n => ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))
<VAR>z : ℂ<VAR>A : Tendsto (fun n => ((↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))) atTop (𝓝 (Complex.sin (↑π * z)))<VAR>this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)<GOAL>Tendsto (fun n => ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))
<VAR>z : ℂ<VAR>this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)<VAR>A : Tendsto (fun n => (↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ((∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)))) atTop (𝓝 (Complex.sin (↑π * z) * 1))<GOAL>Tendsto (fun n => ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))
<VAR>z : ℂ<VAR>this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)<VAR>A : Tendsto (fun n => (↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ((∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)))) atTop (𝓝 (Complex.sin (↑π * z) * 1))<GOAL>Tendsto (fun n => (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))) atTop (𝓝 1)
<VAR>z : ℂ<VAR>this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)<VAR>A : Tendsto (fun n => (↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ((∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)))) atTop (𝓝 (Complex.sin (↑π * z) * 1))<GOAL>Tendsto (fun n => (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n)) atTop (𝓝 1)
<VAR>z : ℂ<VAR>this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)<VAR>A : Tendsto (fun n => (↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ((∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)))) atTop (𝓝 (Complex.sin (↑π * z) * 1))<VAR>this : ContinuousOn (fun x => Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))<GOAL>Tendsto (fun n => (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n)) atTop (𝓝 1)
<VAR>z : ℂ<VAR>this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)<VAR>A : Tendsto (fun n => (↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ((∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)))) atTop (𝓝 (Complex.sin (↑π * z) * 1))<VAR>this : ContinuousOn (fun x => Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))<GOAL>(fun n => (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n)) = fun n => (∫ (x : ℝ) in 0 ..π / 2, ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n)
<VAR>z : ℂ<VAR>this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)<VAR>A : Tendsto (fun n => (↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ((∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)))) atTop (𝓝 (Complex.sin (↑π * z) * 1))<VAR>this : ContinuousOn (fun x => Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))<GOAL>𝓝 1 = 𝓝 (Complex.cos (2 * z * ↑0))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s✝ t✝ A B : Set β<VAR>a : α<VAR>x✝ : β<VAR>s t : Set α<VAR>x : α<GOAL>x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s✝ t✝ A B : Set β<VAR>a : α<VAR>x✝ : β<VAR>s t : Set α<VAR>x : α<GOAL>(x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z : P<VAR>f : P ≃ᵃ[R] P'<GOAL>Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z : P<VAR>f : P ≃ᵃ[R] P'<GOAL>Function.Injective ⇑↑f
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List (α × β)<GOAL>l.unzip.2 = map Prod.snd l
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>h : M✶.RkPos<VAR>hB : M.Base M.E<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<GOAL>f a = ⨆ n, ↑(eapprox f n) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α), ⨆ n, ↑(eapprox f n) a ∂μ = ⨆ n, ∫⁻ (a : α), ↑(eapprox f n) a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∀ (n : ℕ), Measurable ↑(eapprox f n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Monotone fun n => ↑(eapprox f n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>n : ℕ<GOAL>∫⁻ (a : α), ↑(eapprox f n) a ∂μ = (eapprox f n).lintegral μ
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Z ⟶ X<VAR>w : h ≫ f = h ≫ g<VAR>inst✝² : HasEqualizer f g<VAR>inst✝¹ : HasEqualizer (G.map f) (G.map g)<VAR>inst✝ : PreservesLimit (parallelPair f g) G<GOAL>(iso G f g).inv ≫ G.map (equalizer.ι f g) = equalizer.ι (G.map f) (G.map g)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Z ⟶ X<VAR>w : h ≫ f = h ≫ g<VAR>inst✝² : HasEqualizer f g<VAR>inst✝¹ : HasEqualizer (G.map f) (G.map g)<VAR>inst✝ : PreservesLimit (parallelPair f g) G<GOAL>𝟙 (G.obj (equalizer f g)) ≫ G.map (equalizer.ι f g) = (iso G f g).hom ≫ equalizer.ι (G.map f) (G.map g)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>hp : p ≠ 0<VAR>h : p.degree < q.degree<GOAL>p.natDegree < q.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>hp : p ≠ 0<VAR>h : p.degree < q.degree<VAR>hq : q ≠ 0<GOAL>p.natDegree < q.natDegree
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<GOAL>IsCompl N N' ↔ IsCompl ↑N ↑N'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>τ : Type u_4<VAR>T : TopologicalSpace α<VAR>F : Realizer α<VAR>s : Set α<VAR>a : α<GOAL>s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>τ : Type u_4<VAR>T : TopologicalSpace α<VAR>F : Realizer α<VAR>s : Set α<VAR>a : α<VAR>this : s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s<GOAL>s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f✝ g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<VAR>f : α → β<VAR>x : β<GOAL>(x ∈ s.biUnion fun a => {f a}) ↔ x ∈ image f s
<VAR>R : Type u_1<VAR>p k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : k ≠ 0<VAR>h : ¬k = 1<GOAL>μ (p ^ k) = 0
<VAR>R : Type u_1<VAR>p k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : k ≠ 0<VAR>h : ¬k = 1<GOAL>¬Squarefree (p ^ k)
<VAR>R : Type u_1<VAR>p k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : k ≠ 0<VAR>h : ¬k = 1<GOAL>¬Squarefree p ∨ ¬k = 1
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : DivInvMonoid G<VAR>inst✝¹ : Preorder G<VAR>inst✝ : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : G<VAR>H : 1 ≤ x<VAR>n : ℕ<GOAL>1 ≤ x ^ ↑n
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : DivInvMonoid G<VAR>inst✝¹ : Preorder G<VAR>inst✝ : CovariantClass G G (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : G<VAR>H : 1 ≤ x<VAR>n : ℕ<GOAL>1 ≤ x ^ n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<GOAL>s ∩ {a} = ∅ ↔ a ∉ s
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hg : DifferentiableAt 𝕜 g x<GOAL>DifferentiableAt 𝕜 (fun y => f y - g y) x ↔ DifferentiableAt 𝕜 f x
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>R' : Type v<VAR>inst✝¹ : CommMonoid R'<VAR>R'' : Type u_1<VAR>inst✝ : CommMonoid R''<VAR>φ : AddChar R R'<VAR>f : R' →* R''<VAR>hφ : φ.IsPrimitive<VAR>hf : Function.Injective ⇑f<VAR>a : R<VAR>ha : a ≠ 0<GOAL>(f.compAddChar φ).mulShift a ≠ 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<GOAL>f.cycleOf x = 1 ↔ f x = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<GOAL>(∀ (x_1 : α), (if f.SameCycle x x_1 then f x_1 else x_1) = x_1) ↔ f x = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y✝ : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>h : f x = x<VAR>y : α<GOAL>(if f.SameCycle x y then f y else y) = y