ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : InnerProductSpace 𝕜 E'<VAR>inst✝⁹ : CompleteSpace E'<VAR>inst✝⁸ : NormedSpace ℝ E'<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>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(Lp F p μ) → Prop<VAR>h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)<VAR>h_add : ∀ ⦃f g : α → F⦄ (hf : Memℒp f p μ) (hg : Memℒp g p μ), AEStronglyMeasurable' m f μ → AEStronglyMeasurable' m g μ → Disjoint (Function.support f) (Function.support g) → P (Memℒp.toLp f hf) → P (Memℒp.toLp g hg) → P (Memℒp.toLp f hf + Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P ↑f}<VAR>f : ↥(Lp F p μ)<VAR>hf : AEStronglyMeasurable' m (↑↑f) μ<VAR>f' : ↥(lpMeas F ℝ m p μ) := ⟨f, hf⟩<VAR>g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'<VAR>hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g<GOAL>IsClosed {f | (fun g => P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm g)) f}
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommSemiring k<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra k A<VAR>inst✝ : Monoid G<VAR>r : k<GOAL>(↑↑__src✝).toFun ((algebraMap k A) r) = (algebraMap k (MonoidAlgebra A G)) r
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommSemiring k<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra k A<VAR>inst✝ : Monoid G<VAR>r : k<VAR>x✝ : G<GOAL>((↑↑__src✝).toFun ((algebraMap k A) r)) x✝ = ((algebraMap k (MonoidAlgebra A G)) r) x✝
<VAR>F : Type u<VAR>K✝¹ : Type v<VAR>L : Type w<VAR>inst✝³ : Field K✝¹<VAR>inst✝² : Field L<VAR>inst✝¹ : Field F<VAR>n✝ : ℕ<VAR>K✝ : Type u<VAR>inst✝ : Field K✝<VAR>n : ℕ<VAR>ih : (fun n => ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Splits (algebraMap K (SplittingFieldAux n f)) f) n<VAR>K : Type u<VAR>x✝ : Field K<VAR>f : K[X]<VAR>hf : f.natDegree = n.succ<GOAL>Splits (algebraMap K (SplittingFieldAux n.succ f)) f
<VAR>F : Type u<VAR>K✝¹ : Type v<VAR>L : Type w<VAR>inst✝³ : Field K✝¹<VAR>inst✝² : Field L<VAR>inst✝¹ : Field F<VAR>n✝ : ℕ<VAR>K✝ : Type u<VAR>inst✝ : Field K✝<VAR>n : ℕ<VAR>ih : (fun n => ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Splits (algebraMap K (SplittingFieldAux n f)) f) n<VAR>K : Type u<VAR>x✝ : Field K<VAR>f : K[X]<VAR>hf : f.natDegree = n.succ<GOAL>Splits (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor)) ((X - C (AdjoinRoot.root f.factor)) * f.removeFactor)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s s₁ s₂ t t₁ t₂ : Finset α<VAR>h : 0 < Eₘ[s, t]<VAR>H : ¬(s.Nonempty ∧ t.Nonempty)<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s s₁ s₂ t t₁ t₂ : Finset α<VAR>h : 0 < Eₘ[s, t]<VAR>H : s = ∅ ∨ t = ∅<GOAL>False
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hIX : M.Basis I X<VAR>hJX : M.Basis J X<VAR>hXY : X ⊆ Y<VAR>hJY : M.Basis J Y<GOAL>M.Basis I Y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hIX : M.Basis I X<VAR>hJX : M.Basis J X<VAR>hXY : X ⊆ Y<VAR>hJY : M.Basis J Y<GOAL>(M ↾ Y).Base I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hIX : M.Basis I X<VAR>hJX : M.Basis J X<VAR>hXY : X ⊆ Y<VAR>hJY : (M ↾ Y).Base J<GOAL>(M ↾ Y).Base I
<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✝ : CommGroupWithZero G₀<VAR>a✝ b✝ c d a b : G₀<GOAL>a ^ 2 * b / a = a * b
<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✝ : CommGroupWithZero G₀<VAR>a b✝ c d b : G₀<GOAL>0 ^ 2 * b / 0 = 0 * b
<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✝ : CommGroupWithZero G₀<VAR>a✝ b✝ c d a b : G₀<VAR>ha : a ≠ 0<GOAL>a ^ 2 * b / a = a * b
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : LaxMonoidalFunctor C D<VAR>X Y X' Y' : C<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y'<GOAL>(F.map f ⊗ F.map g) ≫ F.μ Y Y' = F.μ X X' ≫ F.map (f ⊗ g)
<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<VAR>m : M →ₗ[R] P<VAR>n : N →ₗ[R] Q<VAR>x✝¹ : M<VAR>x✝ : N<GOAL>(((TensorProduct.mk R M N).compr₂ ((((TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q)).compr₂ ↑(homTensorHomEquiv R M N P Q)) m) n)) x✝¹) x✝ = (((TensorProduct.mk R M N).compr₂ ((((TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q)).compr₂ (homTensorHomMap R M N P Q)) m) n)) x✝¹) x✝
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>t : RBNode α<GOAL>all p t = true ↔ All (fun x => p x = true) t
<VAR>a b : ℝ<VAR>ha : a ≤ 0<VAR>z : ℂ<VAR>hz : |z.im| ≤ b<VAR>hb : b ≤ π / 2<GOAL>abs (cexp (↑a * (cexp z + cexp (-z)))) ≤ rexp (a * Real.cos b * rexp |z.re|)
<VAR>a b : ℝ<VAR>ha : a ≤ 0<VAR>z : ℂ<VAR>hz : |z.im| ≤ b<VAR>hb : b ≤ π / 2<GOAL>a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)
<VAR>a b : ℝ<VAR>ha : a ≤ 0<VAR>z : ℂ<VAR>hz : |z.im| ≤ b<VAR>hb : b ≤ π / 2<VAR>this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)<GOAL>a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)
<VAR>a b : ℝ<VAR>ha : a ≤ 0<VAR>z : ℂ<VAR>hz : |z.im| ≤ b<VAR>hb : b ≤ π / 2<VAR>this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)<GOAL>Real.cos b ≤ Real.cos |z.im|
<VAR>a b : ℝ<VAR>ha : a ≤ 0<VAR>z : ℂ<VAR>hz : |z.im| ≤ b<VAR>hb : b ≤ π / 2<VAR>this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)<GOAL>0 ≤ Real.cos b
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K A B : Set α<VAR>hA : IsCompact A<VAR>hB : IsClosed B<VAR>h : Disjoint A B<GOAL>∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K A B : Set α<VAR>hA : IsCompact A<VAR>hB : IsClosed B<VAR>h : Disjoint A B<VAR>this : Bᶜ ∈ 𝓝ˢ A<GOAL>∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K A B : Set α<VAR>hA : IsCompact A<VAR>hB : IsClosed B<VAR>h : Disjoint A B<VAR>this : ∃ i ∈ 𝓤 α, ⋃ x ∈ A, ball x (id i) ⊆ Bᶜ<GOAL>∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K A B : Set α<VAR>hA : IsCompact A<VAR>hB : IsClosed B<VAR>h : Disjoint A B<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ<GOAL>∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K A B : Set α<VAR>hA : IsCompact A<VAR>hB : IsClosed B<VAR>h : Disjoint A B<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVsymm : SymmetricRel V<VAR>hVU : V ○ V ⊆ U<GOAL>∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K A B : Set α<VAR>hA : IsCompact A<VAR>hB : IsClosed B<VAR>h : Disjoint A B<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVsymm : SymmetricRel V<VAR>hVU : V ○ V ⊆ U<VAR>x : α<GOAL>x ∈ ⋃ x ∈ A, ball x V → x ∉ ⋃ x ∈ B, ball x V
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K A B : Set α<VAR>hA : IsCompact A<VAR>hB : IsClosed B<VAR>h : Disjoint A B<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVsymm : SymmetricRel V<VAR>hVU : V ○ V ⊆ U<VAR>x : α<GOAL>(∃ i, ∃ (_ : i ∈ A), x ∈ ball i V) → ¬∃ i, ∃ (_ : i ∈ B), x ∈ ball i V
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K A B : Set α<VAR>hA : IsCompact A<VAR>hB : IsClosed B<VAR>h : Disjoint A B<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVsymm : SymmetricRel V<VAR>hVU : V ○ V ⊆ U<VAR>x a : α<VAR>ha : a ∈ A<VAR>hxa : x ∈ ball a V<VAR>b : α<VAR>hb : b ∈ B<VAR>hxb : x ∈ ball b V<GOAL>False
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K A B : Set α<VAR>hA : IsCompact A<VAR>hB : IsClosed B<VAR>h : Disjoint A B<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVsymm : SymmetricRel V<VAR>hVU : V ○ V ⊆ U<VAR>x a : α<VAR>ha : a ∈ A<VAR>hxa : a ∈ ball x V<VAR>b : α<VAR>hb : b ∈ B<VAR>hxb : b ∈ ball x V<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p q : Submodule R M<GOAL>Subsingleton (Submodule R M) ↔ Subsingleton (AddSubmonoid M)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝³ : (i : ι) → Module R (M₁ i)<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M'<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>f : MultilinearMap R M M₂<VAR>m : (i : Fin n) → M i.castSucc<VAR>c : R<VAR>x : M (last n)<GOAL>f (snoc m (c • x)) = c • f (snoc m x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<GOAL>(μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<GOAL>μ.singularPart ν ⟂ₘ ν
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d✝ : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (d + x / c) = c • ∫ (x : ℝ) in d + a / c..d + b / c, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>inst✝ : Nonempty α<VAR>hs : autoParam s.Finite _auto✝<GOAL>s.ncard ≤ 1 ↔ ∃ x, s ⊆ {x}
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a b : Multiset { a // Irreducible a }<GOAL>(↑a + ↑b).prod = FactorSet.prod ↑a * FactorSet.prod ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : MetricSpace β<VAR>inst✝ : NormedAddCommGroup E<GOAL>∀ (s : Set (C(α, β) × C(α, β))), s ∈ uniformity C(α, β) ↔ ∃ t ∈ uniformity (α →ᵇ β), ∀ (x y : C(α, β)), ((equivBoundedOfCompact α β) x, (equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : MetricSpace β<VAR>inst✝ : NormedAddCommGroup E<GOAL>∀ (s : Set (C(α, β) × C(α, β))), (∃ i, (IsCompact i.1 ∧ ∃ i_1, 0 < i_1 ∧ {p | dist p.1 p.2 ≤ i_1} ⊆ i.2) ∧ {fg | ∀ x ∈ i.1, (fg.1 x, fg.2 x) ∈ i.2} ⊆ s) ↔ ∃ t, (∃ i, 0 < i ∧ {p | dist p.1 p.2 ≤ i} ⊆ t) ∧ ∀ (x y : C(α, β)), ((equivBoundedOfCompact α β) x, (equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>n : ℕ<VAR>f : Fin n → β<GOAL>(List.ofFn f).prod = ∏ i : Fin n, f i
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<GOAL>(toLin v₁ v₁) 1 = LinearMap.id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>h : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)<VAR>x : α<VAR>xs : x ∈ s<VAR>t : Set α<VAR>open_t : IsOpen t<VAR>xt : x ∈ t<VAR>ct : ContinuousOn f (s ∩ t)<VAR>this : ContinuousWithinAt f (s ∩ t) x<GOAL>ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>n : ℕ<GOAL>1 ≤ ↑(n + 1)
<VAR>ι : Type u_1<VAR>m : Type u_2<VAR>n✝ : Type u_3<VAR>p : Type u_4<VAR>α : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n✝<VAR>inst✝¹ : Fintype p<VAR>n : ℕ<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>M : Matrix (Fin n.succ) (Fin n.succ) R<GOAL>M 0 0 + ∑ i : Fin n, (M.submatrix Fin.succ Fin.succ).diag i = ∑ i : Fin n.succ, M.diag i
<VAR>ι : Type u_1<VAR>m : Type u_2<VAR>n✝ : Type u_3<VAR>p : Type u_4<VAR>α : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n✝<VAR>inst✝¹ : Fintype p<VAR>n : ℕ<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>M : Matrix (Fin n.succ) (Fin n.succ) R<GOAL>M 0 0 + ∑ i : Fin n, (M.submatrix Fin.succ Fin.succ).diag i = ∑ i : Option (Fin n), M.diag ((finSuccEquiv n).symm i)
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f g✝ : K[X]<VAR>hfg : map i (f * g✝) ≠ 0<VAR>h : Splits i (f * g✝)<VAR>g : L[X]<VAR>hgi : Irreducible g<VAR>hg : g ∣ map i f<GOAL>g ∣ map i (f * g✝)
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f g✝ : K[X]<VAR>hfg : map i (f * g✝) ≠ 0<VAR>h : Splits i (f * g✝)<VAR>g : L[X]<VAR>hgi : Irreducible g<VAR>hg : g ∣ map i f<GOAL>g ∣ map i f * map i g✝
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f g✝ : K[X]<VAR>hfg : map i (f * g✝) ≠ 0<VAR>h : Splits i (f * g✝)<VAR>g : L[X]<VAR>hgi : Irreducible g<VAR>hg : g ∣ map i g✝<GOAL>g ∣ map i (f * g✝)
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f g✝ : K[X]<VAR>hfg : map i (f * g✝) ≠ 0<VAR>h : Splits i (f * g✝)<VAR>g : L[X]<VAR>hgi : Irreducible g<VAR>hg : g ∣ map i g✝<GOAL>g ∣ map i f * map i g✝
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<GOAL>finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ IsPrincipal (maximalIdeal R)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<GOAL>(∃ x, ⊤ = span (ResidueField R) {(maximalIdeal R).toCotangent x}) ↔ ∃ a, maximalIdeal R = span R {a}
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<GOAL>(∃ x, span R {(Submodule.subtype (maximalIdeal R)) x} = maximalIdeal R) ↔ ∃ a, span R {a} = maximalIdeal R
<VAR>R : Type u_1<VAR>inst✝ : Ring R<GOAL>cyclotomic 2 R = X + 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<VAR>h : a < b<GOAL>Ioc a b = cons b (Ioo a b) ⋯
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>m₁ m₂ : M<VAR>a : α<VAR>h₁ : a ∈ fixedBy α m₁<VAR>h₂ : a ∈ fixedBy α m₂<GOAL>a ∈ fixedBy α (m₁ * m₂)
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i : (Quotient.out (aleph 1).ord).α<GOAL>#↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i : (Quotient.out (aleph 1).ord).α<GOAL>∀ (x : (Quotient.out (aleph 1).ord).α), (∀ (y : (Quotient.out (aleph 1).ord).α), (Quotient.out (aleph 1).ord).r y x → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀) → #↑(generateMeasurableRec s x) ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i✝ i : (Quotient.out (aleph 1).ord).α<VAR>IH : ∀ (y : (Quotient.out (aleph 1).ord).α), (Quotient.out (aleph 1).ord).r y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀<GOAL>#↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i✝ i : (Quotient.out (aleph 1).ord).α<VAR>IH : ∀ (y : (Quotient.out (aleph 1).ord).α), (Quotient.out (aleph 1).ord).r y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀<VAR>A : ℵ₀ ≤ aleph 1<GOAL>#↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i✝ i : (Quotient.out (aleph 1).ord).α<VAR>IH : ∀ (y : (Quotient.out (aleph 1).ord).α), (Quotient.out (aleph 1).ord).r y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀<VAR>A : ℵ₀ ≤ aleph 1<VAR>B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀<GOAL>#↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i✝ i : (Quotient.out (aleph 1).ord).α<VAR>IH : ∀ (y : (Quotient.out (aleph 1).ord).α), (Quotient.out (aleph 1).ord).r y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀<VAR>A : ℵ₀ ≤ aleph 1<VAR>B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀<VAR>C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀<GOAL>#↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i✝ i : (Quotient.out (aleph 1).ord).α<VAR>IH : ∀ (y : (Quotient.out (aleph 1).ord).α), (Quotient.out (aleph 1).ord).r y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀<VAR>A : ℵ₀ ≤ aleph 1<VAR>B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀<VAR>C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀<VAR>J : #↑(⋃ j, generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀<GOAL>#↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i✝ i : (Quotient.out (aleph 1).ord).α<VAR>IH : ∀ (y : (Quotient.out (aleph 1).ord).α), (Quotient.out (aleph 1).ord).r y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀<VAR>A : ℵ₀ ≤ aleph 1<VAR>B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀<VAR>C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀<VAR>J : #↑(⋃ j, generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀<GOAL>#↑((s ∪ {∅} ∪ compl '' ⋃ j, generateMeasurableRec s ↑j) ∪ range fun f => ⋃ n, ↑(f n)) ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i✝ i : (Quotient.out (aleph 1).ord).α<VAR>IH : ∀ (y : (Quotient.out (aleph 1).ord).α), (Quotient.out (aleph 1).ord).r y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀<VAR>A : ℵ₀ ≤ aleph 1<VAR>B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀<VAR>C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀<VAR>J : #↑(⋃ j, generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀<GOAL>#↑s ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i✝ i : (Quotient.out (aleph 1).ord).α<VAR>IH : ∀ (y : (Quotient.out (aleph 1).ord).α), (Quotient.out (aleph 1).ord).r y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀<VAR>A : ℵ₀ ≤ aleph 1<VAR>B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀<VAR>C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀<VAR>J : #↑(⋃ j, generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀<GOAL>#↑{∅} ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i✝ i : (Quotient.out (aleph 1).ord).α<VAR>IH : ∀ (y : (Quotient.out (aleph 1).ord).α), (Quotient.out (aleph 1).ord).r y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀<VAR>A : ℵ₀ ≤ aleph 1<VAR>B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀<VAR>C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀<VAR>J : #↑(⋃ j, generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀<GOAL>#↑(range fun f => ⋃ n, ↑(f n)) ≤ max (#↑s) 2 ^ ℵ₀
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI✝ : I ≠ 0<VAR>hJ : J ≠ 0<VAR>hI : ¬I = 0<GOAL>(dual A K I)⁻¹ ≤ I
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI✝ : I ≠ 0<VAR>hJ : J ≠ 0<VAR>hI : ¬I = 0<GOAL>(dual A K I)⁻¹ = (fun J => J * (dual A K I)⁻¹) ((fun x => I * x) I⁻¹)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI✝ : I ≠ 0<VAR>hJ : J ≠ 0<VAR>hI : ¬I = 0<GOAL>I = (fun J => J * (dual A K I)⁻¹) ((fun x => I * x) (dual A K I))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>s t : Set α<VAR>d : ℝ<VAR>hs : s.Nontrivial<GOAL>d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
<VAR>n : ℕ<GOAL>↑n + 1 = 0
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝¹ : Category.{v'', u''} D<VAR>X Y : C<VAR>inst✝ : FinitaryPreExtensive C<VAR>n : ℕ<VAR>F : Discrete (Fin n) ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>f : Fin n → C := F.obj ∘ Discrete.mk<GOAL>IsUniversalColimit c
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝¹ : Category.{v'', u''} D<VAR>X Y : C<VAR>inst✝ : FinitaryPreExtensive C<VAR>n : ℕ<VAR>F : Discrete (Fin n) ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>f : Fin n → C := F.obj ∘ Discrete.mk<VAR>this : F = Discrete.functor f<GOAL>IsUniversalColimit c
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y X : C<VAR>s : Cone (Functor.empty C)<VAR>P : IsLimit s<VAR>t : BinaryFan X s.pt<VAR>Q : IsLimit t<GOAL>t.fst ≫ Q.lift (mk (𝟙 X) (P.lift { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } })) = 𝟙 t.pt
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y X : C<VAR>s : Cone (Functor.empty C)<VAR>P : IsLimit s<VAR>t : BinaryFan X s.pt<VAR>Q : IsLimit t<GOAL>∀ (j : Discrete WalkingPair), (t.fst ≫ Q.lift (mk (𝟙 X) (P.lift { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }))) ≫ t.π.app j = 𝟙 t.pt ≫ t.π.app j