ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∀ ⦃f g : α → F'⦄ (hf : Memℒp f 1 μ) (hg : Memℒp g 1 μ), Disjoint (Function.support f) (Function.support g) → (fun f => ∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ) (Memℒp.toLp f hf) → (fun f => ∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ) (Memℒp.toLp g hg) → (fun f => ∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ) (Memℒp.toLp f hf + Memℒp.toLp g hg)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>Continuous fun f => ∫ (x : α) in s, ↑↑((condexpL1CLM F' hm μ) f) x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : ↥(Lp F' 1 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>Continuous fun f => ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<GOAL>Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<GOAL>(∀ (y : Ω →ᵇ ℝ≥0), Tendsto (fun i => ((topDualPairing ℝ≥0 (Ω →ᵇ ℝ≥0)) (μs i).toWeakDualBCNN) y) F (𝓝 (((topDualPairing ℝ≥0 (Ω →ᵇ ℝ≥0)) μ.toWeakDualBCNN) y))) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H : IsCoprime (x * y) z<GOAL>IsCoprime y z
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H : IsCoprime (y * x) z<GOAL>IsCoprime y z
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : Presentation R S<VAR>i : P.rels<GOAL>(aeval P.val) (P.relation i) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : Presentation R S<VAR>i : P.rels<GOAL>P.relation i ∈ Ideal.span (Set.range P.relation)
<VAR>a x z✝ z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>Tendsto arg (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
<VAR>a x z✝ z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>Tendsto (fun x => Real.arcsin ((-x).im / abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
<VAR>a x z✝ z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>𝓝 (-π) = 𝓝 ((Real.arcsin ∘ (im ∘ Neg.neg / ⇑abs)) z - π)
<VAR>a x z✝ z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>abs z ≠ 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>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<VAR>N₂ : LieSubmodule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf : f.ker = ⊥<GOAL>comap f (map f N) = N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>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<VAR>N₂ : LieSubmodule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf : f.ker = ⊥<GOAL>↑(comap f (map f N)) = ↑N
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : NonAssocSemiring R<VAR>inst✝¹ : NonAssocSemiring S<VAR>ϕ : R →+* S<VAR>inst✝ : CharZero S<VAR>a b : ℕ<VAR>h : ↑a = ↑b<GOAL>↑a = ↑b
<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>S : Type u_5<VAR>S₂ : Type u_6<VAR>M : Type u_7<VAR>N : Type u_8<VAR>P : Type u_9<VAR>Rₗ : Type u_10<VAR>Mₗ : Type u_11<VAR>Nₗ : Type u_12<VAR>Pₗ : Type u_13<VAR>inst✝¹⁸ : Semiring R<VAR>inst✝¹⁷ : Semiring S<VAR>inst✝¹⁶ : Semiring R₂<VAR>inst✝¹⁵ : Semiring S₂<VAR>inst✝¹⁴ : CommSemiring Rₗ<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Mₗ<VAR>inst✝⁹ : AddCommMonoid Nₗ<VAR>inst✝⁸ : AddCommMonoid Pₗ<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module S N<VAR>inst✝⁵ : Module R₂ P<VAR>inst✝⁴ : Module S₂ P<VAR>inst✝³ : Module Rₗ Mₗ<VAR>inst✝² : Module Rₗ Nₗ<VAR>inst✝¹ : Module Rₗ Pₗ<VAR>inst✝ : SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>b₁ : Basis ι₁ R M<VAR>b₂ : Basis ι₂ S N<VAR>b₁' : Basis ι₁ Rₗ Mₗ<VAR>b₂' : Basis ι₂ Rₗ Nₗ<VAR>B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<VAR>x : M<VAR>y : N<GOAL>((b₁.repr x).sum fun i xi => (b₂.repr y).sum fun j yj => ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) = (B x) y
<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>S : Type u_5<VAR>S₂ : Type u_6<VAR>M : Type u_7<VAR>N : Type u_8<VAR>P : Type u_9<VAR>Rₗ : Type u_10<VAR>Mₗ : Type u_11<VAR>Nₗ : Type u_12<VAR>Pₗ : Type u_13<VAR>inst✝¹⁸ : Semiring R<VAR>inst✝¹⁷ : Semiring S<VAR>inst✝¹⁶ : Semiring R₂<VAR>inst✝¹⁵ : Semiring S₂<VAR>inst✝¹⁴ : CommSemiring Rₗ<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Mₗ<VAR>inst✝⁹ : AddCommMonoid Nₗ<VAR>inst✝⁸ : AddCommMonoid Pₗ<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module S N<VAR>inst✝⁵ : Module R₂ P<VAR>inst✝⁴ : Module S₂ P<VAR>inst✝³ : Module Rₗ Mₗ<VAR>inst✝² : Module Rₗ Nₗ<VAR>inst✝¹ : Module Rₗ Pₗ<VAR>inst✝ : SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>b₁ : Basis ι₁ R M<VAR>b₂ : Basis ι₂ S N<VAR>b₁' : Basis ι₁ Rₗ Mₗ<VAR>b₂' : Basis ι₂ Rₗ Nₗ<VAR>B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<VAR>x : M<VAR>y : N<GOAL>((b₁.repr x).sum fun i xi => (b₂.repr y).sum fun j yj => ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) = (B ((Finsupp.total ι₁ M R ⇑b₁) (b₁.repr x))) ((Finsupp.total ι₂ N S ⇑b₂) (b₂.repr y))
<VAR>k : Type u<VAR>inst✝⁶ : Field k<VAR>F : Type u_1<VAR>K : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field A<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra F A<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>L : IntermediateField F A<VAR>hL : ∀ (x : K), Splits (algebraMap F ↥L) (minpoly F x)<VAR>f : K →ₐ[F] A<VAR>x : K<GOAL>Splits (algebraMap F ↥L) (minpoly F (f x))
<VAR>k : Type u<VAR>inst✝⁶ : Field k<VAR>F : Type u_1<VAR>K : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field A<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra F A<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>L : IntermediateField F A<VAR>hL : ∀ (x : K), Splits (algebraMap F ↥L) (minpoly F x)<VAR>f : K →ₐ[F] A<VAR>x : K<GOAL>Splits (algebraMap F ↥L) (minpoly F x)
<VAR>R : Type u<VAR>a✝ b✝ : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q : R[X]<VAR>S : Type u_1<VAR>inst✝ : SMulZeroClass S R<VAR>a : S<VAR>n : ℕ<VAR>b : R<GOAL>a • Finsupp.single n b = Finsupp.single n (a • b)
<VAR>n : ℤ<VAR>hn : n % 4 = 3<GOAL>χ₄ ↑n = -1
<VAR>n : ℤ<VAR>hn : n % 4 = 3<GOAL>χ₄ ↑3 = -1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : OrderedSemiring 𝕜<VAR>inst✝⁴ : AddCommMonoid E<VAR>inst✝³ : AddCommMonoid F<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : Module 𝕜 β<VAR>s : Set E<VAR>f g : E → β<GOAL>ConcaveOn 𝕜 s (-f) ↔ ConvexOn 𝕜 s f
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : AddCommGroup N<VAR>inst✝¹⁰ : AddCommGroup P<VAR>inst✝⁹ : AddCommGroup Q<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R N<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : Module R Q<VAR>inst✝⁴ : Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Free R N<VAR>inst✝¹ : Module.Finite R N<VAR>inst✝ : Nontrivial R<GOAL>↑(rTensorHomEquivHomRTensor R M P Q) = rTensorHomToHomRTensor R M P Q
<VAR>L : Language<VAR>κ : Cardinal.{w}<VAR>T : L.Theory<VAR>h : κ.Categorical T<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>hS : T.IsSatisfiable<VAR>hT : ∀ (M : T.ModelType), Infinite ↑M<VAR>φ : L.Sentence<GOAL>T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
<VAR>L : Language<VAR>κ : Cardinal.{w}<VAR>T : L.Theory<VAR>h : κ.Categorical T<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>hS : T.IsSatisfiable<VAR>hT : ∀ (M : T.ModelType), Infinite ↑M<VAR>φ : L.Sentence<VAR>w✝ : T.ModelType<VAR>h✝ : #↑w✝ = κ<GOAL>T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
<VAR>L : Language<VAR>κ : Cardinal.{w}<VAR>T : L.Theory<VAR>h : κ.Categorical T<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>hS : T.IsSatisfiable<VAR>hT : ∀ (M : T.ModelType), Infinite ↑M<VAR>φ : L.Sentence<VAR>w✝ : T.ModelType<VAR>h✝ : #↑w✝ = κ<GOAL>(∀ (M : T.ModelType), ↑M ⊨ φ) ∨ ∀ (M : T.ModelType), ↑M ⊨ Formula.not φ
<VAR>L : Language<VAR>κ : Cardinal.{w}<VAR>T : L.Theory<VAR>h : κ.Categorical T<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>hS : T.IsSatisfiable<VAR>hT : ∀ (M : T.ModelType), Infinite ↑M<VAR>φ : L.Sentence<VAR>w✝ : T.ModelType<VAR>h✝ : #↑w✝ = κ<VAR>con : (∃ M, ¬↑M ⊨ φ) ∧ ∃ M, ¬↑M ⊨ Formula.not φ<GOAL>False
<VAR>L : Language<VAR>κ : Cardinal.{w}<VAR>T : L.Theory<VAR>h : κ.Categorical T<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>hS : T.IsSatisfiable<VAR>hT : ∀ (M : T.ModelType), Infinite ↑M<VAR>φ : L.Sentence<VAR>w✝ : T.ModelType<VAR>h✝ : #↑w✝ = κ<VAR>MF : T.ModelType<VAR>hMF : ¬↑MF ⊨ φ<VAR>MT : T.ModelType<VAR>hMT : ¬↑MT ⊨ Formula.not φ<GOAL>False
<VAR>L : Language<VAR>κ : Cardinal.{w}<VAR>T : L.Theory<VAR>h : κ.Categorical T<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>hS : T.IsSatisfiable<VAR>hT : ∀ (M : T.ModelType), Infinite ↑M<VAR>φ : L.Sentence<VAR>w✝ : T.ModelType<VAR>h✝ : #↑w✝ = κ<VAR>MF : T.ModelType<VAR>hMF : ¬↑MF ⊨ φ<VAR>MT : T.ModelType<VAR>hMT : ↑MT ⊨ φ<GOAL>False
<VAR>L : Language<VAR>κ : Cardinal.{w}<VAR>T : L.Theory<VAR>h : κ.Categorical T<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>hS : T.IsSatisfiable<VAR>hT : ∀ (M : T.ModelType), Infinite ↑M<VAR>φ : L.Sentence<VAR>w✝ : T.ModelType<VAR>h✝ : #↑w✝ = κ<VAR>MF : T.ModelType<VAR>hMF : ¬↑MF ⊨ φ<VAR>MT : T.ModelType<VAR>hMT : ↑MT ⊨ φ<VAR>this✝ : Infinite ↑MT<VAR>this : Infinite ↑MF<GOAL>↑MF ⊨ φ
<VAR>L : Language<VAR>κ : Cardinal.{w}<VAR>T : L.Theory<VAR>h : κ.Categorical T<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>hS : T.IsSatisfiable<VAR>hT : ∀ (M : T.ModelType), Infinite ↑M<VAR>φ : L.Sentence<VAR>w✝ : T.ModelType<VAR>h✝ : #↑w✝ = κ<VAR>MF : T.ModelType<VAR>hMF : ¬↑MF ⊨ φ<VAR>MT : T.ModelType<VAR>hMT : ↑MT ⊨ φ<VAR>this✝ : Infinite ↑MT<VAR>this : Infinite ↑MF<VAR>NT : Bundled L.Structure<VAR>MNT : ↑MT ≅[L] ↑NT<VAR>hNT : #↑NT = κ<GOAL>↑MF ⊨ φ
<VAR>L : Language<VAR>κ : Cardinal.{w}<VAR>T : L.Theory<VAR>h : κ.Categorical T<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>hS : T.IsSatisfiable<VAR>hT : ∀ (M : T.ModelType), Infinite ↑M<VAR>φ : L.Sentence<VAR>w✝ : T.ModelType<VAR>h✝ : #↑w✝ = κ<VAR>MF : T.ModelType<VAR>hMF : ¬↑MF ⊨ φ<VAR>MT : T.ModelType<VAR>hMT : ↑MT ⊨ φ<VAR>this✝ : Infinite ↑MT<VAR>this : Infinite ↑MF<VAR>NT : Bundled L.Structure<VAR>MNT : ↑MT ≅[L] ↑NT<VAR>hNT : #↑NT = κ<VAR>NF : Bundled L.Structure<VAR>MNF : ↑MF ≅[L] ↑NF<VAR>hNF : #↑NF = κ<GOAL>↑MF ⊨ φ
<VAR>L : Language<VAR>κ : Cardinal.{w}<VAR>T : L.Theory<VAR>h : κ.Categorical T<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>hS : T.IsSatisfiable<VAR>hT : ∀ (M : T.ModelType), Infinite ↑M<VAR>φ : L.Sentence<VAR>w✝ : T.ModelType<VAR>h✝ : #↑w✝ = κ<VAR>MF : T.ModelType<VAR>hMF : ¬↑MF ⊨ φ<VAR>MT : T.ModelType<VAR>hMT : ↑MT ⊨ φ<VAR>this✝ : Infinite ↑MT<VAR>this : Infinite ↑MF<VAR>NT : Bundled L.Structure<VAR>MNT : ↑MT ≅[L] ↑NT<VAR>hNT : #↑NT = κ<VAR>NF : Bundled L.Structure<VAR>MNF : ↑MF ≅[L] ↑NF<VAR>hNF : #↑NF = κ<VAR>TF : ↑(ElementarilyEquivalent.toModel T MNT) ≃[L] ↑(ElementarilyEquivalent.toModel T MNF)<GOAL>↑MF ⊨ φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : SuccOrder α<VAR>a b : α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : NoMaxOrder α<GOAL>a < succ ⊥ ↔ a = ⊥
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a b : R<VAR>S : Type v<VAR>x✝ y x : R<GOAL>(mk (span {x})) x = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℤ<VAR>this : ‖↑k‖ < 1 ↔ ↑p ∣ k<GOAL>‖↑k‖ < 1 ↔ ↑p ∣ k
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : Module R M✝<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>T : Type u_5<VAR>inst✝⁵ : AddCommGroup T<VAR>inst✝⁴ : Module (AdicCompletion I R) T<VAR>ι : Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>M : ι → Type u_7<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>x : AdicCompletion I (Fin n → R)<GOAL>(piEquivFin I n) x = (pi I fun x => R) x
<VAR>a : UnitAddCircle<VAR>x : ℝ<GOAL>evenKernel (-a) x = evenKernel a x
<VAR>x a' : ℝ<GOAL>evenKernel (-↑a') x = evenKernel (↑a') x
<VAR>n m : ℕ<VAR>α : Sort u_1<VAR>k : ℕ<VAR>f g : Fin k → α<GOAL>HEq f g ↔ ∀ (i : Fin k), f i = g ⟨↑i, ⋯⟩
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<VAR>M : T.ModelType<VAR>v : α → ↑M<VAR>xs : Fin n → ↑M<GOAL>(φ ⟹ ψ ⇔ ∼φ ⊔ ψ).Realize v xs
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<GOAL>(matrixToStdBasis K).det = ∏ _k : { w // w.IsComplex }, (2⁻¹ • !![1, 1; -I, I]).det
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<GOAL>∏ _k : { w // w.IsComplex }, (2⁻¹ • !![1, 1; -I, I]).det = ∏ _k : { w // w.IsComplex }, 2⁻¹ * I
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x✝¹ : { w // w.IsComplex }<VAR>x✝ : x✝¹ ∈ univ<GOAL>(2⁻¹ • !![1, 1; -I, I]).det = 2⁻¹ * I
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<GOAL>∏ _k : { w // w.IsComplex }, 2⁻¹ * I = (2⁻¹ * I) ^ Fintype.card { w // w.IsComplex }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝⁶ : SemilatticeSup β<VAR>inst✝⁵ : OrderBot β<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderClosedTopology β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>i : ℕ → β<VAR>f : α → β<VAR>n : ℕ<VAR>a : α<VAR>hf : Measurable f<GOAL>↑((Finset.range n).sup fun k => (const α (i k)).restrict {a | i k ≤ f a}) a = (Finset.range n).sup fun k => if i k ≤ f a then i k else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝⁶ : SemilatticeSup β<VAR>inst✝⁵ : OrderBot β<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderClosedTopology β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>i : ℕ → β<VAR>f : α → β<VAR>n : ℕ<VAR>a : α<VAR>hf : Measurable f<GOAL>((Finset.range n).sup fun c => ↑((const α (i c)).restrict {a | i c ≤ f a}) a) = (Finset.range n).sup fun k => if i k ≤ f a then i k else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝⁶ : SemilatticeSup β<VAR>inst✝⁵ : OrderBot β<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderClosedTopology β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>i : ℕ → β<VAR>f : α → β<VAR>n : ℕ<VAR>a : α<VAR>hf : Measurable f<GOAL>(fun c => ↑((const α (i c)).restrict {a | i c ≤ f a}) a) = fun k => if i k ≤ f a then i k else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝⁶ : SemilatticeSup β<VAR>inst✝⁵ : OrderBot β<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderClosedTopology β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>i : ℕ → β<VAR>f : α → β<VAR>n : ℕ<VAR>a : α<VAR>hf : Measurable f<VAR>k : ℕ<GOAL>↑((const α (i k)).restrict {a | i k ≤ f a}) a = if i k ≤ f a then i k else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝⁶ : SemilatticeSup β<VAR>inst✝⁵ : OrderBot β<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderClosedTopology β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>i : ℕ → β<VAR>f : α → β<VAR>n : ℕ<VAR>a : α<VAR>hf : Measurable f<VAR>k : ℕ<GOAL>{a | i k ≤ f a}.indicator (↑(const α (i k))) a = if i k ≤ f a then i k else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝⁶ : SemilatticeSup β<VAR>inst✝⁵ : OrderBot β<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderClosedTopology β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : OpensMeasurableSpace β<VAR>i : ℕ → β<VAR>f : α → β<VAR>n : ℕ<VAR>a : α<VAR>hf : Measurable f<VAR>k : ℕ<GOAL>MeasurableSet {a | i k ≤ f a}
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>B A₁ : C<VAR>f : A₁ ⟶ B<VAR>inst✝ : Mono f<VAR>X Y : Subobject B<VAR>h₁ : mk f ≤ X<VAR>h₂ : X ≤ Y<GOAL>ofMkLE f X h₁ ≫ X.ofLE Y h₂ = ofMkLE f Y ⋯
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>B A₁ : C<VAR>f : A₁ ⟶ B<VAR>inst✝ : Mono f<VAR>X Y : Subobject B<VAR>h₁ : mk f ≤ X<VAR>h₂ : X ≤ Y<GOAL>(underlyingIso f).inv ≫ underlying.map (h₁.hom ≫ h₂.hom) = (underlyingIso f).inv ≫ underlying.map ⋯.hom
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : FirstCountableTopology X<VAR>ν : Measure α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → E<VAR>a : α<GOAL>∫ (x : α), f a ∂Measure.dirac a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>f g f' : α →ₘ[μ] β<VAR>hf : f ≤ f'<VAR>hg : g ≤ f'<GOAL>f ⊔ g ≤ f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>f g f' : α →ₘ[μ] β<VAR>hf : ↑f ≤ᶠ[ae μ] ↑f'<VAR>hg : ↑g ≤ᶠ[ae μ] ↑f'<GOAL>↑(f ⊔ g) ≤ᶠ[ae μ] ↑f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>f g f' : α →ₘ[μ] β<VAR>hf : ↑f ≤ᶠ[ae μ] ↑f'<VAR>hg : ↑g ≤ᶠ[ae μ] ↑f'<VAR>a✝ : α<VAR>haf : ↑f a✝ ≤ ↑f' a✝<VAR>hag : ↑g a✝ ≤ ↑f' a✝<VAR>ha_sup : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝<GOAL>↑(f ⊔ g) a✝ ≤ ↑f' a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>f g f' : α →ₘ[μ] β<VAR>hf : ↑f ≤ᶠ[ae μ] ↑f'<VAR>hg : ↑g ≤ᶠ[ae μ] ↑f'<VAR>a✝ : α<VAR>haf : ↑f a✝ ≤ ↑f' a✝<VAR>hag : ↑g a✝ ≤ ↑f' a✝<VAR>ha_sup : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝<GOAL>↑f a✝ ⊔ ↑g a✝ ≤ ↑f' a✝
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>α : E<VAR>S : Set E<VAR>x : E<VAR>hx : x ∈ adjoin F S<GOAL>∃ T, ↑T ⊆ S ∧ x ∈ adjoin F ↑T
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>α : E<VAR>S : Set E<VAR>x : E<VAR>hx : x ∈ ⨆ i, F⟮↑i⟯<GOAL>∃ T, ↑T ⊆ S ∧ x ∈ adjoin F ↑T
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>α : E<VAR>S : Set E<VAR>x : E<VAR>hx : x ∈ ⨆ i, F⟮↑i⟯<VAR>s : Finset ↑S<VAR>hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯<GOAL>∃ T, ↑T ⊆ S ∧ x ∈ adjoin F ↑T
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>α : E<VAR>S : Set E<VAR>x : E<VAR>hx : x ∈ ⨆ i, F⟮↑i⟯<VAR>s : Finset ↑S<VAR>hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯<GOAL>⨆ i ∈ s, F⟮↑i⟯ ≤ adjoin F ↑(Finset.image Subtype.val s)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>α : E<VAR>S : Set E<VAR>x : E<VAR>hx : x ∈ ⨆ i, F⟮↑i⟯<VAR>s : Finset ↑S<VAR>hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯<GOAL>∀ i ∈ s, {↑i} ≤ ↑(adjoin F (Subtype.val '' ↑s))
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>α : E<VAR>S : Set E<VAR>x : E<VAR>hx : x ∈ ⨆ i, F⟮↑i⟯<VAR>s : Finset ↑S<VAR>hx' : x ∈ ⨆ i ∈ s, F⟮↑i⟯<VAR>i✝ : ↑S<VAR>h : i✝ ∈ s<GOAL>↑i✝ ∈ ↑(adjoin F (Subtype.val '' ↑s))
<VAR>u v : Level<VAR>n nn n' : ℕ<VAR>pn : NormNum.IsNat n nn<VAR>pn' : nn = n'.succ<GOAL>Finset.range n = Finset.cons n' (Finset.range n') ⋯
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>E : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<GOAL>dimH univ = 1