ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>h : c ∣ a + b<VAR>ha : ¬c ∣ a<VAR>hc : ¬c ≤ a % c + b % c<GOAL>False
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>h : c ∣ a + b<VAR>ha : ¬c ∣ a<VAR>hc : ¬c ≤ a % c + b % c<VAR>this : (a + b) % c = a % c + b % c<GOAL>False
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>x₀ : α 0<VAR>x : (i : Fin n) → α i.succ<VAR>s₀ : Finset (α 0)<VAR>s : (i : Fin n) → Finset (α i.succ)<GOAL>cons x₀ x ∈ piFinset (cons s₀ s) ↔ x₀ ∈ s₀ ∧ x ∈ piFinset s
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>i : Fin r ⊕ Unit<GOAL>((listTransvecCol M).prod * M) (inr ()) i = M (inr ()) i
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Surjective ⇑f<VAR>y : AdicCompletion I N<GOAL>∃ a, (map I f) a = y
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Surjective ⇑f<VAR>y : AdicCompletion I N<VAR>b : AdicCauchySequence I N<GOAL>∃ a, (map I f) a = (mk I N) b
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → AddGroup (β i)<VAR>s : Finset ι<VAR>x y : (i : ↑↑s) → β ↑i<VAR>i : ι<GOAL>(mk s (x - y)) i = (mk s x - mk s y) i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → AddGroup (β i)<VAR>s : Finset ι<VAR>x y : (i : ↑↑s) → β ↑i<VAR>i : ι<GOAL>(if H : i ∈ s then (x - y) ⟨i, H⟩ else 0) = (if H : i ∈ s then x ⟨i, H⟩ else 0) - if H : i ∈ s then y ⟨i, H⟩ else 0
<VAR>V : Type u<VAR>inst✝ : Quiver V<VAR>X Y : Paths (Quiver.Symmetrify V)<VAR>p : X ⟶ Y<GOAL>Quot.mk (Quotient.CompClosure redStep) (p ≫ Quiver.Path.reverse p) = Quot.mk (Quotient.CompClosure redStep) (𝟙 X)
<VAR>V : Type u<VAR>inst✝ : Quiver V<VAR>X Y : Paths (Quiver.Symmetrify V)<VAR>p : X ⟶ Y<GOAL>EqvGen (Quotient.CompClosure redStep) (p ≫ Quiver.Path.reverse p) (𝟙 X)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<GOAL>normEDS b c d 3 = c
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>n : σ →₀ ℕ<VAR>a : R<GOAL>(coeff R n) ((monomial R n) a) = a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : ↥(Lp E 2 μ)<GOAL>∫ (a : α), ⟪↑↑f a, ↑↑f a⟫_𝕜 ∂μ = ↑(∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : ↥(Lp E 2 μ)<GOAL>∫ (a : α), ↑‖↑↑f a‖ ^ 2 ∂μ = ↑(∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : ↥(Lp E 2 μ)<GOAL>∫ (x : α), ‖↑↑f x‖ ^ 2 ∂μ = (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : ↥(Lp E 2 μ)<GOAL>(∫⁻ (a : α), ENNReal.ofReal (‖↑↑f a‖ ^ 2) ∂μ).toReal = (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : ↥(Lp E 2 μ)<GOAL>0 ≤ᶠ[ae μ] fun x => ‖↑↑f x‖ ^ 2
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : ↥(Lp E 2 μ)<GOAL>AEStronglyMeasurable (fun x => ‖↑↑f x‖ ^ 2) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : ↥(Lp E 2 μ)<VAR>x : α<VAR>h_two : 2 = ↑2<GOAL>ENNReal.ofReal (‖↑↑f x‖ ^ 2) = ↑(‖↑↑f x‖₊ ^ 2)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : ↥(Lp E 2 μ)<VAR>x : α<VAR>h_two : 2 = ↑2<GOAL>↑‖↑↑f x‖₊ ^ 2 = ↑(‖↑↑f x‖₊ ^ 2)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>y₁ y₂ : β<GOAL>nndist ((WithLp.equiv p (α × β)).symm (0, y₁)) ((WithLp.equiv p (α × β)).symm (0, y₂)) = nndist y₁ y₂
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>h e f : L<VAR>m : M<VAR>μ : R<VAR>t : IsSl2Triple h e f<VAR>P✝ P : t.HasPrimitiveVectorWith m μ<VAR>n : ℕ<GOAL>⁅f, ((toEnd R L M) f ^ n) m⁆ = ((toEnd R L M) f ^ (n + 1)) m
<VAR>α : Type u<VAR>a b : Set α<VAR>u : Ultrafilter α<VAR>ua : u ∈ (fun s => {u | s ∈ u}) a<VAR>ub : u ∈ (fun s => {u | s ∈ u}) b<GOAL>∃ t₃ ∈ ultrafilterBasis α, u ∈ t₃ ∧ t₃ ⊆ (fun s => {u | s ∈ u}) a ∩ (fun s => {u | s ∈ u}) b
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : OrderedSemiring β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : 0 ≤ᶠ[l] f<VAR>hg : 0 ≤ᶠ[l] g<GOAL>0 ≤ᶠ[l] f * g
<VAR>α : Sort u<VAR>β✝ : α → Sort v<VAR>α' : Sort w<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq α'<VAR>f✝ g : (a : α) → β✝ a<VAR>a✝ : α<VAR>b✝ : β✝ a✝<VAR>β : Sort u_1<VAR>f : α → β<VAR>a' : α<VAR>b : β<VAR>a : α<GOAL>update f a' b a = if a = a' then b else f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = ((κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η).comapRight ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = ((κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η).comapRight ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = ((κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η).comapRight ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = ((κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η).comapRight ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<VAR>h_prod_embed : MeasurableEmbedding (Prod.map id e)<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = ((κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η).comapRight ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<VAR>h_prod_embed : MeasurableEmbedding (Prod.map id e)<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = (κ'.fst ⊗ₖ η).comapRight h_prod_embed
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<VAR>h_prod_embed : MeasurableEmbedding (Prod.map id e)<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ'.fst ⊗ₖ η.comapRight he
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<VAR>h_prod_embed : MeasurableEmbedding (Prod.map id e)<VAR>h_fst : κ'.fst = κ.fst<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ'.fst ⊗ₖ η.comapRight he
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<VAR>h_prod_embed : MeasurableEmbedding (Prod.map id e)<VAR>h_fst : κ'.fst = κ.fst<VAR>a : α<VAR>t : Set (β × Ω)<VAR>ht : MeasurableSet t<GOAL>((κ.fst ⊗ₖ borelMarkovFromReal Ω η) a) t = ((κ.fst ⊗ₖ η.comapRight he) a) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<VAR>h_prod_embed : MeasurableEmbedding (Prod.map id e)<VAR>h_fst : κ'.fst = κ.fst<VAR>a : α<VAR>t : Set (β × Ω)<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β), ((borelMarkovFromReal Ω η) (a, b)) {c | (b, c) ∈ t} ∂κ.fst a = ∫⁻ (b : β), ((η.comapRight he) (a, b)) {c | (b, c) ∈ t} ∂κ.fst a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<VAR>h_prod_embed : MeasurableEmbedding (Prod.map id e)<VAR>h_fst : κ'.fst = κ.fst<VAR>a : α<VAR>t : Set (β × Ω)<VAR>ht : MeasurableSet t<GOAL>(fun b => ((borelMarkovFromReal Ω η) (a, b)) {c | (b, c) ∈ t}) =ᶠ[ae (κ.fst a)] fun b => ((η.comapRight he) (a, b)) {c | (b, c) ∈ t}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<VAR>h_prod_embed : MeasurableEmbedding (Prod.map id e)<VAR>h_fst : κ'.fst = κ.fst<VAR>a : α<VAR>t : Set (β × Ω)<VAR>ht : MeasurableSet t<VAR>h_ae : ∀ᵐ (t : β) ∂κ.fst a, (a, t) ∈ {p | (η p) (range e)ᶜ = 0}<GOAL>(fun b => ((borelMarkovFromReal Ω η) (a, b)) {c | (b, c) ∈ t}) =ᶠ[ae (κ.fst a)] fun b => ((η.comapRight he) (a, b)) {c | (b, c) ∈ t}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<VAR>h_prod_embed : MeasurableEmbedding (Prod.map id e)<VAR>h_fst : κ'.fst = κ.fst<VAR>a✝ : α<VAR>t : Set (β × Ω)<VAR>ht : MeasurableSet t<VAR>h_ae : ∀ᵐ (t : β) ∂κ.fst a✝, (a✝, t) ∈ {p | (η p) (range e)ᶜ = 0}<VAR>a : β<VAR>ha : (η (a✝, a)) (range e)ᶜ = 0<GOAL>((borelMarkovFromReal Ω η) (a✝, a)) {c | (a, c) ∈ t} = ((η.comapRight he) (a✝, a)) {c | (a, c) ∈ t}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<VAR>h_prod_embed : MeasurableEmbedding (Prod.map id e)<VAR>h_fst : κ'.fst = κ.fst<VAR>a✝ : α<VAR>t : Set (β × Ω)<VAR>ht : MeasurableSet t<VAR>h_ae : ∀ᵐ (t : β) ∂κ.fst a✝, (a✝, t) ∈ {p | (η p) (range e)ᶜ = 0}<VAR>a : β<VAR>ha : (η (a✝, a)) (range e)ᶜ = 0<GOAL>((piecewise ⋯ η (deterministic (fun x => Exists.choose ⋯) ⋯)) (a✝, a)) (embeddingReal Ω '' {c | (a, c) ∈ t}) = (η (a✝, a)) (embeddingReal Ω '' {c | (a, c) ∈ t})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<VAR>h_prod_embed : MeasurableEmbedding (Prod.map id e)<VAR>h_fst : κ'.fst = κ.fst<VAR>a✝ : α<VAR>t : Set (β × Ω)<VAR>ht : MeasurableSet t<VAR>h_ae : ∀ᵐ (t : β) ∂κ.fst a✝, (a✝, t) ∈ {p | (η p) (range e)ᶜ = 0}<VAR>a : β<VAR>ha : (η (a✝, a)) (range e)ᶜ = 0<GOAL>MeasurableSet {c | (a, c) ∈ t}
<VAR>X✝ Y : Scheme<VAR>f : X✝ ⟶ Y<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<GOAL>IsQuasiSeparated ↑U
<VAR>X✝ Y : Scheme<VAR>f : X✝ ⟶ Y<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<GOAL>QuasiSeparatedSpace ↑↑U
<VAR>X✝ Y : Scheme<VAR>f : X✝ ⟶ Y<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<GOAL>IsOpen ↑U
<VAR>R✝ : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R✝<VAR>m n : ℕ<VAR>inst✝³ : Semiring R✝<VAR>p✝ q r : R✝[X]<VAR>inst✝² : Semiring S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>i : ℤ<GOAL>eval (↑i) (map f p) = f (eval (↑i) p)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasForget₂ C Ab<VAR>inst✝³ : Preadditive C<VAR>inst✝² : (forget₂ C Ab).Additive<VAR>inst✝¹ : (forget₂ C Ab).PreservesHomology<VAR>inst✝ : HasZeroObject C<VAR>S : ShortComplex C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>Epi f ↔ Function.Surjective ⇑((forget₂ C Ab).map f)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasForget₂ C Ab<VAR>inst✝³ : Preadditive C<VAR>inst✝² : (forget₂ C Ab).Additive<VAR>inst✝¹ : (forget₂ C Ab).PreservesHomology<VAR>inst✝ : HasZeroObject C<VAR>S : ShortComplex C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>Epi f ↔ Epi ((forget₂ C Ab).map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j : JordanDecomposition α<VAR>r : ℝ≥0<GOAL>↑r • j = r • j
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>(aleph 1).IsRegular
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>(succ ℵ₀).IsRegular
<VAR>α : Type u<VAR>c' : Cardinal.{u_1}<VAR>c : ℕ∞<GOAL>toPartENat ↑c ≤ toPartENat c' ↔ ↑c ≤ c'
<VAR>n : ℕ<VAR>f : Vector ℕ n →. ℕ<VAR>g : Vector ℕ (n + 1) → ℕ<VAR>hf : Partrec' f<VAR>hg : Partrec' ↑g<GOAL>Partrec' fun v => Part.map (fun a => g (a ::ᵥ v)) (f v)
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f✝ : X✝ ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f✝) g✝<VAR>X : Scheme<VAR>U : X.Opens<VAR>f g : ↑Γ(X, U)<VAR>𝒰 : X.OpenCover<VAR>h : ∀ (i : 𝒰.J), (Scheme.Hom.app (𝒰.map i) U) f = (Scheme.Hom.app (𝒰.map i) U) g<GOAL>f = g
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f✝ : X✝ ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f✝) g✝<VAR>X : Scheme<VAR>U : X.Opens<VAR>f g : ↑Γ(X, U)<VAR>𝒰 : X.OpenCover<VAR>h : ∀ (i : 𝒰.J), (Scheme.Hom.app (𝒰.map i) U) f = (Scheme.Hom.app (𝒰.map i) U) g<GOAL>U ≤ ⨆ i, Hom.opensRange (𝒰.map (𝒰.f i)) ⊓ U
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f✝ : X✝ ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f✝) g✝<VAR>X : Scheme<VAR>U : X.Opens<VAR>f g : ↑Γ(X, U)<VAR>𝒰 : X.OpenCover<VAR>h : ∀ (i : 𝒰.J), (Scheme.Hom.app (𝒰.map i) U) f = (Scheme.Hom.app (𝒰.map i) U) g<GOAL>∀ (i : ↑↑X.toPresheafedSpace), (X.sheaf.val.map (homOfLE ⋯).op) f = (X.sheaf.val.map (homOfLE ⋯).op) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝³ : Monoid M<VAR>inst✝² : Preorder M<VAR>inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l₁ l₂ : List M<VAR>h : l₁ <+ l₂<VAR>h₁ : ∀ a ∈ l₂, 1 ≤ a<GOAL>l₁.prod ≤ l₂.prod
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : Nonempty α<GOAL>BddBelow ∅
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Fintype α<VAR>x : α<VAR>h : Fintype.card α = 1<GOAL>{x} = univ
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Fintype α<VAR>x : α<VAR>h : Fintype.card α = 1<GOAL>univ.card ≤ {x}.card
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Fintype α<VAR>x : α<VAR>h : Fintype.card α = 1<GOAL>univ.card = {x}.card
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<VAR>n : ℕ<GOAL>↑n < o.card ↔ ↑n < o
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<VAR>n : ℕ<GOAL>↑n.succ ≤ o ↔ succ ↑n ≤ o