ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>this : WfDvdMonoid R<VAR>fx : Multiset R<VAR>hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x<VAR>H : Associates.mk fx.prod = Associates.mk x<GOAL>Multiset.map Associates.mk fx = Multiset.replicate (Multiset.card fx) (Associates.mk ϖ)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>this : WfDvdMonoid R<VAR>fx : Multiset R<VAR>hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x<VAR>H : Associates.mk fx.prod = Associates.mk x<GOAL>Multiset.card (Multiset.map Associates.mk fx) = Multiset.card fx ∧ ∀ b ∈ Multiset.map Associates.mk fx, b = Associates.mk ϖ
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>this : WfDvdMonoid R<VAR>fx : Multiset R<VAR>hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x<VAR>H : Associates.mk fx.prod = Associates.mk x<GOAL>∀ (b : Associates R), ∀ x ∈ fx, Associates.mk x = b → b = Associates.mk ϖ
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>this : WfDvdMonoid R<VAR>fx : Multiset R<VAR>hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x<VAR>H : Associates.mk fx.prod = Associates.mk x<VAR>x✝ : R<VAR>a✝ : x✝ ∈ fx<GOAL>Associates.mk x✝ = Associates.mk ϖ
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>this : WfDvdMonoid R<VAR>fx : Multiset R<VAR>hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x<VAR>H : Associates.mk fx.prod = Associates.mk x<VAR>x✝ : R<VAR>a✝ : x✝ ∈ fx<GOAL>Associated x✝ ϖ
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>this : WfDvdMonoid R<VAR>fx : Multiset R<VAR>hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x<VAR>H : Associates.mk fx.prod = Associates.mk x<VAR>x✝ : R<VAR>a✝ : x✝ ∈ fx<GOAL>Irreducible x✝
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>this : WfDvdMonoid R<VAR>fx : Multiset R<VAR>hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x<VAR>H : Associates.mk fx.prod = Associates.mk x<VAR>x✝ : R<VAR>a✝ : x✝ ∈ fx<GOAL>x✝ ∈ fx
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>a b x : α<GOAL>↑(sign x) * |x| = x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hd : Disjoint x z<VAR>hz : z ≤ y<VAR>hs : y ≤ x ⊔ z<GOAL>y ⊓ x ⊔ z = y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hd : Disjoint x z<VAR>hz : z ≤ y<VAR>hs : (x ⊔ z) ⊓ y = y<GOAL>y ⊓ x ⊔ z = y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hd : Disjoint x z<VAR>hz : z ≤ y<VAR>hs : y ≤ x ⊔ z<GOAL>y ⊓ x ⊓ z = ⊥
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>f : A →ₐ[R] B<VAR>hs✝ : S.FG<VAR>s : Finset A<VAR>hs : Algebra.adjoin R ↑s = S<GOAL>Algebra.adjoin R ↑(Finset.image (⇑f) s) = Subalgebra.map f S
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>x y : α<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>x' y' : β<VAR>h : cmp x y = cmp x' y'<GOAL>x = y ↔ x' = y'
<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✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c d : G₀<VAR>m n : ℕ<VAR>a : G₀<VAR>h : n < m<GOAL>a ^ (m - n) = a ^ m * (a ^ n)⁻¹
<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✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<VAR>h : n < m<GOAL>0 ^ (m - n) = 0 ^ m * (0 ^ n)⁻¹
<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✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c d : G₀<VAR>m n : ℕ<VAR>a : G₀<VAR>h : n < m<VAR>ha : a ≠ 0<GOAL>a ^ (m - n) = a ^ m * (a ^ n)⁻¹
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>f : α → ℝ<GOAL>Tendsto (fun x => rexp (f x)) l (𝓝 0) ↔ Tendsto f l atBot
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>S : Set (LieSubmodule R L M)<GOAL>↑(sInf S) = ⨅ N ∈ S, ↑N
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p✝ q : Submodule R M<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>p : ι → Submodule R M<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p✝ q : Submodule R M<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>p : ι → Submodule R M<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>↑(∅.inf p) = ⋂ i ∈ ∅, ↑(p i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p✝ q : Submodule R M<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>p : ι → Submodule R M<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>i : ι<VAR>s : Finset ι<VAR>x✝ : i ∉ s<VAR>ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)<GOAL>↑((insert i s).inf p) = ⋂ i_1 ∈ insert i s, ↑(p i_1)
<VAR>M : Type u_1<VAR>S✝ T : Set M<VAR>inst✝ : Mul M<VAR>S : Set M<GOAL>S.centralizer.centralizer.centralizer = S.centralizer
<VAR>M : Type u_1<VAR>S✝ T : Set M<VAR>inst✝ : Mul M<VAR>S : Set M<GOAL>S.centralizer.centralizer.centralizer ⊆ S.centralizer
<VAR>M : Type u_1<VAR>S✝ T : Set M<VAR>inst✝ : Mul M<VAR>S : Set M<VAR>x : M<VAR>hx : x ∈ S.centralizer.centralizer.centralizer<GOAL>x ∈ S.centralizer
<VAR>M : Type u_1<VAR>S✝ T : Set M<VAR>inst✝ : Mul M<VAR>S : Set M<VAR>x : M<VAR>hx : x ∈ S.centralizer.centralizer.centralizer<GOAL>∀ m ∈ S, m * x = x * m
<VAR>M : Type u_1<VAR>S✝ T : Set M<VAR>inst✝ : Mul M<VAR>S : Set M<VAR>x : M<VAR>hx : x ∈ S.centralizer.centralizer.centralizer<VAR>y : M<VAR>hy : y ∈ S<GOAL>y * x = x * y
<VAR>M : Type u_1<VAR>S✝ T : Set M<VAR>inst✝ : Mul M<VAR>S : Set M<VAR>x : M<VAR>hx : ∀ m ∈ S.centralizer.centralizer, m * x = x * m<VAR>y : M<VAR>hy : y ∈ S<GOAL>y * x = x * y
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Martingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => f n ω) atTop atTop
<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 α<VAR>u v : α → ℝ<GOAL>(f =o[l] fun x => ‖g' x‖) ↔ f =o[l] g'
<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 α<VAR>u v : α → ℝ<GOAL>(∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f fun x => ‖g' x‖) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A✝ : Matrix n n α<VAR>b✝ : n → α<VAR>A : Matrix m m α<VAR>e : n ≃ m<VAR>b : n → α<VAR>i : n<GOAL>(A.submatrix ⇑e ⇑e).cramer b i = (A.cramer (b ∘ ⇑e.symm) ∘ ⇑e) i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>f : α → α<VAR>hf : LipschitzWith K f<GOAL>LipschitzWith (K ^ 0) f^[0]
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>f : α → α<VAR>hf : LipschitzWith K f<VAR>n : ℕ<GOAL>LipschitzWith (K ^ (n + 1)) f^[n + 1]
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>f : α → α<VAR>hf : LipschitzWith K f<VAR>n : ℕ<GOAL>LipschitzWith (K ^ n * K) f^[n + 1]
<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>c + ⨆ i, f i = ⨆ i, c + f i
<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, c + f i
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Monoid R<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : DistribMulAction R M<VAR>inst✝¹ : DistribMulAction Rᵐᵒᵖ M<VAR>inst✝ : SMulCommClass R Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>n : ℕ<VAR>h : x.snd <• x.fst = x.fst •> x.snd<GOAL>(x ^ n).snd = n •> (x.snd <• x.fst ^ n.pred)
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : IsDomain R✝<VAR>p✝ q : R✝[X]<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p : R[X]<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>f : ι → R<VAR>hf : Function.Injective f<VAR>heval : ∀ (i : ι), eval (f i) p = 0<VAR>hcard : p.natDegree < Fintype.card ι<GOAL>p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>h : ¬p = 0<GOAL>rootMultiplicity 0 p = p.natTrailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>h : ¬p = 0<GOAL>rootMultiplicity 0 p ≤ p.natTrailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>h : ¬p = 0<GOAL>p.natTrailingDegree ≤ rootMultiplicity 0 p
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<GOAL>p.ball 0 r = ⇑p ⁻¹' Metric.ball 0 r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>h : ∀ a ∈ s, t₁ a ⊆ t₂ a<GOAL>s.biUnion t₁ ⊆ s.biUnion t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>h : ∀ a ∈ s, t₁ a ⊆ t₂ a<VAR>this : ∀ (b : β), ∀ a ∈ s, b ∈ t₁ a → ∃ a ∈ s, b ∈ t₂ a<GOAL>s.biUnion t₁ ⊆ s.biUnion t₂
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>p q : Multiset (Associates α)<VAR>hp : ∀ a ∈ p, Irreducible a<VAR>hq : ∀ a ∈ q, Irreducible a<GOAL>p.prod ≤ q.prod ↔ p ≤ q
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>p q : Multiset (Associates α)<VAR>hp : ∀ a ∈ p, Irreducible a<VAR>hq : ∀ a ∈ q, Irreducible a<GOAL>p.prod ≤ q.prod → p ≤ q
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>p q : Multiset (Associates α)<VAR>hp : ∀ a ∈ p, Irreducible a<VAR>hq : ∀ a ∈ q, Irreducible a<VAR>c : Associates α<VAR>eqc : q.prod = p.prod * c<GOAL>p ≤ q
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>p q : Multiset (Associates α)<VAR>hp : ∀ a ∈ p, Irreducible a<VAR>hq : ∀ a ∈ q, Irreducible a<VAR>c : Associates α<VAR>eqc : q.prod = p.prod * c<VAR>x : Associates α<VAR>hx : x ∈ p + factors c<GOAL>Irreducible x
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>p q : Multiset (Associates α)<VAR>hp : ∀ a ∈ p, Irreducible a<VAR>hq : ∀ a ∈ q, Irreducible a<VAR>c : Associates α<VAR>eqc : q.prod = p.prod * c<GOAL>q.prod = (p + factors c).prod
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>n : ℕ<VAR>hx : ¬x = 0<GOAL>‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f : α → M<VAR>g : α → N<VAR>x : α<GOAL>(x ∈ mulSupport fun x => (f x, g x)) ↔ x ∈ mulSupport f ∪ mulSupport g
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).Δ = φ W.Δ
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>-φ W.b₂ ^ 2 * φ W.b₈ - 8 * φ W.b₄ ^ 3 - 27 * φ W.b₆ ^ 2 + 9 * φ W.b₂ * φ W.b₄ * φ W.b₆ = φ (-W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆)
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : DifferentiableOn ℝ f (Iio a)<VAR>hg' : ∀ x ∈ Iio a, deriv g x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf✝ : DifferentiableOn ℝ f (Iio a)<VAR>hg' : ∀ x ∈ Iio a, deriv g x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l<VAR>hdf : ∀ x ∈ Iio a, DifferentiableAt ℝ f x<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf✝ : DifferentiableOn ℝ f (Iio a)<VAR>hg' : ∀ x ∈ Iio a, deriv g x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l<VAR>hdf : ∀ x ∈ Iio a, DifferentiableAt ℝ f x<VAR>hdg : ∀ x ∈ Iio a, DifferentiableAt ℝ g x<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v<VAR>X : C<VAR>s : yoneda.obj X ⟶ A<VAR>x : F.obj (op (CostructuredArrow.mk s))<GOAL>op (CostructuredArrow.mk s) = op (CostructuredArrow.mk (mk s x).fst)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>t : Set γ<VAR>x : α<GOAL>x ∈ (r • s).core t ↔ x ∈ r.core (s.core t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>t : Set γ<VAR>x : α<GOAL>(∀ (y : γ) (x_1 : β), r x x_1 → s x_1 y → y ∈ t) ↔ ∀ (y : β), r x y → ∀ (y_1 : γ), s y y_1 → y_1 ∈ t
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>M = loopyOn E ↔ M.E = E ∧ ∀ X ⊆ M.E, M.Indep X → X = ∅
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>M.E = E → ((∀ I ⊆ M.E, M.Indep I ↔ I = ∅) ↔ ∀ X ⊆ M.E, M.Indep X → X = ∅)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I X R J : Set α<GOAL>(∀ I ⊆ M.E, M.Indep I ↔ I = ∅) ↔ ∀ X ⊆ M.E, M.Indep X → X = ∅
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>x : M<GOAL>(contractLeft d) ((ι Q) x) = (algebraMap R (CliffordAlgebra Q)) (d x)
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>x : M<GOAL>∀ (m : M) (x fx : CliffordAlgebra Q), ((contractLeftAux Q d) m) ((ι Q) m * x, ((contractLeftAux Q d) m) (x, fx)) = Q m • fx
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f✝ : ↑Γ(X, U)<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>this : IsAffine ↑U<GOAL>IsAffineOpen (f ''ᵁ U)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f✝ : ↑Γ(X, U)<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>this : IsAffine ↑U<GOAL>f ''ᵁ U = Scheme.Hom.opensRange (U.ι ≫ f)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f✝ : ↑Γ(X, U)<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>this : IsAffine ↑U<GOAL>↑(f ''ᵁ U) = ↑(Scheme.Hom.opensRange (U.ι ≫ f))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>x : M<VAR>h : x ∈ f.source<VAR>ht : t ∈ 𝓝[s] x<GOAL>↑(f.extend I).symm ⁻¹' t ∈ 𝓝[↑(f.extend I).symm ⁻¹' s ∩ range ↑I] ↑(f.extend I) x
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.119255, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : ℱ ⟶ ℱ'.val<VAR>X : Dᵒᵖ<GOAL>(sheafHom (whiskerLeft G.op α)).app X = α.app X
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.119255, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : ℱ ⟶ ℱ'.val<VAR>X : Dᵒᵖ<GOAL>yoneda.map ((sheafHom (whiskerLeft G.op α)).app X) = yoneda.map (α.app X)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.119255, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : ℱ ⟶ ℱ'.val<VAR>X : Dᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj (ℱ.obj X)).obj U<GOAL>(yoneda.map ((sheafHom (whiskerLeft G.op α)).app X)).app U a✝ = (yoneda.map (α.app X)).app U a✝
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.119255, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : ℱ ⟶ ℱ'.val<VAR>X : Dᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj (ℱ.obj X)).obj U<GOAL>((sheafYonedaHom (whiskerLeft G.op α)).app X).app U a✝ = (yoneda.map (α.app X)).app U a✝
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.119255, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : ℱ ⟶ ℱ'.val<VAR>X : Dᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj (ℱ.obj X)).obj U<GOAL>(let_fun this := (yoneda.map (α.app X)).app U a✝; this) = ((sheafYonedaHom (whiskerLeft G.op α)).app X).app U a✝
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.119255, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : ℱ ⟶ ℱ'.val<VAR>X : Dᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj (ℱ.obj X)).obj U<GOAL>(pushforwardFamily (homOver (whiskerLeft G.op α) (unop U)) a✝).Compatible
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.119255, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : ℱ ⟶ ℱ'.val<VAR>X : Dᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj (ℱ.obj X)).obj U<GOAL>(pushforwardFamily (homOver (whiskerLeft G.op α) (unop U)) a✝).IsAmalgamation (let_fun this := (yoneda.map (α.app X)).app U a✝; this)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.119255, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{u_5, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : ℱ ⟶ ℱ'.val<VAR>X : Dᵒᵖ<VAR>U : Aᵒᵖ<VAR>a✝ : (yoneda.obj (ℱ.obj X)).obj U<VAR>Y : D<VAR>f : Y ⟶ unop X<VAR>hf : (Sieve.coverByImage G (unop X)).arrows f<GOAL>(ℱ'.val ⋙ coyoneda.obj (op (unop U))).map f.op (let_fun this := (yoneda.map (α.app X)).app U a✝; this) = pushforwardFamily (homOver (whiskerLeft G.op α) (unop U)) a✝ f hf