ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>H : ContDiffOn 𝕜 (↑(n + 1)) f s<VAR>x : E<VAR>hx : x ∈ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>f' : E → E →L[𝕜] F<VAR>hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x<VAR>hf' : ContDiffWithinAt 𝕜 (↑n) f' u x<VAR>o : Set E<VAR>o_open : IsOpen o<VAR>xo : x ∈ o<VAR>ho : s ∩ o ⊆ u<VAR>this✝ : ContDiffWithinAt 𝕜 (↑n) f' s x<VAR>this : o ∩ s ∈ 𝓝[s] x<GOAL>(fun y => fderivWithin 𝕜 f s y) =ᶠ[𝓝[s] x] f'
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>H : ContDiffOn 𝕜 (↑(n + 1)) f s<VAR>x : E<VAR>hx : x ∈ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>f' : E → E →L[𝕜] F<VAR>hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x<VAR>hf' : ContDiffWithinAt 𝕜 (↑n) f' u x<VAR>o : Set E<VAR>o_open : IsOpen o<VAR>xo : x ∈ o<VAR>ho : s ∩ o ⊆ u<VAR>this✝ : ContDiffWithinAt 𝕜 (↑n) f' s x<VAR>this : s ∩ o ∈ 𝓝[s] x<GOAL>(fun y => fderivWithin 𝕜 f s y) =ᶠ[𝓝[s] x] f'
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>H : ContDiffOn 𝕜 (↑(n + 1)) f s<VAR>x : E<VAR>hx : x ∈ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>f' : E → E →L[𝕜] F<VAR>hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x<VAR>hf' : ContDiffWithinAt 𝕜 (↑n) f' u x<VAR>o : Set E<VAR>o_open : IsOpen o<VAR>xo : x ∈ o<VAR>ho : s ∩ o ⊆ u<VAR>this✝ : ContDiffWithinAt 𝕜 (↑n) f' s x<VAR>this : s ∩ o ∈ 𝓝[s] x<VAR>y : E<VAR>hy : y ∈ s ∩ o<GOAL>fderivWithin 𝕜 f s y = f' y
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>H : ContDiffOn 𝕜 (↑(n + 1)) f s<VAR>x : E<VAR>hx : x ∈ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>f' : E → E →L[𝕜] F<VAR>hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x<VAR>hf' : ContDiffWithinAt 𝕜 (↑n) f' u x<VAR>o : Set E<VAR>o_open : IsOpen o<VAR>xo : x ∈ o<VAR>ho : s ∩ o ⊆ u<VAR>this✝ : ContDiffWithinAt 𝕜 (↑n) f' s x<VAR>this : s ∩ o ∈ 𝓝[s] x<VAR>y : E<VAR>hy : y ∈ s ∩ o<VAR>A : fderivWithin 𝕜 f (s ∩ o) y = f' y<GOAL>fderivWithin 𝕜 f s y = f' y
<VAR>G✝ : Type u_1<VAR>H✝ : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : Group G✝<VAR>inst✝² : Fintype G✝<VAR>x : G✝<VAR>n : ℕ<VAR>G : Type u_6<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>g : G<GOAL>g ^ H.index ∈ H
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>π : α → β<VAR>s : Set β<VAR>t : Set α<VAR>a : α<VAR>h : a ∈ t<VAR>ht : IsOpen t<VAR>hs : s ∈ 𝓝 (π a)<GOAL>π ⁻¹' s ∈ 𝓝 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>π : α → β<VAR>s : Set β<VAR>t : Set α<VAR>a : α<VAR>h : a ∈ t<VAR>ht : IsOpen t<VAR>hs : s ∈ 𝓝 (π a)<GOAL>π ⁻¹' s ∈ 𝓝[t] a
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝ : _root_.Finite ι<GOAL>b.dualBasis.toDual ∘ₗ b.toDual = Dual.eval R M
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝ : _root_.Finite ι<VAR>i j : ι<GOAL>((b.dualBasis.toDual ∘ₗ b.toDual) (b i)) (b.dualBasis j) = ((Dual.eval R M) (b i)) (b.dualBasis j)
<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>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>dist p₃ p₂ / (∡ p₃ p₁ p₂).tan = dist p₁ p₂
<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>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₃ p₁ p₂).sign = 1<GOAL>dist p₃ p₂ / (∡ p₃ p₁ p₂).tan = dist p₁ p₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>G : C ⥤ D<VAR>F : D ⥤ C<VAR>A B : C<VAR>X Y : D<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>u : G.obj A ⟶ X<VAR>v : G.obj B ⟶ Y<VAR>sq : CommSq u (G.map i) p v<VAR>adj : G ⊣ F<GOAL>⋯.HasLift ↔ sq.HasLift
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>G : C ⥤ D<VAR>F : D ⥤ C<VAR>A B : C<VAR>X Y : D<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>u : G.obj A ⟶ X<VAR>v : G.obj B ⟶ Y<VAR>sq : CommSq u (G.map i) p v<VAR>adj : G ⊣ F<GOAL>Nonempty ⋯.LiftStruct ↔ Nonempty sq.LiftStruct
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>φ : K →+* ℂ<GOAL>(mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin n.succ → α<GOAL>(ofFn f).tail.get = fun i => f i.succ
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin n.succ → α<VAR>i : Fin (n.succ - 1)<GOAL>(ofFn f).tail.get i = f i.succ
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin n.succ → α<VAR>i : Fin (n.succ - 1)<GOAL>f ⟨↑i + 1, ⋯⟩ = f i.succ
<VAR>c : Code<VAR>v : List ℕ<GOAL>eval (TM2.step tr) (init c v) = halt <$> c.eval v
<VAR>c : Code<VAR>v : List ℕ<VAR>i : Cfg'<VAR>h₁ : TrCfg (stepNormal c Cont.halt v) i<VAR>h₂ : Reaches₁ (TM2.step tr) (init c v) i<GOAL>eval (TM2.step tr) (init c v) = halt <$> c.eval v
<VAR>c : Code<VAR>v : List ℕ<VAR>i : Cfg'<VAR>h₁ : TrCfg (stepNormal c Cont.halt v) i<VAR>h₂ : Reaches₁ (TM2.step tr) (init c v) i<VAR>x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')<GOAL>x ∈ eval (TM2.step tr) (init c v) ↔ x ∈ halt <$> c.eval v
<VAR>c : Code<VAR>v : List ℕ<VAR>i : Cfg'<VAR>h₁ : TrCfg (stepNormal c Cont.halt v) i<VAR>h₂ : Reaches₁ (TM2.step tr) (init c v) i<VAR>x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')<GOAL>x ∈ eval (TM2.step tr) i ↔ x ∈ halt <$> c.eval v
<VAR>c : Code<VAR>v : List ℕ<VAR>i : Cfg'<VAR>h₁ : TrCfg (stepNormal c Cont.halt v) i<VAR>h₂ : Reaches₁ (TM2.step tr) (init c v) i<VAR>x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')<GOAL>x ∈ eval (TM2.step tr) i ↔ ∃ a ∈ c.eval v, halt a = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝² : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝¹ : IsSFiniteKernel η<VAR>a : α<VAR>δ : Type u_5<VAR>inst✝ : TopologicalSpace δ<VAR>f : β × γ → δ<VAR>hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)<GOAL>∀ᵐ (x : β) ∂κ a, AEStronglyMeasurable (fun y => f (x, y)) (η (a, x))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hp0_lt : 0 < p<VAR>hpq : p < q<VAR>hpqr : 1 / p = 1 / q + 1 / r<GOAL>(∫⁻ (a : α), ↑‖b (f a) (g a)‖₊ ^ p ∂μ) ^ (1 / p) ≤ eLpNorm' f q μ * eLpNorm' g r μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hp0_lt : 0 < p<VAR>hpq : p < q<VAR>hpqr : 1 / p = 1 / q + 1 / r<GOAL>(∫⁻ (a : α), ↑(‖f a‖₊ * ‖g a‖₊) ^ p ∂μ) ^ (1 / p) ≤ eLpNorm' f q μ * eLpNorm' g r μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>μ : Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hp0_lt : 0 < p<VAR>hpq : p < q<VAR>hpqr : 1 / p = 1 / q + 1 / r<GOAL>(∫⁻ (a : α), (↑‖f a‖₊ * ↑‖g a‖₊) ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), ↑‖g a‖₊ ^ r ∂μ) ^ (1 / r)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : DecidableEq L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsFractionRing R K<VAR>inst✝³ : Algebra K L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra R L<VAR>inst✝ : IsScalarTower R K L<VAR>x : Kˣ<GOAL>spanSingleton R⁰ ↑x * spanSingleton R⁰ (↑x)⁻¹ = 1
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : DecidableEq L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsFractionRing R K<VAR>inst✝³ : Algebra K L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra R L<VAR>inst✝ : IsScalarTower R K L<VAR>x : Kˣ<GOAL>spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : DecidableEq L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsFractionRing R K<VAR>inst✝³ : Algebra K L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra R L<VAR>inst✝ : IsScalarTower R K L<VAR>x y : Kˣ<GOAL>↑({ toFun := fun x => { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯ }.toFun (x * y)) = ↑({ toFun := fun x => { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯ }.toFun x * { toFun := fun x => { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯ }.toFun y)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : DecidableEq L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsFractionRing R K<VAR>inst✝³ : Algebra K L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra R L<VAR>inst✝ : IsScalarTower R K L<GOAL>↑((fun x => { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ }) 1) = ↑1
<VAR>x y : PartENat<VAR>hx : Decidable x.Dom<VAR>hy : Decidable y.Dom<GOAL>x.toWithTop ≤ y.toWithTop ↔ x ≤ y
<VAR>x : PartENat<VAR>hx : Decidable x.Dom<VAR>hy : Decidable ⊤.Dom<GOAL>x.toWithTop ≤ ⊤.toWithTop ↔ x ≤ ⊤
<VAR>x : PartENat<VAR>hx : Decidable x.Dom<VAR>n✝ : ℕ<VAR>hy : Decidable (↑n✝).Dom<GOAL>x.toWithTop ≤ (↑n✝).toWithTop ↔ x ≤ ↑n✝
<VAR>n✝ : ℕ<VAR>hy : Decidable (↑n✝).Dom<VAR>hx : Decidable ⊤.Dom<GOAL>⊤.toWithTop ≤ (↑n✝).toWithTop ↔ ⊤ ≤ ↑n✝
<VAR>n✝¹ : ℕ<VAR>hy : Decidable (↑n✝¹).Dom<VAR>n✝ : ℕ<VAR>hx : Decidable (↑n✝).Dom<GOAL>(↑n✝).toWithTop ≤ (↑n✝¹).toWithTop ↔ ↑n✝ ≤ ↑n✝¹
<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>i : (mk α✝ β✝ a✝¹ a✝).RightMoves<GOAL>((mk α✝ β✝ a✝¹ a✝).moveRight i).birthday < max (lsub fun i => (a✝¹ i).birthday) (lsub fun i => (a✝ i).birthday)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I = I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) = Associates.mk I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>Associates.mk I ≠ 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>∀ (p : Associates (Ideal R)), Irreducible p → p.count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = p.count (Associates.mk I).factors
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v✝ : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>v : Associates (Ideal R)<VAR>hv : Irreducible v<GOAL>v.count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = v.count (Associates.mk I).factors
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v✝ : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>v : Associates (Ideal R)<VAR>hv : Irreducible v<VAR>J : Ideal R<VAR>hJv : Associates.mk J = v<GOAL>v.count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = v.count (Associates.mk I).factors
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v✝ : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>v : Associates (Ideal R)<VAR>J : Ideal R<VAR>hv : Irreducible J<VAR>hJv : Associates.mk J = v<GOAL>v.count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = v.count (Associates.mk I).factors
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v✝ : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<VAR>v : Associates (Ideal R)<VAR>J : Ideal R<VAR>hv : Irreducible J<VAR>hJv : Associates.mk J = v<GOAL>(Associates.mk J).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = (Associates.mk J).count (Associates.mk I).factors
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : CommRing B<VAR>inst✝ : CommRing C<VAR>f : A →+* B<VAR>hf : Surjective ⇑f<VAR>hker : (ker f).FG<GOAL>f.FinitePresentation
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : CommRing B<VAR>inst✝ : CommRing C<VAR>f : A →+* B<VAR>hf : Surjective ⇑f<VAR>hker : (ker f).FG<GOAL>(f.comp (RingHom.id A)).FinitePresentation
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.23, u_1} C<VAR>inst✝ : Category.{?u.27, u_2} D<VAR>F F' : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>f : G ⟶ G'<VAR>X Y : C<VAR>g : X ⟶ Y<GOAL>F'.map g ≫ (fun X => F'.map ((adj1.unit ≫ whiskerLeft F f).app X) ≫ adj2.counit.app (F.obj X)) Y = (fun X => F'.map ((adj1.unit ≫ whiskerLeft F f).app X) ≫ adj2.counit.app (F.obj X)) X ≫ F.map g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.23, u_1} C<VAR>inst✝ : Category.{?u.27, u_2} D<VAR>F F' : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>f : G ⟶ G'<VAR>X Y : C<VAR>g : X ⟶ Y<GOAL>F'.map (g ≫ (adj1.unit ≫ whiskerLeft F f).app Y) ≫ adj2.counit.app (F.obj Y) = (F'.map ((adj1.unit ≫ whiskerLeft F f).app X) ≫ adj2.counit.app (F.obj X)) ≫ F.map g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.23, u_1} C<VAR>inst✝ : Category.{?u.27, u_2} D<VAR>F F' : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>f : G ⟶ G'<VAR>X Y : C<VAR>g : X ⟶ Y<GOAL>F'.map ((adj1.unit ≫ whiskerLeft F f).app X ≫ (F ⋙ G').map g) ≫ adj2.counit.app (F.obj Y) = (F'.map ((adj1.unit ≫ whiskerLeft F f).app X) ≫ adj2.counit.app (F.obj X)) ≫ F.map g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.23, u_1} C<VAR>inst✝ : Category.{?u.27, u_2} D<VAR>F F' : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>f : F' ⟶ F<VAR>X Y : D<VAR>g : X ⟶ Y<GOAL>adj2.unit.app (G.obj X) ≫ G'.map (F'.map (G.map g)) ≫ G'.map (f.app (G.obj Y) ≫ adj1.counit.app Y) = (fun X => adj2.unit.app (G.obj X) ≫ G'.map (f.app (G.obj X) ≫ adj1.counit.app X)) X ≫ G'.map g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.23, u_1} C<VAR>inst✝ : Category.{?u.27, u_2} D<VAR>F F' : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>f : F' ⟶ F<VAR>X Y : D<VAR>g : X ⟶ Y<GOAL>adj2.unit.app (G.obj X) ≫ G'.map (F'.map (G.map g) ≫ f.app (G.obj Y) ≫ adj1.counit.app Y) = (adj2.unit.app (G.obj X) ≫ G'.map (f.app (G.obj X) ≫ adj1.counit.app X)) ≫ G'.map g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.23, u_1} C<VAR>inst✝ : Category.{?u.27, u_2} D<VAR>F F' : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>f : G ⟶ G'<VAR>X : D<GOAL>((fun f => { app := fun X => adj2.unit.app (G.obj X) ≫ G'.map (f.app (G.obj X) ≫ adj1.counit.app X), naturality := ⋯ }) ((fun f => { app := fun X => F'.map ((adj1.unit ≫ whiskerLeft F f).app X) ≫ adj2.counit.app (F.obj X), naturality := ⋯ }) f)).app X = f.app X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.23, u_1} C<VAR>inst✝ : Category.{?u.27, u_2} D<VAR>F F' : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>f : G ⟶ G'<VAR>X : D<GOAL>adj1.unit.app (G.obj X) ≫ f.app (F.obj (G.obj X)) ≫ G'.map (adj1.counit.app X) = f.app X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.23, u_1} C<VAR>inst✝ : Category.{?u.27, u_2} D<VAR>F F' : C ⥤ D<VAR>G G' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>f : G ⟶ G'<VAR>X : D<GOAL>(adj1.unit.app (G.obj X) ≫ G.map (adj1.counit.app X)) ≫ f.app ((𝟭 D).obj X) = f.app X
<VAR>R : Type u<VAR>L : Type v<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>k : ℕ<VAR>N N₁ N₂ : LieSubmodule R L M<GOAL>LieModule.IsNilpotent R L ↥↑N ↔ ∃ k, N ≤ ucs k ⊥
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hp : Prime p<VAR>hn : n ≠ 0<GOAL>¬p ∣ n / p ^ n.factorization p
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hp : Prime p<VAR>hn : n ≠ 0<GOAL>¬1 ≤ (n / p ^ n.factorization p).factorization p
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hp : Prime p<VAR>hn : n ≠ 0<GOAL>¬1 ≤ (n.factorization - (p ^ n.factorization p).factorization) p
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K✝ : Subgroup G<VAR>k : Set G<VAR>K : Set (Subgroup G)<VAR>Kne : K.Nonempty<VAR>hK : DirectedOn (fun x x_1 => x ≤ x_1) K<VAR>x : G<GOAL>x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K✝ : Subgroup G<VAR>k : Set G<VAR>K : Set (Subgroup G)<VAR>Kne : K.Nonempty<VAR>hK : DirectedOn (fun x x_1 => x ≤ x_1) K<VAR>x : G<VAR>this : Nonempty ↑K<GOAL>x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SemilatticeSup M<VAR>inst✝ : OrderBot M<VAR>w : σ → M<GOAL>weightedTotalDegree w 0 = ⊥
<VAR>θ : Angle<VAR>h : 0 ≤ θ.sign<GOAL>↑|θ.toReal| = θ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T1Space X<VAR>inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot<VAR>s : Set X<VAR>hs : Dense s<VAR>t : Finset X<GOAL>Dense (s \ ↑t)
<VAR>o : Ordinal.{u_1}<GOAL>let_fun this := ⋯; HEq (nim o).moveLeft fun i => nim (typein (fun x x_1 => x < x_1) i)
<VAR>o : Ordinal.{u_1}<GOAL>let_fun this := ⋯; HEq (mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)).moveLeft fun i => nim (typein (fun x x_1 => x < x_1) i)
<VAR>α : Type u_1<VAR>n : ZNum<GOAL>-n.pred = (-n).succ
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W : Submodule K V<VAR>inst✝ : Module.Free K ↥W<GOAL>Module.rank K ↥W ≤ 1 ↔ W.IsPrincipal
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W : Submodule K V<VAR>inst✝ : Module.Free K ↥W<GOAL>(∃ v₀, ∀ (v : ↥W), ∃ r, r • v₀ = v) ↔ ∃ a, (∀ v ∈ W, ∃ r, r • a = v) ∧ a ∈ W
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.14791, u_1} C<VAR>P : Karoubi C<GOAL>P.p = P.p ≫ P.p ≫ P.p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν✝ : Measure α<VAR>mb : MeasurableSpace β<VAR>ν : Measure β<VAR>g : α → β<VAR>hg : MeasurePreserving g μ ν<VAR>f : β → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>a : ↥(adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(adjoin R s)) r)<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)<VAR>b : A<VAR>hb : b ∈ adjoin R s<GOAL>p ⟨b, hb⟩