ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>s : Set (γ × β)<VAR>hs : MeasurableSet s<GOAL>(κ.swapRight a) s = (κ a) {p | p.swap ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>s : Set (γ × β)<VAR>hs : MeasurableSet s<GOAL>(κ a) (Prod.swap ⁻¹' s) = (κ a) {p | p.swap ∈ s}
<VAR>k n m : Nat<VAR>H1 : k.Coprime n<VAR>H2 : k ∣ m * n<GOAL>k ∣ m
<VAR>k n m : Nat<VAR>H1 : k.Coprime n<VAR>H2 : k ∣ m * n<VAR>t : k ∣ (m * k).gcd (m * n) := dvd_gcd (Nat.dvd_mul_left k m) H2<GOAL>k ∣ m
<VAR>x✝ y✝ x y : ℝ<GOAL>√x / x = (√x)⁻¹
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>P' : Type uP'<VAR>Q' : Type uQ'<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : Semiring A<VAR>inst✝²⁹ : Semiring B<VAR>inst✝²⁸ : Algebra R A<VAR>inst✝²⁷ : Algebra R B<VAR>inst✝²⁶ : AddCommMonoid M<VAR>inst✝²⁵ : Module R M<VAR>inst✝²⁴ : Module A M<VAR>inst✝²³ : Module B M<VAR>inst✝²² : IsScalarTower R A M<VAR>inst✝²¹ : IsScalarTower R B M<VAR>inst✝²⁰ : SMulCommClass A B M<VAR>inst✝¹⁹ : AddCommMonoid N<VAR>inst✝¹⁸ : Module R N<VAR>inst✝¹⁷ : AddCommMonoid P<VAR>inst✝¹⁶ : Module R P<VAR>inst✝¹⁵ : Module A P<VAR>inst✝¹⁴ : Module B P<VAR>inst✝¹³ : IsScalarTower R A P<VAR>inst✝¹² : IsScalarTower R B P<VAR>inst✝¹¹ : SMulCommClass A B P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : Module R Q<VAR>inst✝⁸ : AddCommMonoid P'<VAR>inst✝⁷ : Module R P'<VAR>inst✝⁶ : Module A P'<VAR>inst✝⁵ : Module B P'<VAR>inst✝⁴ : IsScalarTower R A P'<VAR>inst✝³ : IsScalarTower R B P'<VAR>inst✝² : SMulCommClass A B P'<VAR>inst✝¹ : AddCommMonoid Q'<VAR>inst✝ : Module R Q'<VAR>x✝¹ x✝ : M →ₗ[A] N →ₗ[R] P<VAR>x : M<VAR>y : N<GOAL>(lift (x✝¹ + x✝)) (x ⊗ₜ[R] y) = (lift x✝¹ + lift x✝) (x ⊗ₜ[R] y)
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>P' : Type uP'<VAR>Q' : Type uQ'<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : Semiring A<VAR>inst✝²⁹ : Semiring B<VAR>inst✝²⁸ : Algebra R A<VAR>inst✝²⁷ : Algebra R B<VAR>inst✝²⁶ : AddCommMonoid M<VAR>inst✝²⁵ : Module R M<VAR>inst✝²⁴ : Module A M<VAR>inst✝²³ : Module B M<VAR>inst✝²² : IsScalarTower R A M<VAR>inst✝²¹ : IsScalarTower R B M<VAR>inst✝²⁰ : SMulCommClass A B M<VAR>inst✝¹⁹ : AddCommMonoid N<VAR>inst✝¹⁸ : Module R N<VAR>inst✝¹⁷ : AddCommMonoid P<VAR>inst✝¹⁶ : Module R P<VAR>inst✝¹⁵ : Module A P<VAR>inst✝¹⁴ : Module B P<VAR>inst✝¹³ : IsScalarTower R A P<VAR>inst✝¹² : IsScalarTower R B P<VAR>inst✝¹¹ : SMulCommClass A B P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : Module R Q<VAR>inst✝⁸ : AddCommMonoid P'<VAR>inst✝⁷ : Module R P'<VAR>inst✝⁶ : Module A P'<VAR>inst✝⁵ : Module B P'<VAR>inst✝⁴ : IsScalarTower R A P'<VAR>inst✝³ : IsScalarTower R B P'<VAR>inst✝² : SMulCommClass A B P'<VAR>inst✝¹ : AddCommMonoid Q'<VAR>inst✝ : Module R Q'<VAR>x✝¹ : B<VAR>x✝ : M →ₗ[A] N →ₗ[R] P<VAR>x : M<VAR>y : N<GOAL>({ toFun := lift, map_add' := ⋯ }.toFun (x✝¹ • x✝)) (x ⊗ₜ[R] y) = ((RingHom.id B) x✝¹ • { toFun := lift, map_add' := ⋯ }.toFun x✝) (x ⊗ₜ[R] y)
<VAR>m n : ℤ<VAR>hne : m ≠ n<GOAL>1 ≤ dist m n
<VAR>m n : ℤ<VAR>hne : m ≠ n<GOAL>1 ≤ |↑m - ↑n|
<VAR>m n : ℤ<VAR>hne : m ≠ n<GOAL>1 ≤ |m - n|
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>inst✝¹² : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M✝ : Type uM<VAR>inst✝⁸ : TopologicalSpace M✝<VAR>inst✝⁷ : ChartedSpace H M✝<VAR>inst✝⁶ : SmoothManifoldWithCorners I M✝<VAR>inst✝⁵ : SigmaCompactSpace M✝<VAR>inst✝⁴ : T2Space M✝<VAR>t : M✝ → Set F<VAR>n : ℕ∞<VAR>M : Type u_1<VAR>inst✝³ : MetricSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : SigmaCompactSpace M<VAR>K U : ι → Set M<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<GOAL>∃ δ, (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x (δ x) ⊆ U i
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>inst✝¹² : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M✝ : Type uM<VAR>inst✝⁸ : TopologicalSpace M✝<VAR>inst✝⁷ : ChartedSpace H M✝<VAR>inst✝⁶ : SmoothManifoldWithCorners I M✝<VAR>inst✝⁵ : SigmaCompactSpace M✝<VAR>inst✝⁴ : T2Space M✝<VAR>t : M✝ → Set F<VAR>n : ℕ∞<VAR>M : Type u_1<VAR>inst✝³ : MetricSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : SigmaCompactSpace M<VAR>K U : ι → Set M<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>δ : C^⊤⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯<VAR>hδ0 : ∀ (x : M), 0 < δ x<VAR>hδ : ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i<GOAL>∃ δ, (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x (δ x) ⊆ U i
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>inst✝¹² : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M✝ : Type uM<VAR>inst✝⁸ : TopologicalSpace M✝<VAR>inst✝⁷ : ChartedSpace H M✝<VAR>inst✝⁶ : SmoothManifoldWithCorners I M✝<VAR>inst✝⁵ : SigmaCompactSpace M✝<VAR>inst✝⁴ : T2Space M✝<VAR>t : M✝ → Set F<VAR>n : ℕ∞<VAR>M : Type u_1<VAR>inst✝³ : MetricSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : SigmaCompactSpace M<VAR>K U : ι → Set M<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>δ : C^⊤⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯<VAR>hδ0 : ∀ (x : M), 0 < δ x<VAR>hδ : ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i<VAR>i : ι<VAR>x : M<VAR>hx : x ∈ K i<GOAL>closedBall x (δ x) ⊆ U i
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>inst✝¹² : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M✝ : Type uM<VAR>inst✝⁸ : TopologicalSpace M✝<VAR>inst✝⁷ : ChartedSpace H M✝<VAR>inst✝⁶ : SmoothManifoldWithCorners I M✝<VAR>inst✝⁵ : SigmaCompactSpace M✝<VAR>inst✝⁴ : T2Space M✝<VAR>t : M✝ → Set F<VAR>n : ℕ∞<VAR>M : Type u_1<VAR>inst✝³ : MetricSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : SigmaCompactSpace M<VAR>K U : ι → Set M<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>δ : C^⊤⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯<VAR>hδ0 : ∀ (x : M), 0 < δ x<VAR>hδ : ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i<VAR>i : ι<VAR>x : M<VAR>hx : x ∈ K i<GOAL>EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>ι : Type u_2<VAR>l : Filter ι<VAR>f : ι → Set α<VAR>x : α<GOAL>Tendsto f l (v.filterAt x) ↔ (∀ᶠ (i : ι) in l, f i ∈ v.setsAt x) ∧ ∀ ε > 0, ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>n : ℕ<GOAL>(X ^ n).natSepDegree = if n = 0 then 0 else 1
<VAR>a✝ b✝ c✝ d : Ordinal.{u}<VAR>a b c : Ordinal.{u_1}<GOAL>a ⨳ (b ♯ c) = a ⨳ b ♯ a ⨳ c
<VAR>a✝ b✝ c✝ d✝ : Ordinal.{u}<VAR>a b c a' : Ordinal.{u_1}<VAR>ha : a' < a<VAR>d : Ordinal.{u_1}<VAR>hd : d < b ♯ c<GOAL>a' ⨳ (b ♯ c) ♯ a ⨳ d < a ⨳ b ♯ a ⨳ c ♯ a' ⨳ d
<VAR>a✝ b✝ c✝ d✝ : Ordinal.{u}<VAR>a b c d : Ordinal.{u_1}<VAR>hd : d < a ⨳ b<GOAL>d ♯ a ⨳ c < a ⨳ (b ♯ c)
<VAR>a✝ b✝ c✝ d✝ : Ordinal.{u}<VAR>a b c d : Ordinal.{u_1}<VAR>hd : d < a ⨳ c<GOAL>a ⨳ b ♯ d < a ⨳ (b ♯ c)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α✝<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α✝<VAR>α : Type u_3<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s<GOAL>s.OrdConnected
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α✝<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α✝<VAR>α : Type u_3<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s<GOAL>∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α✝<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α✝<VAR>α : Type u_3<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>hxy : x ≤ y<GOAL>Icc x y ⊆ s
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α✝<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α✝<VAR>α : Type u_3<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s<VAR>x : α<VAR>hx hy : x ∈ s<VAR>hxy : x ≤ x<GOAL>Icc x x ⊆ s
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α✝<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α✝<VAR>α : Type u_3<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>hxy : x ≤ y<VAR>hxy' : x < y<GOAL>Icc x y ⊆ s
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α✝<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α✝<VAR>α : Type u_3<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>hxy : x ≤ y<VAR>hxy' : x < y<GOAL>insert x (insert y (Ioo x y)) ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝ : Preorder β<VAR>K : Set α<VAR>h₁ : IsComplete K<VAR>u : β → α<VAR>h₂ : ∀ (n : β), u n ∈ K<VAR>h₃ : CauchySeq u<GOAL>u '' univ ⊆ K
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<GOAL>(M ↾ R).Basis' I X ↔ M.Basis' I (X ∩ R) ∧ I ⊆ R
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<GOAL>(((M.Indep I ∧ I ⊆ R) ∧ I ⊆ X) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ R → y ⊆ X → I ⊆ y → I = y) ↔ ((M.Indep I ∧ I ⊆ X ∧ I ⊆ R) ∧ ∀ ⦃y : Set α⦄, M.Indep y → y ⊆ X → y ⊆ R → I ⊆ y → I = y) ∧ I ⊆ R
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>s * closure {1} = s
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>∀ (U : Set G), IsOpen U → (fun t => t • closure {1} = t) U
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>∀ (t : Set G), MeasurableSet t → (fun t => t • closure {1} = t) t → (fun t => t • closure {1} = t) tᶜ
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>∀ (f : ℕ → Set G), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), (fun t => t • closure {1} = t) (f i)) → (fun t => t • closure {1} = t) (⋃ i, f i)
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w'<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : Nonempty M<VAR>κ : Cardinal.{w}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>h3 : lift.{w', w} κ ≤ lift.{w, w'} #M<GOAL>∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w'<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : Nonempty M<VAR>κ : Cardinal.{w}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>h3 : lift.{w', w} κ ≤ lift.{w, w'} #M<VAR>S : L.ElementarySubstructure M<VAR>left✝ : ∅ ⊆ ↑S<VAR>hS : lift.{w, w'} #↥S = lift.{w', w} κ<GOAL>∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w'<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : Nonempty M<VAR>κ : Cardinal.{w}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>h3 : lift.{w', w} κ ≤ lift.{w, w'} #M<VAR>S : L.ElementarySubstructure M<VAR>left✝ : ∅ ⊆ ↑S<VAR>hS : lift.{w, w'} #↥S = lift.{w', w} κ<VAR>this : Small.{w, w'} ↥S<GOAL>∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w'<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : Nonempty M<VAR>κ : Cardinal.{w}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>h3 : lift.{w', w} κ ≤ lift.{w, w'} #M<VAR>S : L.ElementarySubstructure M<VAR>left✝ : ∅ ⊆ ↑S<VAR>hS : lift.{w, w'} #↥S = lift.{w', w} κ<VAR>this : Small.{w, w'} ↥S<GOAL>lift.{w', w} #↑(Equiv.bundledInduced L (equivShrink ↥S)) = lift.{w, w'} #↥S
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>α : Type u_5<VAR>E : α → Type u_4<GOAL>IsEmpty (Sigma E) ↔ ∀ (a : α), IsEmpty (E a)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<GOAL>2 * ↑π * I ≠ 0
<VAR>α : Type u<VAR>c : Cardinal.{u_1}<GOAL>toPartENat c = ⊤ ↔ ℵ₀ ≤ c
<VAR>α : Type u<VAR>c : Cardinal.{u_1}<GOAL>↑(toENat c) = PartENat.withTopEquiv.symm ⊤ ↔ PartENat.withTopEquiv.symm (toENat c) = PartENat.withTopEquiv.symm ⊤
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>t : Triangle ℝ P<VAR>p : P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h : 2 • ∡ (t.points i₁) p (t.points i₃) = 2 • ∡ (t.points i₁) (t.points i₂) (t.points i₃)<VAR>t'p : Fin 3 → P := Function.update t.points i₂ p<VAR>h₁ : t'p i₁ = t.points i₁<VAR>h₂ : t'p i₂ = p<GOAL>p ∈ Simplex.circumsphere t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>t : Triangle ℝ P<VAR>p : P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h : 2 • ∡ (t.points i₁) p (t.points i₃) = 2 • ∡ (t.points i₁) (t.points i₂) (t.points i₃)<VAR>t'p : Fin 3 → P := Function.update t.points i₂ p<VAR>h₁ : t'p i₁ = t.points i₁<VAR>h₂ : t'p i₂ = p<VAR>h₃ : t'p i₃ = t.points i₃<GOAL>p ∈ Simplex.circumsphere t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>t : Triangle ℝ P<VAR>p : P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h : 2 • ∡ (t.points i₁) p (t.points i₃) = 2 • ∡ (t.points i₁) (t.points i₂) (t.points i₃)<VAR>t'p : Fin 3 → P := Function.update t.points i₂ p<VAR>h₁ : t'p i₁ = t.points i₁<VAR>h₂ : t'p i₂ = p<VAR>h₃ : t'p i₃ = t.points i₃<VAR>ha : AffineIndependent ℝ t'p<GOAL>p ∈ Simplex.circumsphere t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>t : Triangle ℝ P<VAR>p : P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h : 2 • ∡ (t.points i₁) p (t.points i₃) = 2 • ∡ (t.points i₁) (t.points i₂) (t.points i₃)<VAR>t'p : Fin 3 → P := Function.update t.points i₂ p<VAR>h₁ : t'p i₁ = t.points i₁<VAR>h₂ : t'p i₂ = p<VAR>h₃ : t'p i₃ = t.points i₃<VAR>ha : AffineIndependent ℝ t'p<VAR>t' : Triangle ℝ P := { points := t'p, independent := ha }<VAR>h₁' : t'.points i₁ = t.points i₁<VAR>h₂' : t'.points i₂ = p<VAR>h₃' : t'.points i₃ = t.points i₃<VAR>h' : 2 • ∡ (t'.points i₁) (t'.points i₂) (t'.points i₃) = 2 • ∡ (t.points i₁) (t.points i₂) (t.points i₃)<GOAL>p ∈ Simplex.circumsphere t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>t : Triangle ℝ P<VAR>p : P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h : 2 • ∡ (t.points i₁) p (t.points i₃) = 2 • ∡ (t.points i₁) (t.points i₂) (t.points i₃)<VAR>t'p : Fin 3 → P := Function.update t.points i₂ p<VAR>h₁ : t'p i₁ = t.points i₁<VAR>h₂ : t'p i₂ = p<VAR>h₃ : t'p i₃ = t.points i₃<VAR>ha : AffineIndependent ℝ t'p<VAR>t' : Triangle ℝ P := { points := t'p, independent := ha }<VAR>h₁' : t'.points i₁ = t.points i₁<VAR>h₂' : t'.points i₂ = p<VAR>h₃' : t'.points i₃ = t.points i₃<VAR>h' : 2 • ∡ (t'.points i₁) (t'.points i₂) (t'.points i₃) = 2 • ∡ (t.points i₁) (t.points i₂) (t.points i₃)<GOAL>t'.points i₂ ∈ Simplex.circumsphere t'
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>W.addXYZ P Q = addZ P Q • ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), 1]
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<VAR>hZ : ∀ {n : ℕ}, IsUnit (addZ P Q ^ n)<GOAL>W.addXYZ P Q = addZ P Q • ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), 1]
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M' : Type u_3<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : Subsingleton M<VAR>x✝ : Ideal R<GOAL>x✝ ∈ associatedPrimes R M ↔ x✝ ∈ ∅
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M' : Type u_3<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : Subsingleton M<VAR>x✝ : Ideal R<GOAL>x✝ ∉ associatedPrimes R M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f g s t : ι → α<VAR>a b : α<VAR>u : ℕ → α<GOAL>u 0 ⊔ ⨆ i, u (i + 1) = ⨆ x ∈ {0} ∪ range Nat.succ, u x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f g s t : ι → α<VAR>a b : α<VAR>u : ℕ → α<GOAL>⨆ x ∈ {0} ∪ range Nat.succ, u x = ⨆ i, u i
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G✝<VAR>inst✝¹ : Group G✝<VAR>s✝ : Set G✝<VAR>G : Type u_4<VAR>inst✝ : CommGroup G<VAR>s t : Set G<VAR>x : G<GOAL>x ∈ closure (s ∪ t) ↔ ∃ y ∈ closure s, ∃ z ∈ closure t, y * z = x
<VAR>G✝ : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G✝<VAR>inst✝¹ : Group G✝<VAR>s✝ : Set G✝<VAR>G : Type u_4<VAR>inst✝ : CommGroup G<VAR>s t : Set G<VAR>x : G<GOAL>(∃ y, (∃ y_1 ∈ Monoid.Closure s, ∃ z ∈ Monoid.Closure t, y_1 * z = y) ∧ ∃ z, (∃ y ∈ Monoid.Closure (Inv.inv ⁻¹' s), ∃ z_1 ∈ Monoid.Closure (Inv.inv ⁻¹' t), y * z_1 = z) ∧ y * z = x) ↔ ∃ y, (∃ y_1 ∈ Monoid.Closure s, ∃ z ∈ Monoid.Closure (Inv.inv ⁻¹' s), y_1 * z = y) ∧ ∃ z, (∃ y ∈ Monoid.Closure t, ∃ z_1 ∈ Monoid.Closure (Inv.inv ⁻¹' t), y * z_1 = z) ∧ y * z = x
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>W.dblX P / W.dblZ P ^ 2 = W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>α : E<VAR>hprim : F⟮α⟯ = ⊤<GOAL>FiniteDimensional F E
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>α : E<VAR>hprim : F⟮α⟯ = ⊤<VAR>hfin : FiniteDimensional F ↥F⟮α⟯<GOAL>FiniteDimensional F E
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>α : E<VAR>hprim : F⟮α⟯ = ⊤<VAR>hfin : FiniteDimensional F ↥⊤<GOAL>FiniteDimensional F E
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>f : Set (α × α) → Filter β<VAR>h : Monotone f<GOAL>((𝓤 α).lift fun s => f (s ○ s)) = ((𝓤 α).lift' fun s => s ○ s).lift f
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>f : Set (α × α) → Filter β<VAR>h : Monotone f<GOAL>Monotone fun s => s ○ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>f : Set (α × α) → Filter β<VAR>h : Monotone f<GOAL>Monotone f
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M₁<VAR>inst✝ : Module R M₁<VAR>I I' : R →+* R<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>hB' : B.SeparatingRight<GOAL>B.SeparatingLeft