ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y Z : Scheme<VAR>e : Y ≅ Z<VAR>f : X ⟶ Y<VAR>hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f<GOAL>stalkwise (fun {R S} [CommRing R] [CommRing S] => P) (f ≫ e.hom)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y Z : Scheme<VAR>e : Y ≅ Z<VAR>f : X ⟶ Y<VAR>hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f<GOAL>∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.stalkMap (f ≫ e.hom) x)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y Z : Scheme<VAR>e : Y ≅ Z<VAR>f : X ⟶ Y<VAR>hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f<VAR>x : ↑↑X.toPresheafedSpace<GOAL>P (Scheme.Hom.stalkMap (f ≫ e.hom) x)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y Z : Scheme<VAR>e : Y ≅ Z<VAR>f : X ⟶ Y<VAR>hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f<VAR>x : ↑↑X.toPresheafedSpace<GOAL>P (Scheme.Hom.stalkMap e.hom (f.val.base x) ≫ Scheme.Hom.stalkMap f x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a \ a ∆ b = a ⊓ b
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>V W : FGModuleCat K<GOAL>FGModuleCatCoevaluation K V ▷ V ≫ (α_ V (FGModuleCatDual K V) V).hom ≫ V ◁ FGModuleCatEvaluation K V = (λ_ V).hom ≫ (ρ_ V).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 1).HasBasis p U<GOAL>(𝓤 α).HasBasis p fun i => {x | x.2 / x.1 ∈ U i}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 1).HasBasis p U<GOAL>(Filter.comap (fun x => x.2 / x.1) (𝓝 1)).HasBasis p fun i => {x | x.2 / x.1 ∈ U i}
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>n : ℕ<VAR>h : lowerCentralSeries G n ≤ center G<GOAL>lowerCentralSeries G (n + 1) = ⊥
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>n : ℕ<VAR>h : lowerCentralSeries G n ≤ center G<GOAL>∀ y ∈ {x | ∃ p ∈ lowerCentralSeries G n, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}, y = 1
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>n : ℕ<VAR>h : lowerCentralSeries G n ≤ center G<VAR>y : G<VAR>hy1 : y ∈ lowerCentralSeries G n<VAR>z : G<GOAL>y * z * y⁻¹ * z⁻¹ = 1
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>n : ℕ<VAR>h : lowerCentralSeries G n ≤ center G<VAR>y : G<VAR>hy1 : y ∈ lowerCentralSeries G n<VAR>z : G<GOAL>z * y = y * z
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>V₂ : Type v'<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : _root_.Finite K<VAR>inst✝ : FiniteDimensional K V<GOAL>_root_.Finite V
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>V₂ : Type v'<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : _root_.Finite K<VAR>inst✝ : FiniteDimensional K V<VAR>val✝ : Fintype K<GOAL>_root_.Finite V
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>inst✝ : l.NeBot<VAR>s : Set 𝕜<VAR>hs : IsOpen s<VAR>hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s<VAR>hf : ∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s<VAR>hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>hx : x ∈ s<GOAL>HasDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>inst✝ : l.NeBot<VAR>s : Set 𝕜<VAR>hs : IsOpen s<VAR>hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s<VAR>hf : ∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s<VAR>hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>hx : x ∈ s<GOAL>∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) ((deriv ∘ f) n x) x
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionCommMonoid α<VAR>a b✝ c d : α<VAR>h : IsUnit a<VAR>b : α<GOAL>a / (a * b) = b⁻¹
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<GOAL>((gradedMul R 𝒜 ℬ) x) 1 = x
<VAR>i n : ℕ<VAR>h0 : n ≠ 0<VAR>hi : i.Coprime n<GOAL>IsPrimitiveRoot (cexp (2 * ↑π * I * (↑i / ↑n))) n
<VAR>i n : ℕ<VAR>h0 : n ≠ 0<VAR>hi : i.Coprime n<GOAL>cexp (2 * ↑π * I * (↑i / ↑n)) ^ n = 1 ∧ ∀ (l : ℕ), cexp (2 * ↑π * I * (↑i / ↑n)) ^ l = 1 → n ∣ l
<VAR>i n : ℕ<VAR>h0 : n ≠ 0<VAR>hi : i.Coprime n<GOAL>(∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) ∧ ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l
<VAR>x : ℝ<VAR>h0x : 0 < x<VAR>hxp : x < π / 2<GOAL>0 < tan x
<VAR>x : ℝ<VAR>h0x : 0 < x<VAR>hxp : x < π / 2<GOAL>0 < sin x / cos x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>x✝ y : G<VAR>i : ℤ<VAR>x : G<GOAL>IsOfFinOrder x⁻¹ ↔ IsOfFinOrder x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>x : G<VAR>n : ℕ<GOAL>orderOf x ∣ card G
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>a : R<GOAL>(coeff R n) ((C R) a) = if n = 0 then a else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>x y : α × β<GOAL>(hasse (α × β)).Adj x y ↔ (hasse α □ hasse β).Adj x y
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>r : R<VAR>f : R⟦X⟧<GOAL>(r • f).derivativeFun = r • f.derivativeFun
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>f : α → β<VAR>hf : MeasurePreserving f μa μb<VAR>hfe : MeasurableEmbedding f<VAR>s : Set β<GOAL>μa (f ⁻¹' s) = μb s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<VAR>H : Surjective f<GOAL>f '' s ∪ f '' sᶜ = univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set α<VAR>H : Surjective f<GOAL>f '' (s ∪ sᶜ) = univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>r' : β → β → Prop<VAR>s t : Set α<VAR>a✝ b✝ : α<VAR>hs : IsStrongAntichain r s<VAR>f : α → β<VAR>hf : Surjective f<VAR>h : ∀ (a b : α), r' (f a) (f b) → r a b<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : f a ≠ f b<VAR>c : α<GOAL>¬r' (f a) (f c) ∨ ¬r' (f b) (f c)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>A : Matrix n n α<VAR>B : Matrix n m α<VAR>inst✝ : Invertible A<GOAL>A * (⅟A * B) = B
<VAR>R : CommRingCat<GOAL>Spec.map (Scheme.ΓSpecIso R).hom = adjunction.unit.app (Spec R)
<VAR>R : CommRingCat<VAR>this : adjunction.unit.app (Scheme.Spec.obj (op R)) ≫ Scheme.Spec.map (adjunction.counit.app (op R)) = 𝟙 (Scheme.Spec.obj (op R))<GOAL>Spec.map (Scheme.ΓSpecIso R).hom = adjunction.unit.app (Spec R)
<VAR>R : CommRingCat<VAR>this : adjunction.unit.app (Spec R) ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)<GOAL>Spec.map (Scheme.ΓSpecIso R).hom = adjunction.unit.app (Spec R)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b a : α<VAR>s : Multiset α<GOAL>fold op b (a ::ₘ s) = fold op (op b a) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>im ⟪x, y⟫_𝕜 = -im ⟪y, x⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>∫⁻ (x : α), max (f x) (g x) ∂μ = ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hm : MeasurableSet {x | f x ≤ g x}<GOAL>∫⁻ (x : α), max (f x) (g x) ∂μ = ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hm : MeasurableSet {x | f x ≤ g x}<GOAL>∫⁻ (x : α) in {x | f x ≤ g x}, max (f x) (g x) ∂μ + ∫⁻ (x : α) in {x | f x ≤ g x}ᶜ, max (f x) (g x) ∂μ = ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hm : MeasurableSet {x | f x ≤ g x}<GOAL>∫⁻ (x : α) in {x | f x ≤ g x}, max (f x) (g x) ∂μ + ∫⁻ (x : α) in {x | f x ≤ g x}ᶜ, max (f x) (g x) ∂μ = ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {a | f a ≤ g a}ᶜ, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hm : MeasurableSet {x | f x ≤ g x}<GOAL>∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≤ g x} → max (f x) (g x) = g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hm : MeasurableSet {x | f x ≤ g x}<GOAL>∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≤ g x}ᶜ → max (f x) (g x) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>hg : Measurable g<VAR>a : γ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((κ ∘ₖ deterministic g hg) a) s = ((κ.comap g hg) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : CompleteSpace F<VAR>u : α → ℝ<VAR>f : α → β → F<VAR>hu : Summable u<VAR>hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n<GOAL>TendstoUniformly (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : α), f n x) atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : CompleteSpace F<VAR>u : α → ℝ<VAR>f : α → β → F<VAR>hu : Summable u<VAR>hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n<GOAL>TendstoUniformlyOn (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : α), f n x) atTop univ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>g : OneHom N P<VAR>f₁ f₂ : OneHom M N<VAR>hg : Function.Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>x : M<GOAL>g (f₁ x) = g (f₂ x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : DenselyOrdered α<VAR>a : α<VAR>s : Set α<GOAL>(∃ u, toDual a < toDual u ∧ Icc (toDual a) (toDual u) ⊆ ⇑ofDual ⁻¹' s) ↔ ∃ l < a, Icc l a ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : DenselyOrdered α<VAR>a : α<VAR>s : Set α<GOAL>(∃ u, toDual a < toDual u ∧ ⇑ofDual ⁻¹' Icc u a ⊆ ⇑ofDual ⁻¹' s) ↔ ∃ l < a, Icc l a ⊆ s
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f✝ : X ⟶ Y<VAR>d₁ d₂ d₃ : Factorisation f✝<VAR>f : d₁.Hom d₂<VAR>g : d₂.Hom d₃<GOAL>d₁.ι ≫ f.h ≫ g.h = d₃.ι
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f✝ : X ⟶ Y<VAR>d₁ d₂ d₃ : Factorisation f✝<VAR>f : d₁.Hom d₂<VAR>g : d₂.Hom d₃<GOAL>(f.h ≫ g.h) ≫ d₃.π = d₁.π
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<VAR>q : ℚ<GOAL>re ↑q = ↑q
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t : Set X<VAR>e : X ≃ᵢ Y<VAR>s : Set Y<GOAL>dimH (⇑e ⁻¹' s) = dimH s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ Z : C<VAR>f✝ : Y✝ ⟶ X✝<VAR>S R : Sieve X✝<VAR>X : C<VAR>hX : IsTerminal X<VAR>I : Type u_1<VAR>Y : I → C<VAR>f : (i : I) → Y i ⟶ X<GOAL>ofArrows Y f = ofObjects Y X
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ Z : C<VAR>f✝ : Y✝ ⟶ X✝<VAR>S R : Sieve X✝<VAR>X : C<VAR>hX : IsTerminal X<VAR>I : Type u_1<VAR>Y : I → C<VAR>f : (i : I) → Y i ⟶ X<VAR>W : C<VAR>g : W ⟶ X<GOAL>(ofObjects Y X).arrows g → (ofArrows Y f).arrows g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ Z : C<VAR>f✝ : Y✝ ⟶ X✝<VAR>S R : Sieve X✝<VAR>X : C<VAR>hX : IsTerminal X<VAR>I : Type u_1<VAR>Y : I → C<VAR>f : (i : I) → Y i ⟶ X<VAR>W : C<VAR>g : W ⟶ X<GOAL>(∃ i, Nonempty (W ⟶ Y i)) → ∃ i a, g = a ≫ f i
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ Z : C<VAR>f✝ : Y✝ ⟶ X✝<VAR>S R : Sieve X✝<VAR>X : C<VAR>hX : IsTerminal X<VAR>I : Type u_1<VAR>Y : I → C<VAR>f : (i : I) → Y i ⟶ X<VAR>W : C<VAR>g : W ⟶ X<VAR>i : I<VAR>h : W ⟶ Y i<GOAL>∃ i a, g = a ≫ f i
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hf : MonotoneOn f s<GOAL>∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hf : MonotoneOn f s<GOAL>∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ), x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hf : MonotoneOn f s<VAR>a b : ℝ<VAR>as : a ∈ s<VAR>bs : b ∈ s<VAR>a✝ : a < b<GOAL>∀ᵐ (x : ℝ), x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hf : MonotoneOn f s<VAR>a b : ℝ<VAR>as : a ∈ s<VAR>bs : b ∈ s<VAR>a✝ : a < b<VAR>g : ℝ → ℝ<VAR>hg : Monotone g<VAR>gf : EqOn f g (s ∩ Icc a b)<GOAL>∀ᵐ (x : ℝ), x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hf : MonotoneOn f s<VAR>a b : ℝ<VAR>as : a ∈ s<VAR>bs : b ∈ s<VAR>a✝ : a < b<VAR>g : ℝ → ℝ<VAR>hg : Monotone g<VAR>gf : EqOn f g (s ∩ Icc a b)<VAR>x : ℝ<VAR>hx : DifferentiableAt ℝ g x<GOAL>x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hf : MonotoneOn f s<VAR>a b : ℝ<VAR>as : a ∈ s<VAR>bs : b ∈ s<VAR>a✝ : a < b<VAR>g : ℝ → ℝ<VAR>hg : Monotone g<VAR>gf : EqOn f g (s ∩ Icc a b)<VAR>x : ℝ<VAR>hx : DifferentiableAt ℝ g x<VAR>h'x : x ∈ s ∩ Ioo a b<GOAL>DifferentiableWithinAt ℝ f s x
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hf : MonotoneOn f s<VAR>a b : ℝ<VAR>as : a ∈ s<VAR>bs : b ∈ s<VAR>a✝ : a < b<VAR>g : ℝ → ℝ<VAR>hg : Monotone g<VAR>gf : EqOn f g (s ∩ Icc a b)<VAR>x : ℝ<VAR>hx : DifferentiableAt ℝ g x<VAR>h'x : x ∈ s ∩ Ioo a b<GOAL>f =ᶠ[𝓝[s] x] g
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hf : MonotoneOn f s<VAR>a b : ℝ<VAR>as : a ∈ s<VAR>bs : b ∈ s<VAR>a✝ : a < b<VAR>g : ℝ → ℝ<VAR>hg : Monotone g<VAR>gf : EqOn f g (s ∩ Icc a b)<VAR>x : ℝ<VAR>hx : DifferentiableAt ℝ g x<VAR>h'x : x ∈ s ∩ Ioo a b<VAR>this : Ioo a b ∈ 𝓝[s] x<GOAL>f =ᶠ[𝓝[s] x] g
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>hf : MonotoneOn f s<VAR>a b : ℝ<VAR>as : a ∈ s<VAR>bs : b ∈ s<VAR>a✝ : a < b<VAR>g : ℝ → ℝ<VAR>hg : Monotone g<VAR>gf : EqOn f g (s ∩ Icc a b)<VAR>x : ℝ<VAR>hx : DifferentiableAt ℝ g x<VAR>h'x : x ∈ s ∩ Ioo a b<VAR>this : Ioo a b ∈ 𝓝[s] x<VAR>y : ℝ<VAR>hy : y ∈ s<VAR>h'y : y ∈ Ioo a b<GOAL>f y = g y
<VAR>α : Type u<VAR>L✝ L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>inst✝ : DecidableEq α<VAR>x✝ : FreeGroup α<VAR>L : List (α × Bool)<GOAL>reduce (toWord (Quot.mk Red.Step L)) = toWord (Quot.mk Red.Step L)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>a : α<VAR>hl : l.Nodup<VAR>hl' : l'.Nodup<VAR>h : l.toFinset = l'.toFinset<GOAL>l ~ l'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>a : α<VAR>hl : l.Nodup<VAR>hl' : l'.Nodup<VAR>h : l.toFinset = l'.toFinset<GOAL>↑l = ↑l'
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ x y : List α<GOAL>x = x ++ y ↔ y = []
<GOAL>StrictConcaveOn ℝ (Ioi 0) log
<GOAL>∀ {x y z : ℝ}, x ∈ Ioi 0 → z ∈ Ioi 0 → x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝³ : HasHomotopyCofiber φ<VAR>inst✝² : DecidableRel c.Rel<VAR>inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)<VAR>inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))<VAR>i j : ι<VAR>hij : c.Rel j i<GOAL>inlX K i j hij ≫ (π K).f j = 0
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝³ : HasHomotopyCofiber φ<VAR>inst✝² : DecidableRel c.Rel<VAR>inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)<VAR>inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))<VAR>i j : ι<VAR>hij : c.Rel j i<GOAL>((Homotopy.ofEq ⋯).trans (Homotopy.equivSubZero (Homotopy.refl (𝟙 K)))).hom i j = 0
<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>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>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 f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>hs : UniqueMDiffWithinAt I s x<VAR>h : MDifferentiableAt I I' f x<GOAL>mfderivWithin I I' f s x = mfderiv I I' 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>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>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 f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>hs : UniqueMDiffWithinAt I s x<VAR>h : MDifferentiableAt I I' f x<GOAL>mfderivWithin I I' f s x = mfderivWithin I I' f univ x
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝ : TopologicalSpace H<VAR>PG : Pregroupoid H<VAR>e e' : PartialHomeomorph H H<VAR>he' : e ≈ e'<VAR>he : PG.property (↑e) e.source<GOAL>PG.property (↑e') e'.source
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝ : TopologicalSpace H<VAR>PG : Pregroupoid H<VAR>e e' : PartialHomeomorph H H<VAR>he' : e ≈ e'<VAR>he : PG.property (↑e) e.source<GOAL>PG.property (↑e') e.source
<VAR>α : Type u_1<VAR>inst✝¹ : Mul α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x y : α<GOAL>(equivShrink α) (x * y) = (equivShrink α) x * (equivShrink α) y
<VAR>α : Type u_1<VAR>inst✝¹ : Mul α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x y : α<GOAL>(equivShrink α) (x * y) = (equivShrink α).symm.symm ((equivShrink α).symm ((equivShrink α) x) * (equivShrink α).symm ((equivShrink α) y))
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<GOAL>(ComplexShape.down ℕ).next 0 = 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>h : angle x y = 0<GOAL>‖x - y‖ = |‖x‖ - ‖y‖|
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>h : angle x y = 0<GOAL>‖x‖ ^ 2 - 2 * (‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>w : E<GOAL>(ContinuousLinearMap.id 𝕜 E) w = (K.subtypeL.comp (orthogonalProjection K) + Kᗮ.subtypeL.comp (orthogonalProjection Kᗮ)) w
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g✝ : S →+* T<VAR>f : R →+* S<VAR>hf : (algebraMap R T).SurjectiveOnStalks<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>J : Ideal (S ⊗[R] T)<VAR>hJ : J.IsPrime<GOAL>Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (algebraMap S (S ⊗[R] T)) J) J (algebraMap S (S ⊗[R] T)) ⋯)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g✝ : S →+* T<VAR>f : R →+* S<VAR>hf : (algebraMap R T).SurjectiveOnStalks<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>J : Ideal (S ⊗[R] T)<VAR>hJ : J.IsPrime<GOAL>∀ (s : S ⊗[R] T), ∃ x r, ∃ c ∉ J, (algebraMap S (S ⊗[R] T)) r ∉ J ∧ c * (algebraMap S (S ⊗[R] T)) r * s = c * (algebraMap S (S ⊗[R] T)) x