ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m₁ m₂ : M<VAR>X : C<GOAL>(F.μ (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫ (F.μ m₁ (𝟙_ M ⊗ m₂)).app X ≫ (F.map (α_ m₁ (𝟙_ M) m₂).inv).app X ≫ (F.μIso (m₁ ⊗ 𝟙_ M) m₂).inv.app X = (F.μ (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫ (F.map (λ_ m₂).hom).app ((F.obj m₁).obj X) ≫ (F.obj m₂).map ((F.map (ρ_ m₁).inv).app X)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m₁ m₂ : M<VAR>X : C<GOAL>(F.μ (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫ (F.μ m₁ (𝟙_ M ⊗ m₂)).app X ≫ (F.map (α_ m₁ (𝟙_ M) m₂).inv).app X ≫ (F.μIso (m₁ ⊗ 𝟙_ M) m₂).inv.app X = (F.obj m₂).map (F.εIso.inv.app ((F.obj m₁).obj X) ≫ (F.map (ρ_ m₁).inv).app X)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<GOAL>xᶜ ⊔ x = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<VAR>h₀ : LinearIndependent (ι := { x // x ∈ Set.Iic n }) 𝕜 (f ∘ Subtype.val)<VAR>h : gramSchmidt 𝕜 f n = 0<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<VAR>h₀ : LinearIndependent (ι := { x // x ∈ Set.Iic n }) 𝕜 (f ∘ Subtype.val)<VAR>h : gramSchmidt 𝕜 f n = 0<VAR>h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<VAR>h₀ : LinearIndependent (ι := { x // x ∈ Set.Iic n }) 𝕜 (f ∘ Subtype.val)<VAR>h : gramSchmidt 𝕜 f n = 0<VAR>h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)<VAR>h₂ : (f ∘ Subtype.val) ⟨n, ⋯⟩ ∈ span 𝕜 (f ∘ Subtype.val '' Set.Iio ⟨n, ⋯⟩)<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<VAR>h₀ : LinearIndependent (ι := { x // x ∈ Set.Iic n }) 𝕜 (f ∘ Subtype.val)<VAR>h : gramSchmidt 𝕜 f n = 0<VAR>h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)<VAR>h₂ : (f ∘ Subtype.val) ⟨n, ⋯⟩ ∈ span 𝕜 (f ∘ Subtype.val '' Set.Iio ⟨n, ⋯⟩)<GOAL>⟨n, ⋯⟩ ∉ Set.Iio ⟨n, ⋯⟩
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : Semifield R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : HasContinuousInv₀ R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a✝ : A<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>a : Aˣ<GOAL>spectrum R ↑a ⊆ {0}ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁷ : Monoid α<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : MulAction α β<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : SMulPosMono α β<VAR>inst✝ : SMulPosReflectLE α β<VAR>hb : 0 < b<GOAL>b ≤ a • b ↔ 1 • b ≤ a • b
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<VAR>n : ℕ<GOAL>re ↑n = ↑n
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>m : Multiset α<VAR>f f' : α → β<VAR>hf : ∀ a ∈ m, f a = f' a<GOAL>HEq (map f m) (map f' m)
<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>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : β × γ → E<VAR>F : E → ℝ≥0∞<VAR>hf : Integrable f ((κ ⊗ₖ η) a)<VAR>hg : Integrable g ((κ ⊗ₖ η) a)<GOAL>∫⁻ (x : β), F (∫ (y : γ), f (x, y) - g (x, y) ∂η (a, x)) ∂κ a = ∫⁻ (x : β), F (∫ (y : γ), f (x, y) ∂η (a, x) - ∫ (y : γ), g (x, y) ∂η (a, x)) ∂κ a
<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>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : β × γ → E<VAR>F : E → ℝ≥0∞<VAR>hf : Integrable f ((κ ⊗ₖ η) a)<VAR>hg : Integrable g ((κ ⊗ₖ η) a)<GOAL>(fun x => F (∫ (y : γ), f (x, y) - g (x, y) ∂η (a, x))) =ᶠ[ae (κ a)] fun x => F (∫ (y : γ), f (x, y) ∂η (a, x) - ∫ (y : γ), g (x, y) ∂η (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>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : β × γ → E<VAR>F : E → ℝ≥0∞<VAR>hf : Integrable f ((κ ⊗ₖ η) a)<VAR>hg : Integrable g ((κ ⊗ₖ η) a)<VAR>a✝ : β<VAR>h2f : Integrable (fun y => f (a✝, y)) (η (a, a✝))<VAR>h2g : Integrable (fun y => g (a✝, y)) (η (a, a✝))<GOAL>F (∫ (y : γ), f (a✝, y) - g (a✝, y) ∂η (a, a✝)) = F (∫ (y : γ), f (a✝, y) ∂η (a, a✝) - ∫ (y : γ), g (a✝, y) ∂η (a, a✝))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>inst✝ : DenselyOrdered α<GOAL>(Ioo a b).Nonempty ↔ a < b
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α → β → E<VAR>hf : StronglyMeasurable (uncurry f)<GOAL>MeasurableSet {x | Integrable (f x) ν}
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α → β → E<VAR>hf : StronglyMeasurable (uncurry f)<GOAL>MeasurableSet {x | HasFiniteIntegral (f x) ν}
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>P : K[X]<VAR>k : ℕ<VAR>sep : P.Separable<VAR>nil : minpoly K f ∣ P ^ k<GOAL>∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>P : K[X]<VAR>k : ℕ<VAR>sep : P.Separable<VAR>nil : minpoly K f ∣ P ^ k<VAR>ff : ↥(adjoin K {f}) := ⟨f, ⋯⟩<GOAL>∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>P : K[X]<VAR>k : ℕ<VAR>sep : P.Separable<VAR>nil : minpoly K f ∣ P ^ k<VAR>ff : ↥(adjoin K {f}) := ⟨f, ⋯⟩<VAR>P' : K[X] := derivative P<GOAL>∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>P : K[X]<VAR>k : ℕ<VAR>sep : P.Separable<VAR>nil : minpoly K f ∣ P ^ k<VAR>ff : ↥(adjoin K {f}) := ⟨f, ⋯⟩<VAR>P' : K[X] := derivative P<VAR>nil' : IsNilpotent ((aeval ff) P)<GOAL>∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>P : K[X]<VAR>k : ℕ<VAR>sep : P.Separable<VAR>nil : minpoly K f ∣ P ^ k<VAR>ff : ↥(adjoin K {f}) := ⟨f, ⋯⟩<VAR>P' : K[X] := derivative P<VAR>nil' : IsNilpotent ((aeval ff) P)<VAR>sep' : IsUnit ((aeval ff) P')<GOAL>∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>P : K[X]<VAR>k✝ : ℕ<VAR>sep : P.Separable<VAR>nil : minpoly K f ∣ P ^ k✝<VAR>ff : ↥(adjoin K {f}) := ⟨f, ⋯⟩<VAR>P' : K[X] := derivative P<VAR>nil' : IsNilpotent ((aeval ff) P)<VAR>sep' : IsUnit ((aeval ff) P')<VAR>s : End K V<VAR>mem : s ∈ adjoin K {f}<VAR>hss : (aeval ⟨s, mem⟩) P = 0<VAR>k : ℕ<VAR>hk : (ff - ⟨s, mem⟩) ^ k = 0<GOAL>∃ n ∈ adjoin K {f}, ∃ s ∈ adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>P : K[X]<VAR>k✝ : ℕ<VAR>sep : P.Separable<VAR>nil : minpoly K f ∣ P ^ k✝<VAR>ff : ↥(adjoin K {f}) := ⟨f, ⋯⟩<VAR>P' : K[X] := derivative P<VAR>nil' : IsNilpotent ((aeval ff) P)<VAR>sep' : IsUnit ((aeval ff) P')<VAR>s : End K V<VAR>mem : s ∈ adjoin K {f}<VAR>hss : (aeval ⟨s, mem⟩) P = 0<VAR>k : ℕ<VAR>hk : (ff - ⟨s, mem⟩) ^ k = 0<GOAL>f - s ∈ adjoin K {f}
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>P : K[X]<VAR>k✝ : ℕ<VAR>sep : P.Separable<VAR>nil : minpoly K f ∣ P ^ k✝<VAR>ff : ↥(adjoin K {f}) := ⟨f, ⋯⟩<VAR>P' : K[X] := derivative P<VAR>nil' : IsNilpotent ((aeval ff) P)<VAR>sep' : IsUnit ((aeval ff) P')<VAR>s : End K V<VAR>mem : s ∈ adjoin K {f}<VAR>hss : (aeval ⟨s, mem⟩) P = 0<VAR>k : ℕ<VAR>hk : (ff - ⟨s, mem⟩) ^ k = 0<GOAL>(f - s) ^ k = 0
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>P : K[X]<VAR>k✝ : ℕ<VAR>sep : P.Separable<VAR>nil : minpoly K f ∣ P ^ k✝<VAR>ff : ↥(adjoin K {f}) := ⟨f, ⋯⟩<VAR>P' : K[X] := derivative P<VAR>nil' : IsNilpotent ((aeval ff) P)<VAR>sep' : IsUnit ((aeval ff) P')<VAR>s : End K V<VAR>mem : s ∈ adjoin K {f}<VAR>hss : (aeval ⟨s, mem⟩) P = 0<VAR>k : ℕ<VAR>hk : (ff - ⟨s, mem⟩) ^ k = 0<GOAL>s.IsSemisimple
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>x✝ y : α<VAR>r : ℝ<VAR>f : α → α<VAR>hf : LipschitzWith K f<VAR>x : α<VAR>n : ℕ<GOAL>dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * ↑K ^ n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>x✝ y : α<VAR>r : ℝ<VAR>f : α → α<VAR>hf : LipschitzWith K f<VAR>x : α<VAR>n : ℕ<GOAL>dist (f^[n] x) ((f^[n] ∘ f) x) ≤ ↑K ^ n * dist x (f x)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<VAR>w : W<GOAL>cs.length (t * w) ≠ cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<VAR>w : W<GOAL>cs.lengthParity (t * w) ≠ cs.lengthParity w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w✝ w : W<VAR>i : B<GOAL>cs.lengthParity (w * cs.simple i * w⁻¹ * w✝) ≠ cs.lengthParity w✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R : Type u_5<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : Unique Rˣ<VAR>p₁ p₂ : R<VAR>k₁ k₂ : ℕ<VAR>hp₁ : Prime p₁<VAR>hp₂ : Prime p₂<VAR>hk₁ : 0 < k₁<VAR>h : p₁ ^ k₁ = p₂ ^ k₂<GOAL>p₁ = p₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R : Type u_5<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : Unique Rˣ<VAR>p₁ p₂ : R<VAR>k₁ k₂ : ℕ<VAR>hp₁ : Prime p₁<VAR>hp₂ : Prime p₂<VAR>hk₁ : 0 < k₁<VAR>h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂<GOAL>p₁ ~ᵤ p₂
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<VAR>d : ℝ≥0∞<GOAL>diam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C<VAR>h₁₂ : X₁₂ ⟶ X₁₃<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₂₂ : X₂₂ ⟶ X₂₃<VAR>h₁₃ : X₁₁ ⟶ X₁₃<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₁₃ : X₁₃ ⟶ X₂₃<VAR>s : IsPullback h₁₃ v₁₁ v₁₃ (h₂₁ ≫ h₂₂)<VAR>t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂<GOAL>h₁₃ ≫ v₁₃ = (v₁₁ ≫ h₂₁) ≫ h₂₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>a b : α<VAR>d : αˣ<GOAL>a * b ~ᵤ a * (b * ↑d)
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a b : R<VAR>h : gcd a b = a<GOAL>gcd a b ∣ b
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a b : R<VAR>h : a ∣ b<GOAL>gcd a b = a
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Group G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>ρ : Representation k G V<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>v : V<VAR>hv : v ∈ ρ.invariants<GOAL>ρ.averageMap v = v
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Group G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>ρ : Representation k G V<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>v : V<VAR>hv : ∀ (g : G), (ρ g) v = v<GOAL>ρ.averageMap v = v
<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>e : σ ≃ Fin n<VAR>φ : MvPolynomial (Option σ) R<GOAL>(finSuccEquiv R n) ((rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)) φ) = Polynomial.map (rename ⇑e).toRingHom ((optionEquivLeft R σ) φ)
<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>e : σ ≃ Fin n<VAR>φ : MvPolynomial (Option σ) R<GOAL>(finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom = (mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)
<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>e : σ ≃ Fin n<VAR>φ : MvPolynomial (Option σ) R<GOAL>∀ (r : R), ((finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom) (C r) = ((mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (C r)
<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>e : σ ≃ Fin n<VAR>φ : MvPolynomial (Option σ) R<GOAL>∀ (i : Option σ), ((finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom) (X i) = ((mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (X i)
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : AddTorsor G P<VAR>p₁ p₂ p₃ : P<GOAL>p₁ -ᵥ p₂ +ᵥ p₃ = p₃ -ᵥ p₂ +ᵥ p₁
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : AddTorsor G P<VAR>p₁ p₂ p₃ : P<GOAL>p₁ -ᵥ p₂ + (p₃ -ᵥ p₁ - (p₃ -ᵥ p₂)) = 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>i : ι<VAR>x : A<GOAL>Homogeneous 𝒜 ((GradedRing.proj 𝒜 i) x)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<GOAL>(homogeneousHull 𝒜 I).toIdeal = (⨆ i, { toSubmodule := span (⇑(GradedRing.proj 𝒜 i) '' ↑I), is_homogeneous' := ⋯ }).toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<GOAL>⨆ i, span (⇑(GradedRing.proj 𝒜 i) '' ↑I) = ⨆ i, { toSubmodule := span (⇑(GradedRing.proj 𝒜 i) '' ↑I), is_homogeneous' := ⋯ }.toIdeal
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<GOAL>constantCoeff (wittStructureRat p Φ 0) = constantCoeff Φ
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x : Z<GOAL>x ∈ e.source ↔ proj x ∈ e.baseSet
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>inst✝² : GroupWithZero G₀<VAR>inst✝¹ : Bornology G₀<VAR>inst✝ : MulAction G₀ α<VAR>s t u : Set α<VAR>S : Set (Set α)<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>t ⊆ c • s ↔ MapsTo (fun x => c⁻¹ • x) t s
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>inst✝² : GroupWithZero G₀<VAR>inst✝¹ : Bornology G₀<VAR>inst✝ : MulAction G₀ α<VAR>s t u : Set α<VAR>S : Set (Set α)<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>t ⊆ (fun x => c⁻¹ • x) ⁻¹' s ↔ MapsTo (fun x => c⁻¹ • x) t s
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : g • z ∈ 𝒟ᵒ<GOAL>z = g • z
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : g • z ∈ 𝒟ᵒ<VAR>n : ℤ<VAR>hn : ∀ (z : ℍ), g • z = T ^ n • z<GOAL>z = g • z
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>n : ℤ<VAR>hg : T ^ n • z ∈ 𝒟ᵒ<VAR>hn : ∀ (z : ℍ), g • z = T ^ n • z<GOAL>z = T ^ n • z
<VAR>xl xr : Type u<VAR>x₁ y₁ x₂ y₂ : PGame<VAR>hx : x₁ ≈ x₂<VAR>hy : y₁ ≈ y₂<GOAL>x₁ ⧏ y₁ ∧ y₁ ⧏ x₁ ↔ x₂ ⧏ y₂ ∧ y₂ ⧏ x₂
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>Sn : S.IsNormal<VAR>c d : C<VAR>p : c ⟶ d<GOAL>BijOn (fun γ => Groupoid.inv p ≫ γ ≫ p) (S.arrows c c) (S.arrows d d)
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>Sn : S.IsNormal<VAR>c d : C<VAR>p : c ⟶ d<VAR>γ₁ : c ⟶ c<VAR>x✝¹ : γ₁ ∈ S.arrows c c<VAR>γ₂ : c ⟶ c<VAR>x✝ : γ₂ ∈ S.arrows c c<VAR>h : (fun γ => Groupoid.inv p ≫ γ ≫ p) γ₁ = (fun γ => Groupoid.inv p ≫ γ ≫ p) γ₂<GOAL>γ₁ = γ₂
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>Sn : S.IsNormal<VAR>c d : C<VAR>p : c ⟶ d<VAR>δ : d ⟶ d<VAR>δS : δ ∈ S.arrows d d<GOAL>(fun γ => Groupoid.inv p ≫ γ ≫ p) (p ≫ δ ≫ Groupoid.inv p) = δ
<VAR>a✝ b c d m n a : ℤ<GOAL>(-a.pred).pred = -a
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • closure s + b • interior s ⊆ interior s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>b • interior s + a • closure s ⊆ interior s
<VAR>R : Type u_1<VAR>inst✝ : AddMonoidWithOne R<VAR>m n : ℕ<GOAL>↑(m + n) = ↑m + ↑n
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>F : (X →ᵇ ℝ) → Y →ᵇ ℝ<VAR>hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3<VAR>hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>F : (X →ᵇ ℝ) → Y →ᵇ ℝ<VAR>hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3<VAR>hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖<VAR>g : ℕ → Y →ᵇ ℝ := fun n => (fun g => g + F (f - g.compContinuous e))^[n] 0<VAR>g0 : g 0 = 0<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>F : (X →ᵇ ℝ) → Y →ᵇ ℝ<VAR>hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3<VAR>hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖<VAR>g : ℕ → Y →ᵇ ℝ := fun n => (fun g => g + F (f - g.compContinuous e))^[n] 0<VAR>g0 : g 0 = 0<VAR>g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>F : (X →ᵇ ℝ) → Y →ᵇ ℝ<VAR>hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3<VAR>hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖<VAR>g : ℕ → Y →ᵇ ℝ := fun n => (fun g => g + F (f - g.compContinuous e))^[n] 0<VAR>g0 : g 0 = 0<VAR>g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)<VAR>hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>F : (X →ᵇ ℝ) → Y →ᵇ ℝ<VAR>hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3<VAR>hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖<VAR>g : ℕ → Y →ᵇ ℝ := fun n => (fun g => g + F (f - g.compContinuous e))^[n] 0<VAR>g0 : g 0 = 0<VAR>g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)<VAR>hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖<VAR>hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>F : (X →ᵇ ℝ) → Y →ᵇ ℝ<VAR>hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3<VAR>hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖<VAR>g : ℕ → Y →ᵇ ℝ := fun n => (fun g => g + F (f - g.compContinuous e))^[n] 0<VAR>g0 : g 0 = 0<VAR>g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)<VAR>hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖<VAR>hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n<VAR>hg_cau : CauchySeq g<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f