ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>inst✝¹ : IsIso a<VAR>inst✝ : Mono f<GOAL>a = a ≫ 𝟙 X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>inst✝¹ : IsIso a<VAR>inst✝ : Mono f<GOAL>f = 𝟙 X ≫ f
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>x + ↑n * ↑m ≤ (⇑f)^[n] x ↔ x + ↑m ≤ f x
<VAR>n✝ p : ℕ<VAR>hp : Prime p<VAR>h2 : p ≠ 2<VAR>n : ℕ<VAR>hn : p = 2 * n + 1<GOAL>p - 1 = n + n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p r✝ : R[X]<VAR>hp : p.Monic<VAR>r : R[X]<VAR>h0 : p * r ≠ 0<VAR>hl : (p * r).natDegree < p.natDegree<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p r✝ : R[X]<VAR>hp : p.Monic<VAR>r : R[X]<VAR>h0 : p * r ≠ 0<VAR>hl : p.natDegree + r.natDegree < p.natDegree<GOAL>False
<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>k✝ : ℕ<VAR>N N₁ N₂ : LieSubmodule R L M<VAR>k : ℕ<GOAL>lcs k N₁ ≤ N₂ ↔ N₁ ≤ ucs k N₂
<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>k✝ : ℕ<VAR>N N₁ N₂ : LieSubmodule R L M<VAR>k : ℕ<GOAL>k = 0 + k
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<VAR>hQz : Q z ≠ 0<GOAL>W'.add P Q = (P x * Q z) • Q
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MulAction G α<VAR>M : Type u_3<VAR>inst✝³ : Monoid M<VAR>inst✝² : MulAction M α<VAR>inst✝¹ : FaithfulSMul G α<VAR>inst✝ : FaithfulSMul M α<VAR>g h : G<VAR>ne_one : g ≠ 1<VAR>disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)<GOAL>¬Commute g h
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MulAction G α<VAR>M : Type u_3<VAR>inst✝³ : Monoid M<VAR>inst✝² : MulAction M α<VAR>inst✝¹ : FaithfulSMul G α<VAR>inst✝ : FaithfulSMul M α<VAR>g h : G<VAR>disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)<VAR>comm : Commute g h<GOAL>g = 1
<VAR>a✝ b✝ : ℤ<VAR>n : ℕ<VAR>a b : ℤ<VAR>ha : 0 ≤ a<VAR>hb : b ≤ 0<GOAL>a.natAbs = b.natAbs ↔ a = -b
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>hlead : f.eraseLead ≠ 0<VAR>hnext : f.nextCoeff = 0<GOAL>2 ≤ f.natDegree
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>hnext : f.nextCoeff = 0<VAR>hlead : f.natDegree < 2<GOAL>f.eraseLead = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>hnext : f.nextCoeff = 0<VAR>hlead : (∃ x, C x = f) ∨ ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = f<GOAL>f.eraseLead = 0
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>r : Cofix F → Cofix F → Prop<VAR>h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest<VAR>r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y<VAR>x y : Cofix F<VAR>rxy : r x y<GOAL>x = y
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>r : Cofix F → Cofix F → Prop<VAR>h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest<VAR>r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y<VAR>x y : Cofix F<VAR>rxy : r x y<GOAL>∀ (x : Cofix F), r' x x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>r : Cofix F → Cofix F → Prop<VAR>h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest<VAR>r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y<VAR>x y : Cofix F<VAR>rxy : r x y<GOAL>∀ (x y : Cofix F), r' x y → Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>r : Cofix F → Cofix F → Prop<VAR>h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest<VAR>r' : Cofix F → Cofix F → Prop := fun x y => x = y ∨ r x y<VAR>x y : Cofix F<VAR>rxy : r x y<GOAL>r' x y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>S : ℕ → Set α := spanningSets μ<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>S : ℕ → Set α := spanningSets μ<GOAL>μ ({a | ¬f a = 0 a} ∩ ⋃ b, spanningSets μ b) = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>S : ℕ → Set α := spanningSets μ<GOAL>∀ (i : ℕ), μ ({a | ¬f a = 0 a} ∩ spanningSets μ i) = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>S : ℕ → Set α := spanningSets μ<VAR>n : ℕ<GOAL>μ ({a | ¬f a = 0 a} ∩ spanningSets μ n) = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>S : ℕ → Set α := spanningSets μ<VAR>n : ℕ<VAR>h_meas_n : MeasurableSet (S n)<GOAL>μ ({a | ¬f a = 0 a} ∩ spanningSets μ n) = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>S : ℕ → Set α := spanningSets μ<VAR>n : ℕ<VAR>h_meas_n : MeasurableSet (S n)<VAR>hμn : μ (S n) < ⊤<GOAL>μ ({a | ¬f a = 0 a} ∩ spanningSets μ n) = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>S : ℕ → Set α := spanningSets μ<VAR>n : ℕ<VAR>h_meas_n : MeasurableSet (S n)<VAR>hμn : μ (S n) < ⊤<GOAL>(μ.restrict (S n)) {a | ¬f a = 0 a} = 0
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>m n : ℕ<VAR>ha : IsUnit A.det<VAR>h : n ≤ m<GOAL>A ^ (m - n) = A ^ m * (A ^ n)⁻¹
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>m n : ℕ<VAR>ha : IsUnit A.det<VAR>h : n ≤ m<GOAL>IsUnit (A ^ n).det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>ht : μ tᶜ = 0<GOAL>μ (s ∩ t) = μ s
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>Real.sin (angle x y + angle x (x - y) + angle y (y - x)) = 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>Real.sin (angle x y) * -Real.cos (angle x y) + Real.cos (angle x y) * Real.sin (angle x y) = 0
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<GOAL>⊤ ≤ Submodule.span ℤ (Set.range (eval C)) ↔ ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))<GOAL>Submodule.span ℤ (Set.range (Products.eval C)) ≤ Submodule.span ℤ (Set.range (eval C))
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))<GOAL>Set.range (Products.eval C) ⊆ ↑(Submodule.span ℤ (Set.range (eval C)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E✝ I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α → β<VAR>E : Set β<GOAL>(loopyOn E).comap f = loopyOn (f ⁻¹' E)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E✝ I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α → β<VAR>E : Set β<GOAL>((loopyOn E).comap f).E = f ⁻¹' E ∧ ∀ X ⊆ ((loopyOn E).comap f).E, ((loopyOn E).comap f).Indep X → 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]<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>hm : f.Monic<VAR>h : f.natSepDegree = 1<GOAL>∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m
<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>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>hm : f.Monic<VAR>h : f.natSepDegree = 1<VAR>p : F[X]<VAR>hM : p.Monic<VAR>hI : Irreducible p<VAR>hf : p ∣ f<GOAL>∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m
<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>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>hm : f.Monic<VAR>h : f.natSepDegree = 1<VAR>p : F[X]<VAR>hM : p.Monic<VAR>hI : Irreducible p<VAR>hf : p ∣ f<VAR>hD : p.natSepDegree = 1<GOAL>∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m
<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>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>hm : f.Monic<VAR>h : f.natSepDegree = 1<VAR>p : F[X]<VAR>hM : p.Monic<VAR>hI : Irreducible p<VAR>hf : p ∣ f<VAR>hD : p.natSepDegree = 1<VAR>n : ℕ<VAR>y : F<VAR>H : n = 0 ∨ y ∉ (frobenius F q).range<VAR>hp : p = X ^ q ^ n - C y<GOAL>∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m
<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>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>hm : f.Monic<VAR>h : f.natSepDegree = 1<VAR>p : F[X]<VAR>hM : p.Monic<VAR>hI : Irreducible p<VAR>hf : p ∣ f<VAR>hD : p.natSepDegree = 1<VAR>n : ℕ<VAR>y : F<VAR>H : n = 0 ∨ y ∉ (frobenius F q).range<VAR>hp : p = X ^ q ^ n - C y<VAR>hF : multiplicity.Finite p f<GOAL>∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m
<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>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>hm : f.Monic<VAR>h : f.natSepDegree = 1<VAR>p : F[X]<VAR>hM : p.Monic<VAR>hI : Irreducible p<VAR>hf : p ∣ f<VAR>hD : p.natSepDegree = 1<VAR>n : ℕ<VAR>y : F<VAR>H : n = 0 ∨ y ∉ (frobenius F q).range<VAR>hp : p = X ^ q ^ n - C y<VAR>hF : multiplicity.Finite p f<VAR>hne : (multiplicity p f).get hF ≠ 0<GOAL>∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m
<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>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>hm : f.Monic<VAR>h : f.natSepDegree = 1<VAR>p : F[X]<VAR>hM : p.Monic<VAR>hI : Irreducible p<VAR>hf : p ∣ f<VAR>hD : p.natSepDegree = 1<VAR>n : ℕ<VAR>y : F<VAR>H : n = 0 ∨ y ∉ (frobenius F q).range<VAR>hp : p = X ^ q ^ n - C y<VAR>hF : multiplicity.Finite p f<VAR>hne : (multiplicity p f).get hF ≠ 0<GOAL>f = (X ^ q ^ n - C y) ^ (multiplicity p f).get hF
<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>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>hm : f.Monic<VAR>h : f.natSepDegree = 1<VAR>p : F[X]<VAR>hM : p.Monic<VAR>hI : Irreducible p<VAR>hf✝ : p ∣ f<VAR>hD : p.natSepDegree = 1<VAR>n : ℕ<VAR>y : F<VAR>H✝ : n = 0 ∨ y ∉ (frobenius F q).range<VAR>hp : p = X ^ q ^ n - C y<VAR>hF : multiplicity.Finite p f<VAR>hne : (multiplicity p f).get hF ≠ 0<VAR>c : F[X]<VAR>hf : f = p ^ (multiplicity p f).get hF * c<VAR>H : ¬p ∣ c<GOAL>f = (X ^ q ^ n - C y) ^ (multiplicity p f).get hF
<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>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>hm : f.Monic<VAR>p : F[X]<VAR>hM : p.Monic<VAR>hI : Irreducible p<VAR>hf✝ : p ∣ f<VAR>hD : p.natSepDegree = 1<VAR>n : ℕ<VAR>y : F<VAR>H✝ : n = 0 ∨ y ∉ (frobenius F q).range<VAR>hp : p = X ^ q ^ n - C y<VAR>hF : multiplicity.Finite p f<VAR>hne : (multiplicity p f).get hF ≠ 0<VAR>c : F[X]<VAR>h : c.natDegree = 0<VAR>hf : f = p ^ (multiplicity p f).get hF * c<VAR>H : ¬p ∣ c<GOAL>f = (X ^ q ^ n - C y) ^ (multiplicity p f).get hF
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : RCLike K<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module K E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : IsScalarTower ℝ K E<VAR>r : ℝ<VAR>x : E<GOAL>r • x = ↑r • x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : Integrable f μ<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : Integrable f μ<VAR>hN : μ N = 0<VAR>this : 0 < μ {x | f x ≤ ⨍ (a : α), f a ∂μ}<GOAL>∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : Integrable f μ<VAR>hN : μ N = 0<VAR>this : 0 < μ ({x | f x ≤ ⨍ (a : α), f a ∂μ} \ N)<GOAL>∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : Integrable f μ<VAR>hN : μ N = 0<VAR>this : 0 < μ ({x | f x ≤ ⨍ (a : α), f a ∂μ} \ N)<VAR>x : α<VAR>hx : x ∈ {x | f x ≤ ⨍ (a : α), f a ∂μ}<VAR>hxN : x ∉ N<GOAL>∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s t : Multiset α<VAR>a : α<VAR>d₁ : s.Nodup<VAR>d₂ : t.Nodup<GOAL>(s + t).Nodup ↔ s.Disjoint t
<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>ι' : Sort u_7<VAR>inst✝ : CompleteLattice α<VAR>s : ι' → α<GOAL>⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i.down
<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>ι' : Sort u_7<VAR>inst✝ : CompleteLattice α<VAR>s : ι' → α<GOAL>⨆ x, s (Equiv.plift x) = ⨆ i, s i.down
<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✝ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>p : α → Prop<VAR>hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)<VAR>hs : ∀ b ∈ s, p (f b)<GOAL>WithBot.recBotCoe True p ↑(s.sup' H f)
<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✝ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>p : α → Prop<VAR>hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)<VAR>hs : ∀ b ∈ s, p (f b)<GOAL>WithBot.recBotCoe True p (s.sup (WithBot.some ∘ f))
<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✝ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>p : α → Prop<VAR>hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)<VAR>hs : ∀ b ∈ s, p (f b)<VAR>a₁ : WithBot α<VAR>h₁ : WithBot.recBotCoe True p a₁<VAR>a₂ : WithBot α<VAR>h₂ : WithBot.recBotCoe True p a₂<GOAL>WithBot.recBotCoe True p (a₁ ⊔ a₂)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) ⁻¹' Iic b = Iic (b + a)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → X → α<VAR>x₀ : X<GOAL>EquicontinuousAt F x₀ ↔ ContinuousAt (⇑UniformFun.ofFun ∘ swap F) x₀
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → X → α<VAR>x₀ : X<GOAL>EquicontinuousAt F x₀ ↔ ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝 x₀, (⇑UniformFun.ofFun ∘ swap F) x ∈ {g | ((⇑UniformFun.ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α i}
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a : α<VAR>h : IsLowerSet ↑𝒜<VAR>s : Finset α<GOAL>s ∈ Finset.memberSubfamily a 𝒜 → s ∈ Finset.nonMemberSubfamily a 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a : α<VAR>h : IsLowerSet ↑𝒜<VAR>s : Finset α<GOAL>insert a s ∈ 𝒜 ∧ a ∉ s → s ∈ 𝒜 ∧ a ∉ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommGroup α<VAR>a : α<VAR>l : List α<GOAL>(a :: l).alternatingProd = a / l.alternatingProd
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<GOAL>cos (angle x y) = 1 ↔ angle x y = 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<GOAL>cos (angle x y) = cos 0 ↔ angle x y = 0
<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>n✝¹ n✝ x✝ : ℕ<VAR>h : x✝ = n✝¹.mul (10 ^ n✝)<GOAL>OfScientific.ofScientific (↑n✝¹) false ↑n✝ = ↑x✝
<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>n✝¹ n✝ x✝ : ℕ<VAR>h : x✝ = n✝¹.mul (10 ^ n✝)<GOAL>↑(Rat.ofScientific (OfNat.ofNat ↑n✝¹) false (OfNat.ofNat ↑n✝)) = ↑x✝
<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>n✝¹ n✝ x✝ : ℕ<VAR>h : x✝ = n✝¹.mul (10 ^ n✝)<GOAL>↑(↑(OfNat.ofNat n✝¹) * 10 ^ OfNat.ofNat n✝) = ↑n✝¹ * 10 ^ n✝
<VAR>x : Cardinal.{u_1}<VAR>hx : x ≤ ℵ₀<GOAL>x ∈ range ofENat
<VAR>x y z : ℝ<GOAL>0 < sinh x ↔ 0 < x
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : 0 < a.re<GOAL>∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * ↑n ^ 2)
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>ν : ProbabilityMeasure Ω<GOAL>ν univ ≠ 0
<VAR>x y : ℤ<GOAL>x.lcm y = x.natAbs.lcm y.natAbs
<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) = ∑ ij ∈ Finset.filter (fun ij => ij.1 + ij.2 = n) (DFinsupp.support r ×ˢ DFinsupp.support r'), ↑(r ij.1) * ↑(r' ij.2)
<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>∑ i ∈ DFinsupp.support r ×ˢ DFinsupp.support r', ↑(((of (fun i => ↥(A i)) (i.1 + i.2)) (GradedMonoid.GMul.mul (r i.1) (r' i.2))) n) = ∑ ij ∈ Finset.filter (fun ij => ij.1 + ij.2 = n) (DFinsupp.support r ×ˢ DFinsupp.support r'), ↑(r ij.1) * ↑(r' ij.2)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>s : S<VAR>hs : IsIntegral R s<VAR>p : R[X]<VAR>hp : minpoly R s ∣ p<GOAL>(Polynomial.aeval s) p = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>π : α → Type u_6<VAR>π' : β → Type u_7<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>g : (a : α) → π a → π' (f a)<VAR>a : α<VAR>l : Filter (π' (f a))<GOAL>map (Sigma.mk a) (comap (g a) l) = comap (Sigma.map f g) (map (Sigma.mk (f a)) l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>π : α → Type u_6<VAR>π' : β → Type u_7<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>g : (a : α) → π a → π' (f a)<VAR>a : α<VAR>l : Filter (π' (f a))<GOAL>(comap (Sigma.map f g) (map (Sigma.mk (f a)) l)).HasBasis (fun s => s ∈ l) fun i => Sigma.mk a '' (g a ⁻¹' id i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>π : α → Type u_6<VAR>π' : β → Type u_7<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>g : (a : α) → π a → π' (f a)<VAR>a : α<VAR>l : Filter (π' (f a))<VAR>x✝ : Set (π' (f a))<GOAL>Sigma.mk a '' (g a ⁻¹' id x✝) = Sigma.map f g ⁻¹' (Sigma.mk (f a) '' id x✝)
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>s : Set Gᵐᵒᵖ<GOAL>(closure s).unop = closure (MulOpposite.op ⁻¹' s)
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>s : Set Gᵐᵒᵖ<GOAL>sInf {a | s ⊆ MulOpposite.unop ⁻¹' ↑a} = sInf {K | MulOpposite.op ⁻¹' s ⊆ ↑K}
<VAR>ι : Sort u_1<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>s : Set Gᵐᵒᵖ<VAR>a : Subgroup G<GOAL>a ∈ {a | s ⊆ MulOpposite.unop ⁻¹' ↑a} ↔ a ∈ {K | MulOpposite.op ⁻¹' s ⊆ ↑K}
<VAR>R : Type u_1<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p q : F[X]<VAR>f g : RatFunc F<VAR>r : F<GOAL>↑(r • f) = r • ↑f