ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<VAR>fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>T : Finset S<VAR>hT : Algebra.adjoin R ↑T = ⊤<VAR>y : S<VAR>r : R<VAR>hr : r ∈ ↑M<VAR>hy : (algebraMap S S') y ∈ Algebra.adjoin R (⇑fₐ '' ↑T)<VAR>H : Algebra.adjoin R (⇑(algebraMap S S') '' ↑T) ≤ Subalgebra.restrictScalars R (Algebra.adjoin R' (⇑(algebraMap S S') '' ↑T))<GOAL>IsLocalization.mk' S' 1 ⟨f r, ⋯⟩ * (algebraMap S S') y = IsLocalization.mk' R' 1 ⟨r, hr⟩ • (algebraMap S S') y
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<VAR>fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>T : Finset S<VAR>hT : Algebra.adjoin R ↑T = ⊤<VAR>y : S<VAR>r : R<VAR>hr : r ∈ ↑M<VAR>hy : (algebraMap S S') y ∈ Algebra.adjoin R (⇑fₐ '' ↑T)<VAR>H : Algebra.adjoin R (⇑(algebraMap S S') '' ↑T) ≤ Subalgebra.restrictScalars R (Algebra.adjoin R' (⇑(algebraMap S S') '' ↑T))<GOAL>IsLocalization.mk' S' 1 ⟨f r, ⋯⟩ * (algebraMap S S') y = (algebraMap R' S') (IsLocalization.mk' R' 1 ⟨r, hr⟩) * (algebraMap S S') y
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<VAR>fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯<VAR>T : Finset S<VAR>hT : Algebra.adjoin R ↑T = ⊤<VAR>y : S<VAR>r : R<VAR>hr : r ∈ ↑M<VAR>hy : (algebraMap S S') y ∈ Algebra.adjoin R (⇑fₐ '' ↑T)<VAR>H : Algebra.adjoin R (⇑(algebraMap S S') '' ↑T) ≤ Subalgebra.restrictScalars R (Algebra.adjoin R' (⇑(algebraMap S S') '' ↑T))<GOAL>IsLocalization.mk' S' 1 ⟨f r, ⋯⟩ * (algebraMap S S') y = IsLocalization.mk' S' (f 1) ⟨f ↑⟨r, hr⟩, ⋯⟩ * (algebraMap S S') y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : BooleanAlgebra α<VAR>a b c d : α<GOAL>a ⇔ b ⇔ a = b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Mul G<VAR>inst✝¹ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>inst✝ : Subsingleton G<GOAL>UniqueMul A B a0 b0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : q.degree ≤ p.degree<VAR>a✝ : Nontrivial R<GOAL>q.degree + (p /ₘ q).degree = p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : q.degree ≤ p.degree<VAR>a✝ : Nontrivial R<VAR>hdiv0 : p /ₘ q ≠ 0<GOAL>q.degree + (p /ₘ q).degree = p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : q.degree ≤ p.degree<VAR>a✝ : Nontrivial R<VAR>hdiv0 : p /ₘ q ≠ 0<VAR>hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0<GOAL>q.degree + (p /ₘ q).degree = p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>h : q.degree ≤ p.degree<VAR>a✝ : Nontrivial R<VAR>hdiv0 : p /ₘ q ≠ 0<VAR>hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0<VAR>hmod : (p %ₘ q).degree < (q * (p /ₘ q)).degree<GOAL>q.degree + (p /ₘ q).degree = p.degree
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.IsLeftInversion w (cs.simple i) ↔ cs.IsLeftDescent w i
<VAR>R R' : Type u<VAR>M M' : Type v<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Ring R'<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : ContinuousConstSMul R M<VAR>inst✝² : Module R' M'<VAR>inst✝¹ : ContinuousConstSMul R' M'<VAR>inst✝ : ContinuousAdd M<VAR>s : Submodule R M<GOAL>Dense ↑s ↔ s.topologicalClosure = ⊤
<VAR>R R' : Type u<VAR>M M' : Type v<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Ring R'<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : ContinuousConstSMul R M<VAR>inst✝² : Module R' M'<VAR>inst✝¹ : ContinuousConstSMul R' M'<VAR>inst✝ : ContinuousAdd M<VAR>s : Submodule R M<GOAL>closure ↑s = Set.univ ↔ ↑s.topologicalClosure = ↑⊤
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>hsp : ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure<GOAL>⨆ i, LinearMap.range (LinearIsometry.toSpanSingleton 𝕜 E ⋯).toLinearMap = span 𝕜 (Set.range v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → β<GOAL>Integrable f Measure.count ↔ Summable fun 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>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → β<GOAL>(Summable fun x => ‖f x‖) → AEStronglyMeasurable f Measure.count
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → β<VAR>hs : Summable fun x => ‖f x‖<GOAL>AEStronglyMeasurable f Measure.count
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → β<VAR>hs : Summable fun x => ‖f x‖<VAR>hs' : (Function.support f).Countable<GOAL>AEStronglyMeasurable f Measure.count
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → β<VAR>hs : Summable fun x => ‖f x‖<VAR>hs' : (Function.support f).Countable<VAR>this✝ : MeasurableSpace β := borel β<VAR>this : BorelSpace β<GOAL>AEStronglyMeasurable f Measure.count
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → β<VAR>hs : Summable fun x => ‖f x‖<VAR>hs' : (Function.support f).Countable<VAR>this✝ : MeasurableSpace β := borel β<VAR>this : BorelSpace β<GOAL>AEMeasurable f Measure.count
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : MeasurableSingletonClass α<VAR>f : α → β<VAR>hs : Summable fun x => ‖f x‖<VAR>hs' : (Function.support f).Countable<VAR>this✝ : MeasurableSpace β := borel β<VAR>this : BorelSpace β<GOAL>∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂Measure.count, f x ∈ t
<VAR>C : Type u'<VAR>inst✝⁴ : Category.{v', u'} C<VAR>J : GrothendieckTopology C<VAR>R : Sheaf J RingCat<VAR>inst✝³ : HasWeakSheafify J AddCommGrp<VAR>inst✝² : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝¹ : J.HasSheafCompose (forget₂ RingCat AddCommGrp)<VAR>M N P : SheafOfModules R<VAR>σ : M.GeneratingSections<VAR>p : M ⟶ N<VAR>inst✝ : Epi p<GOAL>Epi (N.freeHomEquiv.symm fun i => sectionsMap p (σ.s i))
<VAR>C : Type u'<VAR>inst✝⁴ : Category.{v', u'} C<VAR>J : GrothendieckTopology C<VAR>R : Sheaf J RingCat<VAR>inst✝³ : HasWeakSheafify J AddCommGrp<VAR>inst✝² : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝¹ : J.HasSheafCompose (forget₂ RingCat AddCommGrp)<VAR>M N P : SheafOfModules R<VAR>σ : M.GeneratingSections<VAR>p : M ⟶ N<VAR>inst✝ : Epi p<GOAL>Epi (M.freeHomEquiv.symm σ.s ≫ p)
<VAR>a x z✝ z : ℂ<GOAL>(↑z.arg).toReal = z.arg
<VAR>p b : ℝ<VAR>hb : 0 < b<VAR>hp : 1 < p<GOAL>(fun x => rexp (-b * x ^ p)) =o[atTop] fun x => rexp (-x)
<VAR>p b : ℝ<VAR>hb : 0 < b<VAR>hp : 1 < p<GOAL>Tendsto (fun x => -x - -b * x ^ p) atTop atTop
<VAR>p b : ℝ<VAR>hb : 0 < b<VAR>hp : 1 < p<GOAL>Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop
<VAR>p b : ℝ<VAR>hb : 0 < b<VAR>hp : 1 < p<GOAL>Tendsto (fun x => b * x ^ (p - 1) + -1) atTop atTop
<VAR>p b : ℝ<VAR>hb : 0 < b<VAR>hp : 1 < p<GOAL>Tendsto (fun x => b * x ^ (p - 1)) atTop atTop
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_1<VAR>b✝ : Basis ι R M<VAR>N O : Submodule R M<VAR>b : Basis ι R ↥O<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>hgen : generator (ϕ.submoduleImage N) = 0<GOAL>N = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_1<VAR>b✝ : Basis ι R M<VAR>N O : Submodule R M<VAR>b : Basis ι R ↥O<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>hgen : generator (ϕ.submoduleImage N) = 0<GOAL>∀ x ∈ N, x = 0
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_1<VAR>b✝ : Basis ι R M<VAR>N O : Submodule R M<VAR>b : Basis ι R ↥O<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>hgen : generator (ϕ.submoduleImage N) = 0<VAR>x : M<VAR>hx : x ∈ N<GOAL>x = 0
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_1<VAR>b✝ : Basis ι R M<VAR>N O : Submodule R M<VAR>b : Basis ι R ↥O<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>hgen : generator (ϕ.submoduleImage N) = 0<VAR>x : M<VAR>hx : x ∈ N<VAR>i : ι<GOAL>(b.repr ⟨x, ⋯⟩) i = (b.repr 0) i
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_1<VAR>b✝ : Basis ι R M<VAR>N O : Submodule R M<VAR>b : Basis ι R ↥O<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬⊥ < ψ.submoduleImage N<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>hgen : generator (ϕ.submoduleImage N) = 0<VAR>x : M<VAR>hx : x ∈ N<VAR>i : ι<GOAL>(b.repr ⟨x, ⋯⟩) i = (b.repr 0) i
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_1<VAR>b✝ : Basis ι R M<VAR>N O : Submodule R M<VAR>b : Basis ι R ↥O<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬⊥ < ψ.submoduleImage N<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>hgen : generator (ϕ.submoduleImage N) = 0<VAR>x : M<VAR>hx : x ∈ N<VAR>i : ι<GOAL>(b.repr ⟨x, ⋯⟩) i = 0
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_1<VAR>b✝ : Basis ι R M<VAR>N O : Submodule R M<VAR>b : Basis ι R ↥O<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬⊥ < ψ.submoduleImage N<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>hgen : generator (ϕ.submoduleImage N) = 0<VAR>x : M<VAR>hx : x ∈ N<VAR>i : ι<GOAL>(b.repr ⟨x, ⋯⟩) i ∈ (Finsupp.lapply i ∘ₗ ↑b.repr).submoduleImage N
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v✝ w : V<VAR>hM : M.IsMatching<VAR>hM' : M'.IsMatching<VAR>hd : Disjoint M.support M'.support<VAR>v : V<VAR>hv : v ∈ (M ⊔ M').verts<GOAL>∃! w, (M ⊔ M').Adj v w
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v✝ w : V<VAR>hM : M.IsMatching<VAR>hM' : M'.IsMatching<VAR>hd : Disjoint M.support M'.support<VAR>v : V<VAR>hv : v ∈ (M ⊔ M').verts<VAR>aux : ∀ {N N' : G.Subgraph}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w<GOAL>∃! w, (M ⊔ M').Adj v w
<VAR>R : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝²⁰ : CommSemiring R<VAR>inst✝¹⁹ : AddCommMonoid M✝<VAR>inst✝¹⁸ : Module R M✝<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁷ : CommRing R₁<VAR>inst✝¹⁶ : AddCommGroup M₁<VAR>inst✝¹⁵ : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹⁴ : CommSemiring R₂<VAR>inst✝¹³ : AddCommMonoid M₂<VAR>inst✝¹² : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝¹¹ : CommRing R₃<VAR>inst✝¹⁰ : AddCommGroup M₃<VAR>inst✝⁹ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>B : BilinForm R M✝<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂ : BilinForm R₂ M₂<VAR>n : Type u_11<VAR>o : Type u_12<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : Fintype o<VAR>inst✝³ : DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>M₂' : Type u_13<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R₂ M₂'<VAR>c : Basis o R₂ M₂'<VAR>inst✝ : DecidableEq o<VAR>M : Matrix n n R₂<VAR>P Q : Matrix n o R₂<VAR>x y : M₂'<GOAL>((((toBilin b) M).comp ((toLin c b) P) ((toLin c b) Q)) x) y = (((toBilin c) (Pᵀ * M * Q)) x) y
<VAR>R : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝²⁰ : CommSemiring R<VAR>inst✝¹⁹ : AddCommMonoid M✝<VAR>inst✝¹⁸ : Module R M✝<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁷ : CommRing R₁<VAR>inst✝¹⁶ : AddCommGroup M₁<VAR>inst✝¹⁵ : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹⁴ : CommSemiring R₂<VAR>inst✝¹³ : AddCommMonoid M₂<VAR>inst✝¹² : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝¹¹ : CommRing R₃<VAR>inst✝¹⁰ : AddCommGroup M₃<VAR>inst✝⁹ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>B : BilinForm R M✝<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂ : BilinForm R₂ M₂<VAR>n : Type u_11<VAR>o : Type u_12<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : Fintype o<VAR>inst✝³ : DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>M₂' : Type u_13<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R₂ M₂'<VAR>c : Basis o R₂ M₂'<VAR>inst✝ : DecidableEq o<VAR>M : Matrix n n R₂<VAR>P Q : Matrix n o R₂<VAR>x y : M₂'<GOAL>((((toLinearMap₂ b b) M).comp ((toLin c b) P) ((toLin c b) Q)) x) y = ((((toLinearMap₂ b b) M).compl₁₂ ((toLin c b) P) ((toLin c b) Q)) x) y
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>hab : b < a<VAR>hf : f =O[atTop] fun x => x ^ (-a)<GOAL>(fun t => log t • f t) =O[atTop] fun x => x ^ (-b)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>hab : b < a<VAR>hf : f =O[atTop] fun x => x ^ (-a)<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>(fun x => x ^ (a - b) • x ^ (-a)) t = (fun x => x ^ (-b)) t
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>hab : b < a<VAR>hf : f =O[atTop] fun x => x ^ (-a)<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>t ^ (a - b) • t ^ (-a) = t ^ (-b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>p : ι' → Prop<VAR>q : ι → ι' → Prop<VAR>s : (x : ι) → (y : ι') → p y ∧ q x y → Set α<GOAL>⋃ x, ⋃ y, ⋃ (h : p y ∧ q x y), s x y h = ⋃ y, ⋃ (hy : p y), ⋃ x, ⋃ (hx : q x y), s x y ⋯
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab : a ≤ b<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<VAR>h : ∀ x ∈ Icc a b, f x ≤ g x<GOAL>∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab : a ≤ b<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<VAR>h : ∀ x ∈ Icc a b, f x ≤ g x<VAR>H : ∀ x ∈ Ioc a b, f x ≤ g x := fun x hx => h x (Ioc_subset_Icc_self hx)<GOAL>∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : AddCommGroup M''<VAR>inst✝ : Module R M''<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>r : R<VAR>h : Function.Injective ⇑(DistribMulAction.toLinearMap R M r)<GOAL>IsSMulRegular (M ⧸ N) r ↔ r • ⊤ ⊓ N ≤ r • N
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : AddCommGroup M''<VAR>inst✝ : Module R M''<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>r : R<VAR>h : Function.Injective ⇑(DistribMulAction.toLinearMap R M r)<GOAL>map ((LinearMap.lsmul R M) r) ⊤ ⊓ N ≤ map ((LinearMap.lsmul R M) r) N ↔ r • ⊤ ⊓ N ≤ r • N
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>A : Matrix ι ι R<VAR>f : Module.End R M<VAR>h : (PiToModule.fromMatrix R b) A = (PiToModule.fromEnd R b) f<VAR>r : R<GOAL>(PiToModule.fromMatrix R b) (r • A) = (PiToModule.fromEnd R b) (r • f)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s t : Multiset α<VAR>f✝ g : α → Multiset β<VAR>m : Multiset α<VAR>f f' : α → Multiset β<VAR>hf : ∀ a ∈ m, HEq (f a) (f' a)<GOAL>HEq (m.bind f) (m.bind f')
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s t : Multiset α<VAR>f✝ g : α → Multiset β<VAR>m : Multiset α<VAR>f f' : α → Multiset β<VAR>hf : ∀ a ∈ m, f a = f' a<GOAL>HEq (m.bind f) (m.bind f')
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>R' : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝⁴ : FunLike F E ℝ<VAR>inst✝³ : Group E<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>r : R<VAR>p q : GroupSeminorm E<VAR>x y : ℝ<GOAL>r • max x y = max (r • x) (r • y)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>f : R[X]<VAR>inst✝¹ : Algebra R S<VAR>T : Type u_1<VAR>inst✝ : CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<VAR>z : S<VAR>w : R[X]<VAR>hzw : h.map w = z<GOAL>eval₂ i x (h.repr z) = eval₂ i x w
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>f : R[X]<VAR>inst✝¹ : Algebra R S<VAR>T : Type u_1<VAR>inst✝ : CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<VAR>z : S<VAR>w : R[X]<VAR>hzw : f ∣ h.repr z - w<GOAL>eval₂ i x (h.repr z) = eval₂ i x w
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>f : R[X]<VAR>inst✝¹ : Algebra R S<VAR>T : Type u_1<VAR>inst✝ : CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<VAR>z : S<VAR>w y : R[X]<VAR>hy : h.repr z - w = f * y<GOAL>eval₂ i x (h.repr z) = eval₂ i x w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>E B I : Set α<VAR>h : BijOn f E N.E<GOAL>(N.comapOn E f)✶ = N✶.comapOn E f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>E B✝ I : Set α<VAR>h : BijOn f E N.E<VAR>B : Set α<VAR>hB : B ⊆ (N.comapOn E f)✶.E<GOAL>(N.comapOn E f)✶.Base B ↔ (N✶.comapOn E f).Base B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>E B✝ I : Set α<VAR>h : BijOn f E N.E<VAR>B : Set α<VAR>hB : B ⊆ (N.comapOn E f)✶.E<GOAL>f '' B ⊆ N.E
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>g : G<VAR>a : α<GOAL>a ∈ orbit G (g • a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>u v : Fin 2<GOAL>(pathGraph 2).Adj u v ↔ ⊤.Adj u v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α α<VAR>μ : Measure α<VAR>hκ : κ.Invariant μ<GOAL>κ ∘ₖ const α μ = const α μ
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>hf : BddAbove (range f)<VAR>c : Cardinal.{v}<GOAL>(⨆ i, f i) + c = ⨆ i, f i + c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>hf : BddAbove (range f)<VAR>c : Cardinal.{v}<VAR>this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c<GOAL>(⨆ i, f i) + c = ⨆ i, f i + c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>hf : BddAbove (range f)<VAR>c : Cardinal.{v}<VAR>this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c<GOAL>(⨆ i, f i) + c ≤ ⨆ i, f i + c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>hf : BddAbove (range f)<VAR>c : Cardinal.{v}<VAR>this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c<VAR>bdd : BddAbove (range fun x => f x + c)<GOAL>(⨆ i, f i) + c ≤ ⨆ i, f i + c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>hf : BddAbove (range f)<VAR>c : Cardinal.{v}<VAR>this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c<VAR>bdd : BddAbove (range fun x => f x + c)<VAR>hs : ⨆ i, f i < ℵ₀<GOAL>(⨆ i, f i) + c ≤ ⨆ i, f i + c