ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>G : Type u_1 → Type u_1<VAR>inst✝¹ : Applicative G<VAR>inst✝ : CommApplicative G<VAR>α β γ : Type u_1<VAR>g : α → G β<VAR>h : β → γ<VAR>x : Multiset α<VAR>a✝ : List α<GOAL>Functor.map h <$> traverse g ⟦a✝⟧ = traverse (Functor.map h ∘ g) ⟦a✝⟧
<VAR>F : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>G : Type u_1 → Type u_1<VAR>inst✝¹ : Applicative G<VAR>inst✝ : CommApplicative G<VAR>α β γ : Type u_1<VAR>g : α → G β<VAR>h : β → γ<VAR>x : Multiset α<VAR>a✝ : List α<GOAL>(Coe.coe ∘ Functor.map h) <$> Traversable.traverse g a✝ = Coe.coe <$> Traversable.traverse (Functor.map h ∘ g) a✝
<VAR>F : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>G : Type u_1 → Type u_1<VAR>inst✝¹ : Applicative G<VAR>inst✝ : CommApplicative G<VAR>α β γ : Type u_1<VAR>g : α → G β<VAR>h : β → γ<VAR>x : Multiset α<VAR>a✝ : List α<GOAL>Coe.coe <$> Functor.map h <$> Traversable.traverse g a✝ = Coe.coe <$> (Functor.map (Functor.map h) ∘ Traversable.traverse g) a✝
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m n : E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : Integrable f' volume<VAR>hf : Integrable f volume<VAR>hE : CompleteSpace E<GOAL>∫ (x : ℝ), f' x = 0
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m n : E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : Integrable f' volume<VAR>hf : Integrable f volume<VAR>hE : CompleteSpace E<VAR>A : Tendsto f atBot (𝓝 0)<GOAL>∫ (x : ℝ), f' x = 0
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m n : E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : Integrable f' volume<VAR>hf : Integrable f volume<VAR>hE : CompleteSpace E<VAR>A : Tendsto f atBot (𝓝 0)<VAR>B : Tendsto f atTop (𝓝 0)<GOAL>∫ (x : ℝ), f' x = 0
<VAR>x : ℕ<VAR>h : (↑x).Dom<GOAL>(↑x).get h = x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<GOAL>Collinear k s ↔ ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<GOAL>Collinear k ∅ ↔ ∃ p₀ v, ∀ p ∈ ∅, ∃ r, p = r • v +ᵥ p₀
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<GOAL>Collinear k s ↔ ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
<VAR>X : Compactum<VAR>A : Set X.A<VAR>x✝ : X.A<GOAL>x✝ ∈ Compactum.cl A ↔ x✝ ∈ closure A
<VAR>X : Compactum<VAR>A : Set X.A<VAR>x✝ : X.A<GOAL>x✝ ∈ Compactum.cl A ↔ ∃ u, A ∈ u ∧ ↑u ≤ 𝓝 x✝
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : Fintype β<VAR>ha : a ≠ 0<GOAL>a • Set.univ = Set.univ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : GroupWithZero α<VAR>s✝ t s : Set α<GOAL>s / 0 ⊆ 0
<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<GOAL>ContDiff 𝕜 1 f ↔ ∃ f', Continuous f' ∧ ∀ (x : E), HasFDerivAt f (f' x) x
<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>x✝ : E → E →L[𝕜] F<GOAL>Continuous x✝ ↔ ContDiff 𝕜 (↑Nat.zero) x✝
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hf : StronglyMeasurable f<VAR>c : ℝ<VAR>hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(hf.approxBounded c n) x) atTop (𝓝 (f x))
<GOAL>StrictConcaveOn ℝ (Iio 0) log
<GOAL>∀ ⦃x : ℝ⦄, x ∈ Iio 0 → ∀ ⦃y : ℝ⦄, y ∈ Iio 0 → x ≠ y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • log x + b • log y < log (a • x + b • y)
<VAR>x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<VAR>hy : y < 0<VAR>hxy : x ≠ y<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hx' : 0 < -x<VAR>hy' : 0 < -y<GOAL>a • log x + b • log y < log (a • x + b • y)
<VAR>x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<VAR>hy : y < 0<VAR>hxy : x ≠ y<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hx' : 0 < -x<VAR>hy' : 0 < -y<VAR>hxy' : -x ≠ -y<GOAL>a • log x + b • log y < log (a • x + b • y)
<VAR>m✝ n✝ m n : ℕ<VAR>nzm : NeZero m<VAR>h : m ≤ n<GOAL>Injective cast
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra K F<VAR>ι : Type w<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>x : L<GOAL>(norm K) x = (norm K) (AdjoinSimple.gen K x) ^ finrank (↥K⟮x⟯) L
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra K F<VAR>ι : Type w<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>x : L<VAR>this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L<GOAL>(norm K) x = (norm K) (AdjoinSimple.gen K x) ^ finrank (↥K⟮x⟯) L
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra K F<VAR>ι : Type w<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>x : L<VAR>this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L<VAR>pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L<GOAL>(norm K) x = (norm K) (AdjoinSimple.gen K x) ^ finrank (↥K⟮x⟯) L
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra K F<VAR>ι : Type w<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>x : L<VAR>this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L<VAR>pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L<VAR>pbx : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis ⋯<GOAL>(norm K) x = (norm K) (AdjoinSimple.gen K x) ^ finrank (↥K⟮x⟯) L
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra K F<VAR>ι : Type w<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>x : L<VAR>this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L<VAR>pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L<VAR>pbx : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis ⋯<GOAL>∏ k : Fin pbL.dim, ((leftMulMatrix pbx.basis) (AdjoinSimple.gen K x)).det = ((leftMulMatrix pbx.basis) (AdjoinSimple.gen K ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)))).det ^ finrank (↥K⟮(algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)⟯) L
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra K F<VAR>ι : Type w<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>x : L<VAR>this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L<VAR>pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L<VAR>pbx : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis ⋯<GOAL>((leftMulMatrix pbx.basis) (AdjoinSimple.gen K x)).det ^ pbL.dim = ((leftMulMatrix pbx.basis) (AdjoinSimple.gen K ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)))).det ^ finrank (↥K⟮(algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)⟯) L
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra K F<VAR>ι : Type w<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>x : L<VAR>this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L<VAR>pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L<VAR>pbx : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis ⋯<GOAL>pbL.dim = finrank (↥K⟮(algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)⟯) L
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>((-o).kahler x) y = (starRingEnd ℂ) ((o.kahler x) y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f g s t : ι → α<VAR>a b : α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨆ i, ⨆ (_ : i ≥ n), u i = ⨆ i, u (i + n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f g s t : ι → α<VAR>a b : α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>∀ i ≥ n, u i ≤ ⨆ i, u (i + n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f g s t : ι → α<VAR>a b : α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>∀ (i : ℕ), u (i + n) ≤ ⨆ i, ⨆ (_ : i ≥ n), u i
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Mul β<VAR>f g : FreeMagma α →ₙ* β<VAR>h : ⇑f ∘ of = ⇑g ∘ of<VAR>x x✝ y✝ : FreeMagma α<VAR>a✝¹ : f x✝ = g x✝<VAR>a✝ : f y✝ = g y✝<GOAL>f (x✝ * y✝) = g (x✝ * y✝)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : CommMonoid P<VAR>f : M →* P<VAR>g : N →* P<VAR>x : N<GOAL>((f.coprod g).comp (inr M N)) x = g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>b : β<GOAL>f ×ˢ pure b = map (fun a => (a, b)) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>b : β<GOAL>map ((fun g => g b) ∘ Prod.mk) f = map (fun a => (a, b)) f
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a b : WithBot α<VAR>h : a ≠ 0<GOAL>a * ⊥ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>M : Type u_4<VAR>inst✝¹ : Fintype α<VAR>inst✝ : CommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>h₁ : a ≠ b<VAR>h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1<GOAL>∏ x : α, f x = f a * f b
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>h_deg_le : f.degree ≤ ↑s.card<VAR>h_deg_eq : f.degree = g.degree<VAR>hlc : f.leadingCoeff = g.leadingCoeff<VAR>h_eval : ∀ i ∈ s, eval (v i) f = eval (v i) g<GOAL>f = g
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>g : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>h_deg_le : degree 0 ≤ ↑s.card<VAR>h_deg_eq : degree 0 = g.degree<VAR>hlc : leadingCoeff 0 = g.leadingCoeff<VAR>h_eval : ∀ i ∈ s, eval (v i) 0 = eval (v i) g<GOAL>0 = g
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>h_deg_le : f.degree ≤ ↑s.card<VAR>h_deg_eq : f.degree = g.degree<VAR>hlc : f.leadingCoeff = g.leadingCoeff<VAR>h_eval : ∀ i ∈ s, eval (v i) f = eval (v i) g<VAR>hf : f ≠ 0<GOAL>f = g
<VAR>α : Type u_1<VAR>inst✝ : Infinite α<VAR>s : Finset α<GOAL>#↑(↑s)ᶜ = #α
<VAR>α : Type u_1<VAR>inst✝ : Infinite α<VAR>s : Finset α<GOAL>#↑↑s < #α
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hPz : P z = 0<GOAL>addU P Q = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : CharP k p<VAR>x : 𝕎 k<VAR>hx : x.coeff 0 ≠ 0<VAR>y : kˣ := Units.mk0 (x.coeff 0) hx<VAR>hy : x.coeff 0 = ↑y<GOAL>IsUnit x
<VAR>α : Type u_1<VAR>m0✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>(μ.withDensity f).trim hm = (μ.trim hm).withDensity f
<VAR>α : Type u_1<VAR>m0✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>((μ.withDensity f).trim hm) s = ((μ.trim hm).withDensity f) s
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.Disjoint []
<VAR>α : Type u_1<VAR>l : List α<GOAL>[].Disjoint l
<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₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<VAR>hn : ¬Collinear ℝ {p₁, p₂, p₄}<GOAL>Cospherical {p₁, p₂, 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₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<VAR>hn : ¬Collinear ℝ {p₁, p₂, p₄}<VAR>hn' : ¬Collinear ℝ {p₁, p₃, p₄}<GOAL>Cospherical {p₁, p₂, 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₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<VAR>hn : ¬Collinear ℝ {p₁, p₂, p₄}<VAR>hn' : ¬Collinear ℝ {p₁, p₃, p₄}<VAR>t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }<GOAL>Cospherical {p₁, p₂, 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₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<VAR>hn : ¬Collinear ℝ {p₁, p₂, p₄}<VAR>hn' : ¬Collinear ℝ {p₁, p₃, p₄}<VAR>t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }<VAR>t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }<GOAL>Cospherical {p₁, p₂, 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₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<VAR>hn : ¬Collinear ℝ {p₁, p₂, p₄}<VAR>hn' : ¬Collinear ℝ {p₁, p₃, p₄}<VAR>t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }<VAR>t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }<GOAL>∃ s, {p₁, p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius
<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₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<VAR>hn : ¬Collinear ℝ {p₁, p₂, p₄}<VAR>hn' : ¬Collinear ℝ {p₁, p₃, p₄}<VAR>t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }<VAR>t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }<GOAL>{p₁, p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius
<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₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<VAR>hn : ¬Collinear ℝ {p₁, p₂, p₄}<VAR>hn' : ¬Collinear ℝ {p₁, p₃, p₄}<VAR>t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }<VAR>t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }<GOAL>p₁ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius ∧ p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius ∧ p₃ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius ∧ p₄ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius
<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₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<VAR>hn : ¬Collinear ℝ {p₁, p₂, p₄}<VAR>hn' : ¬Collinear ℝ {p₁, p₃, p₄}<VAR>t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }<VAR>t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }<GOAL>p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius
<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₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<VAR>hn : ¬Collinear ℝ {p₁, p₂, p₄}<VAR>hn' : ¬Collinear ℝ {p₁, p₃, p₄}<VAR>t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }<VAR>t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }<GOAL>p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t₁).center (Affine.Simplex.circumsphere t₁).radius
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν ν₁ ν₂ μ : Measure α<VAR>inst✝⁴ : IsFiniteMeasure ν₁<VAR>inst✝³ : IsFiniteMeasure ν₂<VAR>inst✝² : ν₁.HaveLebesgueDecomposition μ<VAR>inst✝¹ : ν₂.HaveLebesgueDecomposition μ<VAR>inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ<GOAL>(ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν ν₁ ν₂ μ : Measure α<VAR>inst✝⁴ : IsFiniteMeasure ν₁<VAR>inst✝³ : IsFiniteMeasure ν₂<VAR>inst✝² : ν₁.HaveLebesgueDecomposition μ<VAR>inst✝¹ : ν₂.HaveLebesgueDecomposition μ<VAR>inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ<GOAL>μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν ν₁ ν₂ μ : Measure α<VAR>inst✝⁴ : IsFiniteMeasure ν₁<VAR>inst✝³ : IsFiniteMeasure ν₂<VAR>inst✝² : ν₁.HaveLebesgueDecomposition μ<VAR>inst✝¹ : ν₂.HaveLebesgueDecomposition μ<VAR>inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ<GOAL>AEMeasurable ((ν₁ + ν₂).rnDeriv μ) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν ν₁ ν₂ μ : Measure α<VAR>inst✝⁴ : IsFiniteMeasure ν₁<VAR>inst✝³ : IsFiniteMeasure ν₂<VAR>inst✝² : ν₁.HaveLebesgueDecomposition μ<VAR>inst✝¹ : ν₂.HaveLebesgueDecomposition μ<VAR>inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ<GOAL>AEMeasurable (ν₁.rnDeriv μ + ν₂.rnDeriv μ) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν ν₁ ν₂ μ : Measure α<VAR>inst✝⁴ : IsFiniteMeasure ν₁<VAR>inst✝³ : IsFiniteMeasure ν₂<VAR>inst✝² : ν₁.HaveLebesgueDecomposition μ<VAR>inst✝¹ : ν₂.HaveLebesgueDecomposition μ<VAR>inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ<GOAL>∫⁻ (x : α), (ν₁ + ν₂).rnDeriv μ x ∂μ ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>ha : AddLECancellable a<VAR>h : a + c < b<GOAL>c + a < b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<GOAL>↑s.innerDualCone = ⋂ i, ↑{↑i}.innerDualCone
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : TopologicalSpace α<VAR>f : α → G<VAR>s✝ : Set α<VAR>x✝ : α<VAR>ι : Sort u_1<VAR>p : ι → Prop<VAR>s : ι → Set G<VAR>hb : (𝓝 1).HasBasis p s<VAR>x : G<GOAL>(𝓝 x).HasBasis p fun i => {y | y / x ∈ s i}
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : TopologicalSpace α<VAR>f : α → G<VAR>s✝ : Set α<VAR>x✝ : α<VAR>ι : Sort u_1<VAR>p : ι → Prop<VAR>s : ι → Set G<VAR>hb : (𝓝 1).HasBasis p s<VAR>x : G<GOAL>(Filter.comap (fun x_1 => x_1 * x⁻¹) (𝓝 1)).HasBasis p fun i => {y | y / x ∈ s i}
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : TopologicalSpace α<VAR>f : α → G<VAR>s✝ : Set α<VAR>x✝ : α<VAR>ι : Sort u_1<VAR>p : ι → Prop<VAR>s : ι → Set G<VAR>hb : (𝓝 1).HasBasis p s<VAR>x : G<GOAL>(Filter.comap (fun x_1 => x_1 * x⁻¹) (𝓝 1)).HasBasis p fun i => {y | y * x⁻¹ ∈ s i}
<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>x : α<GOAL>ContinuousWithinAt f univ x ↔ ContinuousAt f x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : OrderedRing R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module R V<VAR>inst✝⁴ : AddTorsor V P<VAR>inst✝³ : AddCommGroup V'<VAR>inst✝² : Module R V'<VAR>inst✝¹ : AddTorsor V' P'<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>x y z : P<VAR>h : Wbtw R x y z<GOAL>Wbtw R z x y ↔ x = y