ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>f✝ g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace α<VAR>f : α →ᵇ β<VAR>M : ℝ<VAR>M0 : 0 < M<GOAL>‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>f✝ g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace α<VAR>f : α →ᵇ β<VAR>M : ℝ<VAR>M0 : 0 < M<GOAL>dist f 0 < M ↔ ∀ (x : α), dist (f x) 0 < M
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁶ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁵ : TopologicalSpace M<VAR>inst✝¹⁴ : ChartedSpace H M<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<GOAL>ContMDiffOn I I n (↑(OpenEmbedding.toPartialHomeomorph e h).symm) (range e)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁶ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁵ : TopologicalSpace M<VAR>inst✝¹⁴ : ChartedSpace H M<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>this : SmoothManifoldWithCorners I M<GOAL>ContMDiffOn I I n (↑(OpenEmbedding.toPartialHomeomorph e h).symm) (range e)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁶ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁵ : TopologicalSpace M<VAR>inst✝¹⁴ : ChartedSpace H M<VAR>inst✝¹³ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>inst✝⁷ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁴ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝³ : TopologicalSpace M''<VAR>inst✝² : ChartedSpace H'' M''<VAR>e✝ : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n✝ : ℕ∞<VAR>inst✝¹ : Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>inst✝ : Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>this : SmoothManifoldWithCorners I M<GOAL>ContinuousOn (↑(OpenEmbedding.toPartialHomeomorph e h).symm) (range e) ∧ ∀ (x : H) (y : M), ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ ↑(OpenEmbedding.toPartialHomeomorph e h).symm ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (range e ∩ ↑(OpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I y).source))
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁶ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : SmoothManifoldWithCorners I M<VAR>inst✝² : T2Space M<VAR>inst✝¹ : NormalSpace M<VAR>inst✝ : SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<GOAL>∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ (x : M) in 𝓝ˢ t, f x = 1) ∧ ∀ (x : M), f x ∈ Icc 0 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁶ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : SmoothManifoldWithCorners I M<VAR>inst✝² : T2Space M<VAR>inst✝¹ : NormalSpace M<VAR>inst✝ : SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>u : Set M<VAR>u_op : IsOpen u<VAR>hsu : s ⊆ u<VAR>hut : closure u ⊆ tᶜ<GOAL>∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ (x : M) in 𝓝ˢ t, f x = 1) ∧ ∀ (x : M), f x ∈ Icc 0 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁶ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : SmoothManifoldWithCorners I M<VAR>inst✝² : T2Space M<VAR>inst✝¹ : NormalSpace M<VAR>inst✝ : SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>u : Set M<VAR>u_op : IsOpen u<VAR>hsu : s ⊆ u<VAR>hut : closure u ⊆ tᶜ<VAR>v : Set M<VAR>v_op : IsOpen v<VAR>htv : t ⊆ v<VAR>hvu : closure v ⊆ (closure u)ᶜ<GOAL>∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ (x : M) in 𝓝ˢ t, f x = 1) ∧ ∀ (x : M), f x ∈ Icc 0 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁶ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : SmoothManifoldWithCorners I M<VAR>inst✝² : T2Space M<VAR>inst✝¹ : NormalSpace M<VAR>inst✝ : SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>u : Set M<VAR>u_op : IsOpen u<VAR>hsu : s ⊆ u<VAR>hut : closure u ⊆ tᶜ<VAR>v : Set M<VAR>v_op : IsOpen v<VAR>htv : t ⊆ v<VAR>hvu : closure v ⊆ (closure u)ᶜ<VAR>f : C^⊤⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯<VAR>hfu : EqOn (⇑f) 0 (closure u)<VAR>hfv : EqOn (⇑f) 1 (closure v)<VAR>hf : ∀ (x : M), f x ∈ Icc 0 1<GOAL>∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ (x : M) in 𝓝ˢ t, f x = 1) ∧ ∀ (x : M), f x ∈ Icc 0 1
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<GOAL>(fun t => inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ ^ 2
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>x✝ : R<GOAL>inverse (↑x + x✝) - ↑x⁻¹ + ↑x⁻¹ * x✝ * ↑x⁻¹ = inverse (↑x + x✝) - (∑ i ∈ range 2, (-↑x⁻¹ * x✝) ^ i) * ↑x⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>s : Set β<GOAL>IsClosed s ↔ ∀ (i : ι), IsClosed (Subtype.val ⁻¹' s)
<VAR>σ R : Type u<VAR>inst✝ : CommSemiring R<GOAL>max (max (lift.{u, u} #R) (lift.{u, u} #σ)) ℵ₀ ≤ max (max #R #σ) ℵ₀
<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>S T : Subalgebra R A<VAR>h : S.toSubsemiring = T.toSubsemiring<VAR>x : A<GOAL>x ∈ S ↔ x ∈ T
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝² : Semiring α<VAR>inst✝¹ : LinearOrder α<VAR>a b c d : α<VAR>inst✝ : MulPosStrictMono α<VAR>h : 0 < c<GOAL>0 ≤ b * c ↔ 0 ≤ b
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : Module R N<VAR>Q : QuadraticMap R M N<VAR>inst✝² : IsCancelAdd R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : CharZero R<VAR>B : BilinMap R M R<VAR>x y : M<VAR>h : LinearMap.IsSymm B<GOAL>B.toQuadraticMap.IsOrtho x y ↔ LinearMap.IsOrtho B x y
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : Module R N<VAR>Q : QuadraticMap R M N<VAR>inst✝² : IsCancelAdd R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : CharZero R<VAR>B : BilinMap R M R<VAR>x y : M<VAR>h : LinearMap.IsSymm B<VAR>this : AddCancelMonoid R := let __src := inst✝²; let __src_1 := inferInstanceAs (AddCommMonoid R); AddCancelMonoid.mk ⋯<GOAL>B.toQuadraticMap.IsOrtho x y ↔ LinearMap.IsOrtho B x y
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : Module R N<VAR>Q : QuadraticMap R M N<VAR>inst✝² : IsCancelAdd R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : CharZero R<VAR>B : BilinMap R M R<VAR>x y : M<VAR>h : LinearMap.IsSymm B<VAR>this : AddCancelMonoid R := let __src := inst✝²; let __src_1 := inferInstanceAs (AddCommMonoid R); AddCancelMonoid.mk ⋯<GOAL>(B x) x + (B y) y + ((B y) x + (B x) y) = (B x) x + (B y) y ↔ (B x) y = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>φ ψ : R⟦X⟧<GOAL>(φ * ψ).order = φ.order + ψ.order
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>S : F →ₗ.[𝕜] E<VAR>hT : Dense ↑T.domain<VAR>inst✝ : CompleteSpace E<VAR>y : ↥T.adjointDomain<VAR>x : ↥T.domain<GOAL>⟪(adjointAux hT) y, ↑x⟫_𝕜 = ⟪↑y, ↑T x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>S : F →ₗ.[𝕜] E<VAR>hT : Dense ↑T.domain<VAR>inst✝ : CompleteSpace E<VAR>y : ↥T.adjointDomain<VAR>x : ↥T.domain<GOAL>⟪{ toFun := fun y => (InnerProductSpace.toDual 𝕜 E).symm (adjointDomainMkCLMExtend hT y), map_add' := ⋯ } y, ↑x⟫_𝕜 = ⟪↑y, ↑T x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>S : F →ₗ.[𝕜] E<VAR>hT : Dense ↑T.domain<VAR>inst✝ : CompleteSpace E<VAR>y : ↥T.adjointDomain<VAR>x : ↥T.domain<GOAL>(adjointDomainMkCLMExtend hT y) ↑x = ⟪↑y, ↑T x⟫_𝕜
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹³ : Ring k<VAR>inst✝¹² : AddCommGroup V1<VAR>inst✝¹¹ : Module k V1<VAR>inst✝¹⁰ : AffineSpace V1 P1<VAR>inst✝⁹ : AddCommGroup V2<VAR>inst✝⁸ : Module k V2<VAR>inst✝⁷ : AffineSpace V2 P2<VAR>inst✝⁶ : AddCommGroup V3<VAR>inst✝⁵ : Module k V3<VAR>inst✝⁴ : AffineSpace V3 P3<VAR>inst✝³ : AddCommGroup V4<VAR>inst✝² : Module k V4<VAR>inst✝¹ : AffineSpace V4 P4<VAR>inst✝ : NoZeroSMulDivisors k V1<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>(lineMap p₀ p₁) c = p₁ ↔ p₀ = p₁ ∨ c = 1
<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>α : E<VAR>halg : ¬IsAlgebraic F α<GOAL>finSepDegree F ↥F⟮α⟯ ∣ finrank F ↥F⟮α⟯
<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>α : E<VAR>halg : ¬IsAlgebraic F α<VAR>this : finrank F ↥F⟮α⟯ = 0<GOAL>finSepDegree F ↥F⟮α⟯ ∣ finrank F ↥F⟮α⟯
<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>α : E<VAR>halg : ¬IsAlgebraic F α<VAR>this : finrank F ↥F⟮α⟯ = 0<GOAL>finSepDegree F ↥F⟮α⟯ ∣ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c x : α<GOAL>x ∈ Ioi a ∪ {a} ↔ x ∈ Ici a
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>W✝ X✝ Y✝ Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g✝ : W✝ ⟶ Y✝<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>W X X' Y Z Z' : C<VAR>f : W ⟶ X<VAR>f' : X ⟶ X'<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>h' : X' ⟶ Z'<VAR>i : Y ⟶ Z<VAR>i' : Z ⟶ Z'<VAR>hsq₁ : CommSq f g h i<VAR>hsq₂ : CommSq f' h h' i'<GOAL>(f ≫ f') ≫ h' = g ≫ i ≫ i'
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<VAR>hp₂p₁ : ¬p₂ = p₁<VAR>hp₃p₁ : ¬p₃ = p₁<GOAL>∡ p₂ p₁ p₃ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<VAR>hp₂p₁ : ¬p₂ = p₁<VAR>hp₃p₁ : ¬p₃ = p₁<GOAL>∠ p₂ p₁ p₃ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>this : Fintype α<GOAL>Nat.card (Option α) = Nat.card α + 1
<VAR>J : Type v'<VAR>inst✝⁹ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁷ : Category.{?u.207926, u_1} K<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_2} D<VAR>inst✝⁵ : HasColimitsOfShape J C<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝⁴ : Gr.Full<VAR>inst✝³ : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsVanKampenColimit c<VAR>inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝¹ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>inst✝ : (X : C) → (i : J) → (f : X ⟶ c.pt) → PreservesLimit (cospan f (c.ι.app i)) Gl<VAR>this✝ : PreservesLimitsOfSize.{?u.211386, ?u.211385, u_3, v, u_2, u} Gr<VAR>this : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<GOAL>Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁹ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁷ : Category.{?u.207926, u_1} K<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_2} D<VAR>inst✝⁵ : HasColimitsOfShape J C<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝⁴ : Gr.Full<VAR>inst✝³ : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsVanKampenColimit c<VAR>inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝¹ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>inst✝ : (X : C) → (i : J) → (f : X ⟶ c.pt) → PreservesLimit (cospan f (c.ι.app i)) Gl<VAR>this✝ : PreservesLimitsOfSize.{?u.211386, ?u.211385, u_3, v, u_2, u} Gr<VAR>this : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<GOAL>Nonempty (IsColimit c') → ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁹ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁷ : Category.{?u.207926, u_1} K<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_2} D<VAR>inst✝⁵ : HasColimitsOfShape J C<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝⁴ : Gr.Full<VAR>inst✝³ : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsVanKampenColimit c<VAR>inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝¹ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>inst✝ : (X : C) → (i : J) → (f : X ⟶ c.pt) → PreservesLimit (cospan f (c.ι.app i)) Gl<VAR>this✝ : PreservesLimitsOfSize.{?u.211386, ?u.211385, u_3, v, u_2, u} Gr<VAR>this : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : IsColimit c'<VAR>j : J<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<GOAL>IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁹ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁷ : Category.{?u.207926, u_1} K<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_2} D<VAR>inst✝⁵ : HasColimitsOfShape J C<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝⁴ : Gr.Full<VAR>inst✝³ : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsVanKampenColimit c<VAR>inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝¹ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>inst✝ : (X : C) → (i : J) → (f : X ⟶ c.pt) → PreservesLimit (cospan f (c.ι.app i)) Gl<VAR>this✝ : PreservesLimitsOfSize.{?u.211386, ?u.211385, u_3, v, u_2, u} Gr<VAR>this : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : IsColimit c'<VAR>j : J<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<GOAL>IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁹ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁷ : Category.{?u.207926, u_1} K<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_2} D<VAR>inst✝⁵ : HasColimitsOfShape J C<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝⁴ : Gr.Full<VAR>inst✝³ : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsVanKampenColimit c<VAR>inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝¹ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>inst✝ : (X : C) → (i : J) → (f : X ⟶ c.pt) → PreservesLimit (cospan f (c.ι.app i)) Gl<VAR>this✝ : PreservesLimitsOfSize.{?u.211386, ?u.211385, u_3, v, u_2, u} Gr<VAR>this : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : IsColimit c'<VAR>j : J<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<VAR>hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j<GOAL>IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁹ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁷ : Category.{?u.207926, u_1} K<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_2} D<VAR>inst✝⁵ : HasColimitsOfShape J C<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝⁴ : Gr.Full<VAR>inst✝³ : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsVanKampenColimit c<VAR>inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝¹ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>inst✝ : (X : C) → (i : J) → (f : X ⟶ c.pt) → PreservesLimit (cospan f (c.ι.app i)) Gl<VAR>this✝² : PreservesLimitsOfSize.{?u.211386, ?u.211385, u_3, v, u_2, u} Gr<VAR>this✝¹ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : IsColimit c'<VAR>j : J<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<VAR>hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j<VAR>β : F' ⋙ Gr ⋙ Gl ≅ F' := isoWhiskerLeft F' (asIso adj.counit) ≪≫ F'.rightUnitor<VAR>hl : IsColimit ((Cocones.precompose β.hom).obj c') := (IsColimit.precomposeHomEquiv β c').symm hc'<VAR>hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))<VAR>this✝ : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))<VAR>this : f = (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })<GOAL>IsPullback (c'.ι.app j) (β.inv.app j ≫ Gl.map (Gr.map (α'.app j))) ((hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })) ((Gl.mapCocone c).ι.app j)