ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>b m : ℝ<VAR>x y : E<VAR>f : E → ℝ<VAR>hb : 0 ≤ b<VAR>ha : 0 ≤ 1 - b<VAR>hab : 1 - b + b = 1<GOAL>(1 - b) * (f x - m / 2 * ‖x‖ ^ 2) + b * (f y - m / 2 * ‖y‖ ^ 2) + m / 2 * ((1 - b) ^ 2 * ‖x‖ ^ 2 + 2 * ((1 - b) * (b * ⟪x, y⟫_ℝ)) + b ^ 2 * ‖y‖ ^ 2) = (1 - b) * f x + b * f y - m / 2 * (1 - b) * b * (‖x‖ ^ 2 - 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2)
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>aleph o₁ + aleph o₂ = aleph (max o₁ o₂)
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n✝ : ℕ<VAR>n : ℤ<VAR>ha : a ≠ 0<GOAL>a ^ (-n) * a ^ n = 1
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n✝ : ℕ<VAR>n : ℤ<VAR>ha : a ≠ 0<GOAL>(a ^ n)⁻¹ * a ^ n = 1
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>l : Filter X<VAR>y : X<VAR>hmem : s ∈ l<VAR>h : ∀ x ∈ s, ClusterPt x l → x = y<GOAL>l ≤ 𝓝 y
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>l : Filter X<VAR>y : X<VAR>hmem : s ∈ l<VAR>h : ∀ x ∈ s, ClusterPt x l → x = y<VAR>f : Ultrafilter X<VAR>hf : ↑f ≤ l<GOAL>↑f ≤ 𝓝 y
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>l : Filter X<VAR>y : X<VAR>hmem : s ∈ l<VAR>h : ∀ x ∈ s, ClusterPt x l → x = y<VAR>f : Ultrafilter X<VAR>hf : ↑f ≤ l<VAR>x : X<VAR>hxs : x ∈ s<VAR>hx : ↑f ≤ 𝓝 x<GOAL>x = y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Semifield R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : HasContinuousInv₀ R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>IsUnit (cfc f a) ↔ ∀ x ∈ spectrum R a, f x ≠ 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Semifield R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : HasContinuousInv₀ R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>0 ∉ f '' spectrum R a ↔ ∀ x ∈ spectrum R a, f x ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β<VAR>o : Option α<VAR>h : (Option.map f o).isSome = true<GOAL>o.isSome = true
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t s : Set A<VAR>x : A<VAR>f : A →ₗ[R] B<VAR>hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂<VAR>h : x ∈ adjoin R s<GOAL>f x ∈ adjoin R (⇑f '' (s ∪ {1}))
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t s : Set A<VAR>x : A<VAR>f : A →ₗ[R] B<VAR>hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂<VAR>h : x ∈ adjoin R s<VAR>r : R<GOAL>(fun a => f a ∈ adjoin R (⇑f '' (s ∪ {1}))) ((algebraMap R A) r)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t s : Set A<VAR>x : A<VAR>f : A →ₗ[R] B<VAR>hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂<VAR>h : x ∈ adjoin R s<VAR>r : R<VAR>this : f 1 ∈ adjoin R (⇑f '' (s ∪ {1}))<GOAL>(fun a => f a ∈ adjoin R (⇑f '' (s ∪ {1}))) ((algebraMap R A) r)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t s : Set A<VAR>x : A<VAR>f : A →ₗ[R] B<VAR>hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂<VAR>h : x ∈ adjoin R s<VAR>r : R<VAR>this : f 1 ∈ adjoin R (⇑f '' (s ∪ {1}))<GOAL>f ((algebraMap R A) r) = r • f 1
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t s : Set A<VAR>x : A<VAR>f : A →ₗ[R] B<VAR>hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂<VAR>h : x ∈ adjoin R s<VAR>r : R<VAR>this : f 1 ∈ adjoin R (⇑f '' (s ∪ {1}))<GOAL>f (r • 1) = r • f 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<GOAL>((lift R) f).toLinearMap ∘ₗ ι R = f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>i : ℕ<GOAL>(proj 𝒜 i) a ^ m ∈ 𝒜 (m * i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>i : ℕ<GOAL>f ^ i ∈ 𝒜 (m * i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a : A<VAR>i : ℕ<GOAL>f ^ i ∈ 𝒜 (i * m)
<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocRing R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>k : ℕ<GOAL>↑k = ↑(k % p + p * (k / p))
<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocRing R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>k : ℕ<GOAL>↑(k % p + p * (k / p)) = ↑(k % p)
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>inst✝¹ : Infinite X<VAR>inst✝ : DiscreteTopology X<VAR>inhabited_h : Inhabited X<GOAL>¬Continuous ⇑CofiniteTopology.of.symm
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>inst✝¹ : Infinite X<VAR>inst✝ : DiscreteTopology X<VAR>inhabited_h : Inhabited X<GOAL>∃ x, ¬Tendsto (⇑CofiniteTopology.of.symm) (𝓝 x) (𝓝 (CofiniteTopology.of.symm x))
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>inst✝¹ : Infinite X<VAR>inst✝ : DiscreteTopology X<VAR>inhabited_h : Inhabited X<GOAL>¬Tendsto (⇑CofiniteTopology.of.symm) (𝓝 (CofiniteTopology.of ↑default)) (𝓝 (CofiniteTopology.of.symm (CofiniteTopology.of ↑default)))
<VAR>F : Type u → Type v<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>G : Type u → Type w<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>η η' : ApplicativeTransformation F G<VAR>h : ∀ (α : Type u) (x : F α), (fun {α} => η.app α) x = (fun {α} => η'.app α) x<GOAL>η = η'
<VAR>F : Type u → Type v<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>G : Type u → Type w<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>η η' : ApplicativeTransformation F G<VAR>h : ∀ (α : Type u) (x : F α), (fun {α} => η.app α) x = (fun {α} => η'.app α) x<GOAL>(fun {α} => η.app α) = fun {α} => η'.app α
<VAR>F : Type u → Type v<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>G : Type u → Type w<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>η η' : ApplicativeTransformation F G<VAR>h : ∀ (α : Type u) (x : F α), (fun {α} => η.app α) x = (fun {α} => η'.app α) x<VAR>α : Type u<GOAL>η.app α = η'.app α
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p✝ p₁ p₂ : X → Prop<VAR>inst✝¹ : TopologicalSpace X<VAR>F : Filter α<VAR>φ : β → α<VAR>p : Filter β<VAR>u : α → X<VAR>inst✝ : p.NeBot<VAR>h : Tendsto φ p F<VAR>H : Tendsto (u ∘ φ) p (𝓝 x)<GOAL>MapClusterPt x F u
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p✝ p₁ p₂ : X → Prop<VAR>inst✝¹ : TopologicalSpace X<VAR>F : Filter α<VAR>φ : β → α<VAR>p : Filter β<VAR>u : α → X<VAR>inst✝ : p.NeBot<VAR>h : Tendsto φ p F<VAR>H : Tendsto (u ∘ φ) p (𝓝 x)<VAR>this : map (u ∘ φ) p ≤ map u F<GOAL>MapClusterPt x F u
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p✝ p₁ p₂ : X → Prop<VAR>inst✝¹ : TopologicalSpace X<VAR>F : Filter α<VAR>φ : β → α<VAR>p : Filter β<VAR>u : α → X<VAR>inst✝ : p.NeBot<VAR>h : Tendsto φ p F<VAR>H : Tendsto (u ∘ φ) p (𝓝 x)<VAR>this✝ : map (u ∘ φ) p ≤ map u F<VAR>this : map (u ∘ φ) p ≤ 𝓝 x ⊓ map u F<GOAL>MapClusterPt x F u
<VAR>θ : ℂ<GOAL>cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2
<VAR>θ : ℂ<VAR>h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1<GOAL>cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2
<VAR>θ : ℂ<VAR>h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1<GOAL>(∃ n, 2 * I * θ = ↑π * I + ↑n * (2 * ↑π * I)) ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2
<VAR>θ : ℂ<VAR>h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1<VAR>x : ℤ<GOAL>2 * I * θ = ↑π * I + ↑x * (2 * ↑π * I) ↔ θ = (2 * ↑x + 1) * ↑π / 2
<VAR>θ : ℂ<VAR>h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1<VAR>x : ℤ<GOAL>↑π * I + ↑x * (2 * ↑π * I) = 2 * I * ((2 * ↑x + 1) * ↑π / 2)
<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✝⁶ : IsDomain A<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : IsDedekindDomain A<VAR>P : Ideal A<VAR>hP : P ≠ ⊥<VAR>pP : P.IsPrime<VAR>Aₘ : Type u_4<VAR>inst✝³ : CommRing Aₘ<VAR>inst✝² : IsDomain Aₘ<VAR>inst✝¹ : Algebra A Aₘ<VAR>inst✝ : IsLocalization.AtPrime Aₘ P<GOAL>DiscreteValuationRing Aₘ
<VAR>F : Type u_1<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝ : CompleteSpace F<GOAL>MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x}
<VAR>F : Type u_1<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝ : CompleteSpace F<VAR>this : IsComplete univ<GOAL>MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x}
<VAR>F : Type u_1<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝ : CompleteSpace F<VAR>this : IsComplete univ<VAR>x✝ : ℝ<GOAL>DifferentiableWithinAt ℝ f (Ici x✝) x✝ ↔ DifferentiableWithinAt ℝ f (Ici x✝) x✝ ∧ derivWithin f (Ici x✝) x✝ ∈ univ
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : l.Nodup<GOAL>pmap l.prev l ⋯ = l.rotate (l.length - 1)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : l.Nodup<GOAL>(pmap l.prev l ⋯).length = (l.rotate (l.length - 1)).length
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h : l.Nodup<GOAL>∀ (n : ℕ) (h₁ : n < (pmap l.prev l ⋯).length) (h₂ : n < (l.rotate (l.length - 1)).length), (pmap l.prev l ⋯).nthLe n h₁ = (l.rotate (l.length - 1)).nthLe n h₂
<VAR>g✝ : SL(2, ℤ)<VAR>z : ℍ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>g : SL(2, R)<GOAL>IsCoprime (↑g 1 0) (↑g 1 1)
<VAR>g✝ : SL(2, ℤ)<VAR>z : ℍ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>g : SL(2, R)<GOAL>-↑g 0 1 * ↑g 1 0 + ↑g 0 0 * ↑g 1 1 = 1
<VAR>g✝ : SL(2, ℤ)<VAR>z : ℍ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>g : SL(2, R)<GOAL>(↑g).det = 1
<VAR>X : Type u<GOAL>{ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map (𝟙 X) = 𝟙 ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X)
<VAR>X : Type u<GOAL>autoParam (∀ (X_1 Y : ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X)) (f : X_1 ⟶ Y), ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map (𝟙 X)).map f = eqToHom ⋯ ≫ (𝟙 ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X)).map f ≫ eqToHom ⋯) _auto✝
<VAR>X : Type u<GOAL>∀ (X_1 : ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X)), ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map (𝟙 X)).obj X_1 = (𝟙 ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X)).obj X_1
<VAR>X✝ Y✝ Z✝ : Type u<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>{ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map (f ≫ g) = { obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map f ≫ { obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map g
<VAR>X✝ Y✝ Z✝ : Type u<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>autoParam (∀ (X Y : ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X✝)) (f_1 : X ⟶ Y), ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map f ≫ { obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map g).map f_1 ≫ eqToHom ⋯) _auto✝
<VAR>X✝ Y✝ Z✝ : Type u<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>∀ (X : ↑({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.obj X✝)), ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map (f ≫ g)).obj X = ({ obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map f ≫ { obj := fun X => Cat.of (Discrete X), map := fun {X Y} f => id (Discrete.functor (Discrete.mk ∘ f)) }.map g).obj X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>π : δ → Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : (a : δ) → MeasurableSpace (π a)<VAR>inst✝ : MeasurableSpace γ<VAR>f : δ' ≃ δ<GOAL>Measurable ⇑(piCongrLeft π f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>π : δ → Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : (a : δ) → MeasurableSpace (π a)<VAR>inst✝ : MeasurableSpace γ<VAR>f : δ' ≃ δ<GOAL>∀ (a : δ), Measurable fun x => (piCongrLeft π f) x a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>π : δ → Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : (a : δ) → MeasurableSpace (π a)<VAR>inst✝ : MeasurableSpace γ<VAR>f : δ' ≃ δ<VAR>i : δ<GOAL>Measurable fun x => (piCongrLeft π f) x i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>π : δ → Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : (a : δ) → MeasurableSpace (π a)<VAR>inst✝ : MeasurableSpace γ<VAR>f : δ' ≃ δ<VAR>i : δ<GOAL>Measurable fun x => cast ⋯ (x (f.symm i))
<VAR>x : ℂ<VAR>hx₁ : -π < x.im<VAR>hx₂ : x.im ≤ π<GOAL>log (cexp x) = x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>f : X → Y<VAR>inst✝ : DiscreteTopology X<VAR>hf : Tendsto f (cocompact X) (cocompact Y)<GOAL>cofinite = cocompact X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>hdvd : a ∣ b<VAR>heq : 0 = multiplicity a b<GOAL>multiplicity a b < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>hdvd : a ∣ b<VAR>heq : 0 = multiplicity a b<GOAL>a ^ 1 ∣ b
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>z τ : ℂ<VAR>hz : |z.im| ≤ S<VAR>hτ : T ≤ τ.im<VAR>n : ℤ<GOAL>‖jacobiTheta₂_term n z τ‖ ≤ rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>z τ : ℂ<VAR>hz : |z.im| ≤ S<VAR>hτ : T ≤ τ.im<VAR>n : ℤ<GOAL>↑n ^ 2 * T + -(2 * S * ↑|n|) ≤ ↑n ^ 2 * τ.im + 2 * ↑n * z.im
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>z τ : ℂ<VAR>hz : |z.im| ≤ S<VAR>hτ : T ≤ τ.im<VAR>n : ℤ<GOAL>-(2 * S * ↑|n|) ≤ 2 * ↑n * z.im
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>z τ : ℂ<VAR>hz : |z.im| ≤ S<VAR>hτ : T ≤ τ.im<VAR>n : ℤ<GOAL>↑|n| * -S ≤ ↑n * z.im
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>z τ : ℂ<VAR>hz : |z.im| ≤ S<VAR>hτ : T ≤ τ.im<VAR>n : ℤ<GOAL>↑|n| * -S ≤ -|↑n * z.im|
<VAR>S T : ℝ<VAR>hT : 0 < T<VAR>z τ : ℂ<VAR>hz : |z.im| ≤ S<VAR>hτ : T ≤ τ.im<VAR>n : ℤ<GOAL>|↑n| * |z.im| ≤ |↑n| * S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<VAR>h : r.dom ⊆ s<GOAL>r.image s = r.codom
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : AddTorsor G P<VAR>p₁ p₂ p₃ : P<GOAL>p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>f : Ω → ℝ := embeddingReal Ω<GOAL>∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>f : Ω → ℝ := embeddingReal Ω<VAR>hf : MeasurableEmbedding (embeddingReal Ω)<GOAL>∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>f : Ω → ℝ := embeddingReal Ω<VAR>hf : MeasurableEmbedding (embeddingReal Ω)<VAR>ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ<VAR>hρ'def : ρ' = Measure.map (Prod.map id f) ρ<GOAL>∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>f : Ω → ℝ := embeddingReal Ω<VAR>hf : MeasurableEmbedding (embeddingReal Ω)<VAR>ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ<VAR>hρ'def : ρ' = Measure.map (Prod.map id f) ρ<VAR>hρ' : ρ'.fst = ρ.fst<GOAL>∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>f : Ω → ℝ := embeddingReal Ω<VAR>hf : MeasurableEmbedding (embeddingReal Ω)<VAR>ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ<VAR>hρ'def : ρ' = Measure.map (Prod.map id f) ρ<VAR>hρ' : ρ'.fst = ρ.fst<VAR>hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f ⋯) x = ρ'.condKernel x<GOAL>∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>f : Ω → ℝ := embeddingReal Ω<VAR>hf : MeasurableEmbedding (embeddingReal Ω)<VAR>ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ<VAR>hρ'def : ρ' = Measure.map (Prod.map id f) ρ<VAR>hρ' : ρ'.fst = ρ.fst<VAR>hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f ⋯) x = ρ'.condKernel x<GOAL>∀ᵐ (x : α) ∂ρ.fst, ∀ (s : Set ℝ), MeasurableSet s → (ρ'.condKernel x) s = (ρ.condKernel x) (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>f : Ω → ℝ := embeddingReal Ω<VAR>hf : MeasurableEmbedding (embeddingReal Ω)<VAR>ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ<VAR>hρ'def : ρ' = Measure.map (Prod.map id f) ρ<VAR>hρ' : ρ'.fst = ρ.fst<VAR>hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f ⋯) x = ρ'.condKernel x<GOAL>Measure.map (Prod.map id f) ρ = ρ.fst ⊗ₘ ρ.condKernel.map f ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>f : Ω → ℝ := embeddingReal Ω<VAR>hf : MeasurableEmbedding (embeddingReal Ω)<VAR>ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ<VAR>hρ'def : ρ' = Measure.map (Prod.map id f) ρ<VAR>hρ' : ρ'.fst = ρ.fst<VAR>hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f ⋯) x = ρ'.condKernel x<VAR>s : Set (α × ℝ)<VAR>hs : MeasurableSet s<GOAL>(Measure.map (Prod.map id f) ρ) s = (ρ.fst ⊗ₘ ρ.condKernel.map f ⋯) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>f : Ω → ℝ := embeddingReal Ω<VAR>hf : MeasurableEmbedding (embeddingReal Ω)<VAR>ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ<VAR>hρ'def : ρ' = Measure.map (Prod.map id f) ρ<VAR>hρ' : ρ'.fst = ρ.fst<VAR>hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f ⋯) x = ρ'.condKernel x<VAR>s : Set (α × ℝ)<VAR>hs : MeasurableSet s<GOAL>(Measure.map (Prod.map id f) (ρ.fst ⊗ₘ ρ.condKernel)) s = (ρ.fst ⊗ₘ ρ.condKernel.map f ⋯) s