ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>r : R<VAR>i j : ℕ<VAR>h : i ≤ j<VAR>f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i<GOAL>↑↑((f j) r).val - ↑↑((f i) r).val = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>r : R<VAR>i j : ℕ<VAR>h : i ≤ j<VAR>f_compat : (ZMod.castHom ⋯ (ZMod (p ^ i))).comp (f j) = f i<GOAL>↑↑((f j) r).val - ↑↑((ZMod.castHom ⋯ (ZMod (p ^ i))) ((f j) r)).val = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>((γ.leftShift a n' hn').leftUnshift n hn').v p q hpq = γ.v p q hpq
<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₄ p₅ p₆ : P<VAR>h₁₂₄₅ : affineSpan ℝ {p₁, p₂} ∥ affineSpan ℝ {p₄, p₅}<VAR>h₃₂₆₅ : affineSpan ℝ {p₃, p₂} ∥ affineSpan ℝ {p₆, p₅}<GOAL>2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H : Subgroup G<VAR>a b : G<GOAL>(setoid ↑H ↑⊥).Rel a b ↔ (QuotientGroup.rightRel H).Rel a b
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H : Subgroup G<VAR>a b : G<GOAL>(∃ a_1 ∈ H, ∃ b_1 ∈ ⊥, b = a_1 * a * b_1) ↔ b * a⁻¹ ∈ H
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<GOAL>vectorSpan k s = Submodule.span k ((fun x => x -ᵥ p) '' (s \ {p}))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<GOAL>Submodule.span k (insert (p -ᵥ p) ((fun x => x -ᵥ p) '' (s \ {p}))) = Submodule.span k ((fun x => x -ᵥ p) '' (s \ {p}))
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>P : Karoubi (SimplicialObject C)<GOAL>(((whiskeringLeft (SimplicialObject C) (Karoubi (SimplicialObject C)) (Karoubi (SimplicialObject C))).obj (toKaroubi (SimplicialObject C))).preimage (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans)).app P = (N₂ ⋙ Γ₂).map P.decompId_i ≫ (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app P.X ≫ P.decompId_p
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>S : Set ι<VAR>hS : #↑S < c<VAR>s t : (i : ι) → i ∈ S → Set α<VAR>h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi<GOAL>⋃ i, ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>S : Set ι<VAR>hS : #↑S < c<VAR>s t : (i : ι) → i ∈ S → Set α<VAR>h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi<GOAL>⋃ x, s ↑x ⋯ ≤ᶠ[l] ⋃ x, t ↑x ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>m n : ℕ<VAR>h : m < n<GOAL>(fun x => x ^ n) =o[𝓝 0] fun x => x ^ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>m p : ℕ<VAR>hp0 : 0 < p<VAR>h : m < m + p<GOAL>(fun x => x ^ (m + p)) =o[𝓝 0] fun x => x ^ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>m p : ℕ<VAR>hp0 : 0 < p<VAR>h : m < m + p<GOAL>(fun x => x ^ m * x ^ p) =o[𝓝 0] fun x => x ^ m * 1 ^ p
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>m : ℕ∞<VAR>f : M → E<VAR>hf : ContMDiff I 𝓘(ℝ, E) m f<VAR>hf' : ∀ (x : M), f x ∈ sphere 0 1<GOAL>ContMDiff I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) m (Set.codRestrict f (sphere 0 1) hf')
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>m : ℕ∞<VAR>f : M → E<VAR>hf : ContMDiff I 𝓘(ℝ, E) m f<VAR>hf' : ∀ (x : M), f x ∈ sphere 0 1<GOAL>Continuous (Set.codRestrict f (sphere 0 1) hf') ∧ ∀ (y : ↑(sphere 0 1)), ContMDiffOn I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) m (↑(extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) y) ∘ Set.codRestrict f (sphere 0 1) hf') (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) y).source)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>m : ℕ∞<VAR>f : M → E<VAR>hf : ContMDiff I 𝓘(ℝ, E) m f<VAR>hf' : ∀ (x : M), f x ∈ sphere 0 1<GOAL>∀ (y : ↑(sphere 0 1)), ContMDiffOn I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) m (↑(extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) y) ∘ Set.codRestrict f (sphere 0 1) hf') (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) y).source)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>m : ℕ∞<VAR>f : M → E<VAR>hf : ContMDiff I 𝓘(ℝ, E) m f<VAR>hf' : ∀ (x : M), f x ∈ sphere 0 1<VAR>v : ↑(sphere 0 1)<GOAL>ContMDiffOn I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) m (↑(extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v) ∘ Set.codRestrict f (sphere 0 1) hf') (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v).source)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>m : ℕ∞<VAR>f : M → E<VAR>hf : ContMDiff I 𝓘(ℝ, E) m f<VAR>hf' : ∀ (x : M), f x ∈ sphere 0 1<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<GOAL>ContMDiffOn I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) m (↑(extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v) ∘ Set.codRestrict f (sphere 0 1) hf') (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v).source)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>m : ℕ∞<VAR>f : M → E<VAR>hf : ContMDiff I 𝓘(ℝ, E) m f<VAR>hf' : ∀ (x : M), f x ∈ sphere 0 1<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>h : ContDiffOn ℝ ⊤ (⇑U) Set.univ<GOAL>ContMDiffOn I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) m (↑(extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v) ∘ Set.codRestrict f (sphere 0 1) hf') (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v).source)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>m : ℕ∞<VAR>f : M → E<VAR>hf : ContMDiff I 𝓘(ℝ, E) m f<VAR>hf' : ∀ (x : M), f x ∈ sphere 0 1<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>h : ContDiffOn ℝ ⊤ (⇑U) Set.univ<VAR>H₁ : ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) ⊤ (⇑U ∘ stereoToFun ↑(-v)) ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)<GOAL>ContMDiffOn I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) m (↑(extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v) ∘ Set.codRestrict f (sphere 0 1) hf') (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v).source)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>m : ℕ∞<VAR>f : M → E<VAR>hf : ContMDiff I 𝓘(ℝ, E) m f<VAR>hf' : ∀ (x : M), f x ∈ sphere 0 1<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>h : ContDiffOn ℝ ⊤ (⇑U) Set.univ<VAR>H₁ : ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) ⊤ (⇑U ∘ stereoToFun ↑(-v)) ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)<VAR>H₂ : ContMDiffOn I 𝓘(ℝ, E) m f Set.univ<GOAL>ContMDiffOn I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) m (↑(extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v) ∘ Set.codRestrict f (sphere 0 1) hf') (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v).source)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>m : ℕ∞<VAR>f : M → E<VAR>hf : ContMDiff I 𝓘(ℝ, E) m f<VAR>hf' : ∀ (x : M), f x ∈ sphere 0 1<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>h : ContDiffOn ℝ ⊤ (⇑U) Set.univ<VAR>H₁ : ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) ⊤ (⇑U ∘ stereoToFun ↑(-v)) ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)<VAR>H₂ : ContMDiffOn I 𝓘(ℝ, E) m f Set.univ<GOAL>Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v).source = Set.univ ∩ f ⁻¹' ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>m : ℕ∞<VAR>f : M → E<VAR>hf : ContMDiff I 𝓘(ℝ, E) m f<VAR>hf' : ∀ (x : M), f x ∈ sphere 0 1<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>h : ContDiffOn ℝ ⊤ (⇑U) Set.univ<VAR>H₁ : ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) ⊤ (⇑U ∘ stereoToFun ↑(-v)) ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)<VAR>H₂ : ContMDiffOn I 𝓘(ℝ, E) m f Set.univ<VAR>x : M<GOAL>x ∈ Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v).source ↔ x ∈ Set.univ ∩ f ⁻¹' ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>m : ℕ∞<VAR>f : M → E<VAR>hf : ContMDiff I 𝓘(ℝ, E) m f<VAR>hf' : ∀ (x : M), f x ∈ sphere 0 1<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>h : ContDiffOn ℝ ⊤ (⇑U) Set.univ<VAR>H₁ : ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) ⊤ (⇑U ∘ stereoToFun ↑(-v)) ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)<VAR>H₂ : ContMDiffOn I 𝓘(ℝ, E) m f Set.univ<VAR>x : M<VAR>hfxv : f x = -↑v ↔ ⟪f x, -↑v⟫_ℝ = 1<GOAL>x ∈ Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v).source ↔ x ∈ Set.univ ∩ f ⁻¹' ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>m : ℕ∞<VAR>f : M → E<VAR>hf : ContMDiff I 𝓘(ℝ, E) m f<VAR>hf' : ∀ (x : M), f x ∈ sphere 0 1<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>h : ContDiffOn ℝ ⊤ (⇑U) Set.univ<VAR>H₁ : ContMDiffOn 𝓘(ℝ, E) 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) ⊤ (⇑U ∘ stereoToFun ↑(-v)) ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)<VAR>H₂ : ContMDiffOn I 𝓘(ℝ, E) m f Set.univ<VAR>x : M<VAR>hfxv : f x = -↑v ↔ ⟪f x, -↑v⟫_ℝ = 1<GOAL>x ∈ Set.codRestrict f (sphere 0 1) hf' ⁻¹' (stereographic' n (-v)).source ∩ Set.univ ↔ x ∈ Set.univ ∩ ({a | ¬⟪-↑v, f a⟫_ℝ = 1} ∩ Set.univ)
<VAR>c d : ℝ≥0∞<VAR>r p q a b : ℝ≥0<GOAL>(↑a).toReal < (↑b).toReal ↔ ↑a < ↑b
<VAR>C : Type u_3<VAR>inst✝¹ : Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>inst✝ : Category.{u_2, u_4} D<VAR>F : C ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>F₁ F₂ : Quotient r ⥤ D<VAR>h : functor r ⋙ F₁ = functor r ⋙ F₂<GOAL>F₁ = F₂
<VAR>C : Type u_3<VAR>inst✝¹ : Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>inst✝ : Category.{u_2, u_4} D<VAR>F : C ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>F₁ F₂ : Quotient r ⥤ D<VAR>h : functor r ⋙ F₁ = functor r ⋙ F₂<GOAL>F₁ = lift r (functor r ⋙ F₂) ?m.14535
<VAR>C : Type u_3<VAR>inst✝¹ : Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>inst✝ : Category.{u_2, u_4} D<VAR>F : C ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>F₁ F₂ : Quotient r ⥤ D<VAR>h : functor r ⋙ F₁ = functor r ⋙ F₂<GOAL>∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ F₂).map f₁ = (functor r ⋙ F₂).map f₂
<VAR>C : Type u_3<VAR>inst✝¹ : Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>inst✝ : Category.{u_2, u_4} D<VAR>F : C ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>F₁ F₂ : Quotient r ⥤ D<VAR>h : functor r ⋙ F₁ = functor r ⋙ F₂<GOAL>F₁ = lift r (functor r ⋙ F₂) ⋯
<VAR>C : Type u_3<VAR>inst✝¹ : Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>inst✝ : Category.{u_2, u_4} D<VAR>F : C ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>F₁ F₂ : Quotient r ⥤ D<VAR>h : functor r ⋙ F₁ = functor r ⋙ F₂<GOAL>functor r ⋙ F₁ = functor r ⋙ F₂
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<GOAL>a < ⊤ → ∀ (n : ℕ), a ^ n < ⊤
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>m / n = (m - m % n) / n
<VAR>a b c d m k : ℕ<VAR>p q : ℕ → Prop<GOAL>m / 0 = (m - m % 0) / 0
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hn : n > 0<GOAL>m / n = (m - m % n) / n
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>inst✝ : CommSemiring S₂<VAR>f : R →+* S₁<VAR>g : σ → S₂<VAR>φ : S₁ →+* S₂<VAR>p : MvPolynomial σ R<GOAL>eval₂ φ g ((map f) p) = eval₂ (φ.comp f) g p
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>(coclosedLindelof X).HasBasis (fun s => IsClosed s ∧ IsLindelof s) compl
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>(⨅ s, ⨅ (_ : IsClosed s ∧ IsLindelof s), 𝓟 sᶜ).HasBasis (fun s => IsClosed s ∧ IsLindelof s) compl
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>∀ (i : Set X), IsClosed i ∧ IsLindelof i → ∀ (j : Set X), IsClosed j ∧ IsLindelof j → ∃ k, (IsClosed k ∧ IsLindelof k) ∧ kᶜ ⊆ iᶜ ∧ kᶜ ⊆ jᶜ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t✝ s : Set X<VAR>hs₁ : IsClosed s<VAR>hs₂ : IsLindelof s<VAR>t : Set X<VAR>ht₁ : IsClosed t<VAR>ht₂ : IsLindelof t<GOAL>∃ k, (IsClosed k ∧ IsLindelof k) ∧ kᶜ ⊆ sᶜ ∧ kᶜ ⊆ tᶜ
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>inst✝¹ : Functor m<VAR>inst✝ : LawfulFunctor m<VAR>x✝ : m α<VAR>h✝ : SatisfiesM p x✝<VAR>H : ∀ {a : α}, p a → q a<VAR>x : m { a // p a }<VAR>h : Subtype.val <$> x = x✝<GOAL>Subtype.val <$> (fun x => match x with | ⟨a, h⟩ => ⟨a, ⋯⟩) <$> x = x✝
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>p q : α → Prop<VAR>inst✝¹ : Functor m<VAR>inst✝ : LawfulFunctor m<VAR>x✝ : m α<VAR>h✝ : SatisfiesM p x✝<VAR>H : ∀ {a : α}, p a → q a<VAR>x : m { a // p a }<VAR>h : Subtype.val <$> x = x✝<GOAL>(Subtype.val ∘ fun x => match x with | ⟨a, h⟩ => ⟨a, ⋯⟩) <$> x = Subtype.val <$> x
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : AddMonoid R<VAR>S1 S2 : R<VAR>p1 : isSumSq S1<VAR>p2 : isSumSq S2<GOAL>isSumSq (S1 + S2)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup β<VAR>s✝ t✝ : Set α<VAR>a b : α<VAR>s : Set α<VAR>t : Set β<VAR>u : Finset α<VAR>hu : u.Nonempty<VAR>hus : ↑u ⊆ s<VAR>v : Finset β<VAR>hv : v.Nonempty<VAR>hvt : ↑v ⊆ t<GOAL>(u.sup' hu id, v.sup' hv id) ∈ supClosure (s ×ˢ t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup β<VAR>s✝ t✝ : Set α<VAR>a b : α<VAR>s : Set α<VAR>t : Set β<VAR>u : Finset α<VAR>hu : u.Nonempty<VAR>hus : ↑u ⊆ s<VAR>v : Finset β<VAR>hv : v.Nonempty<VAR>hvt : ↑v ⊆ t<GOAL>↑(u ×ˢ v) ⊆ s ×ˢ t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup β<VAR>s✝ t✝ : Set α<VAR>a b : α<VAR>s : Set α<VAR>t : Set β<VAR>u : Finset α<VAR>hu : u.Nonempty<VAR>hus : ↑u ⊆ s<VAR>v : Finset β<VAR>hv : v.Nonempty<VAR>hvt : ↑v ⊆ t<GOAL>(u ×ˢ v).sup' ⋯ id = (u.sup' hu id, v.sup' hv id)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ∆ (b \ a) = a ⊔ b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a \ (b \ a) ⊔ b \ a = a ⊔ b
<VAR>m n : ℕ+<GOAL>(↑m).gcd ↑n = 1 ↔ m.gcd n = 1
<VAR>m n : ℕ+<GOAL>(↑m).gcd ↑n = 1 ↔ ↑(m.gcd n) = ↑1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g : α → ℝ≥0∞<GOAL>∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g : α → ℝ≥0∞<GOAL>∫⁻ (a : α), (f * g) a ∂μ ≤ ∫⁻ (a : α), g a ∂μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g : α → ℝ≥0∞<GOAL>⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>f_meas : Measurable f<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g i : α → ℝ≥0∞<VAR>i_meas : Measurable i<VAR>hi : i ≤ f * g<GOAL>∫⁻ (a : α), i a ∂μ ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f