ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D✝ : GlueData C<VAR>D : GlueData (Type v)<VAR>x : D.glued<GOAL>∃ i y, Multicoequalizer.π D.diagram i y = x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D✝ : GlueData C<VAR>D : GlueData (Type v)<VAR>x : D.glued<GOAL>∃ i y, (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram) y = x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D✝ : GlueData C<VAR>D : GlueData (Type v)<VAR>x' : D.sigmaOpens<GOAL>∃ i y, (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram) y = D.π x'
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D✝ : GlueData C<VAR>D : GlueData (Type v)<VAR>x' : D.sigmaOpens<GOAL>∃ i y, (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram) y = D.π ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).hom x'))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D✝ : GlueData C<VAR>D : GlueData (Type v)<VAR>x' : D.sigmaOpens<VAR>i : D.J<VAR>y : D.U i<GOAL>∃ i_1 y_1, (Sigma.ι D.diagram.right i_1 ≫ Multicoequalizer.sigmaπ D.diagram) y_1 = D.π ((colimit.isoColimitCocone (Types.coproductColimitCocone D.U)).inv ⟨i, y⟩)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ₁ χ₂ χ₃ : ↥H → R<VAR>hχ : χ₁ + χ₂ = χ₃<VAR>x : ↥(rootSpace H χ₁)<VAR>m : ↥(weightSpace M χ₂)<GOAL>↑((rootSpaceWeightSpaceProduct R L H M χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] m)) = ⁅↑x, ↑m⁆
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>hp : ↑p.den ≠ 0<VAR>hq : ↑q.num ≠ 0<GOAL>↑(p / q) = ↑p / ↑q
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>hp : ↑p.den ≠ 0<VAR>hq : ↑q.num ≠ 0<GOAL>↑(p.num * ↑q.den) / ↑(↑p.den * q.num) = ↑p.num * ↑q.den / (↑p.den * ↑q.num)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>hp : ↑p.den ≠ 0<VAR>hq : ↑q.num ≠ 0<GOAL>↑(↑p.den * q.num) ≠ 0
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>F✝ : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α✝<VAR>inst✝⁵ : PseudoEMetricSpace β✝<VAR>inst✝⁴ : FunLike F✝ α✝ β✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>inst✝³ : PseudoMetricSpace α<VAR>inst✝² : PseudoMetricSpace β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DilationClass F α β<VAR>f : F<VAR>x y : α<GOAL>dist (f x) (f y) = ↑(ratio f) * dist x y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<GOAL>s.tail.destruct = s.destruct >>= tail.aux
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<GOAL>(fun o => Option.rec nil Prod.snd o) <$> s.destruct >>= destruct = s.destruct >>= tail.aux
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<GOAL>(s.destruct >>= fun x => Pure.pure (Option.rec nil Prod.snd x) >>= destruct) = s.destruct >>= tail.aux
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<GOAL>(fun x => Pure.pure (Option.rec nil Prod.snd x) >>= destruct) = tail.aux
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x : α<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(∑ i ∈ Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π✝ : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝¹ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π✝ i)<VAR>f✝ : X → (i : ι) → π✝ i<VAR>n : ℕ<VAR>π : Fin (n + 1) → Type u_8<VAR>inst✝ : (i : Fin (n + 1)) → TopologicalSpace (π i)<VAR>i : Fin (n + 1)<VAR>f : Y → π i<VAR>l : Filter Y<VAR>x : π i<VAR>hf : Tendsto f l (𝓝 x)<VAR>g : Y → (j : Fin n) → π (i.succAbove j)<VAR>y : (j : Fin n) → π (i.succAbove j)<VAR>hg : Tendsto g l (𝓝 y)<VAR>j : Fin (n + 1)<GOAL>∀ (j : Fin n), Tendsto (fun i_1 => i.insertNth (f i_1) (g i_1) (i.succAbove j)) l (𝓝 (i.insertNth x y (i.succAbove j)))
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUV' : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<GOAL>|↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id)) - ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))| ≤ ε / 5
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUV' : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<GOAL>ε / 5 = 2 * (ε / 10)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>inst✝¹¹ : Category.{u_9, u_1} C₁<VAR>inst✝¹⁰ : Category.{u_8, u_2} C₂<VAR>inst✝⁹ : Category.{u_7, u_3} D<VAR>inst✝⁸ : Preadditive C₁<VAR>inst✝⁷ : Preadditive C₂<VAR>inst✝⁶ : Preadditive D<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K₁ L₁ : HomologicalComplex C₁ c₁<VAR>f₁ f₁' : K₁ ⟶ L₁<VAR>h₁ : Homotopy f₁ f₁'<VAR>K₂ L₂ : HomologicalComplex C₂ c₂<VAR>f₂ : K₂ ⟶ L₂<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>inst✝⁵ : F.Additive<VAR>inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>c : ComplexShape J<VAR>inst✝³ : DecidableEq J<VAR>inst✝² : TotalComplexShape c₁ c₂ c<VAR>inst✝¹ : K₁.HasMapBifunctor K₂ F c<VAR>inst✝ : L₁.HasMapBifunctor L₂ F c<VAR>i₁ i₁' : I₁<VAR>hi₁ : c₁.Rel i₁ i₁'<VAR>i₂ i₂' : I₂<VAR>hi₂ : c₂.Rel i₂ i₂'<VAR>j : J<VAR>hj : c₁.π c₂ c (i₁', i₂) = j<GOAL>c₁.ε₁ c₂ c (i₁, i₂) • (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c i₁ i₂ j = -(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>inst✝¹¹ : Category.{u_9, u_1} C₁<VAR>inst✝¹⁰ : Category.{u_8, u_2} C₂<VAR>inst✝⁹ : Category.{u_7, u_3} D<VAR>inst✝⁸ : Preadditive C₁<VAR>inst✝⁷ : Preadditive C₂<VAR>inst✝⁶ : Preadditive D<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K₁ L₁ : HomologicalComplex C₁ c₁<VAR>f₁ f₁' : K₁ ⟶ L₁<VAR>h₁ : Homotopy f₁ f₁'<VAR>K₂ L₂ : HomologicalComplex C₂ c₂<VAR>f₂ : K₂ ⟶ L₂<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>inst✝⁵ : F.Additive<VAR>inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>c : ComplexShape J<VAR>inst✝³ : DecidableEq J<VAR>inst✝² : TotalComplexShape c₁ c₂ c<VAR>inst✝¹ : K₁.HasMapBifunctor K₂ F c<VAR>inst✝ : L₁.HasMapBifunctor L₂ F c<VAR>i₁ i₁' : I₁<VAR>hi₁ : c₁.Rel i₁ i₁'<VAR>i₂ i₂' : I₂<VAR>hi₂ : c₂.Rel i₂ i₂'<VAR>j : J<VAR>hj : c₁.π c₂ c (i₁', i₂) = j<VAR>hj' : c₁.π c₂ c (i₁, i₂') = j<GOAL>c₁.ε₁ c₂ c (i₁, i₂) • (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c i₁ i₂ j = -(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.158173, u_1} C<VAR>inst✝¹ : Category.{?u.158177, u_2} D<VAR>inst✝ : Abelian C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hf₁ : S₁.f = 0<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<GOAL>φ.τ₂ ≫ S₂.g = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.158177, u_2} D<VAR>inst✝ : Abelian C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hf₁ : S₁.f = 0<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<GOAL>QuasiIso φ ↔ (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.158177, u_2} D<VAR>inst✝ : Abelian C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hf₁ : S₁.f = 0<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<VAR>w : φ.τ₂ ≫ S₂.g = 0<GOAL>QuasiIso φ ↔ (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.158177, u_2} D<VAR>inst✝ : Abelian C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hf₁ : S₁.f = 0<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<VAR>w : φ.τ₂ ≫ S₂.g = 0<GOAL>IsIso (S₂.liftCycles φ.τ₂ ⋯) ↔ (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S.leftInv<GOAL>↑x * ↑((S.leftInvEquiv hS) x) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : s.encard = t.encard<GOAL>s.Infinite ↔ t.Infinite
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<GOAL>(map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>h : p.natDegree = 0<GOAL>(map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>h : p.natDegree ≠ 0<GOAL>(map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>h : p.natDegree ≠ 0<VAR>h2 : p ≠ 0<GOAL>(map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>h : p.natDegree ≠ 0<VAR>h2 : p ≠ 0<VAR>h3 : p.degree ≠ ↑0<GOAL>(map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>h : p.natDegree ≠ 0<VAR>h2 : p ≠ 0<VAR>h3 : p.degree ≠ ↑0<GOAL>(f p.leadingCoeff ≠ 0 ∨ p = 0) ∨ (map f p).degree = ↑0 ∧ p.degree = ⊥ ∨ (map f p).degree = ⊥ ∧ p.degree = ↑0 ↔ f p.leadingCoeff ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X]<VAR>h : p.natDegree ≠ 0<VAR>h2 : p ≠ 0<VAR>h3 : p.degree ≠ ↑0<GOAL>map f p = 0 → p.degree = 0 → ¬f p.leadingCoeff = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>n : ℕ<GOAL>a + ↑(n + 1) ≤ b + ↑(n + 1) ↔ a ≤ b
<VAR>n : ℤ<GOAL>(n * n).negOnePow = n.negOnePow
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>p₁ p₂ p : P<VAR>h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)<VAR>h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)<VAR>h₁' : p ∈ affineSpan R {t.points i₁, p₁}<VAR>h₂' : p ∈ affineSpan R {t.points i₂, p₂}<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<GOAL>Sbtw R (t.points i₁) p p₁
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>p₁ p₂ p : P<VAR>h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)<VAR>h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)<VAR>h₁' : p ∈ affineSpan R {t.points i₁, p₁}<VAR>h₂' : p ∈ affineSpan R {t.points i₂, p₂}<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>hp : p ∈ affineSpan R (Set.range t.points)<GOAL>Sbtw R (t.points i₁) p p₁
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>p₁ p₂ p : P<VAR>h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)<VAR>h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)<VAR>h₁' : p ∈ affineSpan R {t.points i₁, p₁}<VAR>h₂' : p ∈ affineSpan R {t.points i₂, p₂}<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>hp : p ∈ affineSpan R (Set.range t.points)<VAR>h₁i : p₁ ∈ ⇑(lineMap (t.points i₂) (t.points i₃)) '' Set.Ioo 0 1<GOAL>Sbtw R (t.points i₁) p p₁
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>p₁ p₂ p : P<VAR>h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)<VAR>h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)<VAR>h₁' : p ∈ affineSpan R {t.points i₁, p₁}<VAR>h₂' : p ∈ affineSpan R {t.points i₂, p₂}<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>hp : p ∈ affineSpan R (Set.range t.points)<VAR>h₁i : p₁ ∈ ⇑(lineMap (t.points i₂) (t.points i₃)) '' Set.Ioo 0 1<VAR>h₂i : p₂ ∈ ⇑(lineMap (t.points i₁) (t.points i₃)) '' Set.Ioo 0 1<GOAL>Sbtw R (t.points i₁) p p₁
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>p₁ p₂ p : P<VAR>h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)<VAR>h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)<VAR>h₁' : p ∈ affineSpan R {t.points i₁, p₁}<VAR>h₂' : p ∈ affineSpan R {t.points i₂, p₂}<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>hp : p ∈ affineSpan R (Set.range t.points)<VAR>h₁i : ∃ x ∈ Set.Ioo 0 1, (lineMap (t.points i₂) (t.points i₃)) x = p₁<VAR>h₂i : ∃ x ∈ Set.Ioo 0 1, (lineMap (t.points i₁) (t.points i₃)) x = p₂<GOAL>Sbtw R (t.points i₁) p p₁
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>p : P<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>hp : p ∈ affineSpan R (Set.range t.points)<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>h₁' : p ∈ affineSpan R {t.points i₁, (lineMap (t.points i₂) (t.points i₃)) r₁}<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>h₂' : p ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<GOAL>Sbtw R (t.points i₁) p ((lineMap (t.points i₂) (t.points i₃)) r₁)
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>w : Fin (2 + 1) → R<VAR>hw : ∑ i : Fin (2 + 1), w i = 1<VAR>hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)<VAR>h₁' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₁, (lineMap (t.points i₂) (t.points i₃)) r₁}<VAR>h₂' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<GOAL>Sbtw R (t.points i₁) ((Finset.affineCombination R Finset.univ t.points) w) ((lineMap (t.points i₂) (t.points i₃)) r₁)
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>w : Fin (2 + 1) → R<VAR>hw : ∑ i : Fin (2 + 1), w i = 1<VAR>hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)<VAR>h₁' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₁, (lineMap (t.points i₂) (t.points i₃)) r₁}<VAR>h₂' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<VAR>h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)<GOAL>Sbtw R (t.points i₁) ((Finset.affineCombination R Finset.univ t.points) w) ((lineMap (t.points i₂) (t.points i₃)) r₁)
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>w : Fin (2 + 1) → R<VAR>hw : ∑ i : Fin (2 + 1), w i = 1<VAR>hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)<VAR>h₁' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₁, (lineMap (t.points i₂) (t.points i₃)) r₁}<VAR>h₂' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<VAR>h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)<VAR>h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)<GOAL>Sbtw R (t.points i₁) ((Finset.affineCombination R Finset.univ t.points) w) ((lineMap (t.points i₂) (t.points i₃)) r₁)
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>w : Fin (2 + 1) → R<VAR>hw : ∑ i : Fin (2 + 1), w i = 1<VAR>hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)<VAR>h₁' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {(Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationSingleWeights R i₁), (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)}<VAR>h₂' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<VAR>h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)<VAR>h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)<GOAL>Sbtw R ((Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationSingleWeights R i₁)) ((Finset.affineCombination R Finset.univ t.points) w) ((Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁))
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>w : Fin (2 + 1) → R<VAR>hw : ∑ i : Fin (2 + 1), w i = 1<VAR>hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)<VAR>h₁' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {(Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationSingleWeights R i₁), (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)}<VAR>h₂' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<VAR>h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)<VAR>h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)<GOAL>Sbtw R (Finset.affineCombinationSingleWeights R i₁ i₁) (w i₁) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁ i₁)