ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P Q R : C<VAR>f✝ : P ⟶ Q<VAR>g✝ : Q ⟶ R<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : Arrow.mk f ≅ Arrow.mk g<VAR>h : StrongEpi f<VAR>this : Epi (f ≫ e.hom.right)<GOAL>Epi (e.inv.left ≫ f ≫ e.hom.right)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>P Q R : C<VAR>f✝ : P ⟶ Q<VAR>g✝ : Q ⟶ R<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : Arrow.mk f ≅ Arrow.mk g<VAR>h : StrongEpi f<VAR>X Y : C<VAR>z : X ⟶ Y<VAR>inst✝ : Mono z<GOAL>HasLiftingProperty g z
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s t u : Multiset α<GOAL>ndunion 0 t ≤ u ↔ 0 ⊆ u ∧ t ≤ u
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s t u : Multiset α<VAR>x✝¹ : α<VAR>x✝ : Multiset α<VAR>h : x✝.ndunion t ≤ u ↔ x✝ ⊆ u ∧ t ≤ u<GOAL>(x✝¹ ::ₘ x✝).ndunion t ≤ u ↔ x✝¹ ::ₘ x✝ ⊆ u ∧ t ≤ u
<VAR>n : ℕ<GOAL>range n.succ = n ::ₘ range n
<VAR>n : ℕ<GOAL>↑[n] + ↑(List.range n) = n ::ₘ range n
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝³ : BooleanAlgebra α<VAR>inst✝² : BooleanAlgebra β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : BoundedLatticeHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a ∆ b) = f a ∆ f b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddMonoid G<VAR>inst✝¹ : AddMonoid H<VAR>inst✝ : AddConstMapClass F G H a b<VAR>f : F<VAR>x : G<VAR>n : ℕ<GOAL>f (x + n • a) = f x + n • b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>inst✝ : Nonempty α<VAR>f : α → β<VAR>a : α<VAR>b : β<VAR>h : ∃ a, f a = b<GOAL>f (invFun f b) = b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>G : AddSubgroup R<VAR>k : ℤ<VAR>g : R<VAR>h : g ∈ G<GOAL>↑k * g ∈ G
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>G : AddSubgroup R<VAR>k : ℤ<VAR>g : R<VAR>h : g ∈ G<GOAL>↑k * g = k • g
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<GOAL>map (fun x => x.fst) Finset.univ.val = m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<VAR>this : map Prod.fst m.toEnumFinset.val = m<GOAL>map (fun x => x.fst) Finset.univ.val = m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<VAR>this : map Prod.fst (Finset.map m.coeEmbedding Finset.univ).val = m<GOAL>map (fun x => x.fst) Finset.univ.val = m
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hIX : M.Basis I X<VAR>hIY : M.Basis I Y<GOAL>M.Basis I (X ∪ Y)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hIX : M.Basis I X<VAR>hIY : M.Basis I Y<GOAL>M.Indep I
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>s : Set α<VAR>t : Set α := toMeasurable μ s<GOAL>∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>s : Set α<VAR>t : Set α := toMeasurable μ s<VAR>A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))<GOAL>∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>s : Set α<VAR>t : Set α := toMeasurable μ s<VAR>A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))<VAR>B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1<GOAL>∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>s : Set α<VAR>t : Set α := toMeasurable μ s<VAR>A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))<VAR>B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1<VAR>x : α<VAR>hx : Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))<VAR>h'x : t.indicator 1 x = 1<GOAL>Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>s : Set α<VAR>t : Set α := toMeasurable μ s<VAR>A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))<VAR>B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1<VAR>x : α<VAR>hx : Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 1)<VAR>h'x : t.indicator 1 x = 1<GOAL>Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>s : Set α<VAR>t : Set α := toMeasurable μ s<VAR>A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))<VAR>B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1<VAR>x : α<VAR>hx : Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 1)<VAR>h'x : t.indicator 1 x = 1<GOAL>(fun a => μ (t ∩ a) / μ a) =ᶠ[v.filterAt x] fun a => μ (s ∩ a) / μ a
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>s : Set α<VAR>t : Set α := toMeasurable μ s<VAR>A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))<VAR>B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1<VAR>x : α<VAR>hx : Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 1)<VAR>h'x : t.indicator 1 x = 1<VAR>a✝ : Set α<VAR>ha : MeasurableSet a✝<GOAL>μ (t ∩ a✝) / μ a✝ = μ (s ∩ a✝) / μ a✝
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>s : Set α<VAR>t : Set α := toMeasurable μ s<VAR>A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))<VAR>B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1<VAR>x : α<VAR>hx : Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 1)<VAR>h'x : t.indicator 1 x = 1<VAR>a✝ : Set α<VAR>ha : MeasurableSet a✝<GOAL>μ (t ∩ a✝) = μ (s ∩ a✝)
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>↑n.pred'.succ' = ↑n
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeriesHasSum (fun x => cexp (2 * ↑π * I * ↑a * ↑x)) s (expZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<GOAL>LSeries.term (fun x => cexp (2 * ↑π * I * ↑a * ↑x)) s n = cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeries.term (fun x => cexp (2 * ↑π * I * ↑a * ↑x)) s 0 = cexp (2 * ↑π * I * ↑a * ↑0) / ↑0 ^ s
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>LSeries.term (fun x => cexp (2 * ↑π * I * ↑a * ↑x)) s n = cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p (x + ↑r)<GOAL>LiouvilleWith p x
<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>f : F[X]<GOAL>f.natSepDegree ≤ f.natDegree
<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>f : F[X]<VAR>this : Multiset.card (map (algebraMap F f.SplittingField) f).roots ≤ (map (algebraMap F f.SplittingField) f).natDegree<GOAL>f.natSepDegree ≤ f.natDegree
<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>f : F[X]<VAR>this : Multiset.card (f.aroots f.SplittingField) ≤ f.natDegree<GOAL>f.natSepDegree ≤ f.natDegree
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x✝ : α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hx : f x ≠ x<GOAL>(f.toCycle hf).Nodup
<VAR>a✝ b✝ : ℤ<VAR>n✝ a b n : ℕ<VAR>a_lt_n : a < n<VAR>b_lt_n : b < n<GOAL>(↑a - ↑b).natAbs < n
<VAR>a✝ b✝ : ℤ<VAR>n✝ a b n : ℕ<VAR>a_lt_n : a < n<VAR>b_lt_n : b < n<GOAL>|↑a - ↑b| < ↑n
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>range (snd R M M₂) = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a✝ b✝ c d a b : G<GOAL>a * (b * a⁻¹) = b
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Nontrivial S<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hp : p.Monic<GOAL>∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Nontrivial S<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hp : p.Monic<VAR>hR : Subsingleton R<GOAL>∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Nontrivial S<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hp : p.Monic<VAR>hR : Nontrivial R<GOAL>∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Nontrivial S<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hp : p.Monic<VAR>hR : Nontrivial R<VAR>H : erase p.natDegree p + X ^ p.natDegree = p<GOAL>∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Nontrivial S<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hp : p.Monic<VAR>hR : Nontrivial R<VAR>H : erase p.natDegree p + X ^ p.natDegree = p<VAR>h0 : ¬erase p.natDegree p = 0<GOAL>∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Nontrivial S<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hp : p.Monic<VAR>hR : Nontrivial R<VAR>H : erase p.natDegree p + X ^ p.natDegree = p<VAR>h0 : ¬erase p.natDegree p = 0<VAR>q : R[X]<VAR>hq : map f q = erase p.natDegree p ∧ q.degree = (erase p.natDegree p).degree<GOAL>∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Nontrivial S<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hp : p.Monic<VAR>hR : Nontrivial R<VAR>H : erase p.natDegree p + X ^ p.natDegree = p<VAR>h0 : ¬erase p.natDegree p = 0<VAR>q : R[X]<VAR>hq : map f q = erase p.natDegree p ∧ q.degree = (erase p.natDegree p).degree<VAR>p_neq_0 : p ≠ 0<GOAL>∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Nontrivial S<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hp : p.Monic<VAR>hR : Nontrivial R<VAR>H : erase p.natDegree p + X ^ p.natDegree = p<VAR>h0 : ¬erase p.natDegree p = 0<VAR>q : R[X]<VAR>hq : map f q = erase p.natDegree p ∧ q.degree = (erase p.natDegree p).degree<VAR>p_neq_0 : p ≠ 0<VAR>hdeg : q.degree < (X ^ p.natDegree).degree<GOAL>∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Nontrivial S<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hp : p.Monic<VAR>hR : Nontrivial R<VAR>H : erase p.natDegree p + X ^ p.natDegree = p<VAR>h0 : ¬erase p.natDegree p = 0<VAR>q : R[X]<VAR>hq : map f q = erase p.natDegree p ∧ q.degree = (erase p.natDegree p).degree<VAR>p_neq_0 : p ≠ 0<VAR>hdeg : q.degree < (X ^ p.natDegree).degree<GOAL>map f (q + X ^ p.natDegree) = p
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Nontrivial S<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hp : p.Monic<VAR>hR : Nontrivial R<VAR>H : erase p.natDegree p + X ^ p.natDegree = p<VAR>h0 : ¬erase p.natDegree p = 0<VAR>q : R[X]<VAR>hq : map f q = erase p.natDegree p ∧ q.degree = (erase p.natDegree p).degree<VAR>p_neq_0 : p ≠ 0<VAR>hdeg : q.degree < (X ^ p.natDegree).degree<GOAL>(q + X ^ p.natDegree).degree = p.degree
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Semiring α<VAR>i : m<VAR>j : n<VAR>i' : m<VAR>j' : n<GOAL>stdBasisMatrix i j 1 i' j' = vecMulVec (fun i' => if i = i' then 1 else 0) (fun j' => if j = j' then 1 else 0) i' j'
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Semiring α<VAR>i : m<VAR>j : n<VAR>i' : m<VAR>j' : n<GOAL>(if i = i' ∧ j = j' then 1 else 0) = if j = j' then if i = i' then 1 else 0 else 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Semiring α<VAR>i : m<VAR>j : n<VAR>i' : m<VAR>j' : n<GOAL>(if j = j' ∧ i = i' then 1 else 0) = if j = j' then if i = i' then 1 else 0 else 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝¹ : CommMonoid β<VAR>f : ι → κ<VAR>inst✝ : DecidablePred fun x => x ∈ Set.range f<VAR>s : Finset κ<VAR>hf : Set.InjOn f (f ⁻¹' ↑s)<VAR>g : κ → β<GOAL>∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ filter (fun x => x ∈ Set.range f) s, g x
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<GOAL>univ.{u, v}.ord = Ordinal.univ.{u, v}
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{max (u + 1) v}<VAR>h : o < Ordinal.univ.{u, v}<GOAL>o.card < univ.{u, v}
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{max (u + 1) v}<VAR>h : o < Ordinal.univ.{u, v}<VAR>this : ∃ a, lift.principalSeg.toRelEmbedding a = o<GOAL>o.card < univ.{u, v}
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o✝ : Ordinal.{max (u + 1) v}<VAR>h : o✝ < Ordinal.univ.{u, v}<VAR>o : Ordinal.{u}<VAR>h' : lift.principalSeg.toRelEmbedding o = o✝<GOAL>o✝.card < univ.{u, v}
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o✝ : Ordinal.{max (u + 1) v}<VAR>h : o✝ < Ordinal.univ.{u, v}<VAR>o : Ordinal.{u}<VAR>h' : lift.principalSeg.toRelEmbedding o = o✝<GOAL>lift.{max (u + 1) v, u} o.card < univ.{u, v}
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x✝ y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>x : Finset α × Finset α<VAR>hx : x = (s, t)<GOAL>min (minOrder α) ↑(s.card + t.card - 1) ≤ ↑(s * t).card
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x✝ y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>x : Finset α × Finset α<VAR>hx : x.1 = s ∧ x.2 = t<GOAL>min (minOrder α) ↑(s.card + t.card - 1) ≤ ↑(s * t).card
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x✝ y x : Finset α × Finset α<VAR>hs : x.1.Nonempty<VAR>ht : x.2.Nonempty<GOAL>min (minOrder α) ↑(x.1.card + x.2.card - 1) ≤ ↑(x.1 * x.2).card
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x✝ y x : Finset α × Finset α<VAR>hs : x.1.Nonempty<VAR>ht : x.2.Nonempty<GOAL>∀ y ∈ {x | x.1.Nonempty ∧ x.2.Nonempty}, (∀ z ∈ {x | x.1.Nonempty ∧ x.2.Nonempty}, DevosMulRel z y → (fun x => min (minOrder α) ↑(x.1.card + x.2.card - 1) ≤ ↑(x.1 * x.2).card) z) → (fun x => min (minOrder α) ↑(x.1.card + x.2.card - 1) ≤ ↑(x.1 * x.2).card) y
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : (s, t).1.Nonempty<VAR>ht : (s, t).2.Nonempty<VAR>ih : ∀ z ∈ {x | x.1.Nonempty ∧ x.2.Nonempty}, DevosMulRel z (s, t) → (fun x => min (minOrder α) ↑(x.1.card + x.2.card - 1) ≤ ↑(x.1 * x.2).card) z<GOAL>min (minOrder α) ↑((s, t).1.card + (s, t).2.card - 1) ≤ ↑((s, t).1 * (s, t).2).card
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>ih : ∀ (a b : Finset α), a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(a * b).card ∨ a.card + b.card ≤ (a * b).card + 1<GOAL>minOrder α ≤ ↑(s * t).card ∨ s.card + t.card ≤ (s * t).card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>ih : ∀ (a b : Finset α), a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(a * b).card ∨ a.card + b.card ≤ (a * b).card + 1<VAR>hts : t.card < s.card<GOAL>minOrder α ≤ ↑(s * t).card ∨ s.card + t.card ≤ (s * t).card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>ih : ∀ (a b : Finset α), a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(a * b).card ∨ a.card + b.card ≤ (a * b).card + 1<VAR>hst : s.card ≤ t.card<GOAL>minOrder α ≤ ↑(s * t).card ∨ s.card + t.card ≤ (s * t).card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>t : Finset α<VAR>ht : t.Nonempty<VAR>a : α<VAR>hs : {a}.Nonempty<VAR>ih : ∀ (a_1 b : Finset α), a_1.Nonempty → b.Nonempty → DevosMulRel (a_1, b) ({a}, t) → minOrder α ≤ ↑(a_1 * b).card ∨ a_1.card + b.card ≤ (a_1 * b).card + 1<VAR>hst : {a}.card ≤ t.card<GOAL>minOrder α ≤ ↑({a} * t).card ∨ {a}.card + t.card ≤ ({a} * t).card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>ih : ∀ (a b : Finset α), a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(a * b).card ∨ a.card + b.card ≤ (a * b).card + 1<VAR>hst : s.card ≤ t.card<VAR>a : α<VAR>ha : a ∈ ↑s<VAR>b : α<VAR>hb : b ∈ ↑s<VAR>hab : a ≠ b<GOAL>minOrder α ≤ ↑(s * t).card ∨ s.card + t.card ≤ (s * t).card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>ih : ∀ (a b : Finset α), a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(a * b).card ∨ a.card + b.card ≤ (a * b).card + 1<VAR>hst : s.card ≤ t.card<VAR>a : α<VAR>ha : a ∈ ↑s<VAR>b : α<VAR>hb : b ∈ ↑s<VAR>hab : a ≠ b<VAR>g : α<VAR>hg : g ≠ 1<VAR>hgs : (s ∩ op g • s).Nonempty<GOAL>minOrder α ≤ ↑(s * t).card ∨ s.card + t.card ≤ (s * t).card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>ih : ∀ (a b : Finset α), a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(a * b).card ∨ a.card + b.card ≤ (a * b).card + 1<VAR>hst : s.card ≤ t.card<VAR>a : α<VAR>ha : a ∈ ↑s<VAR>b : α<VAR>hb : b ∈ ↑s<VAR>hab : a ≠ b<VAR>g : α<VAR>hg : g ≠ 1<VAR>hgs : (s ∩ op g • s).Nonempty<VAR>hsg : op g • s = s<GOAL>minOrder α ≤ ↑(s * t).card ∨ s.card + t.card ≤ (s * t).card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>ih : ∀ (a b : Finset α), a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(a * b).card ∨ a.card + b.card ≤ (a * b).card + 1<VAR>hst : s.card ≤ t.card<VAR>a : α<VAR>ha : a ∈ ↑s<VAR>b : α<VAR>hb : b ∈ ↑s<VAR>hab : a ≠ b<VAR>g : α<VAR>hg : g ≠ 1<VAR>hgs : (s ∩ op g • s).Nonempty<VAR>hsg : op g • s ≠ s<GOAL>minOrder α ≤ ↑(s * t).card ∨ s.card + t.card ≤ (s * t).card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>ih : ∀ (a b : Finset α), a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(a * b).card ∨ a.card + b.card ≤ (a * b).card + 1<VAR>hst : s.card ≤ t.card<VAR>a : α<VAR>ha : a ∈ ↑s<VAR>b : α<VAR>hb : b ∈ ↑s<VAR>hab : a ≠ b<VAR>g : α<VAR>hg : g ≠ 1<VAR>hgs : (s ∩ op g • s).Nonempty<VAR>hsg : (s ∩ op g • s).card < s.card<GOAL>minOrder α ≤ ↑(s * t).card ∨ s.card + t.card ≤ (s * t).card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>ih : ∀ (a b : Finset α), a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(a * b).card ∨ a.card + b.card ≤ (a * b).card + 1<VAR>hst : s.card ≤ t.card<VAR>a : α<VAR>ha : a ∈ ↑s<VAR>b : α<VAR>hb : b ∈ ↑s<VAR>hab : a ≠ b<VAR>g : α<VAR>hg : g ≠ 1<VAR>hgs : (s ∩ op g • s).Nonempty<VAR>hsg : (s ∩ op g • s).card < s.card<VAR>aux1 : ((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2).card ≤ ((s, t).1 * (s, t).2).card<GOAL>minOrder α ≤ ↑(s * t).card ∨ s.card + t.card ≤ (s * t).card + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Group α<VAR>inst✝ : DecidableEq α<VAR>x y : Finset α × Finset α<VAR>s t : Finset α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>ih : ∀ (a b : Finset α), a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(a * b).card ∨ a.card + b.card ≤ (a * b).card + 1<VAR>hst : s.card ≤ t.card<VAR>a : α<VAR>ha : a ∈ ↑s<VAR>b : α<VAR>hb : b ∈ ↑s<VAR>hab : a ≠ b<VAR>g : α<VAR>hg : g ≠ 1<VAR>hgs : (s ∩ op g • s).Nonempty<VAR>hsg : (s ∩ op g • s).card < s.card<VAR>aux1 : ((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2).card ≤ ((s, t).1 * (s, t).2).card<VAR>aux2 : ((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2).card ≤ ((s, t).1 * (s, t).2).card<GOAL>minOrder α ≤ ↑(s * t).card ∨ s.card + t.card ≤ (s * t).card + 1