ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>hB'IB : B' ⊆ I ∪ B<VAR>J : Set α<VAR>hJE : J ⊆ M.E<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hdj : Disjoint J B''<VAR>a✝ : I' ⊆ J<VAR>hJX : J ⊆ X<VAR>hssJ : X ∩ M.E ⊆ B' ∪ J<VAR>hI' : B'' ∩ X ∪ B' \ X ⊆ B'<GOAL>J ⊆ X \ B'
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>hB'IB : B' ⊆ I ∪ B<VAR>J : Set α<VAR>hJE : J ⊆ M.E<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hdj : Disjoint J B''<VAR>a✝ : I' ⊆ J<VAR>hJX : J ⊆ X<VAR>hssJ : X ∩ M.E ⊆ B' ∪ J<VAR>hI' : B'' ∩ X ∪ B' \ X ⊆ B'<VAR>B₁ : Set α<VAR>hB₁ : M.Base B₁<VAR>hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁<VAR>hB₁I : B₁ ⊆ B'' ∩ X ∪ B' \ X ∪ B''<GOAL>J ⊆ X \ B'
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>hB'IB : B' ⊆ I ∪ B<VAR>J : Set α<VAR>hJE : J ⊆ M.E<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hdj : Disjoint J B''<VAR>a✝ : I' ⊆ J<VAR>hJX : J ⊆ X<VAR>hssJ : X ∩ M.E ⊆ B' ∪ J<VAR>hI' : B'' ∩ X ∪ B' \ X ⊆ B'<VAR>B₁ : Set α<VAR>hB₁ : M.Base B₁<VAR>hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁<VAR>hB₁I : B₁ ⊆ B'' ∪ B' \ X<GOAL>J ⊆ X \ B'
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>hB'IB : B' ⊆ I ∪ B<VAR>J : Set α<VAR>hJE : J ⊆ M.E<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hdj : Disjoint J B''<VAR>a✝ : I' ⊆ J<VAR>hJX : J ⊆ X<VAR>hssJ : X ∩ M.E ⊆ B' ∪ J<VAR>hI' : B'' ∩ X ∪ B' \ X ⊆ B'<VAR>B₁ : Set α<VAR>hB₁ : M.Base B₁<VAR>hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁<VAR>hB₁I : B₁ ⊆ B'' ∪ B' \ X<VAR>this : B₁ = B'<GOAL>J ⊆ X \ B'
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>J : Set α<VAR>hJE : J ⊆ M.E<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hdj : Disjoint J B''<VAR>a✝ : I' ⊆ J<VAR>hJX : J ⊆ X<VAR>B₁ : Set α<VAR>hB₁ hB' : M.Base B₁<VAR>hIB' : I ⊆ B₁<VAR>hB'IB : B₁ ⊆ I ∪ B<VAR>hssJ : X ∩ M.E ⊆ B₁ ∪ J<VAR>hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁<VAR>hB₁I : B₁ ⊆ B'' ∪ B₁ \ X<GOAL>J ⊆ X \ B₁
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>J : Set α<VAR>hJE : J ⊆ M.E<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hdj : Disjoint J B''<VAR>a✝ : I' ⊆ J<VAR>hJX : J ⊆ X<VAR>B₁ : Set α<VAR>hB₁ hB' : M.Base B₁<VAR>hIB' : I ⊆ B₁<VAR>hB'IB : B₁ ⊆ I ∪ B<VAR>hssJ : X ∩ M.E ⊆ B₁ ∪ J<VAR>hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁<VAR>hB₁I : B₁ ⊆ B'' ∪ B₁ \ X<VAR>hne : ¬Disjoint J B₁<GOAL>False
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>J : Set α<VAR>hJE : J ⊆ M.E<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hdj : Disjoint J B''<VAR>a✝ : I' ⊆ J<VAR>hJX : J ⊆ X<VAR>B₁ : Set α<VAR>hB₁ hB' : M.Base B₁<VAR>hIB' : I ⊆ B₁<VAR>hB'IB : B₁ ⊆ I ∪ B<VAR>hssJ : X ∩ M.E ⊆ B₁ ∪ J<VAR>hI' hI'B₁ : B'' ∩ X ∪ B₁ \ X ⊆ B₁<VAR>hB₁I : B₁ ⊆ B'' ∪ B₁ \ X<VAR>hne : ¬Disjoint J B₁<VAR>e : α<VAR>heJ : e ∈ J<VAR>heB' : e ∈ B₁<GOAL>False
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I B X : Set α<VAR>M : Matroid α<GOAL>∀ (I : Set α), (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I → I ⊆ M.E
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf'' : ∀ x ∈ interior D, deriv^[2] f x < 0<GOAL>∀ x ∈ interior (interior D), deriv (deriv f) x < 0
<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 : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf : Function.Surjective ⇑f<GOAL>LieSubmodule.map f (lowerCentralSeries R L M k) = lowerCentralSeries R L M₂ k
<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 : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf : Function.Surjective ⇑f<GOAL>lowerCentralSeries R L M₂ k ≤ LieSubmodule.map f (lowerCentralSeries R L M k)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)<VAR>i : ℕ<GOAL>(approxChain f) i ≤ f ((approxChain f) i)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>a : Cardinal.{u}<GOAL>a ≤ o.cof ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>a : Cardinal.{u}<GOAL>a ≤ sInf {a | ∃ ι f, lsub f = o ∧ #ι = a} ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
<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.IsSeparable F E<GOAL>sepDegree F E = Module.rank F E
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝¹¹ : LinearOrderedRing 𝕜<VAR>inst✝¹⁰ : DenselyOrdered 𝕜<VAR>inst✝⁹ : PseudoMetricSpace 𝕜<VAR>inst✝⁸ : OrderTopology 𝕜<VAR>inst✝⁷ : ProperSpace 𝕜<VAR>inst✝⁶ : CompactIccSpace 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : T2Space E<VAR>inst✝² : ContinuousAdd E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>x y : E<GOAL>closure (openSegment 𝕜 x y) = [x-[𝕜]y]
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝¹¹ : LinearOrderedRing 𝕜<VAR>inst✝¹⁰ : DenselyOrdered 𝕜<VAR>inst✝⁹ : PseudoMetricSpace 𝕜<VAR>inst✝⁸ : OrderTopology 𝕜<VAR>inst✝⁷ : ProperSpace 𝕜<VAR>inst✝⁶ : CompactIccSpace 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : T2Space E<VAR>inst✝² : ContinuousAdd E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>x y : E<GOAL>closure ((fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1) = (fun θ => (1 - θ) • x + θ • y) '' closure (Ioo 0 1)
<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>t : Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>h : i₁ ≠ i₂<GOAL>dist t.orthocenter ((EuclideanGeometry.reflection (affineSpan ℝ (t.points '' {i₁, i₂}))) (circumcenter t)) = circumradius t
<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>t : Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>h : i₁ ≠ i₂<GOAL>(-∑ i₁_1 : PointsWithCircumcenterIndex 2, ∑ i₂_1 : PointsWithCircumcenterIndex 2, (mongePointWeightsWithCircumcenter 0 - reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) i₁_1 * (mongePointWeightsWithCircumcenter 0 - reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) i₂_1 * (dist (pointsWithCircumcenter t i₁_1) (pointsWithCircumcenter t i₂_1) * dist (pointsWithCircumcenter t i₁_1) (pointsWithCircumcenter t i₂_1))) / 2 = circumradius t * circumradius t
<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>t : Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>h : i₁ ≠ i₂<GOAL>-(∑ x : Fin (0 + 2 + 1), (∑ x_1 : Fin (0 + 2 + 1), ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) * ((↑(0 + 1))⁻¹ - if x_1 = i₁ ∨ x_1 = i₂ then 1 else 0) * (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1)) * dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1))) + ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) * (-2 / ↑(0 + 1) - -1) * (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) * dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex))) + (∑ x : Fin (0 + 2 + 1), (-2 / ↑(0 + 1) - -1) * ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) * (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) * dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))) + (-2 / ↑(0 + 1) - -1) * (-2 / ↑(0 + 1) - -1) * (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) * dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)))) / 2 = circumradius t * circumradius t
<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>t : Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>h : i₁ ≠ i₂<VAR>hu : {i₁, i₂} ⊆ univ<GOAL>-(∑ x : Fin (0 + 2 + 1), (∑ x_1 : Fin (0 + 2 + 1), ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) * ((↑(0 + 1))⁻¹ - if x_1 = i₁ ∨ x_1 = i₂ then 1 else 0) * (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1)) * dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1))) + ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) * (-2 / ↑(0 + 1) - -1) * (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) * dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex))) + (∑ x : Fin (0 + 2 + 1), (-2 / ↑(0 + 1) - -1) * ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) * (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) * dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))) + (-2 / ↑(0 + 1) - -1) * (-2 / ↑(0 + 1) - -1) * (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) * dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)))) / 2 = circumradius t * circumradius t
<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>t : Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>h : i₁ ≠ i₂<VAR>hu : {i₁, i₂} ⊆ univ<VAR>i₃ : Fin 3<VAR>hi₃ : univ \ {i₁, i₂} = {i₃}<VAR>hi₃₁ : i₃ ≠ i₁<VAR>hi₃₂ : i₃ ≠ i₂<GOAL>-(∑ x : Fin (0 + 2 + 1), (∑ x_1 : Fin (0 + 2 + 1), ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) * ((↑(0 + 1))⁻¹ - if x_1 = i₁ ∨ x_1 = i₂ then 1 else 0) * (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1)) * dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1))) + ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) * (-2 / ↑(0 + 1) - -1) * (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) * dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex))) + (∑ x : Fin (0 + 2 + 1), (-2 / ↑(0 + 1) - -1) * ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) * (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) * dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))) + (-2 / ↑(0 + 1) - -1) * (-2 / ↑(0 + 1) - -1) * (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) * dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)))) / 2 = circumradius t * circumradius t
<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>t : Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>h✝ : i₁ ≠ i₂<VAR>hu : {i₁, i₂} ⊆ univ<VAR>i₃ : Fin 3<VAR>hi₃ : univ \ {i₁, i₂} = {i₃}<VAR>hi₃₁ : i₃ ≠ i₁<VAR>hi₃₂ : i₃ ≠ i₂<VAR>h : ¬(i₃ = i₁ ∨ i₃ = i₂)<GOAL>-((-2 + 1) * (circumradius t * circumradius t)) = circumradius t * circumradius t
<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>x y : L<VAR>m : M<GOAL>((fun x => { toFun := fun m => ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }) (x + y)) m = ((fun x => { toFun := fun m => ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }) x + (fun x => { toFun := fun m => ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }) y) m
<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>t : R<VAR>x : L<VAR>m : M<GOAL>({ toFun := fun x => { toFun := fun m => ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun (t • x)) m = ((RingHom.id R) t • { toFun := fun x => { toFun := fun m => ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun x) m
<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>x y : L<VAR>m : M<GOAL>({ toFun := fun x => { toFun := fun m => ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }.toFun ⁅x, y⁆) m = ⁅{ toFun := fun x => { toFun := fun m => ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }.toFun x, { toFun := fun x => { toFun := fun m => ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }.toFun y⁆ m
<VAR>m n✝ a n : ℕ<GOAL>↑(a % n) = ↑a
<VAR>m n✝ a n : ℕ<GOAL>↑(a % n) = ↑(a % n + n * (a / n))
<VAR>n : ℕ<VAR>m : ℝ<VAR>hm : 2 ≤ m<GOAL>2 / m ^ (n ! * (n + 1)) ≤ 1 / m ^ (n ! * n)
<VAR>n : ℕ<VAR>m : ℝ<VAR>hm : 2 ≤ m<GOAL>2 * m ^ (n ! * n) ≤ 1 * m ^ (n ! * (n + 1))
<VAR>n : ℕ<VAR>m : ℝ<VAR>hm : 2 ≤ m<GOAL>0 < m ^ (n ! * (n + 1))
<VAR>n : ℕ<VAR>m : ℝ<VAR>hm : 2 ≤ m<GOAL>0 < m ^ (n ! * n)
<VAR>n : ℕ<VAR>m : ℝ<VAR>hm : 2 ≤ m<GOAL>2 ≤ m ^ n !
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<VAR>t : Set Y<VAR>x✝ : X<VAR>y : Y<VAR>h : e.IsImage s t<VAR>x : X<VAR>hx : x ∈ e.source<GOAL>↑e x ∈ closure t ↔ x ∈ closure s
<VAR>F✝ : Type u_1<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>t : ℝ<VAR>ht : 1 ≤ t<VAR>x : X<GOAL>(F.extend t) x = f₁ x
<VAR>F✝ : Type u_1<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>t : ℝ<VAR>ht : 1 ≤ t<VAR>x : X<GOAL>(F.extend t) x = F (1, x)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>f : G ⧸ H → G<VAR>hf : ∀ (q : G ⧸ H), ↑(f q) = q<VAR>q₁ q₂ : G ⧸ H<VAR>h : (range f).restrict Quotient.mk'' ⟨f q₁, ⋯⟩ = (range f).restrict Quotient.mk'' ⟨f q₂, ⋯⟩<GOAL>⟨f q₁, ⋯⟩ = ⟨f q₂, ⋯⟩
<VAR>α : Type u_2<VAR>β : α → Type u_1<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (β a)<GOAL>l₁.sigma l₂ = l₁.sigmaTR l₂
<VAR>α : Type u_2<VAR>β : α → Type u_1<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (β a)<GOAL>(l₁.bind fun a => map (Sigma.mk a) (l₂ a)) = (foldl (fun acc a => foldl (fun acc b => acc.push ⟨a, b⟩) acc (l₂ a)) #[] l₁).data
<VAR>α : Type u_2<VAR>β : α → Type u_1<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (β a)<GOAL>(l₁.bind fun a => map (Sigma.mk a) (l₂ a)) = #[].data ++ l₁.bind ?h.h.h.h.G
<VAR>α : Type u_2<VAR>β : α → Type u_1<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (β a)<GOAL>α → List ((a : α) × β a)
<VAR>α : Type u_2<VAR>β : α → Type u_1<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (β a)<GOAL>∀ (acc : Array ((a : α) × β a)) (a : α), (foldl (fun acc b => acc.push ⟨a, b⟩) acc (l₂ a)).data = acc.data ++ ?h.h.h.h.G a
<VAR>α : Type u_2<VAR>β : α → Type u_1<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (β a)<VAR>acc✝ : Array ((a : α) × β a)<VAR>a✝ : α<GOAL>(foldl (fun acc b => acc.push ⟨a✝, b⟩) acc✝ (l₂ a✝)).data = acc✝.data ++ map (Sigma.mk a✝) (l₂ a✝)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ✝ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f g✝ : ι → α<VAR>inst✝² : CommSemiring α<VAR>inst✝¹ : DecidableEq ι<VAR>κ : Type u_6<VAR>inst✝ : Fintype ι<VAR>s : Finset κ<VAR>g : ι → κ → α<GOAL>∑ f ∈ piFinset fun x => s, ∏ i : ι, g i (f i) = ∏ i : ι, ∑ j ∈ s, g i j
<VAR>m n : ℕ<VAR>hd : m ∣ n<VAR>hs : IsSquare (-1)<VAR>f : ZMod n →+* ZMod m := castHom hd (ZMod m)<GOAL>IsSquare (-1)
<VAR>m n : ℕ<VAR>hd : m ∣ n<VAR>hs : IsSquare (-1)<VAR>f : ZMod n →+* ZMod m := castHom hd (ZMod m)<GOAL>IsSquare (f (-1))
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>r s : R<VAR>x y : M<GOAL>2 • x = 2 • x
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v : V<VAR>p : G.Walk u v<VAR>d : G.Dart<VAR>h : d ∈ p.darts<GOAL>d.toProd.2 ∈ p.support
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>S : Type v<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : P.IsPrime<VAR>i : ℕ<VAR>hi : i < e<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>x✝ : S ⧸ P<VAR>x : S<VAR>y✝ : S ⧸ P<VAR>y : S<VAR>h : (quotientToQuotientRangePowQuotSucc f p P a_mem) (Quotient.mk'' x) = (quotientToQuotientRangePowQuotSucc f p P a_mem) (Quotient.mk'' y)<GOAL>Quotient.mk'' x = Quotient.mk'' y
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>S : Type v<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : P.IsPrime<VAR>i : ℕ<VAR>hi : i < e<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>x✝ : S ⧸ P<VAR>x : S<VAR>y✝ : S ⧸ P<VAR>y : S<VAR>h : (quotientToQuotientRangePowQuotSucc f p P a_mem) (Quotient.mk'' x) = (quotientToQuotientRangePowQuotSucc f p P a_mem) (Quotient.mk'' y)<VAR>Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)<GOAL>Quotient.mk'' x = Quotient.mk'' y
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>S : Type v<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : P.IsPrime<VAR>i : ℕ<VAR>hi : i < e<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>x✝ : S ⧸ P<VAR>x : S<VAR>y✝ : S ⧸ P<VAR>y : S<VAR>Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)<VAR>h : ∃ y_1, ↑((powQuotSuccInclusion f p P i) y_1) = (Quotient.mk (P ^ e)) (a * x) - (Quotient.mk (P ^ e)) (a * y)<GOAL>x - y ∈ P
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>S : Type v<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : P.IsPrime<VAR>i : ℕ<VAR>hi : i < e<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>x✝ : S ⧸ P<VAR>x : S<VAR>y✝ : S ⧸ P<VAR>y : S<VAR>Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)<VAR>val✝ : S ⧸ P ^ e<VAR>z : S<VAR>hz : Quot.mk Setoid.r z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))<VAR>h : ↑((powQuotSuccInclusion f p P i) ⟨Quot.mk Setoid.r z, hz⟩) = (Quotient.mk (P ^ e)) (a * x) - (Quotient.mk (P ^ e)) (a * y)<GOAL>x - y ∈ P
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>S : Type v<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : P.IsPrime<VAR>i : ℕ<VAR>hi : i < e<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>x✝ : S ⧸ P<VAR>x : S<VAR>y✝ : S ⧸ P<VAR>y : S<VAR>Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)<VAR>val✝ : S ⧸ P ^ e<VAR>z : S<VAR>hz✝ : Quot.mk Setoid.r z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))<VAR>hz : z ∈ P ^ (i + 1)<VAR>h : ↑((powQuotSuccInclusion f p P i) ⟨Quot.mk Setoid.r z, hz✝⟩) = (Quotient.mk (P ^ e)) (a * x) - (Quotient.mk (P ^ e)) (a * y)<GOAL>x - y ∈ P
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>S : Type v<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : P.IsPrime<VAR>i : ℕ<VAR>hi : i < e<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>x✝ : S ⧸ P<VAR>x : S<VAR>y✝ : S ⧸ P<VAR>y : S<VAR>Pe_le_Pi1 : P ^ e ≤ P ^ (i + 1)<VAR>val✝ : S ⧸ P ^ e<VAR>z : S<VAR>hz✝ : Quot.mk Setoid.r z ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1))<VAR>hz : z ∈ P ^ (i + 1)<VAR>h : z - a * (x - y) ∈ P ^ e<GOAL>x - y ∈ P
<VAR>α : Type u<VAR>inst✝ : DivisionMonoid α<GOAL>∀ (u₁ u₂ : αˣ), ↑(u₁ / u₂) = ↑u₁ / ↑u₂
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<GOAL>∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)