ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 α<GOAL>(∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => -f' x) g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : Countable α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSingletonClass α<VAR>p : PMF α<VAR>μ✝ : Measure α<VAR>inst✝¹ : IsProbabilityMeasure μ✝<VAR>μ : Measure α<VAR>inst✝ : IsProbabilityMeasure μ<GOAL>p.toMeasure = μ ↔ p = μ.toPMF
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝² : PseudoEMetricSpace α<VAR>γ : Type w<VAR>inst✝¹ : EMetricSpace γ<VAR>inst✝ : EMetricSpace β<VAR>f : γ → β<GOAL>UniformEmbedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>z : ℂ<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ re ⁻¹' {0, 1}<GOAL>‖F f ε z‖ ≤ 1
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>z : ℂ<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ re ⁻¹' {0, 1}<GOAL>(ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>m : α × β → γ<VAR>f : Filter α<VAR>g : Filter β<GOAL>map m (f ×ˢ g) = (map (fun a b => m (a, b)) f).seq g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>m : α × β → γ<VAR>f : Filter α<VAR>g : Filter β<GOAL>∀ (s : Set γ), (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔ ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>s : Finset α<GOAL>(↑s).encard = ↑s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>s : Finset α<GOAL>↑⋯.toFinset.card = ↑s.card
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : T1Space E<VAR>inst✝ : Module 𝕜 E<GOAL>(↑↑0).Pointed
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>h : Collinear k s<VAR>p₁ p₂ p₃ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₁p₂ : p₁ ≠ p₂<GOAL>p₃ ∈ affineSpan k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p₁ : P<VAR>h : ∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁<VAR>p₂ p₃ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₁p₂ : p₁ ≠ p₂<GOAL>p₃ ∈ affineSpan k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>v : V<VAR>h : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁<VAR>r₂ : k<VAR>hp₂ : r₂ • v +ᵥ p₁ ∈ s<VAR>hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁<VAR>r₃ : k<VAR>hp₃ : r₃ • v +ᵥ p₁ ∈ s<GOAL>r₃ • v +ᵥ p₁ ∈ affineSpan k {p₁, r₂ • v +ᵥ p₁}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>v : V<VAR>h : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁<VAR>r₂ : k<VAR>hp₂ : r₂ • v +ᵥ p₁ ∈ s<VAR>hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁<VAR>r₃ : k<VAR>hp₃ : r₃ • v +ᵥ p₁ ∈ s<GOAL>∃ r, r • (r₂ • v +ᵥ p₁ -ᵥ p₁) = r₃ • v
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>v : V<VAR>h : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁<VAR>r₂ : k<VAR>hp₂ : r₂ • v +ᵥ p₁ ∈ s<VAR>hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁<VAR>r₃ : k<VAR>hp₃ : r₃ • v +ᵥ p₁ ∈ s<VAR>h₂ : r₂ ≠ 0<GOAL>(r₃ / r₂) • (r₂ • v +ᵥ p₁ -ᵥ p₁) = r₃ • v
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 < x<VAR>hxy : x ≤ y<VAR>hz : z ≤ 0<VAR>this : 0 < y<GOAL>y ^ z ≤ x ^ z
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 < x<VAR>hxy : x ≤ y<VAR>hz : z ≤ 0<VAR>this : 0 < y<GOAL>x ^ (-z) ≤ y ^ (-z)
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 < x<VAR>hxy : x ≤ y<VAR>hz : z ≤ 0<VAR>this : 0 < y<GOAL>0 ≤ y
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 < x<VAR>hxy : x ≤ y<VAR>hz : z ≤ 0<VAR>this : 0 < y<GOAL>0 ≤ x
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 < x<VAR>hxy : x ≤ y<VAR>hz : z ≤ 0<VAR>this : 0 < y<GOAL>0 < x ^ z
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 < x<VAR>hxy : x ≤ y<VAR>hz : z ≤ 0<VAR>this : 0 < y<GOAL>0 < y ^ z
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hg : DifferentiableOn 𝕜 g s<GOAL>DifferentiableOn 𝕜 (fun y => f y - g y) s ↔ DifferentiableOn 𝕜 f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a✝ b a : α<VAR>s t : Finset α<GOAL>s.erase a ∩ t = (s ∩ t).erase a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<GOAL>Disjoint cofinite l ↔ ∃ s ∈ l, s.Finite
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app (e.inverse.obj Y) ≫ (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫ e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app (e.inverse.obj Y) ≫ (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫ e.unitIso.hom.app (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫ e.unitIso.inv.app (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫ e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app (e.inverse.obj Y) ≫ (((e.unit.app (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj Y))) ≫ (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (e.counitInv.app (e.functor.obj (e.inverse.obj Y))))) ≫ e.unitIso.inv.app (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫ e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>((((e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫ (e.functor ⋙ e.inverse).map (e.unit.1 (e.inverse.obj Y))) ≫ (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (e.counitInv.app (e.functor.obj (e.inverse.obj Y))))) ≫ e.unitIso.inv.app (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫ e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫ (e.functor ⋙ e.inverse).map (e.unit.1 (e.inverse.obj Y)) ≫ (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))) ≫ (((e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).hom ≫ (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv ≫ e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫ e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫ (e.functor ⋙ e.inverse).map (e.unit.1 (e.inverse.obj Y)) ≫ (((𝟙 (e.inverse.obj (e.functor.obj (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj Y))))) ≫ (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv) ≫ e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫ e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫ (e.functor ⋙ e.inverse).map (e.unit.1 (e.inverse.obj Y)) ≫ (((e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv ≫ e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫ e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫ (((e.inverse.map (e.counitIso.inv.app (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫ e.inverse.map ((e.inverse ⋙ e.functor).map (e.functor.toPrefunctor.2 (e.unit.1 (e.inverse.obj Y))))) ≫ e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫ e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫ e.inverse.map (e.counitIso.inv.app (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫ ((e.unitInv.app (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫ (𝟭 C).map (e.inverse.map (e.functor.toPrefunctor.2 (e.unit.1 (e.inverse.obj Y))))) ≫ e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫ e.inverse.map (e.counitIso.inv.app (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫ e.unitInv.app (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫ 𝟙 ((e.functor ⋙ e.inverse).obj ((𝟭 C).obj (e.inverse.obj Y))) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫ e.inverse.map (e.counitIso.inv.app (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫ e.unitInv.app (e.inverse.obj (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫ e.inverse.map (e.counitIso.inv.app (e.functor.toPrefunctor.1 ((𝟭 C).obj (e.inverse.obj Y)))) ≫ (e.functor ⋙ e.inverse).map (e.inverse.toPrefunctor.2 (e.counit.app Y)) ≫ e.unitInv.app (e.inverse.toPrefunctor.1 Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app ((𝟭 C).obj (e.inverse.obj Y)) ≫ 𝟙 (e.inverse.obj (e.functor.obj ((𝟭 C).obj (e.inverse.obj Y)))) ≫ e.unitInv.app (e.inverse.toPrefunctor.1 Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>𝟙 ((𝟭 C).obj ((𝟭 C).obj (e.inverse.obj Y))) = 𝟙 (e.inverse.obj Y)
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring A'<VAR>inst✝⁵ : Algebra ℚ A<VAR>inst✝⁴ : Algebra ℚ A'<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring A'<VAR>inst✝¹ : Algebra ℚ A<VAR>inst✝ : Algebra ℚ A'<VAR>n : ℕ<VAR>f : A →+* A'<VAR>n✝ : ℕ<GOAL>(coeff A' n✝) ((map f) (cos A)) = (coeff A' n✝) (cos A')
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : CommGroupWithZero G₀<VAR>a✝ b✝ c✝ d a b c : G₀<GOAL>a / c * b = a * b / c
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁵ : Category.{?u.45682, u_1} C₁<VAR>inst✝⁴ : Category.{?u.45686, u_2} C₂<VAR>inst✝³ : Category.{?u.45690, u_3} C₃<VAR>inst✝² : Category.{?u.45694, u_4} C₄<VAR>inst✝¹ : Category.{?u.45698, u_5} C₁₂<VAR>inst✝ : Category.{?u.45702, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>e : F ≅ F'<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<GOAL>((e.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ((e.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) = 𝟙 (((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁵ : Category.{?u.45682, u_1} C₁<VAR>inst✝⁴ : Category.{?u.45686, u_2} C₂<VAR>inst✝³ : Category.{?u.45690, u_3} C₃<VAR>inst✝² : Category.{?u.45694, u_4} C₄<VAR>inst✝¹ : Category.{?u.45698, u_5} C₁₂<VAR>inst✝ : Category.{?u.45702, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>e : F ≅ F'<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<GOAL>((e.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ((e.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) = 𝟙 (((F'.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Sub α<VAR>inst✝ : Bot α<VAR>a b : WithTop α<GOAL>a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>inst✝ : LocPathConnectedSpace X<VAR>U : Set X<VAR>U_op : IsOpen U<GOAL>IsPathConnected U ↔ IsConnected U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>inst✝ : LocPathConnectedSpace X<VAR>U : Set X<VAR>U_op : IsOpen U<GOAL>PathConnectedSpace ↑U ↔ ConnectedSpace ↑U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>inst✝ : LocPathConnectedSpace X<VAR>U : Set X<VAR>U_op : IsOpen U<VAR>this : LocPathConnectedSpace ↑U<GOAL>PathConnectedSpace ↑U ↔ ConnectedSpace ↑U
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H₁ : Embedding ⇑f<VAR>H₂ : Embedding ⇑g<GOAL>Embedding ⇑(limit.π (cospan f g) WalkingCospan.one)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H₁ : Embedding ⇑f<VAR>H₂ : Embedding ⇑g<VAR>e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S<GOAL>⇑(limit.π (cospan f g) WalkingCospan.one) = ⇑g ∘ ⇑(pullback.snd f g)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H₁ : Embedding ⇑f<VAR>H₂ : Embedding ⇑g<VAR>e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S<GOAL>⇑(limit.π (cospan f g) WalkingCospan.one) = ⇑(pullback.snd f g ≫ g)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H₁ : Embedding ⇑f<VAR>H₂ : Embedding ⇑g<VAR>e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S<GOAL>⇑(limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr) = ⇑(pullback.snd f g ≫ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>inst✝⁵ : Fintype α<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableRel G.Adj<VAR>n✝ : ℕ<VAR>a b c : α<VAR>s : Finset α<VAR>inst✝² : DecidableRel H.Adj<VAR>inst✝¹ : Fintype β<VAR>inst✝ : DecidableEq β<VAR>e : α ≃ β<VAR>n : ℕ<GOAL>(SimpleGraph.map e.toEmbedding G).cliqueSet n = ⇑{ toFun := map e.toEmbedding, inj' := ⋯ } '' G.cliqueSet n
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : TopologicalSpace α✝<VAR>α : Type u_3<VAR>β : Type u_4<VAR>t : TopologicalSpace α<VAR>inst✝⁵ : PolishSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>tβ : TopologicalSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : OpensMeasurableSpace β<VAR>f : α → β<VAR>inst✝ : SecondCountableTopology ↑(range f)<VAR>hf : Measurable f<GOAL>∃ t' ≤ t, Continuous f ∧ PolishSpace α
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : TopologicalSpace α✝<VAR>α : Type u_3<VAR>β : Type u_4<VAR>t : TopologicalSpace α<VAR>inst✝⁵ : PolishSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>tβ : TopologicalSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : OpensMeasurableSpace β<VAR>f : α → β<VAR>inst✝ : SecondCountableTopology ↑(range f)<VAR>hf : Measurable f<VAR>b : Set (Set ↑(range f))<VAR>b_count : b.Countable<VAR>hb : IsTopologicalBasis b<GOAL>∃ t' ≤ t, Continuous f ∧ PolishSpace α
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : TopologicalSpace α✝<VAR>α : Type u_3<VAR>β : Type u_4<VAR>t : TopologicalSpace α<VAR>inst✝⁵ : PolishSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>tβ : TopologicalSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : OpensMeasurableSpace β<VAR>f : α → β<VAR>inst✝ : SecondCountableTopology ↑(range f)<VAR>hf : Measurable f<VAR>b : Set (Set ↑(range f))<VAR>b_count : b.Countable<VAR>hb : IsTopologicalBasis b<VAR>this : Countable ↑b<GOAL>∃ t' ≤ t, Continuous f ∧ PolishSpace α
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : TopologicalSpace α✝<VAR>α : Type u_3<VAR>β : Type u_4<VAR>t : TopologicalSpace α<VAR>inst✝⁵ : PolishSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>tβ : TopologicalSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : OpensMeasurableSpace β<VAR>f : α → β<VAR>inst✝ : SecondCountableTopology ↑(range f)<VAR>hf : Measurable f<VAR>b : Set (Set ↑(range f))<VAR>b_count : b.Countable<VAR>hb : IsTopologicalBasis b<VAR>this✝ : Countable ↑b<VAR>this : ∀ (s : ↑b), IsClopenable (rangeFactorization f ⁻¹' ↑s)<GOAL>∃ t' ≤ t, Continuous f ∧ PolishSpace α
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : TopologicalSpace α✝<VAR>α : Type u_3<VAR>β : Type u_4<VAR>t : TopologicalSpace α<VAR>inst✝⁵ : PolishSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>tβ : TopologicalSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : OpensMeasurableSpace β<VAR>f : α → β<VAR>inst✝ : SecondCountableTopology ↑(range f)<VAR>hf : Measurable f<VAR>b : Set (Set ↑(range f))<VAR>b_count : b.Countable<VAR>hb : IsTopologicalBasis b<VAR>this : Countable ↑b<VAR>T : ↑b → TopologicalSpace α<VAR>Tt : ∀ (s : ↑b), T s ≤ t<VAR>Tpolish : ∀ (s : ↑b), PolishSpace α<VAR>h✝ : ∀ (s : ↑b), IsClosed (rangeFactorization f ⁻¹' ↑s)<VAR>Topen : ∀ (s : ↑b), IsOpen (rangeFactorization f ⁻¹' ↑s)<GOAL>∃ t' ≤ t, Continuous f ∧ PolishSpace α
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : TopologicalSpace α✝<VAR>α : Type u_3<VAR>β : Type u_4<VAR>t : TopologicalSpace α<VAR>inst✝⁵ : PolishSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>tβ : TopologicalSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : OpensMeasurableSpace β<VAR>f : α → β<VAR>inst✝ : SecondCountableTopology ↑(range f)<VAR>hf : Measurable f<VAR>b : Set (Set ↑(range f))<VAR>b_count : b.Countable<VAR>hb : IsTopologicalBasis b<VAR>this : Countable ↑b<VAR>T : ↑b → TopologicalSpace α<VAR>Tt : ∀ (s : ↑b), T s ≤ t<VAR>Tpolish : ∀ (s : ↑b), PolishSpace α<VAR>h✝ : ∀ (s : ↑b), IsClosed (rangeFactorization f ⁻¹' ↑s)<VAR>Topen : ∀ (s : ↑b), IsOpen (rangeFactorization f ⁻¹' ↑s)<VAR>t' : TopologicalSpace α<VAR>t'T : ∀ (i : ↑b), t' ≤ T i<VAR>t't : t' ≤ t<VAR>t'_polish : PolishSpace α<GOAL>∃ t' ≤ t, Continuous f ∧ PolishSpace α
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : TopologicalSpace α✝<VAR>α : Type u_3<VAR>β : Type u_4<VAR>t : TopologicalSpace α<VAR>inst✝⁵ : PolishSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>tβ : TopologicalSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : OpensMeasurableSpace β<VAR>f : α → β<VAR>inst✝ : SecondCountableTopology ↑(range f)<VAR>hf : Measurable f<VAR>b : Set (Set ↑(range f))<VAR>b_count : b.Countable<VAR>hb : IsTopologicalBasis b<VAR>this : Countable ↑b<VAR>T : ↑b → TopologicalSpace α<VAR>Tt : ∀ (s : ↑b), T s ≤ t<VAR>Tpolish : ∀ (s : ↑b), PolishSpace α<VAR>h✝ : ∀ (s : ↑b), IsClosed (rangeFactorization f ⁻¹' ↑s)<VAR>Topen : ∀ (s : ↑b), IsOpen (rangeFactorization f ⁻¹' ↑s)<VAR>t' : TopologicalSpace α<VAR>t'T : ∀ (i : ↑b), t' ≤ T i<VAR>t't : t' ≤ t<VAR>t'_polish : PolishSpace α<GOAL>Continuous f
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : TopologicalSpace α✝<VAR>α : Type u_3<VAR>β : Type u_4<VAR>t : TopologicalSpace α<VAR>inst✝⁵ : PolishSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>tβ : TopologicalSpace β<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : OpensMeasurableSpace β<VAR>f : α → β<VAR>inst✝ : SecondCountableTopology ↑(range f)<VAR>hf : Measurable f<VAR>b : Set (Set ↑(range f))<VAR>b_count : b.Countable<VAR>hb : IsTopologicalBasis b<VAR>this✝ : Countable ↑b<VAR>T : ↑b → TopologicalSpace α<VAR>Tt : ∀ (s : ↑b), T s ≤ t<VAR>Tpolish : ∀ (s : ↑b), PolishSpace α<VAR>h✝ : ∀ (s : ↑b), IsClosed (rangeFactorization f ⁻¹' ↑s)<VAR>Topen : ∀ (s : ↑b), IsOpen (rangeFactorization f ⁻¹' ↑s)<VAR>t' : TopologicalSpace α<VAR>t'T : ∀ (i : ↑b), t' ≤ T i<VAR>t't : t' ≤ t<VAR>t'_polish : PolishSpace α<VAR>this : Continuous (rangeFactorization f)<GOAL>Continuous f
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>xeq : abs ⟨a, f⟩ = x<VAR>h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ<VAR>p : α → Prop<GOAL>Liftp p x ↔ ∀ u ∈ supp x, p u
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>xeq : abs ⟨a, f⟩ = x<VAR>h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ<VAR>p : α → Prop<GOAL>(∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) ↔ ∀ u ∈ supp x, p u