ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝³ : Category.{?u.49535, u_1} E<VAR>F : D ⥤ E<VAR>G✝ : E ⥤ D<VAR>inst✝² : HasWeakSheafify J D<VAR>inst✝¹ : ConcreteCategory D<VAR>inst✝ : J.HasSheafCompose (forget D)<VAR>G : Type (max v₁ u₁) ⥤ D<VAR>adj : G ⊣ forget D<VAR>X : Sheaf J D<GOAL>((whiskeringRight Cᵒᵖ (Type (max u₁ v₁)) D).obj G).map ((sheafToPresheaf J (Type (max u₁ v₁))).map ((sheafEquivSheafOfTypes J).symm.toAdjunction.counit.app ((sheafCompose J (forget D)).obj X))) ≫ ((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv (X.val ⋙ forget D) X.val).symm (𝟙 (X.val ⋙ forget D)) = (X.1.associator (forget D) G).hom ≫ (Adjunction.whiskerRight Cᵒᵖ adj).counit.app X.1
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<GOAL>S₁.rightHomologyIso.inv ≫ rightHomologyMap φ = homologyMap φ ≫ S₂.rightHomologyIso.inv
<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>(pathGraph n).chromaticNumber = 2
<VAR>n : ℕ<VAR>h : 2 ≤ n<VAR>hc : (pathGraph n).Colorable (Fintype.card Bool)<GOAL>(pathGraph n).chromaticNumber = 2
<VAR>n : ℕ<VAR>h : 2 ≤ n<VAR>hc : (pathGraph n).Colorable (Fintype.card Bool)<GOAL>(pathGraph n).chromaticNumber ≤ 2
<VAR>n : ℕ<VAR>h : 2 ≤ n<VAR>hc : (pathGraph n).Colorable (Fintype.card Bool)<GOAL>2 ≤ (pathGraph n).chromaticNumber
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>a : α<VAR>s✝ : Set β<VAR>a✝ : MeasurableSet s✝<GOAL>((κ.map id ⋯) a) s✝ = (κ a) s✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>a : α<VAR>s✝ : Set β<VAR>a✝ : MeasurableSet s✝<GOAL>(Measure.map id (κ a)) s✝ = (κ a) s✝
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<GOAL>#↑(Iio a) = 𝔠
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<GOAL>𝔠 ≤ #↑(Iio a)
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<VAR>h2 : (fun x => a + a - x) '' Iio a = Ioi a<GOAL>𝔠 ≤ #↑(Iio a)
<VAR>α : Type u_1<VAR>t t₁ t₂ : TopologicalSpace α<VAR>s✝ : Set α<VAR>h : ∀ (x : α), 𝓝 x ≤ 𝓝 x<VAR>s : Set α<GOAL>IsOpen s → IsOpen s
<VAR>α : Type u_1<VAR>t t₁ t₂ : TopologicalSpace α<VAR>s✝ : Set α<VAR>h : ∀ (x : α), 𝓝 x ≤ 𝓝 x<VAR>s : Set α<GOAL>(∀ x ∈ s, s ∈ 𝓝 x) → ∀ x ∈ s, s ∈ 𝓝 x
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁹ : Fintype n<VAR>inst✝⁸ : Finite m<VAR>inst✝⁷ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁶ : AddCommMonoid M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>G : Type u_7<VAR>inst✝² : Group G<VAR>inst✝¹ : DistribMulAction G M₁<VAR>inst✝ : SMulCommClass G R M₁<VAR>g : G<VAR>f : M₁ →ₗ[R] M₂<VAR>i✝ : m<VAR>j✝ : n<GOAL>(toMatrix (g • v₁) v₂) f i✝ j✝ = (toMatrix v₁ v₂) (f ∘ₗ DistribMulAction.toLinearMap R M₁ g) i✝ j✝
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁹ : Fintype n<VAR>inst✝⁸ : Finite m<VAR>inst✝⁷ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁶ : AddCommMonoid M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>G : Type u_7<VAR>inst✝² : Group G<VAR>inst✝¹ : DistribMulAction G M₁<VAR>inst✝ : SMulCommClass G R M₁<VAR>g : G<VAR>f : M₁ →ₗ[R] M₂<VAR>i✝ : m<VAR>j✝ : n<GOAL>(v₂.repr (f ((g • v₁) j✝))) i✝ = (v₂.repr ((f ∘ₗ DistribMulAction.toLinearMap R M₁ g) (v₁ j✝))) i✝
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Γ : Type u_4<VAR>inst✝³ : Group Γ<VAR>T : Type u_5<VAR>inst✝² : TopologicalSpace T<VAR>inst✝¹ : MulAction Γ T<VAR>inst✝ : ContinuousConstSMul Γ T<VAR>U : Set T<VAR>hU : IsOpen U<GOAL>IsOpen (Quotient.mk' '' U)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Γ : Type u_4<VAR>inst✝³ : Group Γ<VAR>T : Type u_5<VAR>inst✝² : TopologicalSpace T<VAR>inst✝¹ : MulAction Γ T<VAR>inst✝ : ContinuousConstSMul Γ T<VAR>U : Set T<VAR>hU : IsOpen U<GOAL>IsOpen (⋃ g, (fun x => g • x) '' U)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Bool<VAR>a : List α<VAR>l : List (List α)<GOAL>countP p (a :: l).join = Nat.sum (map (countP p) (a :: l))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>‖⟪x, y⟫_𝕜‖ = ‖⟪y, x⟫_𝕜‖
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i : ↑(atlas H M)<VAR>x : M<VAR>hx : x ∈ (fun i => (↑i).source) i<VAR>v : E<GOAL>(fderivWithin 𝕜 (↑((↑i).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) (↑((↑i).extend I) x)) v = v
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i : ↑(atlas H M)<VAR>x : M<VAR>hx : x ∈ (fun i => (↑i).source) i<VAR>v : E<GOAL>UniqueDiffWithinAt 𝕜 (range ↑I) (↑((↑i).extend I) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i : ↑(atlas H M)<VAR>x : M<VAR>hx : x ∈ (fun i => (↑i).source) i<VAR>v : E<GOAL>↑((↑i).extend I) ∘ ↑((↑i).extend I).symm =ᶠ[𝓝[range ↑I] ↑((↑i).extend I) x] fun x => x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i : ↑(atlas H M)<VAR>x : M<VAR>hx : x ∈ (fun i => (↑i).source) i<VAR>v : E<GOAL>(↑((↑i).extend I) ∘ ↑((↑i).extend I).symm) (↑((↑i).extend I) x) = ↑((↑i).extend I) x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j : ↑(atlas H M)<GOAL>ContinuousOn ((fun i j x => fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) (↑((↑i).extend I) x)) i j) ((fun i => (↑i).source) i ∩ (fun i => (↑i).source) j)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j : ↑(atlas H M)<GOAL>(fun i => (↑i).source) i ∩ (fun i => (↑i).source) j ⊆ ((↑i).extend I).source
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j : ↑(atlas H M)<GOAL>MapsTo (↑((↑i).extend I)) ((fun i => (↑i).source) i ∩ (fun i => (↑i).source) j) (((↑i).extend I).symm ≫ (↑j).extend I).source
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j k : ↑(atlas H M)<VAR>x : M<VAR>hxk : x ∈ (fun i => (↑i).source) k<VAR>hxi : x ∈ (fun i => (↑i).source) i<VAR>hxj : x ∈ (fun i => (↑i).source) j<VAR>v : E<GOAL>((fun i j x => fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) (↑((↑i).extend I) x)) j k x) (((fun i j x => fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) (↑((↑i).extend I) x)) i j x) v) = ((fun i j x => fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) (↑((↑i).extend I) x)) i k x) v
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j k : ↑(atlas H M)<VAR>x : M<VAR>hxk : x ∈ (fun i => (↑i).source) k<VAR>hxi : x ∈ (fun i => (↑i).source) i<VAR>hxj : x ∈ (fun i => (↑i).source) j<VAR>v : E<GOAL>(↑((↑k).extend I) ∘ ↑((↑j).extend I).symm) ∘ ↑((↑j).extend I) ∘ ↑((↑i).extend I).symm =ᶠ[𝓝[range ↑I] ↑((↑i).extend I) x] ↑((↑k).extend I) ∘ ↑((↑i).extend I).symm
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j k : ↑(atlas H M)<VAR>x : M<VAR>hxk : x ∈ (fun i => (↑i).source) k<VAR>hxi : x ∈ (fun i => (↑i).source) i<VAR>hxj : x ∈ (fun i => (↑i).source) j<VAR>v : E<GOAL>((↑((↑k).extend I) ∘ ↑((↑j).extend I).symm) ∘ ↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (↑((↑i).extend I) x) = (↑((↑k).extend I) ∘ ↑((↑i).extend I).symm) (↑((↑i).extend I) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j k : ↑(atlas H M)<VAR>x : M<VAR>hxk : x ∈ (fun i => (↑i).source) k<VAR>hxi : x ∈ (fun i => (↑i).source) i<VAR>hxj : x ∈ (fun i => (↑i).source) j<VAR>v : E<GOAL>DifferentiableWithinAt 𝕜 (↑((↑k).extend I) ∘ ↑((↑j).extend I).symm) (range ↑I) (↑((↑j).extend I) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j k : ↑(atlas H M)<VAR>x : M<VAR>hxk : x ∈ (fun i => (↑i).source) k<VAR>hxi : x ∈ (fun i => (↑i).source) i<VAR>hxj : x ∈ (fun i => (↑i).source) j<VAR>v : E<GOAL>DifferentiableWithinAt 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) (↑((↑i).extend I) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j k : ↑(atlas H M)<VAR>x : M<VAR>hxk : x ∈ (fun i => (↑i).source) k<VAR>hxi : x ∈ (fun i => (↑i).source) i<VAR>hxj : x ∈ (fun i => (↑i).source) j<VAR>v : E<GOAL>MapsTo (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) (range ↑I)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j k : ↑(atlas H M)<VAR>x : M<VAR>hxk : x ∈ (fun i => (↑i).source) k<VAR>hxi : x ∈ (fun i => (↑i).source) i<VAR>hxj : x ∈ (fun i => (↑i).source) j<VAR>v : E<GOAL>UniqueDiffWithinAt 𝕜 (range ↑I) (↑((↑i).extend I) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j k : ↑(atlas H M)<VAR>x : M<VAR>hxk : x ∈ (fun i => (↑i).source) k<VAR>hxi : x ∈ (fun i => (↑i).source) i<VAR>hxj : x ∈ (fun i => (↑i).source) j<VAR>v : E<GOAL>(↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (↑((↑i).extend I) x) = ↑((↑j).extend I) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ : α →. β<VAR>f : α → β<VAR>s : Set β<VAR>x : α<GOAL>x ∈ (↑f).core s ↔ x ∈ f ⁻¹' s
<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₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<GOAL>affineSpan ℝ {t₁.points i₁, t₁.points i₂} = altitude t₂ j₂
<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₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<GOAL>t₁.points i₁ ≠ t₂.points j₂ ∧ t₁.points i₁ ∈ affineSpan ℝ (Set.range t₂.points) ∧ t₁.points i₁ -ᵥ t₂.points j₂ ∈ (affineSpan ℝ (t₂.points '' ↑(univ.erase j₂))).directionᗮ
<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₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<GOAL>t₁.points i₁ ≠ t₁.points i₂ ∧ t₁.points i₁ ∈ affineSpan ℝ (Set.range t₂.points) ∧ t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ (t₂.points '' ↑(univ.erase j₂))).directionᗮ
<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₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<GOAL>t₁.points i₁ ∈ affineSpan ℝ (Set.range t₂.points) ∧ t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ (t₂.points '' ↑(univ.erase j₂))).directionᗮ
<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₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<VAR>he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)<GOAL>t₁.points i₁ ∈ affineSpan ℝ (Set.range t₁.points) ∧ t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ (t₂.points '' ↑(univ.erase j₂))).directionᗮ
<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₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<VAR>he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)<GOAL>t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ (t₂.points '' ↑(univ.erase j₂))).directionᗮ
<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₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<VAR>he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)<VAR>hu : univ.erase j₂ = {j₁, j₃}<GOAL>t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ (t₂.points '' ↑(univ.erase j₂))).directionᗮ
<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₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<VAR>he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)<VAR>hu : univ.erase j₂ = {j₁, j₃}<GOAL>t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ {t₁.orthocenter, t₁.points i₃}).directionᗮ