ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>B : Type u_1<VAR>inst✝⁶ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝⁵ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝³ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝² : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>inst✝¹ : (x : B) → Zero (E₁ x)<VAR>inst✝ : (x : B) → Zero (E₂ x)<GOAL>ContinuousOn ((fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })) ∘ invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
<VAR>B : Type u_1<VAR>inst✝⁶ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝⁵ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝³ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝² : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>inst✝¹ : (x : B) → Zero (E₁ x)<VAR>inst✝ : (x : B) → Zero (E₂ x)<VAR>H₁ : Continuous fun p => ((p.1, p.2.1), p.1, p.2.2)<GOAL>ContinuousOn ((fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })) ∘ invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
<VAR>B : Type u_1<VAR>inst✝⁶ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝⁵ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝³ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝² : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>inst✝¹ : (x : B) → Zero (E₁ x)<VAR>inst✝ : (x : B) → Zero (E₂ x)<VAR>H₁ : Continuous fun p => ((p.1, p.2.1), p.1, p.2.2)<GOAL>MapsTo (fun p => ((p.1, p.2.1), p.1, p.2.2)) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ) ((e₁.baseSet ×ˢ univ) ×ˢ e₂.baseSet ×ˢ univ)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>x : Fin (n + 1) → G<GOAL>((((Linear.homCongr k (diagonalSucc k G n ≪≫ (Representation.ofMulAction k G G).repOfTprodIso 1) (Iso.refl A)).trans ((MonoidalClosed.linearHomEquivComm (of (Representation.ofMulAction k G G)) (of 1) A).trans ((ihom (of 1)).obj A).leftRegularHomEquiv)).trans (Finsupp.llift (CoeSort.coe A) k k (Fin n → G)).symm).symm f).hom (Finsupp.single x 1) = (A.ρ (x 0)) (f fun i => (x i.castSucc)⁻¹ * x i.succ)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>x : Fin (n + 1) → G<GOAL>(((diagonalSucc k G n).hom.hom ≫ ((Representation.ofMulAction k G G).repOfTprodIso 1).hom.hom) ≫ (TensorProduct.uncurry k (CoeSort.coe (of (Representation.ofMulAction k G G))) (CoeSort.coe (of 1)) (CoeSort.coe A)) (((ihom (of 1)).obj A).leftRegularHom ((Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f)).hom) (Finsupp.single x 1) = (A.ρ (x 0)) (f fun i => (x i.castSucc)⁻¹ * x i.succ)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>x : Fin (n + 1) → G<GOAL>(⇑((TensorProduct.uncurry k (CoeSort.coe (of (Representation.ofMulAction k G G))) (CoeSort.coe (of 1)) (CoeSort.coe A)) (((ihom (of 1)).obj A).leftRegularHom ((Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f)).hom) ∘ ⇑((diagonalSucc k G n).hom.hom ≫ ((Representation.ofMulAction k G G).repOfTprodIso 1).hom.hom)) (Finsupp.single x 1) = (A.ρ (x 0)) (f fun i => (x i.castSucc)⁻¹ * x i.succ)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>x : Fin (n + 1) → G<GOAL>((TensorProduct.uncurry k (CoeSort.coe (of (Representation.ofMulAction k G G))) (CoeSort.coe (of 1)) (CoeSort.coe A)) (((ihom (of 1)).obj A).leftRegularHom ((Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f)).hom) (((Representation.ofMulAction k G G).repOfTprodIso 1).hom.hom ((diagonalSucc k G n).hom.hom (Finsupp.single x 1))) = (A.ρ (x 0)) (f fun i => (x i.castSucc)⁻¹ * x i.succ)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>x : Fin (n + 1) → G<GOAL>((TensorProduct.uncurry k (CoeSort.coe (of (Representation.ofMulAction k G G))) (CoeSort.coe (of 1)) (CoeSort.coe A)) (((ihom (of 1)).obj A).leftRegularHom ((Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f)).hom) (Finsupp.single (x 0) 1 ⊗ₜ[k] Finsupp.single (fun i => (x i.castSucc)⁻¹ * x i.succ) 1) = (A.ρ (x 0)) (f fun i => (x i.castSucc)⁻¹ * x i.succ)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>x : Fin (n + 1) → G<GOAL>(1 • (((ihom (of 1)).obj A).ρ (x 0)) ((Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f)) (Finsupp.single (fun i => (x i.castSucc)⁻¹ * x i.succ) 1) = (A.ρ (x 0)) (f fun i => (x i.castSucc)⁻¹ * x i.succ)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>x : Fin (n + 1) → G<GOAL>0 • (((ihom (of 1)).obj A).ρ (x 0)) ((Finsupp.llift (CoeSort.coe A) k k (Fin n → G)) f) = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f : Filter α<VAR>inst✝ : f.NeBot<VAR>p : α → Prop<VAR>q : Prop<GOAL>(∃ᶠ (x : α) in f, p x → q) ↔ (∀ᶠ (x : α) in f, p x) → q
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>m₁ m₂ m₃ m' _mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>s t : Set Ω<GOAL>IndepSets {s} {t} μ ↔ μ (s ∩ t) = μ s * μ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t✝ : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>t : Finset ι<VAR>s : ι → Set X<VAR>hs : ∀ i ∈ t, MeasurableSet (s i)<VAR>h's : (↑t).Pairwise (Disjoint on s)<VAR>hf : ∀ i ∈ t, IntegrableOn f (s i) μ<GOAL>∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>s : ι → Set X<VAR>hs : ∀ i ∈ ∅, MeasurableSet (s i)<VAR>h's : (↑∅).Pairwise (Disjoint on s)<VAR>hf : ∀ i ∈ ∅, IntegrableOn f (s i) μ<GOAL>∫ (x : X) in ⋃ i ∈ ∅, s i, f x ∂μ = ∑ i ∈ ∅, ∫ (x : X) in s i, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t✝ : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>s : ι → Set X<VAR>a : ι<VAR>t : Finset ι<VAR>hat : a ∉ t<VAR>IH : (∀ i ∈ t, MeasurableSet (s i)) → (↑t).Pairwise (Disjoint on s) → (∀ i ∈ t, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ<VAR>hs : ∀ i ∈ insert a t, MeasurableSet (s i)<VAR>h's : (↑(insert a t)).Pairwise (Disjoint on s)<VAR>hf : ∀ i ∈ insert a t, IntegrableOn f (s i) μ<GOAL>∫ (x : X) in ⋃ i ∈ insert a t, s i, f x ∂μ = ∑ i ∈ insert a t, ∫ (x : X) in s i, f x ∂μ
<VAR>x : ℂ<VAR>y : ℝ<GOAL>x ^ ↑y = ↑(abs x ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)
<VAR>y : ℝ<GOAL>0 ^ ↑y = ↑(abs 0 ^ y) * (↑(Real.cos (arg 0 * y)) + ↑(Real.sin (arg 0 * y)) * I)
<VAR>x : ℂ<VAR>y : ℝ<VAR>hx : x ≠ 0<GOAL>x ^ ↑y = ↑(abs x ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : TopologicalGroup G<VAR>f : α → G<VAR>hf : Multipliable f<VAR>e : Set G<VAR>he : e ∈ 𝓝 1<GOAL>e ∈ Filter.map f cofinite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : TopologicalGroup G<VAR>f : α → G<VAR>hf : Multipliable f<VAR>e : Set G<VAR>he : e ∈ 𝓝 1<GOAL>f ⁻¹' e ∈ cofinite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : TopologicalGroup G<VAR>f : α → G<VAR>hf : Multipliable f<VAR>e : Set G<VAR>he : e ∈ 𝓝 1<VAR>s : Finset α<VAR>hs : ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e<GOAL>f ⁻¹' e ∈ cofinite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : TopologicalGroup G<VAR>f : α → G<VAR>hf : Multipliable f<VAR>e : Set G<VAR>he : e ∈ 𝓝 1<VAR>s : Finset α<VAR>hs : ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e<VAR>x : α<VAR>hx : x ∉ s<GOAL>f x ∈ 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>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<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>n : ℕ<GOAL>ContMDiffAt I I' (↑n) f x ↔ ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' (↑n) f x'
<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>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<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>n : ℕ<GOAL>ContMDiffAt I I' (↑n) f x → ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' (↑n) f x'
<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>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<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>n : ℕ<GOAL>(∃ u ∈ 𝓝 x, ContMDiffOn I I' (↑n) f u) → ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' (↑n) f x'
<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>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<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>n : ℕ<VAR>u : Set M<VAR>hu : u ∈ 𝓝 x<VAR>h : ContMDiffOn I I' (↑n) f u<GOAL>∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' (↑n) f x'
<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>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<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>n : ℕ<VAR>u : Set M<VAR>hu : u ∈ 𝓝 x<VAR>h : ContMDiffOn I I' (↑n) f u<VAR>x' : M<VAR>hx' : u ∈ 𝓝 x'<GOAL>ContMDiffAt I I' (↑n) f x'
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<GOAL>Mono f ↔ Function.Injective ⇑f
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<GOAL>Mono f ↔ Mono ((forget TopCat).map f)
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁰ : NormedAddCommGroup D<VAR>inst✝⁹ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : Subsingleton F<GOAL>ContDiffOn 𝕜 n f s
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁰ : NormedAddCommGroup D<VAR>inst✝⁹ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : Subsingleton F<GOAL>ContDiffOn 𝕜 n (fun x => 0) s
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>S : Type u_3<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring S<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : AddCommMonoid M₅<VAR>inst✝⁶ : AddCommMonoid M₆<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M₄<VAR>inst✝¹ : Module R M₅<VAR>inst✝ : Module R M₆<VAR>f✝ f : M →ₗ[R] M₂<VAR>g : M₃ →ₗ[R] M₄<GOAL>Submodule.comap (f.prodMap g) ⊥ = (Submodule.comap f ⊥).prod (Submodule.comap g ⊥)
<VAR>F✝ : Type u_1<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>f₀ f₁ : C(X, Y)<VAR>S : Set X<VAR>F : f₀.HomotopyRel f₁ S<VAR>t : ↑I<VAR>x : X<VAR>hx : x ∈ S<GOAL>F (t, x) = f₁ x
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m n : E<GOAL>fract b m = fract b n ↔ -m + n ∈ span ℤ (Set.range ⇑b)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<GOAL>(map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<GOAL>(map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<GOAL>∀ (d : idx × ℕ →₀ ℕ), (fun x => ↑x) (coeff d (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n)).num = coeff d (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>c : idx × ℕ →₀ ℕ<GOAL>(fun x => ↑x) (coeff c (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n)).num = coeff c (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>c : idx × ℕ →₀ ℕ<GOAL>(fun x => ↑x) (coeff c ((bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) / ↑p ^ n).num = coeff c ((bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) / ↑p ^ n