ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hβ : β.IsNonZero<VAR>hα : ¬α.IsZero<VAR>h : ⇑β = -1 • ⇑α<GOAL>β = -α ∨ β = α
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hβ : β.IsNonZero<VAR>hα : ¬α.IsZero<VAR>h : ⇑β = 0 • ⇑α<GOAL>β = -α ∨ β = α
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hβ : β.IsNonZero<VAR>hα : ¬α.IsZero<VAR>h : ⇑β = 1 • ⇑α<GOAL>β = -α ∨ β = α
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>inst✝² : Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>inst✝¹ : Category.{v₄, u₄} E<VAR>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>X✝ Y✝ : C × D ⥤ E<VAR>T : X✝ ⟶ Y✝<VAR>X : C<VAR>Y Y' : D<VAR>g : Y ⟶ Y'<GOAL>X✝.map (𝟙 X, g) ≫ T.app (X, Y') = T.app (X, Y) ≫ Y✝.map (𝟙 X, g)
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<VAR>C : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>inst✝² : Category.{v₃, u₃} D<VAR>E : Type u₄<VAR>inst✝¹ : Category.{v₄, u₄} E<VAR>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>X✝ Y✝ : C × D ⥤ E<VAR>T : X✝ ⟶ Y✝<VAR>X X' : C<VAR>f : X ⟶ X'<VAR>x✝ : D<GOAL>X✝.map (f, 𝟙 x✝) ≫ T.app (X', x✝) = T.app (X, x✝) ≫ Y✝.map (f, 𝟙 x✝)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>t : Set (PrimeSpectrum R)<GOAL>zeroLocus ↑(vanishingIdeal t) = closure t
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>t : Set (PrimeSpectrum R)<VAR>I : Set R<VAR>hI : closure t = zeroLocus I<GOAL>zeroLocus ↑(vanishingIdeal t) = closure t
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>t : Set (PrimeSpectrum R)<VAR>I : Set R<VAR>hI : closure t = zeroLocus I<GOAL>t ⊆ closure t ∧ t ⊆ zeroLocus ↑(vanishingIdeal t)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : AddGroup R<VAR>inst✝ : Zero Γ<VAR>f : HahnSeries Γ R<VAR>hf : ¬f = 0<GOAL>(-f).order = f.order
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<VAR>h : Pairwise (Disjoint on fun i => (M i).E)<VAR>I : Set α<GOAL>(Matroid.disjointSigma M h).Indep I ↔ (∀ (i : ι), (M i).Indep (I ∩ (M i).E)) ∧ I ⊆ ⋃ i, (M i).E
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>j : J<GOAL>c.ι.app j ≫ t.desc (newCocone D c) ≫ T.ε.app c.pt = c.ι.app j ≫ 𝟙 c.pt
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>j : J<GOAL>(D.obj j).a ≫ T.ε.app (D.obj j).A ≫ c.ι.app j = c.ι.app j
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>j : J<GOAL>c.ι.app j ≫ t.desc (newCocone D c) ≫ T.δ.app c.pt = c.ι.app j ≫ t.desc (newCocone D c) ≫ T.map (t.desc (newCocone D c))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>j : J<GOAL>(D.obj j).a ≫ T.δ.app (D.obj j).A ≫ T.map (T.map (c.ι.app j)) = (D.obj j).a ≫ T.map (c.ι.app j) ≫ T.map (t.desc (newCocone D c))
<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>f : α → ℝ<VAR>hf : Integrable f μ<VAR>c : ℝ<VAR>c_neg : c < 0<GOAL>μ {a | f a ≤ c} < ⊤
<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>f : α → ℝ<VAR>hf : Integrable f μ<VAR>c : ℝ<VAR>c_neg : c < 0<GOAL>{a | f a ≤ c} ⊆ {x | -c ≤ ‖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>f : α → ℝ<VAR>hf : Integrable f μ<VAR>c : ℝ<VAR>c_neg : c < 0<VAR>x : α<VAR>hx : x ∈ {a | f a ≤ c}<GOAL>x ∈ {x | -c ≤ ‖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>f : α → ℝ<VAR>hf : Integrable f μ<VAR>c : ℝ<VAR>c_neg : c < 0<VAR>x : α<VAR>hx : f x ≤ c<GOAL>-c ≤ |f x|
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>symmetric : ∀ x ∈ s, -x ∈ s<VAR>x : E<VAR>this : ∀ (x : E), -x ∈ s ↔ x ∈ s<GOAL>gauge s (-x) = gauge s x
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝¹ : CommSemiring α<VAR>I : Ideal α<VAR>inst✝ : IsDomain α<VAR>b₁ b₂ : α<VAR>h₁ : b₁ ≠ 0<VAR>h₂ : ¬IsUnit b₂<VAR>h : span {b₁} ≤ span {b₁ * b₂}<GOAL>b₁ * b₂ ∣ b₁ * 1
<VAR>a : ℝ<GOAL>interior {z | a ≤ z.re} = {z | a < z.re}
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<GOAL>n.totient ≤ (minpoly ℤ μ).natDegree
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K' : ChainComplex C ℕ<VAR>f : K✝ ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<VAR>j : Fin (n + 1)<VAR>a✝ : n + 1 ≤ ↑j + (n + 1)<GOAL>((Γ₀.splitting K).cofan (op [n + 1])).inj (Splitting.IndexSet.id (op [n + 1])) ≫ (Γ₀.obj K).δ j.succ = 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K' : ChainComplex C ℕ<VAR>f : K✝ ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<VAR>j : Fin (n + 1)<VAR>a✝ : n + 1 ≤ ↑j + (n + 1)<VAR>eq : ((Γ₀.splitting K).cofan (op [n + 1])).inj (Splitting.IndexSet.id (op [n + 1])) ≫ (Γ₀.obj K).map (SimplexCategory.δ j.succ).op = Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫ ((Γ₀.splitting K).cofan (op [n])).inj (Splitting.IndexSet.id (op [n]))<GOAL>((Γ₀.splitting K).cofan (op [n + 1])).inj (Splitting.IndexSet.id (op [n + 1])) ≫ (Γ₀.obj K).δ j.succ = 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K' : ChainComplex C ℕ<VAR>f : K✝ ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<VAR>j : Fin (n + 1)<VAR>a✝ : n + 1 ≤ ↑j + (n + 1)<VAR>eq : ((Γ₀.splitting K).cofan (op [n + 1])).inj (Splitting.IndexSet.id (op [n + 1])) ≫ (Γ₀.obj K).map (SimplexCategory.δ j.succ).op = 0<GOAL>((Γ₀.splitting K).cofan (op [n + 1])).inj (Splitting.IndexSet.id (op [n + 1])) ≫ (Γ₀.obj K).δ j.succ = 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K' : ChainComplex C ℕ<VAR>f : K✝ ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<VAR>j : Fin (n + 1)<VAR>a✝ : n + 1 ≤ ↑j + (n + 1)<VAR>eq : ((Γ₀.splitting K).cofan (op [n + 1])).inj (Splitting.IndexSet.id (op [n + 1])) ≫ (Γ₀.obj K).map (SimplexCategory.δ j.succ).op = Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫ ((Γ₀.splitting K).cofan (op [n])).inj (Splitting.IndexSet.id (op [n]))<GOAL>[n + 1] ≠ [n]
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K' : ChainComplex C ℕ<VAR>f : K✝ ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<VAR>j : Fin (n + 1)<VAR>a✝ : n + 1 ≤ ↑j + (n + 1)<VAR>eq : ((Γ₀.splitting K).cofan (op [n + 1])).inj (Splitting.IndexSet.id (op [n + 1])) ≫ (Γ₀.obj K).map (SimplexCategory.δ j.succ).op = Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫ ((Γ₀.splitting K).cofan (op [n])).inj (Splitting.IndexSet.id (op [n]))<GOAL>¬Isδ₀ (SimplexCategory.δ j.succ)
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommSemiring R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝⁶ : CommSemiring S✝<VAR>inst✝⁵ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S✝<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>r : R<VAR>hr : IsUnit r<VAR>H : Function.Bijective ⇑(algebraMap R S)<VAR>n : ℕ<GOAL>IsUnit ((algebraMap R S) ↑⟨(fun x => r ^ x) n, ⋯⟩)
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommSemiring R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝⁶ : CommSemiring S✝<VAR>inst✝⁵ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S✝<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>r : R<VAR>hr : IsUnit r<VAR>H : Function.Bijective ⇑(algebraMap R S)<VAR>z : S<GOAL>∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommSemiring R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝⁶ : CommSemiring S✝<VAR>inst✝⁵ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S✝<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>r : R<VAR>hr : IsUnit r<VAR>H : Function.Bijective ⇑(algebraMap R S)<VAR>z' : R<GOAL>∃ x, (algebraMap R S) z' * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommSemiring R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝⁶ : CommSemiring S✝<VAR>inst✝⁵ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S✝<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>r : R<VAR>hr : IsUnit r<VAR>H : Function.Bijective ⇑(algebraMap R S)<VAR>x y : R<GOAL>(algebraMap R S) x = (algebraMap R S) y → ∃ c, ↑c * x = ↑c * y
<VAR>R✝ : Type u_1<VAR>inst✝⁷ : CommSemiring R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝⁶ : CommSemiring S✝<VAR>inst✝⁵ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S✝<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>r : R<VAR>hr : IsUnit r<VAR>H : Function.Bijective ⇑(algebraMap R S)<VAR>x y : R<GOAL>x = y → ∃ c, ↑c * x = ↑c * y
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>s t : Set α<VAR>r : ℝ<VAR>c : α<GOAL>(cobounded α).HasBasis (fun x => True) fun i => (fun x => dist x c) ⁻¹' Ici i
<VAR>b : Ordinal.{0}<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<VAR>h₁ : (e.oadd n a).NFBelow b<VAR>h₂ : o.NFBelow b<GOAL>(e.oadd n a + o).NFBelow b
<VAR>b : Ordinal.{0}<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<VAR>h₁ : (e.oadd n a).NFBelow b<VAR>h₂ : o.NFBelow b<VAR>h' : (a + o).NFBelow b<GOAL>(e.oadd n a + o).NFBelow b
<VAR>b : Ordinal.{0}<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<VAR>h₁ : (e.oadd n a).NFBelow b<VAR>h₂ : o.NFBelow b<VAR>h' : (a + o).NFBelow b<GOAL>(e.addAux n (a + o)).NFBelow b
<VAR>b : Ordinal.{0}<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<VAR>h₁ : (e.oadd n a).NFBelow b<VAR>h₂ : o.NFBelow b<VAR>e' : ONote<VAR>n' : ℕ+<VAR>a' : ONote<VAR>h' : (e'.oadd n' a').NFBelow b<GOAL>(e.addAux n (e'.oadd n' a')).NFBelow b
<VAR>b : Ordinal.{0}<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<VAR>h₁ : (e.oadd n a).NFBelow b<VAR>h₂ : o.NFBelow b<VAR>e' : ONote<VAR>n' : ℕ+<VAR>a' : ONote<VAR>h' : (e'.oadd n' a').NFBelow b<VAR>this : (e.cmp e').Compares e e'<GOAL>(e.addAux n (e'.oadd n' a')).NFBelow b
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>z : ℤ_[p]<VAR>hev : Polynomial.eval z F = 0<VAR>hnlt : ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<GOAL>‖z - soln‖ = ‖z - a + (a - soln)‖
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>z : ℤ_[p]<VAR>hev : Polynomial.eval z F = 0<VAR>hnlt : ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>h : ℤ_[p] := z - soln<VAR>q : ℤ_[p]<VAR>hq : Polynomial.eval (soln + h) F = Polynomial.eval soln F + Polynomial.eval soln (Polynomial.derivative F) * h + q * h ^ 2<GOAL>Polynomial.eval (soln + h) F = Polynomial.eval soln (Polynomial.derivative F) * h + q * h ^ 2
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>z : ℤ_[p]<VAR>hev : Polynomial.eval z F = 0<VAR>hnlt : ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>h : ℤ_[p] := z - soln<VAR>q : ℤ_[p]<VAR>hq : Polynomial.eval (soln + h) F = Polynomial.eval soln F + Polynomial.eval soln (Polynomial.derivative F) * h + q * h ^ 2<GOAL>Polynomial.eval soln (Polynomial.derivative F) * h + q * h ^ 2 = (Polynomial.eval soln (Polynomial.derivative F) + q * h) * h
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>z : ℤ_[p]<VAR>hev : Polynomial.eval z F = 0<VAR>hnlt : ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>h : ℤ_[p] := z - soln<VAR>q : ℤ_[p]<VAR>hq : Polynomial.eval (soln + h) F = Polynomial.eval soln F + Polynomial.eval soln (Polynomial.derivative F) * h + q * h ^ 2<VAR>this✝ : (Polynomial.eval soln (Polynomial.derivative F) + q * h) * h = 0<VAR>hne : ¬h = 0<VAR>this : Polynomial.eval soln (Polynomial.derivative F) + q * h = 0<GOAL>Polynomial.eval soln (Polynomial.derivative F) = -q * h
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>z : ℤ_[p]<VAR>hev : Polynomial.eval z F = 0<VAR>hnlt : ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>h : ℤ_[p] := z - soln<VAR>q : ℤ_[p]<VAR>hq : Polynomial.eval (soln + h) F = Polynomial.eval soln F + Polynomial.eval soln (Polynomial.derivative F) * h + q * h ^ 2<VAR>this✝¹ : (Polynomial.eval soln (Polynomial.derivative F) + q * h) * h = 0<VAR>hne : ¬h = 0<VAR>this✝ : Polynomial.eval soln (Polynomial.derivative F) + q * h = 0<VAR>this : Polynomial.eval soln (Polynomial.derivative F) = -q * h<GOAL>‖-q * h‖ ≤ 1 * ‖h‖
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>z : ℤ_[p]<VAR>hev : Polynomial.eval z F = 0<VAR>hnlt : ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>h : ℤ_[p] := z - soln<VAR>q : ℤ_[p]<VAR>hq : Polynomial.eval (soln + h) F = Polynomial.eval soln F + Polynomial.eval soln (Polynomial.derivative F) * h + q * h ^ 2<VAR>this✝¹ : (Polynomial.eval soln (Polynomial.derivative F) + q * h) * h = 0<VAR>hne : ¬h = 0<VAR>this✝ : Polynomial.eval soln (Polynomial.derivative F) + q * h = 0<VAR>this : Polynomial.eval soln (Polynomial.derivative F) = -q * h<GOAL>‖-q‖ * ‖h‖ ≤ 1 * ‖h‖
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>z : ℤ_[p]<VAR>hev : Polynomial.eval z F = 0<VAR>hnlt : ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>h : ℤ_[p] := z - soln<VAR>q : ℤ_[p]<VAR>hq : Polynomial.eval (soln + h) F = Polynomial.eval soln F + Polynomial.eval soln (Polynomial.derivative F) * h + q * h ^ 2<VAR>this✝¹ : (Polynomial.eval soln (Polynomial.derivative F) + q * h) * h = 0<VAR>hne : ¬h = 0<VAR>this✝ : Polynomial.eval soln (Polynomial.derivative F) + q * h = 0<VAR>this : Polynomial.eval soln (Polynomial.derivative F) = -q * h<GOAL>‖z - soln‖ < ‖Polynomial.eval soln (Polynomial.derivative F)‖
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>z : ℤ_[p]<VAR>hev : Polynomial.eval z F = 0<VAR>hnlt : ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>h : ℤ_[p] := z - soln<VAR>q : ℤ_[p]<VAR>hq : Polynomial.eval (soln + h) F = Polynomial.eval soln F + Polynomial.eval soln (Polynomial.derivative F) * h + q * h ^ 2<VAR>this✝¹ : (Polynomial.eval soln (Polynomial.derivative F) + q * h) * h = 0<VAR>hne : ¬h = 0<VAR>this✝ : Polynomial.eval soln (Polynomial.derivative F) + q * h = 0<VAR>this : Polynomial.eval soln (Polynomial.derivative F) = -q * h<GOAL>‖z - soln‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o a : Ordinal.{v}<VAR>e : o = succ a<GOAL>lift.{u, v} o.pred = (lift.{u, v} o).pred
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{v}<VAR>h : ¬∃ a, o = succ a<GOAL>lift.{u, v} o.pred = (lift.{u, v} o).pred
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c d a : α<VAR>n : ℕ<GOAL>a ^ (-Int.negSucc n) = (a ^ Int.negSucc n)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c d a : α<VAR>n : ℕ<GOAL>a ^ (-Int.negSucc n) = a ^ ↑(n + 1)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure S = ⊤<VAR>f : G → ↑R := fun g => toFun hR g<VAR>U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)<GOAL>↑(closure U) * R = ⊤
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure S = ⊤<VAR>f : G → ↑R := fun g => toFun hR g<VAR>U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)<VAR>g : G<VAR>x✝ : g ∈ ⊤<GOAL>g ∈ ↑(closure U) * R
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure S = ⊤<VAR>f : G → ↑R := fun g => toFun hR g<VAR>U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)<VAR>g : G<VAR>x✝ : g ∈ ⊤<GOAL>1 ∈ ↑(closure U) * R
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure S = ⊤<VAR>f : G → ↑R := fun g => toFun hR g<VAR>U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)<VAR>g : G<VAR>x✝ : g ∈ ⊤<GOAL>∀ x ∈ closure S, ∀ y ∈ S, x ∈ ↑(closure U) * R → x * y ∈ ↑(closure U) * R
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure S = ⊤<VAR>f : G → ↑R := fun g => toFun hR g<VAR>U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)<VAR>g : G<VAR>x✝ : g ∈ ⊤<GOAL>∀ x ∈ closure S, ∀ y ∈ S, x ∈ ↑(closure U) * R → x * y⁻¹ ∈ ↑(closure U) * R
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>W✝ X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : PullbackCone f g<VAR>W : C<VAR>k l : W ⟶ t.pt<VAR>h₀ : k ≫ t.fst = l ≫ t.fst<VAR>h₁ : k ≫ t.snd = l ≫ t.snd<GOAL>k ≫ t.π.app none = l ≫ t.π.app none
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁴ : Fintype l<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Unique ι<VAR>inst✝ : SeminormedAddCommGroup α<VAR>v : n → α<GOAL>↑(∑ i : n, ‖v i‖₊) = ∑ i : n, ‖v i‖
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>inst✝ : LinearOrder α✝<VAR>s✝ : Set α✝<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>f : ι → Set α<VAR>c : Set ι<VAR>hn : c.Nonempty<VAR>hc : DirectedOn (fun i j => f i ⊆ f j) c<VAR>s : Finset α<VAR>hs : ↑s ⊆ ⋃ i ∈ c, f i<GOAL>∃ i ∈ c, ↑s ⊆ f i
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>inst✝ : LinearOrder α✝<VAR>s✝ : Set α✝<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>f : ι → Set α<VAR>c : Set ι<VAR>hn : c.Nonempty<VAR>hc : DirectedOn (fun i j => f i ⊆ f j) c<VAR>s : Finset α<VAR>hs : ↑s ⊆ ⋃ x, f ↑x<GOAL>∃ i ∈ c, ↑s ⊆ f i
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>inst✝ : LinearOrder α✝<VAR>s✝ : Set α✝<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>f : ι → Set α<VAR>c : Set ι<VAR>hn : c.Nonempty<VAR>hc : DirectedOn (fun i j => f i ⊆ f j) c<VAR>s : Finset α<VAR>hs : ↑s ⊆ ⋃ x, f ↑x<VAR>this : Nonempty ↑c<GOAL>∃ i ∈ c, ↑s ⊆ f i
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : (a : α) → DecidableEq (N a)<VAR>inst✝ : (a : α) → AddGroup (N a)<VAR>f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a<GOAL>(f - g).neLocus f = g.support
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M₁<VAR>inst✝⁸ : Module R M₁<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : AddCommMonoid N₂<VAR>inst✝⁴ : Module R N₂<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂<VAR>i✝ : n<VAR>j✝ : m<GOAL>(toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m)) B i✝ j✝ = (toMatrix₂' R) B i✝ j✝
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r✝ r₁ r₂ r : ℝ<GOAL>↑‖r‖₊ = ENNReal.ofReal |r|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<GOAL>(∃ n, 0 < μ (s ∩ spanningSets μ n)) ↔ 0 < μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<GOAL>(¬∃ n, 0 < μ (s ∩ spanningSets μ n)) ↔ ¬0 < μ s