ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>ht : IsOpen t<VAR>h't : IsPreconnected t<VAR>hg : ∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y<VAR>hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n<VAR>hy₀ : y₀ ∈ t<VAR>hg0 : Summable fun x => g x y₀<VAR>hy : y ∈ t<GOAL>Summable fun n => g n y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>ht : IsOpen t<VAR>h't : IsPreconnected t<VAR>hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n<VAR>hy₀ : y₀ ∈ t<VAR>hg0 : Summable fun x => g x y₀<VAR>hy : y ∈ t<VAR>hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y<GOAL>Summable fun n => g n y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>ht : IsOpen t<VAR>h't : IsPreconnected t<VAR>hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n<VAR>hy₀ : y₀ ∈ t<VAR>hg0 : Summable fun x => g x y₀<VAR>hy : y ∈ t<VAR>hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y<GOAL>∀ (n : α), ∀ x ∈ t, ‖ContinuousLinearMap.smulRight 1 (g' n x)‖ ≤ u n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<GOAL>IsTopologicalBasis (Set.range fun r => ↑(basicOpen 𝒜 r))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<GOAL>∀ u ∈ Set.range fun r => ↑(basicOpen 𝒜 r), IsOpen u
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<GOAL>∀ (a : ProjectiveSpectrum 𝒜) (u : Set (ProjectiveSpectrum 𝒜)), a ∈ u → IsOpen u → ∃ v ∈ Set.range fun r => ↑(basicOpen 𝒜 r), a ∈ v ∧ v ⊆ u
<VAR>α : Type u_1<VAR>t : Ordnode α<VAR>h : t.dual.Sized<GOAL>t.Sized
<VAR>α : Type u_1<VAR>t : Ordnode α<VAR>h : t.dual.Sized<GOAL>t.dual.dual.Sized
<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>x : F<GOAL>IsSeparable F ((algebraMap F E) 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>x : F<GOAL>(minpoly F x).Separable
<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>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>h : separableClosure E K = ⊥<GOAL>IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E) = separableClosure F K
<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>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>h : separableClosure E K = ⊥<VAR>x : K<VAR>hx : x ∈ separableClosure F K<GOAL>x ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E)
<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>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>h : separableClosure E K = ⊥<VAR>y : E<VAR>hx : (algebraMap E K) y ∈ separableClosure F K<GOAL>(algebraMap E K) y ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Countable ι'<VAR>f : ι' → Set X<VAR>hf : ∀ (i : ι'), IsOpen (f i)<GOAL>∀ t ∈ range f, IsOpen t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Countable ι'<VAR>f : ι' → Set X<VAR>hf : ∀ (i : ι'), IsOpen (f i)<GOAL>⋂ i, f i = ⋂₀ range f
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (aeval r) p = 0<GOAL>num A r ∣ (p.scaleRoots ↑(den A r)).coeff 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (aeval r) p = 0<GOAL>(p.scaleRoots ↑(den A r)).coeff 0 = (p.scaleRoots ↑(den A r)).coeff 0 * num A r ^ 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (aeval r) p = 0<GOAL>∀ (j : ℕ), j ≠ 0 → num A r ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (aeval r) p = 0<VAR>j : ℕ<VAR>hj : j ≠ 0<GOAL>num A r ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (aeval r) p = 0<VAR>j : ℕ<VAR>hj : j ≠ 0<GOAL>num A r ∣ num A r ^ j
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (aeval r) p = 0<VAR>j : ℕ<VAR>hj : j ≠ 0<GOAL>num A r = num A r ^ ⊥.succ
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : FiniteMeasure α<VAR>ν : FiniteMeasure β<VAR>s : Set (α × β)<VAR>s_mble : MeasurableSet s<GOAL>(μ.prod ν) s = (∫⁻ (y : β), ↑μ ((fun x => (x, y)) ⁻¹' s) ∂↑ν).toNNReal
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : { f // IsIdempotentElem f ∧ range f = p }<VAR>x : E<GOAL>↑f x ∈ p
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : { f // IsIdempotentElem f ∧ range f = p }<VAR>x : E<GOAL>↑f x ∈ range ↑f
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : { f // IsIdempotentElem f ∧ range f = p }<VAR>x✝ : ↥p<VAR>x : E<VAR>hx : x ∈ p<GOAL>↑((codRestrict p ↑f ⋯) ↑⟨x, hx⟩) = ↑⟨x, hx⟩
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : { f // IsIdempotentElem f ∧ range f = p }<VAR>x✝ : ↥p<VAR>x : E<VAR>hx : ↑f x ∈ p<GOAL>↑((codRestrict p ↑f ⋯) ↑⟨↑f x, hx⟩) = ↑⟨↑f x, hx⟩
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : { f // ∀ (x : ↥p), f ↑x = x }<VAR>x : E<GOAL>(p.subtype ∘ₗ ↑f * p.subtype ∘ₗ ↑f) x = (p.subtype ∘ₗ ↑f) x
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>ha₁ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<VAR>ha₂ : SpectrumRestricts (-a) ⇑ContinuousMap.realToNNReal<VAR>a✝ : Nontrivial A<GOAL>a = 0
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>ha₁ : ∀ x ∈ σ ℝ a, 0 ≤ x<VAR>ha₂ : ∀ x ∈ σ ℝ (-a), 0 ≤ x<VAR>a✝ : Nontrivial A<GOAL>a = 0
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>ha₁ : ∀ x ∈ σ ℝ a, 0 ≤ x<VAR>ha₂ : ∀ x ∈ σ ℝ (-a), 0 ≤ x<VAR>a✝ : Nontrivial A<GOAL>σ ℝ a ⊆ {0}
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>ha₁ : ∀ x ∈ σ ℝ a, 0 ≤ x<VAR>ha₂ : ∀ x ∈ σ ℝ (-a), 0 ≤ x<VAR>a✝ : Nontrivial A<GOAL>∀ y ∈ σ ℝ a, y = 0
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>ha₁ : ∀ x ∈ σ ℝ a, 0 ≤ x<VAR>a✝ : Nontrivial A<VAR>ha₂ : ∀ (x : ℝ), -x ∈ σ ℝ a → 0 ≤ x<GOAL>∀ y ∈ σ ℝ a, y = 0
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>ha₁ : ∀ x ∈ σ ℝ a, 0 ≤ x<VAR>a✝ : Nontrivial A<VAR>ha₂ : ∀ (x : ℝ), -x ∈ σ ℝ a → 0 ≤ x<VAR>x : ℝ<VAR>hx : x ∈ σ ℝ a<VAR>this : 0 ≤ x<GOAL>x = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → ℝ≥0∞<VAR>hd : AEDisjoint μ s t<VAR>ht : NullMeasurableSet t μ<VAR>hs₀ : μ s ≠ 0<VAR>ht₀ : μ t ≠ 0<VAR>hsμ : μ s ≠ ⊤<VAR>htμ : μ t ≠ ⊤<GOAL>⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in t, f x ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → ℝ≥0∞<VAR>hd : AEDisjoint μ s t<VAR>ht : NullMeasurableSet t μ<VAR>hs₀ : μ s ≠ 0<VAR>ht₀ : μ t ≠ 0<VAR>hsμ : μ s ≠ ⊤<VAR>htμ : μ t ≠ ⊤<GOAL>μ s / (μ s + μ t) + μ t / (μ s + μ t) = 1
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{u₂, u₁} C<VAR>inst✝⁵ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝⁴ : FiberFunctor F<VAR>X A B : C<VAR>inst✝³ : IsConnected A<VAR>inst✝² : IsConnected B<VAR>a : ↑(F.obj A)<VAR>b : ↑(F.obj B)<VAR>i : A ⟶ X<VAR>j : B ⟶ X<VAR>h : F.map i a = F.map j b<VAR>inst✝¹ : Mono i<VAR>inst✝ : Mono j<VAR>Y : C := pullback i j<VAR>u : Y ⟶ A := pullback.fst i j<VAR>v : Y ⟶ B := pullback.snd i j<VAR>G : C ⥤ Type w := F ⋙ FintypeCat.incl<VAR>e : ↑(F.obj Y) ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j<VAR>y : ↑(F.obj Y) := e.symm ⟨(a, b), h⟩<GOAL>∃ f, F.map f.hom a = b
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{u₂, u₁} C<VAR>inst✝⁵ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝⁴ : FiberFunctor F<VAR>X A B : C<VAR>inst✝³ : IsConnected A<VAR>inst✝² : IsConnected B<VAR>a : ↑(F.obj A)<VAR>b : ↑(F.obj B)<VAR>i : A ⟶ X<VAR>j : B ⟶ X<VAR>h : F.map i a = F.map j b<VAR>inst✝¹ : Mono i<VAR>inst✝ : Mono j<VAR>Y : C := pullback i j<VAR>u : Y ⟶ A := pullback.fst i j<VAR>v : Y ⟶ B := pullback.snd i j<VAR>G : C ⥤ Type w := F ⋙ FintypeCat.incl<VAR>e : ↑(F.obj Y) ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j<VAR>y : ↑(F.obj Y) := e.symm ⟨(a, b), h⟩<VAR>hn : IsInitial Y → False<GOAL>∃ f, F.map f.hom a = b
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{u₂, u₁} C<VAR>inst✝⁵ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝⁴ : FiberFunctor F<VAR>X A B : C<VAR>inst✝³ : IsConnected A<VAR>inst✝² : IsConnected B<VAR>a : ↑(F.obj A)<VAR>b : ↑(F.obj B)<VAR>i : A ⟶ X<VAR>j : B ⟶ X<VAR>h : F.map i a = F.map j b<VAR>inst✝¹ : Mono i<VAR>inst✝ : Mono j<VAR>Y : C := pullback i j<VAR>u : Y ⟶ A := pullback.fst i j<VAR>v : Y ⟶ B := pullback.snd i j<VAR>G : C ⥤ Type w := F ⋙ FintypeCat.incl<VAR>e : ↑(F.obj Y) ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j<VAR>y : ↑(F.obj Y) := e.symm ⟨(a, b), h⟩<VAR>hn : IsInitial Y → False<VAR>this : IsIso u<GOAL>∃ f, F.map f.hom a = b
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{u₂, u₁} C<VAR>inst✝⁵ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝⁴ : FiberFunctor F<VAR>X A B : C<VAR>inst✝³ : IsConnected A<VAR>inst✝² : IsConnected B<VAR>a : ↑(F.obj A)<VAR>b : ↑(F.obj B)<VAR>i : A ⟶ X<VAR>j : B ⟶ X<VAR>h : F.map i a = F.map j b<VAR>inst✝¹ : Mono i<VAR>inst✝ : Mono j<VAR>Y : C := pullback i j<VAR>u : Y ⟶ A := pullback.fst i j<VAR>v : Y ⟶ B := pullback.snd i j<VAR>G : C ⥤ Type w := F ⋙ FintypeCat.incl<VAR>e : ↑(F.obj Y) ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j<VAR>y : ↑(F.obj Y) := e.symm ⟨(a, b), h⟩<VAR>hn : IsInitial Y → False<VAR>this✝ : IsIso u<VAR>this : IsIso v<GOAL>∃ f, F.map f.hom a = b
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{u₂, u₁} C<VAR>inst✝⁵ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝⁴ : FiberFunctor F<VAR>X A B : C<VAR>inst✝³ : IsConnected A<VAR>inst✝² : IsConnected B<VAR>a : ↑(F.obj A)<VAR>b : ↑(F.obj B)<VAR>i : A ⟶ X<VAR>j : B ⟶ X<VAR>h : F.map i a = F.map j b<VAR>inst✝¹ : Mono i<VAR>inst✝ : Mono j<VAR>Y : C := pullback i j<VAR>u : Y ⟶ A := pullback.fst i j<VAR>v : Y ⟶ B := pullback.snd i j<VAR>G : C ⥤ Type w := F ⋙ FintypeCat.incl<VAR>e : ↑(F.obj Y) ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j<VAR>y : ↑(F.obj Y) := e.symm ⟨(a, b), h⟩<VAR>hn : IsInitial Y → False<VAR>this✝ : IsIso u<VAR>this : IsIso v<GOAL>F.map ((asIso u).symm ≪≫ asIso v).hom a = b
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{u₂, u₁} C<VAR>inst✝⁵ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝⁴ : FiberFunctor F<VAR>X A B : C<VAR>inst✝³ : IsConnected A<VAR>inst✝² : IsConnected B<VAR>a : ↑(F.obj A)<VAR>b : ↑(F.obj B)<VAR>i : A ⟶ X<VAR>j : B ⟶ X<VAR>h : F.map i a = F.map j b<VAR>inst✝¹ : Mono i<VAR>inst✝ : Mono j<VAR>Y : C := pullback i j<VAR>u : Y ⟶ A := pullback.fst i j<VAR>v : Y ⟶ B := pullback.snd i j<VAR>G : C ⥤ Type w := F ⋙ FintypeCat.incl<VAR>e : ↑(F.obj Y) ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j<VAR>y : ↑(F.obj Y) := e.symm ⟨(a, b), h⟩<VAR>hn : IsInitial Y → False<VAR>this✝ : IsIso u<VAR>this : IsIso v<VAR>hu : G.map u y = a<GOAL>F.map ((asIso u).symm ≪≫ asIso v).hom a = b
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{u₂, u₁} C<VAR>inst✝⁵ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝⁴ : FiberFunctor F<VAR>X A B : C<VAR>inst✝³ : IsConnected A<VAR>inst✝² : IsConnected B<VAR>a : ↑(F.obj A)<VAR>b : ↑(F.obj B)<VAR>i : A ⟶ X<VAR>j : B ⟶ X<VAR>h : F.map i a = F.map j b<VAR>inst✝¹ : Mono i<VAR>inst✝ : Mono j<VAR>Y : C := pullback i j<VAR>u : Y ⟶ A := pullback.fst i j<VAR>v : Y ⟶ B := pullback.snd i j<VAR>G : C ⥤ Type w := F ⋙ FintypeCat.incl<VAR>e : ↑(F.obj Y) ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j<VAR>y : ↑(F.obj Y) := e.symm ⟨(a, b), h⟩<VAR>hn : IsInitial Y → False<VAR>this✝ : IsIso u<VAR>this : IsIso v<VAR>hu : G.map u y = a<VAR>hv : G.map v y = b<GOAL>F.map ((asIso u).symm ≪≫ asIso v).hom a = b
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{u₂, u₁} C<VAR>inst✝⁵ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝⁴ : FiberFunctor F<VAR>X A B : C<VAR>inst✝³ : IsConnected A<VAR>inst✝² : IsConnected B<VAR>a : ↑(F.obj A)<VAR>b : ↑(F.obj B)<VAR>i : A ⟶ X<VAR>j : B ⟶ X<VAR>h : F.map i a = F.map j b<VAR>inst✝¹ : Mono i<VAR>inst✝ : Mono j<VAR>Y : C := pullback i j<VAR>u : Y ⟶ A := pullback.fst i j<VAR>v : Y ⟶ B := pullback.snd i j<VAR>G : C ⥤ Type w := F ⋙ FintypeCat.incl<VAR>e : ↑(F.obj Y) ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j<VAR>y : ↑(F.obj Y) := e.symm ⟨(a, b), h⟩<VAR>hn : IsInitial Y → False<VAR>this✝ : IsIso u<VAR>this : IsIso v<VAR>hu : G.map u y = a<VAR>hv : G.map v y = b<GOAL>(F.map u ≫ F.map ((asIso u).symm ≪≫ asIso v).hom) y = F.map v y
<VAR>α : Type u_1<VAR>inst✝ : Fintype α<VAR>k : ℕ<GOAL>card { s // s.card = k } = (card α).choose k
<VAR>R✝ : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R✝<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R✝<VAR>n✝ : ℕ<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<GOAL>(↑(finSuccEquiv R n).symm).comp (Polynomial.C.comp C) = C
<VAR>R✝ : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R✝<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R✝<VAR>n✝ : ℕ<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>x : R<GOAL>((↑(finSuccEquiv R n).symm).comp (Polynomial.C.comp C)) x = C x
<VAR>R✝ : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R✝<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R✝<VAR>n✝ : ℕ<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>x : R<GOAL>↑(finSuccEquiv R n).symm ((Polynomial.C.comp C) x) = C x
<VAR>R✝ : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R✝<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R✝<VAR>n✝ : ℕ<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>x : R<GOAL>(Polynomial.C.comp C) x = (finSuccEquiv R n) (C x)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hab : a < b<GOAL>(b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hab : a < b<GOAL>(b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ = (b - a - 0) * ∫ (x : Ω), ↑(upcrossingsBefore 0 (b - a) (f - fun x x => a)⁺ N x) ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hab : a < b<GOAL>(b - a) * ∫ (x : Ω), ↑(upcrossingsBefore 0 (b - a) (fun n ω => (f n ω - a)⁺) N x) ∂μ = (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore 0 (b - a) (f - fun x x => a)⁺ N x) ∂μ
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type w<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Linear R C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>r : Rˣ<VAR>g : Y ⟶ Z<GOAL>f ≫ (r • g) = r • f ≫ g
<VAR>n k : ℕ<VAR>hk : k ≤ n<GOAL>k ! * (n - k)! ∣ n !
<VAR>n k : ℕ<VAR>hk : k ≤ n<GOAL>k ! * (n - k)! ∣ n.choose k * (k ! * (n - k)!)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : Field K<VAR>inst✝³ : LieAlgebra K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : ↥H → K<VAR>x y : L<VAR>hx : x ∈ rootSpace H α<VAR>hy : y ∈ rootSpace H β<VAR>hαβ : α + β ≠ 0<VAR>σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)<GOAL>((killingForm K L) x) y = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : Field K<VAR>inst✝³ : LieAlgebra K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : ↥H → K<VAR>x y : L<VAR>hx : x ∈ rootSpace H α<VAR>hy : y ∈ rootSpace H β<VAR>hαβ : α + β ≠ 0<VAR>σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)<VAR>hσ : ∀ (γ : ↥H → K), σ γ ≠ γ<GOAL>((killingForm K L) x) y = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : Field K<VAR>inst✝³ : LieAlgebra K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : ↥H → K<VAR>x y : L<VAR>hx : x ∈ rootSpace H α<VAR>hy : y ∈ rootSpace H β<VAR>hαβ : α + β ≠ 0<VAR>σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)<VAR>hσ : ∀ (γ : ↥H → K), σ γ ≠ γ<VAR>f : Module.End K L := (ad K L) x ∘ₗ (ad K L) y<GOAL>((killingForm K L) x) y = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : Field K<VAR>inst✝³ : LieAlgebra K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : ↥H → K<VAR>x y : L<VAR>hx : x ∈ rootSpace H α<VAR>hy : y ∈ rootSpace H β<VAR>hαβ : α + β ≠ 0<VAR>σ : (↥H → K) → ↥H → K := fun γ => α + (β + γ)<VAR>hσ : ∀ (γ : ↥H → K), σ γ ≠ γ<VAR>f : Module.End K L := (ad K L) x ∘ₗ (ad K L) y<VAR>hf : ∀ (γ : ↥H → K), MapsTo ⇑f ↑(rootSpace H γ) ↑(rootSpace H (σ γ))<GOAL>((killingForm K L) x) y = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioi a \ Ioi b = Ioc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>x : α<GOAL>↑(⌈x⌉ - 1) < x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>x : α<GOAL>↑⌈x⌉ < x + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>x : α<VAR>h₁ : ↑(⌈x⌉ - 1) < x<GOAL>x ≤ ↑(⌈x⌉ - 1) + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>x : α<VAR>h₁ : ↑(⌈x⌉ - 1) < x<GOAL>x ≤ ↑⌈x⌉