ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯<VAR>f' : ℕ → α → β := fun n => AEStronglyMeasurable.mk (f n) ⋯<VAR>hui' : UnifIntegrable f' p μ<VAR>hut' : UnifTight f' p μ<VAR>g' : α → β := AEStronglyMeasurable.mk g ⋯<VAR>hg : StronglyMeasurable g'<VAR>hgg' : g =ᶠ[ae μ] g'<VAR>hg'' : Memℒp g' p μ<VAR>haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))<VAR>haefg : ∀ (n : ℕ), f n - g =ᶠ[ae μ] f' n - g'<VAR>hsnfg : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (f' n - g') p μ<GOAL>Tendsto (fun n => eLpNorm (f' n - g') p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>inst✝ : Encodable α<VAR>a : α<GOAL>(down a).up = a
<VAR>M : Type u_1<VAR>S T : Set M<VAR>a : M<VAR>b : ?m.797<VAR>inst✝¹ : Mul M<VAR>inst✝ : HasDistribNeg M<VAR>ha : a ∈ S.centralizer<VAR>c : M<VAR>hc : c ∈ S<GOAL>c * -a = -a * c
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : DifferentiableOn ℝ f s<VAR>hs : μ s = 0<GOAL>μ (f '' s) = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : DifferentiableOn ℝ f s<VAR>hs : μ s = 0<GOAL>μ (f '' s) ≤ 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : DifferentiableOn ℝ f s<VAR>hs : μ s = 0<VAR>this : ∀ (A : E →L[ℝ] E), ∃ δ, 0 < δ ∧ ∀ (t : Set E), ApproximatesLinearOn f A t δ → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t<GOAL>μ (f '' s) ≤ 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : DifferentiableOn ℝ f s<VAR>hs : μ s = 0<VAR>δ : (E →L[ℝ] E) → ℝ≥0<VAR>hδ : ∀ (A : E →L[ℝ] E), 0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t<GOAL>μ (f '' s) ≤ 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : DifferentiableOn ℝ f s<VAR>hs : μ s = 0<VAR>δ : (E →L[ℝ] E) → ℝ≥0<VAR>hδ : ∀ (A : E →L[ℝ] E), 0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>left✝¹ : Pairwise (Disjoint on t)<VAR>left✝ : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))<GOAL>μ (f '' s) ≤ 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<GOAL>(mk' N).range = ⊤
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>φ✝ ψ : L.Formula α<VAR>v✝ : α → M<VAR>φ : L.Formula (Fin n)<VAR>v : Empty → M<VAR>x : Fin n → M<GOAL>(BoundedFormula.relabel Sum.inr φ).Realize v x ↔ φ.Realize x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedCommGroup α<VAR>m✝ n✝ : ℤ<VAR>a b : α<VAR>ha : 1 < a<VAR>m n : ℤ<VAR>h : m < n<GOAL>a ^ m * a ^ (n - m) = a ^ n
<VAR>α : Type u<VAR>u : Level<VAR>n : ℤ<VAR>d : ℕ<VAR>inst✝ : DivisionRing α<VAR>inv : Invertible ↑d<GOAL>↑n * ⅟↑d = Rat.rawCast n d
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>inst✝ : Invertible 2<GOAL>C ⅟2 * 2 = 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → Preorder (α i)<VAR>x y✝ y : (i : ι) → α i<GOAL>(y ∈ univ.pi fun i => Ici (x i)) ↔ y ∈ Ici x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.77613, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<GOAL>(↑(fst φ)).comp (inl φ) ⋯ + (snd φ).comp (Cochain.ofHom (inr φ)) ⋯ = Cochain.ofHom (𝟙 (mappingCone φ))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MulAction G α<VAR>inst✝⁴ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝³ : Countable G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : SMulInvariantMeasure G α ν<VAR>inst✝ : MeasurableSMul G α<VAR>s : Set α<VAR>fund_dom_s : IsFundamentalDomain G s ν<VAR>vol_s : ν s = 0<GOAL>QuotientMeasureEqMeasurePreimage ν 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MulAction G α<VAR>inst✝⁴ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝³ : Countable G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : SMulInvariantMeasure G α ν<VAR>inst✝ : MeasurableSMul G α<VAR>s : Set α<VAR>fund_dom_s : IsFundamentalDomain G s ν<VAR>vol_s : ν s = 0<GOAL>0 = Measure.map (Quotient.mk α_mod_G) (ν.restrict s)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MulAction G α<VAR>inst✝⁴ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝³ : Countable G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : SMulInvariantMeasure G α ν<VAR>inst✝ : MeasurableSMul G α<VAR>s : Set α<VAR>fund_dom_s : IsFundamentalDomain G s ν<VAR>vol_s : ν s = 0<VAR>U : Set (Quotient α_mod_G)<VAR>meas_U : MeasurableSet U<GOAL>0 U = (Measure.map (Quotient.mk α_mod_G) (ν.restrict s)) U
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MulAction G α<VAR>inst✝⁴ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝³ : Countable G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : SMulInvariantMeasure G α ν<VAR>inst✝ : MeasurableSMul G α<VAR>s : Set α<VAR>fund_dom_s : IsFundamentalDomain G s ν<VAR>vol_s : ν s = 0<VAR>U : Set (Quotient α_mod_G)<VAR>meas_U : MeasurableSet U<GOAL>0 = (Measure.map (Quotient.mk α_mod_G) (ν.restrict s)) U
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MulAction G α<VAR>inst✝⁴ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝³ : Countable G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : SMulInvariantMeasure G α ν<VAR>inst✝ : MeasurableSMul G α<VAR>s : Set α<VAR>fund_dom_s : IsFundamentalDomain G s ν<VAR>vol_s : ν s = 0<VAR>U : Set (Quotient α_mod_G)<VAR>meas_U : MeasurableSet U<GOAL>(Measure.map (Quotient.mk α_mod_G) (ν.restrict s)) U = ν (Quotient.mk α_mod_G ⁻¹' U ∩ s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter β<VAR>m : α → β<GOAL>(comap m f).NeBot ↔ ∀ t ∈ f, ∃ a, m a ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter β<VAR>m : α → β<GOAL>(∀ (s : Set α), ∀ x ∈ f, m ⁻¹' x ⊆ s → s.Nonempty) ↔ ∀ t ∈ f, ∃ a, m a ∈ t
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Fintype α<VAR>c : List ℕ<VAR>hc : c.sum ≤ Fintype.card α<VAR>klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn => ⟨n, hn⟩<VAR>klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl => pmap klift l hl<GOAL>∃ o, map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Fintype α<VAR>c : List ℕ<VAR>hc : c.sum ≤ Fintype.card α<VAR>klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn => ⟨n, hn⟩<VAR>klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl => pmap klift l hl<VAR>hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α<GOAL>∃ o, map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Fintype α<VAR>c : List ℕ<VAR>hc : c.sum ≤ Fintype.card α<VAR>klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn => ⟨n, hn⟩<VAR>klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl => pmap klift l hl<VAR>hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α<VAR>l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt<GOAL>∃ o, map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Fintype α<VAR>c : List ℕ<VAR>hc : c.sum ≤ Fintype.card α<VAR>klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn => ⟨n, hn⟩<VAR>klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl => pmap klift l hl<VAR>hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α<VAR>l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt<VAR>hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a<GOAL>∃ o, map length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise Disjoint o
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Fintype α<VAR>c : List ℕ<VAR>hc : c.sum ≤ Fintype.card α<VAR>klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn => ⟨n, hn⟩<VAR>klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl => pmap klift l hl<VAR>hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α<VAR>l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt<VAR>hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a<GOAL>map length (map (map ⇑(Fintype.equivFin α).symm) l) = c ∧ (∀ s ∈ map (map ⇑(Fintype.equivFin α).symm) l, s.Nodup) ∧ Pairwise Disjoint (map (map ⇑(Fintype.equivFin α).symm) l)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a b : α<GOAL>count a {b} = if a = b then 1 else 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a✝ : α<VAR>m n✝ : ℕ<VAR>a : α<VAR>n : ℕ<GOAL>a ∈ s ^ n ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a
<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>p : TangentBundle I H<GOAL>(chartAt (ModelProd H E) p).source = (TotalSpace.toProd H E).toPartialEquiv.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>p : TangentBundle I H<GOAL>({ toFun := fun p_1 => (p_1.proj, (tangentBundleCore I H).toFiberBundleCore.coordChange ((tangentBundleCore I H).toFiberBundleCore.indexAt p_1.proj) (achart H p.proj) p_1.proj p_1.snd), invFun := fun p_1 => { proj := p_1.1, snd := (tangentBundleCore I H).toFiberBundleCore.coordChange (achart H p.proj) ((tangentBundleCore I H).toFiberBundleCore.indexAt p_1.1) p_1.1 p_1.2 }, source := (tangentBundleCore I H).toFiberBundleCore.proj ⁻¹' (↑(achart H p.proj)).source, target := (↑(achart H p.proj)).source ×ˢ univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ } ≫ₕ (chartAt H p.proj).prod (PartialHomeomorph.refl E)).source = (TotalSpace.toProd H E).toPartialEquiv.source
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∣ p
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁸ : NormedField 𝕜₁<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜₁ E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>𝔖₁ 𝔖₂ : Set (Set E)<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalAddGroup F<VAR>h : 𝔖₂ ⊆ 𝔖₁<VAR>this : UniformSpace F := TopologicalAddGroup.toUniformSpace F<GOAL>instTopologicalSpace σ F 𝔖₁ ≤ instTopologicalSpace σ F 𝔖₂
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁸ : NormedField 𝕜₁<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜₁ E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>𝔖₁ 𝔖₂ : Set (Set E)<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalAddGroup F<VAR>h : 𝔖₂ ⊆ 𝔖₁<VAR>this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<GOAL>instTopologicalSpace σ F 𝔖₁ ≤ instTopologicalSpace σ F 𝔖₂
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁸ : NormedField 𝕜₁<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜₁ E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>𝔖₁ 𝔖₂ : Set (Set E)<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalAddGroup F<VAR>h : 𝔖₂ ⊆ 𝔖₁<VAR>this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<GOAL>UniformSpace.toTopologicalSpace ≤ UniformSpace.toTopologicalSpace
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun y => c y • f y) (c x • f' + c' • f x) x
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Fintype K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Algebra (ZMod p) K<GOAL>(X ^ q - X).roots = univ.val
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i : ι<VAR>inst✝¹ : K.HasHomology i<VAR>inst✝ : L.HasHomology i<VAR>hK : K.ExactAt i<GOAL>QuasiIsoAt f i ↔ L.ExactAt i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i : ι<VAR>inst✝¹ : K.HasHomology i<VAR>inst✝ : L.HasHomology i<VAR>hK : IsZero (K.sc i).homology<GOAL>IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) ↔ IsZero (L.sc i).homology
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x✝ x : Fin n → ℕ<GOAL>x ∈ sphere n d 0 → x ∈ 0
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasBinaryProducts C<VAR>f : X ⟶ Y<GOAL>(prod.rightUnitor X).inv ≫ prod.map f (𝟙 (⊤_ C)) = f ≫ (prod.rightUnitor Y).inv
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<GOAL>x ∈ RingHom.ker (truncate n) ↔ ∀ i < n, x.coeff i = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<GOAL>(∀ (i : Fin n), TruncatedWittVector.coeff i ({ toFun := truncateFun n, map_one' := ⋯, map_mul' := ⋯ } x) = 0) ↔ ∀ i < n, x.coeff i = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 1<VAR>a✝ : Nontrivial R<GOAL>P.toPoly.Monic
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N✝ : Subgroup G<VAR>nN✝ : N✝.Normal<VAR>H : Type v<VAR>inst✝¹ : Group H<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>x : G<GOAL>↑x = 1 ↔ x ∈ N
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N✝ : Subgroup G<VAR>nN✝ : N✝.Normal<VAR>H : Type v<VAR>inst✝¹ : Group H<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>x : G<GOAL>x⁻¹ * 1 ∈ N ↔ x ∈ N
<VAR>α : Sort u_1<VAR>a : α<VAR>h : ∃ a_1, (fun b => a_1 = b) = (mk a).fst := (mk a).snd<GOAL>Classical.choose h = a
<VAR>α : Sort u_1<VAR>a : α<VAR>h : ∃ a_1, (fun b => a_1 = b) = (mk a).fst := (mk a).snd<VAR>this : (fun b => Classical.choose h = b) = (mk a).fst<GOAL>Classical.choose h = a
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>t : TStructure C<VAR>H : ℕ → Prop := fun a => ∀ (n : ℤ), t.LE n ≤ t.LE (n + ↑a)<GOAL>Monotone t.LE
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>t : TStructure C<VAR>H : ℕ → Prop := fun a => ∀ (n : ℤ), t.LE n ≤ t.LE (n + ↑a)<GOAL>∀ (a : ℕ), H a
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>t : TStructure C<VAR>H : ℕ → Prop := fun a => ∀ (n : ℤ), t.LE n ≤ t.LE (n + ↑a)<VAR>H_zero : H 0<GOAL>∀ (a : ℕ), H a
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>t : TStructure C<VAR>H : ℕ → Prop := fun a => ∀ (n : ℤ), t.LE n ≤ t.LE (n + ↑a)<VAR>H_zero : H 0<VAR>H_one : H 1<GOAL>∀ (a : ℕ), H a
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>t : TStructure C<VAR>H : ℕ → Prop := fun a => ∀ (n : ℤ), t.LE n ≤ t.LE (n + ↑a)<VAR>H_zero : H 0<VAR>H_one : H 1<VAR>H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c<GOAL>∀ (a : ℕ), H a
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : DecidableEq μ<VAR>inst✝¹ : CanonicallyOrderedAddCommMonoid μ<VAR>inst✝ : HasAntidiagonal μ<VAR>s : Finset ι<VAR>f : ι →₀ μ<GOAL>f ∈ s.finsuppAntidiag 0 ↔ f ∈ {0}
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹³ : Ring R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M'<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R M'<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : StrongRankCondition R<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : (i : η) → AddCommGroup (φ i)<VAR>inst✝² : (i : η) → Module R (φ i)<VAR>inst✝¹ : ∀ (i : η), Module.Free R (φ i)<VAR>inst✝ : Fintype η<GOAL>Module.rank R (η → M) = ↑(Fintype.card η) * lift.{u₁', v} (Module.rank R M)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>G : D ⥤ C<VAR>F : C ⥤ D<VAR>adj : F ⊣ G<VAR>A : adj.toMonad.Algebra<VAR>B : D<VAR>inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<VAR>f : F.obj A.A ⟶ B<GOAL>F.map A.a ≫ f = adj.counit.app (F.obj A.A) ≫ f ↔ G.map (F.map ((adj.homEquiv A.A B) f)) ≫ G.map (adj.counit.app B) = A.a ≫ (adj.homEquiv A.A B) f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>G : D ⥤ C<VAR>F : C ⥤ D<VAR>adj : F ⊣ G<VAR>A : adj.toMonad.Algebra<VAR>B : D<VAR>inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<VAR>f : F.obj A.A ⟶ B<GOAL>A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (adj.toMonad.obj A.A) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔ G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>G : D ⥤ C<VAR>F : C ⥤ D<VAR>adj : F ⊣ G<VAR>A : adj.toMonad.Algebra<VAR>B : D<VAR>inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<VAR>f : F.obj A.A ⟶ B<GOAL>A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (G.obj (F.obj A.A)) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔ G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>G : D ⥤ C<VAR>F : C ⥤ D<VAR>adj : F ⊣ G<VAR>A : adj.toMonad.Algebra<VAR>B : D<VAR>inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<VAR>f : F.obj A.A ⟶ B<GOAL>A.a ≫ adj.unit.app A.A ≫ G.map f = G.map f ↔ G.map f = A.a ≫ adj.unit.app A.A ≫ G.map f
<VAR>X : Type u_1<VAR>inst✝ : UniformSpace X<VAR>i : (𝓤 X).IsCountablyGenerated<VAR>s : Set X<VAR>h : TotallyBounded s<VAR>this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace<GOAL>TopologicalSpace.IsSeparable s
<VAR>X : Type u_1<VAR>inst✝ : UniformSpace X<VAR>i : (𝓤 X).IsCountablyGenerated<VAR>s : Set X<VAR>this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace<VAR>h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε<GOAL>TopologicalSpace.IsSeparable s