ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R<VAR>c : Fin n → R<VAR>A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0<VAR>A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc<GOAL>Aᵀ.det = Bᵀ.det
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t c : ℝ<GOAL>mgf (fun x => c) μ t = (μ Set.univ).toReal * rexp (t * c)
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>x : ι<VAR>a : α<VAR>s' : Finset ↑{x' | x' ≠ x}<VAR>this : DecidableEq ι<VAR>ha : (image (fun z => ↑z) s').Nonempty → image (fun z => ↑z) s' ≠ univ → (image (fun z => ↑z) s').card < ((image (fun z => ↑z) s').biUnion t).card<GOAL>s'.card ≤ (s'.biUnion fun x' => (t ↑x').erase a).card
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>x : ι<VAR>a : α<VAR>s' : Finset ↑{x' | x' ≠ x}<VAR>this : DecidableEq ι<VAR>ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → s'.card < ((image (fun z => ↑z) s').biUnion t).card<GOAL>s'.card ≤ (s'.biUnion fun x' => (t ↑x').erase a).card
<VAR>K : Type u<VAR>inst✝⁴ : Field K<VAR>R : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : FunLike F K[X] R[X]<VAR>inst✝ : MonoidHomClass F K[X] R[X]<VAR>φ : F<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰<VAR>f : RatFunc K<GOAL>(map φ hφ) f = (algebraMap R[X] (RatFunc R)) (φ f.num) / (algebraMap R[X] (RatFunc R)) (φ f.denom)
<VAR>K : Type u<VAR>inst✝⁴ : Field K<VAR>R : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : FunLike F K[X] R[X]<VAR>inst✝ : MonoidHomClass F K[X] R[X]<VAR>φ : F<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰<VAR>f : RatFunc K<GOAL>f.denom ≠ 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<GOAL>(pderiv y) (X y ^ 2 + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 3 - (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z ^ 2 + C W'.a₄ * X x * X z ^ 4 + C W'.a₆ * X z ^ 6)) = C 2 * X y + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 3
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<GOAL>↑2 * X y ^ (2 - 1) * 1 + (((0 * X x + C W'.a₁ * 0) * X y + C W'.a₁ * X x * 1) * X z + C W'.a₁ * X x * X y * 0) + ((0 * X y + C W'.a₃ * 1) * X z ^ 3 + C W'.a₃ * X y * (↑3 * X z ^ (3 - 1) * 0)) - (↑3 * X x ^ (3 - 1) * 0 + ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 0)) * X z ^ 2 + C W'.a₂ * X x ^ 2 * (↑2 * X z ^ (2 - 1) * 0)) + ((0 * X x + C W'.a₄ * 0) * X z ^ 4 + C W'.a₄ * X x * (↑4 * X z ^ (4 - 1) * 0)) + (0 * X z ^ 6 + C W'.a₆ * (↑6 * X z ^ (6 - 1) * 0))) = 2 * X y + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 3
<VAR>k : ℕ<GOAL>antidiagonalTuple (k + 1) 0 = [0]
<VAR>k : ℕ<GOAL>[Fin.cons (0, 0).1 0] = [0]
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : MonoidHomClass 𝓕 E F<VAR>f : 𝓕<VAR>K : ℝ≥0<VAR>h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖<VAR>x y : E<GOAL>dist x y ≤ ↑K * dist (f x) (f y)
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>r : ℝ<GOAL>(starRingEnd K) ↑r = ↑r
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>r : ℝ<GOAL>re ((starRingEnd K) ↑r) = re ↑r ∧ im ((starRingEnd K) ↑r) = im ↑r
<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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p p₁ p₂ : P<VAR>r : ℝ<VAR>hp₁ : p₁ ∈ affineSpan ℝ (insert p (Set.range s.points))<VAR>hp₂ : p₂ ∈ affineSpan ℝ (insert p (Set.range s.points))<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r<VAR>span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)<GOAL>p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) 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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p p₁ p₂ : P<VAR>r : ℝ<VAR>hp₁ : p₁ ∈ affineSpan ℝ (insert p (Set.range s.points))<VAR>hp₂ : p₂ ∈ affineSpan ℝ (insert p (Set.range s.points))<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r<VAR>span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<GOAL>p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) 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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p p₁ p₂ : P<VAR>r : ℝ<VAR>hp₁ : p₁ ∈ affineSpan ℝ (insert p (Set.range s.points))<VAR>hp₂ : p₂ ∈ affineSpan ℝ (insert p (Set.range s.points))<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r<VAR>span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<VAR>h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter<GOAL>p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) 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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p p₁ p₂ : P<VAR>r : ℝ<VAR>hp₁ : ∃ r, ∃ p0 ∈ affineSpan ℝ (Set.range s.points), p₁ = r • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p0<VAR>hp₂ : ∃ r, ∃ p0 ∈ affineSpan ℝ (Set.range s.points), p₂ = r • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p0<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r<VAR>span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<VAR>h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter<GOAL>p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) 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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p p₁ p₂ : P<VAR>r : ℝ<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r<VAR>span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<VAR>h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter<VAR>r₁ : ℝ<VAR>p₁o : P<VAR>hp₁o : p₁o ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₁o<VAR>r₂ : ℝ<VAR>p₂o : P<VAR>hp₂o : p₂o ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₂o<GOAL>p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) 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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p p₁ p₂ : P<VAR>r : ℝ<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r<VAR>span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<VAR>h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter<VAR>r₁ r₂ : ℝ<VAR>p₂o : P<VAR>hp₂o : p₂o ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₂o<VAR>hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ ↑(s.orthogonalProjectionSpan p₁)<GOAL>p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) 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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p p₁ p₂ : P<VAR>r : ℝ<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r<VAR>span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<VAR>h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter<VAR>r₁ r₂ : ℝ<VAR>p₂o : P<VAR>hp₂o : p₂o ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₂o<VAR>hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter<GOAL>p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) 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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p p₁ p₂ : P<VAR>r : ℝ<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r<VAR>span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<VAR>h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter<VAR>r₁ r₂ : ℝ<VAR>hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter<VAR>hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ ↑(s.orthogonalProjectionSpan p₂)<GOAL>p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) 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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p p₁ p₂ : P<VAR>r : ℝ<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r<VAR>span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<VAR>h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter<VAR>r₁ r₂ : ℝ<VAR>hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter<VAR>hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter<GOAL>p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) 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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p p₁ p₂ : P<VAR>r : ℝ<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r<VAR>span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<VAR>h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter<VAR>r₁ r₂ : ℝ<VAR>hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter<VAR>hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter<VAR>h : s.points 0 ∈ span_s<GOAL>p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) 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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p p₁ p₂ : P<VAR>r : ℝ<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r<VAR>span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<VAR>h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter<VAR>r₁ r₂ : ℝ<VAR>hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter<VAR>hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter<VAR>h : s.points 0 ∈ span_s<VAR>hd₁ : dist p₁ s.circumcenter * dist p₁ s.circumcenter = r * r - s.circumradius * s.circumradius<GOAL>p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) 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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p p₁ p₂ : P<VAR>r : ℝ<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r<VAR>span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<VAR>h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter<VAR>r₁ r₂ : ℝ<VAR>hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter<VAR>hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter<VAR>h : s.points 0 ∈ span_s<VAR>hd₁ : dist p₁ s.circumcenter * dist p₁ s.circumcenter = r * r - s.circumradius * s.circumradius<VAR>hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius<GOAL>p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) 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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p p₁ p₂ : P<VAR>r : ℝ<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r<VAR>span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<VAR>h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter<VAR>r₁ r₂ : ℝ<VAR>hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter<VAR>hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)<VAR>hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter<VAR>h : s.points 0 ∈ span_s<VAR>hd₁ : r₁ * r₁ * ⟪p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p), p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)⟫_ℝ = r₂ * r₂ * ⟪p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p), p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)⟫_ℝ<VAR>hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius<GOAL>p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) p₂
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoidWithOne A<VAR>inst✝² : Module R A<VAR>inst✝¹ : AddCommMonoidWithOne B<VAR>inst✝ : Module R B<VAR>n : ℕ<GOAL>↑n = 1 ⊗ₜ[R] ↑n
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>HasStrictFDerivAt (↑(toPartialHomeomorph f hf)) (↑f') (↑(toPartialHomeomorph f hf).symm (f a))
<VAR>s : ℝ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<GOAL>DifferentiableAt ℝ Gamma s
<VAR>s : ℝ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<GOAL>∀ (m : ℕ), ↑s ≠ -↑m
<VAR>s : ℝ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<GOAL>∀ (m : ℕ), ¬s = -↑m
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>inst✝¹ : MulAction G β<VAR>inst✝ : Nonempty α<GOAL>IsPretransitive G α ↔ Nonempty (Unique (orbitRel.Quotient G α))
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>inst✝¹ : MulAction G β<VAR>inst✝ : Nonempty α<GOAL>Subsingleton (orbitRel.Quotient G α) → Nonempty (orbitRel.Quotient G α)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : CommMonoid G<VAR>tG : IsTorsion G<VAR>x✝ : G<GOAL>x✝ ∈ torsion G ↔ x✝ ∈ ⊤
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F<VAR>m : (i : ι) → E i<GOAL>((liftEquiv 𝕜 E F).symm l) m = (l.compContinuousMultilinearMap (tprodL 𝕜)) m
<VAR>s : Finset ℕ<VAR>m n✝ p n d : ℕ<VAR>h : n.minSqFac = some d<GOAL>d * d ∣ n
<VAR>s : Finset ℕ<VAR>m n✝ p n d : ℕ<VAR>h : n.minSqFac = some d<VAR>this : n.MinSqFacProp n.minSqFac<GOAL>d * d ∣ n
<VAR>s : Finset ℕ<VAR>m n✝ p n d : ℕ<VAR>h : n.minSqFac = some d<VAR>this : n.MinSqFacProp (some d)<GOAL>d * d ∣ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t s : Set α<VAR>ht : MeasurableSet t<GOAL>μ (s ∪ t) + μ (s ∩ t) = μ s + μ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t s : Set α<VAR>ht : MeasurableSet t<GOAL>μ t + μ (s \ t) + μ (s ∩ t) = μ (s ∩ t) + μ (s \ t) + μ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : ℕ → ℝ≥0<GOAL>Summable f ↔ ¬Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop
<VAR>𝒮 : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} 𝒮<VAR>𝒳 : BasedCategory 𝒮<VAR>𝒴 : BasedCategory 𝒮<VAR>F : 𝒳 ⥤ᵇ 𝒴<VAR>R S : 𝒮<VAR>a b : 𝒳.obj<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝ : 𝒴.p.IsHomLift f (F.map φ)<GOAL>𝒳.p.IsHomLift f φ
<VAR>𝒮 : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} 𝒮<VAR>𝒳 : BasedCategory 𝒮<VAR>𝒴 : BasedCategory 𝒮<VAR>F : 𝒳 ⥤ᵇ 𝒴<VAR>R S : 𝒮<VAR>a b : 𝒳.obj<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝ : 𝒴.p.IsHomLift f (F.map φ)<GOAL>f = eqToHom ⋯ ≫ 𝒳.p.map φ ≫ eqToHom ⋯
<VAR>C : Type u<VAR>inst✝¹¹ : Category.{v, u} C<VAR>X Y : C<VAR>D : Type u₂<VAR>inst✝¹⁰ : Category.{w, u₂} D<VAR>E : Type u₃<VAR>inst✝⁹ : Category.{w', u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A✝ A' B B' : C<VAR>inst✝⁸ : HasBinaryProduct A✝ B<VAR>inst✝⁷ : HasBinaryProduct A' B'<VAR>inst✝⁶ : HasBinaryProduct (F.obj A✝) (F.obj B)<VAR>inst✝⁵ : HasBinaryProduct (F.obj A') (F.obj B')<VAR>inst✝⁴ : HasBinaryProduct (G.obj (F.obj A✝)) (G.obj (F.obj B))<VAR>inst✝³ : HasBinaryProduct ((F ⋙ G).obj A✝) ((F ⋙ G).obj B)<VAR>inst✝² : HasBinaryProducts C<VAR>inst✝¹ : HasBinaryProducts D<VAR>A : C<VAR>inst✝ : ∀ (B : C), IsIso (prodComparison F A B)<GOAL>prod.functor.obj A ⋙ F ≅ F ⋙ prod.functor.obj (F.obj A)
<VAR>C : Type u<VAR>inst✝¹¹ : Category.{v, u} C<VAR>X Y : C<VAR>D : Type u₂<VAR>inst✝¹⁰ : Category.{w, u₂} D<VAR>E : Type u₃<VAR>inst✝⁹ : Category.{w', u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A✝ A' B B' : C<VAR>inst✝⁸ : HasBinaryProduct A✝ B<VAR>inst✝⁷ : HasBinaryProduct A' B'<VAR>inst✝⁶ : HasBinaryProduct (F.obj A✝) (F.obj B)<VAR>inst✝⁵ : HasBinaryProduct (F.obj A') (F.obj B')<VAR>inst✝⁴ : HasBinaryProduct (G.obj (F.obj A✝)) (G.obj (F.obj B))<VAR>inst✝³ : HasBinaryProduct ((F ⋙ G).obj A✝) ((F ⋙ G).obj B)<VAR>inst✝² : HasBinaryProducts C<VAR>inst✝¹ : HasBinaryProducts D<VAR>A : C<VAR>inst✝ : ∀ (B : C), IsIso (prodComparison F A B)<GOAL>IsIso { app := fun B => prodComparison F A B, naturality := ⋯ }
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>a : α<VAR>inst✝ : SuccOrder α<VAR>ha : ¬IsMax a<GOAL>¬IsSuccLimit (succ a)
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>a : α<VAR>inst✝ : SuccOrder α<VAR>ha : IsSuccLimit (succ a)<GOAL>IsMax a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0∞<VAR>hr : r < 1<GOAL>Tendsto (fun n => r ^ n) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0<VAR>hr' : ↑r < 1<VAR>hr : ↑r < 1<GOAL>Tendsto (fun n => ↑r ^ n) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0<VAR>hr' : ↑r < 1<VAR>hr : ↑r < 1<GOAL>Tendsto (fun n => ↑r ^ n) atTop (𝓝 ↑0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0<VAR>hr' hr : r < 1<GOAL>Tendsto (HPow.hPow r) atTop (𝓝 0)
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝³ : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝² : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝¹ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i : δ<VAR>inst✝ : Fintype δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<GOAL>∫⋯∫⁻_Finset.univ, f ∂μ = fun x => ∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝³ : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝² : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝¹ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i : δ<VAR>inst✝ : Fintype δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>e : { j // j ∈ Finset.univ } ≃ δ := subtypeUnivEquiv ⋯<GOAL>∫⋯∫⁻_Finset.univ, f ∂μ = fun x => ∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝³ : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝² : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝¹ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y : (i : δ) → π i<VAR>i : δ<VAR>inst✝ : Fintype δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>e : { j // j ∈ Finset.univ } ≃ δ := subtypeUnivEquiv ⋯<VAR>x : (i : δ) → π i<GOAL>(∫⋯∫⁻_Finset.univ, f ∂μ) x = ∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝³ : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝² : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝¹ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y : (i : δ) → π i<VAR>i : δ<VAR>inst✝ : Fintype δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>e : { j // j ∈ Finset.univ } ≃ δ := subtypeUnivEquiv ⋯<VAR>x : (i : δ) → π i<GOAL>(∫⁻ (y : (i : { x // x ∈ Finset.univ }) → π ↑i), f fun i => if hi : i ∈ Finset.univ then y ⟨i, hi⟩ else x i ∂Measure.pi fun i => μ ↑i) = ∫⁻ (a : (b : { j // j ∈ Finset.univ }) → π (e b)), f ((MeasurableEquiv.piCongrLeft π e) a) ∂Measure.pi fun i' => μ (e i')
<VAR>ι : Type u_1<VAR>I✝ J : Box ι<VAR>x y : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>I : Box ι<VAR>i : ι<GOAL>nndist I.lower I.upper / nndist (I.lower i) (I.upper i) * nndist (I.lower i) (I.upper i) ≤ I.distortion * nndist (I.lower i) (I.upper i)
<VAR>ι : Type u_1<VAR>I✝ J : Box ι<VAR>x y : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>I : Box ι<VAR>i : ι<GOAL>nndist I.lower I.upper / nndist (I.lower i) (I.upper i) ≤ I.distortion