ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>sq sq₁ sq₂ : Square C<VAR>h : sq₁.IsPushout<VAR>e : sq₁ ≅ sq₂<GOAL>sq₁.f₁₃ ≫ (evaluation₃.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₃
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>sq sq₁ sq₂ : Square C<VAR>h : sq₁.IsPushout<VAR>e : sq₁ ≅ sq₂<GOAL>sq₁.f₂₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₂.mapIso e).hom ≫ sq₂.f₂₄
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>sq sq₁ sq₂ : Square C<VAR>h : sq₁.IsPushout<VAR>e : sq₁ ≅ sq₂<GOAL>sq₁.f₃₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₃.mapIso e).hom ≫ sq₂.f₃₄
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>f : 𝕜 → B<VAR>x : 𝕜<VAR>hx : x ∈ Ico a (a + p)<GOAL>liftIco p a f ↑x = f x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>f : 𝕜 → B<VAR>x : 𝕜<VAR>hx : x ∈ Ico a (a + p)<VAR>this : (equivIco p a) ↑x = ⟨x, hx⟩<GOAL>liftIco p a f ↑x = f x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>f : 𝕜 → B<VAR>x : 𝕜<VAR>hx : x ∈ Ico a (a + p)<VAR>this : (equivIco p a) ↑x = ⟨x, hx⟩<GOAL>(Ico a (a + p)).restrict f ⟨x, hx⟩ = f x
<VAR>b x✝ y✝ : ℝ<VAR>hb : 1 < b<VAR>x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<VAR>hy : y < 0<VAR>hxy : x < y<GOAL>logb b y < logb b x
<VAR>b x✝ y✝ : ℝ<VAR>hb : 1 < b<VAR>x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<VAR>hy : y < 0<VAR>hxy : x < y<GOAL>logb b |y| < logb b |x|
<VAR>b x✝ y✝ : ℝ<VAR>hb : 1 < b<VAR>x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<VAR>hy : y < 0<VAR>hxy : x < y<GOAL>|y| < |x|
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{?u.360, u_3} E<VAR>P : Cᵒᵖ ⥤ D<VAR>X B : C<VAR>π : X ⟶ B<VAR>c : PullbackCone π π<GOAL>P.map π.op ≫ P.map c.fst.op = P.map π.op ≫ P.map c.snd.op
<VAR>α : Type u<VAR>n : ℕ<GOAL>map Fin.val (finRange n) = range n
<VAR>α : Type u<VAR>n : ℕ<GOAL>map (fun a => a) (range n) = range n
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>x✝ : p ∣ a<VAR>b : α<VAR>hb : a = p * b<VAR>hb0 : b ≠ 0<GOAL>p * b ~ᵤ (p ::ₘ factors b).prod
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>x✝ : p ∣ a<VAR>b : α<VAR>hb : a = p * b<VAR>hb0 : b ≠ 0<GOAL>p * b ~ᵤ p * (factors b).prod
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>f g : Perm α<VAR>hf : f ∈ g.cycleFactorsFinset<GOAL>f.cycleType ≤ g.cycleType
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>f g : Perm α<VAR>hf : f ∈ g.cycleFactorsFinset<VAR>hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a<GOAL>f.cycleType ≤ g.cycleType
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>f g : Perm α<VAR>hf : f ∈ g.cycleFactorsFinset<VAR>hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a<GOAL>Multiset.map (Finset.card ∘ support) {f}.val ≤ Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>f g : Perm α<VAR>hf : f ∈ g.cycleFactorsFinset<VAR>hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a<GOAL>{f}.val ≤ g.cycleFactorsFinset.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a : α<GOAL>{a}.ncard = 1
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : h.IsPreservedBy F<GOAL>(h.map F).f' = F.map h.f'
<VAR>α : Type u_1<VAR>inst✝⁴ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>f✝ : α → β<VAR>γ : Type u_3<VAR>inst✝² : UniformSpace γ<VAR>inst✝¹ : CompleteSpace γ<VAR>inst✝ : T0Space γ<VAR>f : β → γ<VAR>g : α → β<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<VAR>a : α<GOAL>(pkg'.extend f ∘ pkg.map pkg' g) (pkg.coe a) = pkg.extend (f ∘ g) (pkg.coe a)
<VAR>α : Type u_1<VAR>inst✝⁴ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace β<VAR>pkg' : AbstractCompletion β<VAR>f✝ : α → β<VAR>γ : Type u_3<VAR>inst✝² : UniformSpace γ<VAR>inst✝¹ : CompleteSpace γ<VAR>inst✝ : T0Space γ<VAR>f : β → γ<VAR>g : α → β<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<VAR>a : α<GOAL>f (g a) = (f ∘ g) a
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>x✝² x✝¹ : Scheme<VAR>x✝ : x✝² ⟶ x✝¹<GOAL>IsSeparated x✝ ↔ MorphismProperty.diagonal (@IsClosedImmersion) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s✝ : Sym α n<VAR>a b : α<VAR>s : Sym α n.succ<GOAL>∃ a s', s = a ::ₛ s'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s✝ : Sym α n<VAR>a✝ b : α<VAR>s : Sym α n.succ<VAR>a : α<VAR>ha : a ∈ s<GOAL>∃ a s', s = a ::ₛ s'
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S.leftInv<GOAL>↑((S.leftInvEquiv hS) x) * ↑x = 1
<VAR>a : Ordinal.{u}<VAR>ha : 0 < a<GOAL>∀ (b : Ordinal.{u}), deriv (fun x => a * x) b = a ^ ω * b
<VAR>a : Ordinal.{u}<VAR>ha : 0 < a<GOAL>deriv (fun x => a * x) 0 = a ^ ω * 0 ∧ ∀ (a_1 : Ordinal.{u}), deriv (fun x => a * x) a_1 = a ^ ω * a_1 → deriv (fun x => a * x) (succ a_1) = a ^ ω * succ a_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>c : E<VAR>hc : c ≠ 0<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hcs : Memℒp (↑(piecewise s hs (const α c) (const α 0))) p μ<GOAL>μ s < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>c : E<VAR>hc : c ≠ 0<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hcs : Memℒp (↑(piecewise s hs (const α c) (const α 0))) p μ<VAR>this : support ↑(const α c) = Set.univ<GOAL>μ s < ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>p : R<VAR>z : S<VAR>hp : p ∈ comap (algebraMap R S) (conductor R x)<VAR>hz' : z ∈ Ideal.map (algebraMap R S) I<GOAL>(algebraMap R S) p * z ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>p : R<VAR>z : S<VAR>hp : p ∈ comap (algebraMap R S) (conductor R x)<VAR>hz' : ∃ l ∈ Finsupp.supported S S ↑I, (Finsupp.total R S S ⇑(algebraMap R S)) l = z<GOAL>(algebraMap R S) p * z ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>p : R<VAR>z : S<VAR>hp : p ∈ comap (algebraMap R S) (conductor R x)<VAR>l : R →₀ S<VAR>H : l ∈ Finsupp.supported S S ↑I<VAR>H' : (Finsupp.total R S S ⇑(algebraMap R S)) l = z<GOAL>(algebraMap R S) p * z ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>p : R<VAR>z : S<VAR>hp : p ∈ comap (algebraMap R S) (conductor R x)<VAR>l : R →₀ S<VAR>H : l ∈ Finsupp.supported S S ↑I<VAR>H' : (l.sum fun i a => a • (algebraMap R S) i) = z<GOAL>(algebraMap R S) p * z ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>p : R<VAR>z : S<VAR>hp : p ∈ comap (algebraMap R S) (conductor R x)<VAR>l : R →₀ S<VAR>H : l ∈ Finsupp.supported S S ↑I<VAR>H' : (l.sum fun i a => a • (algebraMap R S) i) = z<GOAL>(l.sum fun a c => c • (algebraMap R S) a * (algebraMap R S) p) ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>p : R<VAR>z : S<VAR>hp : p ∈ comap (algebraMap R S) (conductor R x)<VAR>l : R →₀ S<VAR>H : l ∈ Finsupp.supported S S ↑I<VAR>H' : (l.sum fun i a => a • (algebraMap R S) i) = z<VAR>lem : ∀ {a : R}, a ∈ I → l a • (algebraMap R S) a * (algebraMap R S) p ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)<GOAL>(l.sum fun a c => c • (algebraMap R S) a * (algebraMap R S) p) ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>p : R<VAR>z : S<VAR>hp : p ∈ comap (algebraMap R S) (conductor R x)<VAR>l : R →₀ S<VAR>H : l ∈ Finsupp.supported S S ↑I<VAR>H' : (l.sum fun i a => a • (algebraMap R S) i) = z<VAR>lem : ∀ {a : R}, a ∈ I → l a • (algebraMap R S) a * (algebraMap R S) p ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)<VAR>a b : S<GOAL>(fun u => u ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)) a → (fun u => u ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)) b → (fun u => u ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)) (a + b)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>p : R<VAR>z : S<VAR>hp : p ∈ comap (algebraMap R S) (conductor R x)<VAR>l : R →₀ S<VAR>H : l ∈ Finsupp.supported S S ↑I<VAR>H' : (l.sum fun i a => a • (algebraMap R S) i) = z<VAR>lem : ∀ {a : R}, a ∈ I → l a • (algebraMap R S) a * (algebraMap R S) p ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)<GOAL>(fun u => u ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)) 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>p : R<VAR>z : S<VAR>hp : p ∈ comap (algebraMap R S) (conductor R x)<VAR>l : R →₀ S<VAR>H : l ∈ Finsupp.supported S S ↑I<VAR>H' : (l.sum fun i a => a • (algebraMap R S) i) = z<VAR>lem : ∀ {a : R}, a ∈ I → l a • (algebraMap R S) a * (algebraMap R S) p ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)<GOAL>∀ x_1 ∈ l.support, (fun u => u ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)) ((fun a c => c • (algebraMap R S) a * (algebraMap R S) p) x_1 (l x_1))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>c : ℝ≥0<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊<VAR>p : ℝ<VAR>hp : 0 < p<GOAL>(∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) ^ (1 / p) ≤ c • (∫⁻ (a : α), ↑‖g a‖₊ ^ p ∂μ) ^ (1 / p)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>c : ℝ≥0<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊<VAR>p : ℝ<VAR>hp : 0 < p<GOAL>((∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) ^ (1 / p)) ^ p ≤ ↑c ^ p * ((∫⁻ (a : α), ↑‖g a‖₊ ^ p ∂μ) ^ (1 / p)) ^ p
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>c : ℝ≥0<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊<VAR>p : ℝ<VAR>hp : 0 < p<GOAL>∫⁻ (a : α), ↑(‖f a‖₊ ^ p) ∂μ ≤ ∫⁻ (a : α), ↑(c ^ p * ‖g a‖₊ ^ p) ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>c : ℝ≥0<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊<VAR>p : ℝ<VAR>hp : 0 < p<GOAL>∀ᵐ (a : α) ∂μ, ↑(‖f a‖₊ ^ p) ≤ ↑(c ^ p * ‖g a‖₊ ^ p)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>c : ℝ≥0<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊<VAR>p : ℝ<VAR>hp : 0 < p<GOAL>∀ᵐ (a : α) ∂μ, ‖f a‖₊ ≤ c * ‖g a‖₊
<VAR>α : Type u_1<VAR>t t₁ t₂ : TopologicalSpace α<VAR>s : Set α<VAR>inst✝ : TopologicalSpace α<GOAL>DiscreteTopology α ↔ ∀ (x : α), 𝓝[≠] x = ⊥
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>inst✝³ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝² : G.PreservesZeroMorphisms<VAR>inst✝¹ : HasCokernel f<VAR>inst✝ : HasCokernel (G.map f)<VAR>Z : C<VAR>h : Y ⟶ Z<VAR>w : f ≫ h = 0<GOAL>G.map f ≫ G.map h = 0
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>inst✝³ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝² : G.PreservesZeroMorphisms<VAR>inst✝¹ : HasCokernel f<VAR>inst✝ : HasCokernel (G.map f)<VAR>Z : C<VAR>h : Y ⟶ Z<VAR>w : f ≫ h = 0<GOAL>coequalizer.π (G.map f) 0 ≫ cokernelComparison f G ≫ G.map (cokernel.desc f h w) = coequalizer.π (G.map f) 0 ≫ cokernel.desc (G.map f) (G.map h) ⋯
<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✝ : CancelMonoidWithZero M₀<VAR>a b c : M₀<GOAL>a * b = b ↔ a * b = 1 * b
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>coeff 1 n = if n = 0 then 1 else 0
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>coeff 1 n = if 0 = n then 1 else 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ s : Set α<VAR>b : Set (Set α)<VAR>hb : IsTopologicalBasis b<GOAL>IsOpen s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t₁ : TopologicalSpace α<VAR>t₂ t₃ : TopologicalSpace β<GOAL>Continuous f ↔ Continuous f ∧ Continuous f
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>this : (a + b) % c = (a % c + b % c) % c<VAR>hc0 : c = 0<GOAL>((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a * b⁻¹ ≤ c ↔ a ≤ b * c
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>x ⧏ y ↔ x < y ∨ x ‖ y
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>¬y ≤ x ↔ x ≤ y ∧ ¬y ≤ x ∨ ¬y ≤ x ∧ ¬x ≤ y
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>x : E<GOAL>Tendsto (fun a => ‖a‖) (𝓝 x) (𝓝 ‖x‖)
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<GOAL>Disjoint (LinearMap.range (ι R)) 1
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<GOAL>∀ x ∈ LinearMap.range (ι R), x ∈ 1 → x = 0
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : M<VAR>r : R<VAR>hx : (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r<GOAL>(algebraMap R (ExteriorAlgebra R M)) r = 0
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : M<VAR>r : R<VAR>hx : x = 0 ∧ r = 0<GOAL>(algebraMap R (ExteriorAlgebra R M)) r = 0
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x✝ y✝ z x y : R<VAR>g : Γ₀<VAR>hx : v x ≤ g<VAR>hy : v y ≤ g<GOAL>v (x - y) ≤ g
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x✝ y✝ z x y : R<VAR>g : Γ₀<VAR>hx : v x ≤ g<VAR>hy : v y ≤ g<GOAL>v (x + -y) ≤ g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>hs : IsOpen s<GOAL>mk ⁻¹' (mk '' s) = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>hs : IsOpen s<GOAL>mk ⁻¹' (mk '' s) ⊆ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x✝ y✝ z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>hs : IsOpen s<VAR>x y : X<VAR>hys : y ∈ s<VAR>hxy : mk y = mk x<GOAL>x ∈ s
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>S : IntermediateField F K<VAR>inst✝¹ : Algebra.IsAlgebraic F ↥S<VAR>inst✝ : IsPurelyInseparable F E<GOAL>sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥S
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>S : IntermediateField F K<VAR>inst✝¹ : Algebra.IsAlgebraic F ↥S<VAR>inst✝ : IsPurelyInseparable F E<VAR>this : Algebra.IsAlgebraic F ↥(adjoin F ↑S)<GOAL>sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥S
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>S : IntermediateField F K<VAR>inst✝¹ : Algebra.IsAlgebraic F ↥S<VAR>inst✝ : IsPurelyInseparable F E<VAR>this✝ : Algebra.IsAlgebraic F ↥(adjoin F ↑S)<VAR>this : sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥(adjoin F ↑S)<GOAL>sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥S
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(ρ_ X).inv ≫ (β_ X (𝟙_ C)).hom = (λ_ X).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>((ρ_ X).inv ≫ (β_ X (𝟙_ C)).hom) ≫ (λ_ X).hom = (λ_ X).inv ≫ (λ_ X).hom
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>h : M.Indep (insert e I)<GOAL>M.Basis (insert e I) (insert e X)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>h : M.Indep (I ∪ {e})<GOAL>M.Basis (I ∪ {e}) (X ∪ {e})
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>f : 𝓢(E, F)<VAR>k : ℕ<VAR>x₀ : E<GOAL>‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>f : 𝓢(E, F)<VAR>k : ℕ<VAR>x₀ : E<VAR>this : ‖x₀‖ ^ k * ‖iteratedFDeriv ℝ 0 (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f<GOAL>‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f
<VAR>α : Type u_1<VAR>xs : List α<VAR>α✝ : Sort u_2<VAR>f : Nat → α → α✝ → α✝<VAR>i : α✝<VAR>s : Nat<GOAL>foldrIdx f i xs s = foldrIdx (fun i => f (i + s)) i xs
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>S : Type u_3<VAR>R : Type u_4<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : SetLike σ R<VAR>inst✝³ : AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : SetLike.GradedMonoid A<VAR>inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)<VAR>r r' : ⨁ (i : ι), ↥(A i)<VAR>n : ι<GOAL>↑((r * r') n) = DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>S : Type u_3<VAR>R : Type u_4<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : SetLike σ R<VAR>inst✝³ : AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : SetLike.GradedMonoid A<VAR>inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)<VAR>r r' : ⨁ (i : ι), ↥(A i)<VAR>n : ι<GOAL>↑((DFinsupp.sum r fun i ai => DFinsupp.sum r' fun j aj => (of (fun i => ↥(A i)) (i + j)) (GradedMonoid.GMul.mul ai aj)) n) = DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>S : Type u_3<VAR>R : Type u_4<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : SetLike σ R<VAR>inst✝³ : AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : SetLike.GradedMonoid A<VAR>inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)<VAR>r r' : ⨁ (i : ι), ↥(A i)<VAR>n x✝¹ x✝ : ι<GOAL>↑(((of (fun i => ↥(A i)) (x✝¹ + x✝)) (GradedMonoid.GMul.mul (r x✝¹) (r' x✝))) n) = (fun j rj => if x✝¹ + j = n then ↑(r x✝¹) * ↑rj else 0) x✝ (r' x✝)
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>D : Set E<VAR>x : E<VAR>xD : x ∈ D<GOAL>oscillationWithin f D x = 0 ↔ ContinuousWithinAt f D x
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>D : Set E<VAR>x : E<VAR>xD : x ∈ D<VAR>hf : oscillationWithin f D x = 0<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<GOAL>∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>D : Set E<VAR>x : E<VAR>xD : x ∈ D<VAR>hf : oscillationWithin f D x = 0<VAR>ε : ℝ≥0∞<VAR>ε0 : ∃ i, ∃ (_ : i ∈ Filter.map f (𝓝[D] x)), diam i < ε<GOAL>∀ᶠ (x_1 : E) in 𝓝[D] x, edist (f x_1) (f x) < ε