ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : TopCat<VAR>Y : Opens ↑X<VAR>R : Presieve Y<GOAL>presieveOfCoveringAux (coveringOfPresieve Y R) Y = R
<VAR>X : TopCat<VAR>Y : Opens ↑X<VAR>R : Presieve Y<VAR>Z : Opens ↑X<GOAL>presieveOfCoveringAux (coveringOfPresieve Y R) Y = R
<VAR>X : TopCat<VAR>Y : Opens ↑X<VAR>R : Presieve Y<VAR>Z : Opens ↑X<VAR>f : Z ⟶ Y<GOAL>f ∈ presieveOfCoveringAux (coveringOfPresieve Y R) Y ↔ f ∈ R
<VAR>a : ℤ<VAR>m n : ℕ<GOAL>a.gcd (↑m * ↑n) ≠ 1 ↔ a.gcd ↑m ≠ 1 ∨ a.gcd ↑n ≠ 1
<VAR>A : Type u_1<VAR>B✝ : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Ring B✝<VAR>inst✝⁴ : Algebra A B✝<VAR>x✝ : B✝<VAR>inst✝³ : Nontrivial B✝<VAR>B : Type u_4<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Nontrivial B<VAR>S : Subalgebra A B<VAR>x : B<VAR>int : IsIntegral (↥S) x<GOAL>2 ≤ (minpoly (↥S) x).natDegree ↔ x ∉ S
<VAR>A : Type u_1<VAR>B✝ : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Ring B✝<VAR>inst✝⁴ : Algebra A B✝<VAR>x✝ : B✝<VAR>inst✝³ : Nontrivial B✝<VAR>B : Type u_4<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Nontrivial B<VAR>S : Subalgebra A B<VAR>x : B<VAR>int : IsIntegral (↥S) x<GOAL>x ∈ (algebraMap (↥S) B).range ↔ x ∈ S
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝² : Category.{v'', u''} D<VAR>X Y : C<VAR>inst✝¹ : FinitaryExtensive C<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>F : Discrete ι ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<GOAL>IsVanKampenColimit c
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝² : Category.{v'', u''} D<VAR>X Y : C<VAR>inst✝¹ : FinitaryExtensive C<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>F : Discrete ι ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>n : ℕ<VAR>e : ι ≃ Fin n<GOAL>IsVanKampenColimit c
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝² : Category.{v'', u''} D<VAR>X Y : C<VAR>inst✝¹ : FinitaryExtensive C<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>F : Discrete ι ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>n : ℕ<VAR>e : ι ≃ Fin n<GOAL>IsVanKampenColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝² : Category.{v'', u''} D<VAR>X Y : C<VAR>inst✝¹ : FinitaryExtensive C<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>F : Discrete ι ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>n : ℕ<VAR>e : ι ≃ Fin n<GOAL>IsColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a✝ o✝ : Ordinal.{u}<VAR>f✝ : (b : Ordinal.{u}) → b < o✝ → Ordinal.{u}<VAR>a o o' : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<VAR>g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}<VAR>hg : o.IsFundamentalSequence o' g<VAR>i : Ordinal.{u}<VAR>hi : i < o'<GOAL>g i hi < o
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a✝ o✝ : Ordinal.{u}<VAR>f✝ : (b : Ordinal.{u}) → b < o✝ → Ordinal.{u}<VAR>a o o' : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<VAR>g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}<VAR>hg : o.IsFundamentalSequence o' g<VAR>i : Ordinal.{u}<VAR>hi : i < o'<GOAL>g i hi < o'.blsub g
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a✝ o✝ : Ordinal.{u}<VAR>f✝ : (b : Ordinal.{u}) → b < o✝ → Ordinal.{u}<VAR>a o o' : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<VAR>g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}<VAR>hg : o.IsFundamentalSequence o' g<GOAL>a.IsFundamentalSequence o' fun i hi => f (g i hi) ⋯
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a✝ o✝ : Ordinal.{u}<VAR>f✝ : (b : Ordinal.{u}) → b < o✝ → Ordinal.{u}<VAR>a o o' : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<VAR>g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}<VAR>hg : o.IsFundamentalSequence o' g<GOAL>o' ≤ a.cof.ord
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a✝ o✝ : Ordinal.{u}<VAR>f✝ : (b : Ordinal.{u}) → b < o✝ → Ordinal.{u}<VAR>a o o' : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<VAR>g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}<VAR>hg : o.IsFundamentalSequence o' g<GOAL>(o'.blsub fun i hi => f (g i hi) ⋯) = a
<VAR>n : ℕ<VAR>α : Type u_1<VAR>L : List (List α)<VAR>c : Composition L.join.length<VAR>h : map length L = c.blocks<GOAL>L.join.splitWrtComposition c = L
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoMod hp (-a) b = p - toIocMod hp a (-b)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d x y z : P<VAR>r R : ℝ<VAR>hx : x ≠ c<VAR>hy : y ≠ c<GOAL>dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d x y z : P<VAR>r : ℝ<VAR>hx : x ≠ c<VAR>hy : y ≠ c<GOAL>dist (inversion c 0 x) y * dist x c = dist x (inversion c 0 y) * dist y c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d x y z : P<VAR>r R : ℝ<VAR>hx : x ≠ c<VAR>hy : y ≠ c<VAR>hR : R ≠ 0<GOAL>dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d x y z : P<VAR>r R : ℝ<VAR>hx : x ≠ c<VAR>hy : y ≠ c<VAR>hR : R ≠ 0<VAR>hy' : inversion c R y ≠ c<GOAL>dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d x y z : P<VAR>r R : ℝ<VAR>hx : x ≠ c<VAR>hy : y ≠ c<VAR>hR : R ≠ 0<VAR>hy' : inversion c R y ≠ c<GOAL>dist (inversion c R x) (inversion c R (inversion c R y)) * dist x c = dist x (inversion c R y) * dist y c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d x y z : P<VAR>r R : ℝ<VAR>hx : x ≠ c<VAR>hy : y ≠ c<VAR>hR : R ≠ 0<VAR>hy' : inversion c R y ≠ c<GOAL>R ^ 2 / (dist x c * (R ^ 2 / dist y c)) * dist x (inversion c R y) * dist x c = dist x (inversion c R y) * dist y c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d x y z : P<VAR>r R : ℝ<VAR>hx : x ≠ c<VAR>hy : y ≠ c<VAR>hR : R ≠ 0<VAR>hy' : inversion c R y ≠ c<VAR>this : dist x c ≠ 0<GOAL>R ^ 2 / (dist x c * (R ^ 2 / dist y c)) * dist x (inversion c R y) * dist x c = dist x (inversion c R y) * dist y c
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f✝ : ι✝ → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>ι : Type u_3<VAR>f : ι → α<VAR>hf : InjOn f {i | f i ≠ ⊥}<GOAL>Independent f ↔ ∀ (s : Finset ι), s.SupIndep f
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f✝ : ι✝ → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>ι : Type u_3<VAR>f : ι → α<VAR>hf : InjOn f {i | f i ≠ ⊥}<VAR>h : ∀ (s : Finset ι), s.SupIndep f<VAR>i : ι<GOAL>Disjoint (f i) (sSup (f '' {j | j ≠ i}))
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f✝ : ι✝ → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>ι : Type u_3<VAR>f : ι → α<VAR>hf : InjOn f {i | f i ≠ ⊥}<VAR>h : ∀ (s : Finset ι), s.SupIndep f<VAR>i : ι<GOAL>∀ (i_1 : Finset α), ↑i_1 ⊆ f '' {j | j ≠ i} → Disjoint (f i) (i_1.sup id)
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f✝ : ι✝ → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s✝ : Set α<VAR>ι : Type u_3<VAR>f : ι → α<VAR>hf : InjOn f {i | f i ≠ ⊥}<VAR>h : ∀ (s : Finset ι), s.SupIndep f<VAR>i : ι<VAR>s : Finset α<VAR>hs : ↑s ⊆ f '' {j | j ≠ i}<GOAL>Disjoint (f i) (s.sup id)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : HasBinaryCoproducts C<VAR>X Y Z : C<GOAL>(α_ X Y Z).hom ≫ (coprod.braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (coprod.braiding X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (coprod.braiding X Z).hom
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : HasBinaryCoproducts C<VAR>X Y Z : C<GOAL>coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) ≫ coprod.desc coprod.inr coprod.inl ≫ coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) = coprod.map (coprod.desc coprod.inr coprod.inl) (𝟙 Z) ≫ coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) ≫ coprod.map (𝟙 Y) (coprod.desc coprod.inr coprod.inl)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : HasBinaryCoproducts C<VAR>X Y Z : C<GOAL>(α_ X Y Z).inv ≫ (coprod.braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (coprod.braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (coprod.braiding X Z).hom ▷ Y
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : HasBinaryCoproducts C<VAR>X Y Z : C<GOAL>coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) ≫ coprod.desc coprod.inr coprod.inl ≫ coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) = coprod.map (𝟙 X) (coprod.desc coprod.inr coprod.inl) ≫ coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) ≫ coprod.map (coprod.desc coprod.inr coprod.inl) (𝟙 Y)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>ho : OrthocentricSystem s<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<GOAL>affineSpan ℝ (Set.range p) = affineSpan ℝ s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>ho : OrthocentricSystem s<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>ha : AffineIndependent ℝ p<GOAL>affineSpan ℝ (Set.range p) = affineSpan ℝ s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>ha : AffineIndependent ℝ p<VAR>t : Triangle ℝ P<VAR>left✝ : t.orthocenter ∉ Set.range t.points<VAR>hts : s = insert t.orthocenter (Set.range t.points)<GOAL>affineSpan ℝ (Set.range p) = affineSpan ℝ s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>ha : AffineIndependent ℝ p<VAR>t : Triangle ℝ P<VAR>left✝ : t.orthocenter ∉ Set.range t.points<VAR>hts : s = insert t.orthocenter (Set.range t.points)<VAR>hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points)<GOAL>affineSpan ℝ (Set.range p) = affineSpan ℝ s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>ha : AffineIndependent ℝ p<VAR>t : Triangle ℝ P<VAR>left✝ : t.orthocenter ∉ Set.range t.points<VAR>hts : s = insert t.orthocenter (Set.range t.points)<VAR>hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points)<GOAL>(affineSpan ℝ (Set.range p)).direction = (affineSpan ℝ s).direction
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>ha : AffineIndependent ℝ p<VAR>t : Triangle ℝ P<VAR>left✝ : t.orthocenter ∉ Set.range t.points<VAR>hts : s = insert t.orthocenter (Set.range t.points)<VAR>hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points)<VAR>hfd this : FiniteDimensional ℝ ↥(affineSpan ℝ s).direction<GOAL>(affineSpan ℝ (Set.range p)).direction = (affineSpan ℝ s).direction
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<VAR>ha : AffineIndependent ℝ p<VAR>t : Triangle ℝ P<VAR>left✝ : t.orthocenter ∉ Set.range t.points<VAR>hts : s = insert t.orthocenter (Set.range t.points)<VAR>hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points)<VAR>hfd this : FiniteDimensional ℝ ↥(affineSpan ℝ s).direction<GOAL>finrank ℝ ↥(affineSpan ℝ (Set.range p)).direction = finrank ℝ ↥(affineSpan ℝ s).direction
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>inst✝ : IsWellOrder β s<VAR>f : r ≼i s<VAR>h : ¬∃ b, ∀ (x : β), s x b ↔ ∃ y, f y = x<VAR>b x : β<VAR>x✝¹ : ∀ (y : β), s y x → Acc s y<VAR>IH : ∀ (y : β), s y x → ∃ a, f a = y<VAR>hn : ∀ (x_1 : α), ¬f x_1 = x<VAR>y : β<VAR>x✝ : ∃ y_1, f y_1 = y<VAR>a : α<VAR>e : f a = y<GOAL>s (f a) x
<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]<GOAL>p ∈ RingHom.ker (Polynomial.aeval s).toRingHom ↔ p ∈ Ideal.span {minpoly R s}
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : R⟦X⟧<VAR>n : ℕ<GOAL>(coeff R n) (f * g).derivativeFun = (coeff R n) (f • g.derivativeFun + g • f.derivativeFun)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : R⟦X⟧<VAR>n : ℕ<VAR>h₁ : n < n + 1<GOAL>(coeff R n) (f * g).derivativeFun = (coeff R n) (f • g.derivativeFun + g • f.derivativeFun)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : R⟦X⟧<VAR>n : ℕ<VAR>h₁ : n < n + 1<VAR>h₂ : n < n + 1 + 1<GOAL>(coeff R n) (f * g).derivativeFun = (coeff R n) (f • g.derivativeFun + g • f.derivativeFun)
<VAR>R : Type u<VAR>inst✝¹⁰ : Ring R<VAR>ι : Type v<VAR>inst✝⁹ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁸ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁷ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁶ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝³ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝² : (i : ι) → (k : G i) → Decidable (k ≠ 0)<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>x : DirectSum ι G<VAR>H : Submodule.Quotient.mk x = 0<VAR>ind i j : ι<VAR>hij : i ≤ j<VAR>y : G i<VAR>k : ι<VAR>hik : i ≤ k<VAR>hjk : j ≤ k<VAR>x✝ : (DirectSum.lof R ι G i) y - (DirectSum.lof R ι G j) ((f i j hij) y) ∈ {a | ∃ i j, ∃ (H : i ≤ j), ∃ x, (DirectSum.lof R ι G i) x - (DirectSum.lof R ι G j) ((f i j H) x) = a}<GOAL>(DirectSum.toModule R ι (G k) fun i => totalize G f i k) ((DirectSum.lof R ι G i) y - (DirectSum.lof R ι G j) ((f i j hij) y)) = 0
<VAR>R : Type u<VAR>inst✝¹⁰ : Ring R<VAR>ι : Type v<VAR>inst✝⁹ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁸ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁷ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁶ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝³ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝² : (i : ι) → (k : G i) → Decidable (k ≠ 0)<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>x✝² : DirectSum ι G<VAR>H : Submodule.Quotient.mk x✝² = 0<VAR>ind : ι<VAR>x y : DirectSum ι G<VAR>x✝¹ : ∃ j, (∀ k ∈ DFinsupp.support x, k ≤ j) ∧ (DirectSum.toModule R ι (G j) fun i => totalize G f i j) x = 0<VAR>x✝ : ∃ j, (∀ k ∈ DFinsupp.support y, k ≤ j) ∧ (DirectSum.toModule R ι (G j) fun i => totalize G f i j) y = 0<VAR>i : ι<VAR>hi : ∀ k ∈ DFinsupp.support x, k ≤ i<VAR>hxi : (DirectSum.toModule R ι (G i) fun i_1 => totalize G f i_1 i) x = 0<VAR>j : ι<VAR>hj : ∀ k ∈ DFinsupp.support y, k ≤ j<VAR>hyj : (DirectSum.toModule R ι (G j) fun i => totalize G f i j) y = 0<VAR>k : ι<VAR>hik : i ≤ k<VAR>hjk : j ≤ k<GOAL>(DirectSum.toModule R ι (G k) fun i => totalize G f i k) (x + y) = 0
<VAR>R : Type u<VAR>inst✝¹⁰ : Ring R<VAR>ι : Type v<VAR>inst✝⁹ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁸ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁷ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁶ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝³ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝² : (i : ι) → (k : G i) → Decidable (k ≠ 0)<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>x✝² : DirectSum ι G<VAR>H : Submodule.Quotient.mk x✝² = 0<VAR>ind : ι<VAR>x y : DirectSum ι G<VAR>x✝¹ : ∃ j, (∀ k ∈ DFinsupp.support x, k ≤ j) ∧ (DirectSum.toModule R ι (G j) fun i => totalize G f i j) x = 0<VAR>x✝ : ∃ j, (∀ k ∈ DFinsupp.support y, k ≤ j) ∧ (DirectSum.toModule R ι (G j) fun i => totalize G f i j) y = 0<VAR>i : ι<VAR>hi : ∀ k ∈ DFinsupp.support x, k ≤ i<VAR>hxi : (DirectSum.toModule R ι (G i) fun i_1 => totalize G f i_1 i) x = 0<VAR>j : ι<VAR>hj : ∀ k ∈ DFinsupp.support y, k ≤ j<VAR>hyj : (DirectSum.toModule R ι (G j) fun i => totalize G f i j) y = 0<VAR>k : ι<VAR>hik : i ≤ k<VAR>hjk : j ≤ k<GOAL>(DirectSum.toModule R ι (G k) fun i => totalize G f i k) x + (DirectSum.toModule R ι (G k) fun i => totalize G f i k) y = 0
<VAR>R : Type u<VAR>inst✝¹⁰ : Ring R<VAR>ι : Type v<VAR>inst✝⁹ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁸ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁷ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁶ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝³ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝² : (i : ι) → (k : G i) → Decidable (k ≠ 0)<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>x✝² : DirectSum ι G<VAR>H : Submodule.Quotient.mk x✝² = 0<VAR>ind : ι<VAR>x y : DirectSum ι G<VAR>x✝¹ : ∃ j, (∀ k ∈ DFinsupp.support x, k ≤ j) ∧ (DirectSum.toModule R ι (G j) fun i => totalize G f i j) x = 0<VAR>x✝ : ∃ j, (∀ k ∈ DFinsupp.support y, k ≤ j) ∧ (DirectSum.toModule R ι (G j) fun i => totalize G f i j) y = 0<VAR>i : ι<VAR>hi : ∀ k ∈ DFinsupp.support x, k ≤ i<VAR>hxi : (DirectSum.toModule R ι (G i) fun i_1 => totalize G f i_1 i) x = 0<VAR>j : ι<VAR>hj : ∀ k ∈ DFinsupp.support y, k ≤ j<VAR>hyj : (DirectSum.toModule R ι (G j) fun i => totalize G f i j) y = 0<VAR>k : ι<VAR>hik : i ≤ k<VAR>hjk : j ≤ k<GOAL>(f i k hik) ((DirectSum.toModule R ι (G i) fun k => totalize G f k i) x) + (f j k hjk) ((DirectSum.toModule R ι (G j) fun k => totalize G f k j) y) = 0
<VAR>R : Type u<VAR>inst✝¹⁰ : Ring R<VAR>ι : Type v<VAR>inst✝⁹ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁸ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁷ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁶ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝³ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝² : (i : ι) → (k : G i) → Decidable (k ≠ 0)<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>x✝¹ : DirectSum ι G<VAR>H : Submodule.Quotient.mk x✝¹ = 0<VAR>ind : ι<VAR>a : R<VAR>x : DirectSum ι G<VAR>x✝ : ∃ j, (∀ k ∈ DFinsupp.support x, k ≤ j) ∧ (DirectSum.toModule R ι (G j) fun i => totalize G f i j) x = 0<VAR>i : ι<VAR>hi : ∀ k ∈ DFinsupp.support x, k ≤ i<VAR>hxi : (DirectSum.toModule R ι (G i) fun i_1 => totalize G f i_1 i) x = 0<GOAL>(DirectSum.toModule R ι (G i) fun i_1 => totalize G f i_1 i) (a • x) = 0
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeInf α✝<VAR>a b c d : α✝<VAR>α : Type u_1<VAR>A B : SemilatticeInf α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>A = B
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeInf α✝<VAR>a b c d : α✝<VAR>α : Type u_1<VAR>A B : SemilatticeInf α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<VAR>ss : toInf = toInf<GOAL>A = B
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeInf α✝<VAR>a b c d : α✝<VAR>α : Type u_1<VAR>toInf✝¹ : Inf α<VAR>toPartialOrder✝¹ : PartialOrder α<VAR>inf_le_left✝¹ : ∀ (a b : α), a ⊓ b ≤ a<VAR>inf_le_right✝¹ : ∀ (a b : α), a ⊓ b ≤ b<VAR>le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c<VAR>toInf✝ : Inf α<VAR>toPartialOrder✝ : PartialOrder α<VAR>inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a<VAR>inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b<VAR>le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<VAR>ss : toInf = toInf<GOAL>mk inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf_le_left✝ inf_le_right✝ le_inf✝
<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeInf α✝<VAR>a b c d : α✝<VAR>α : Type u_1<VAR>toInf✝¹ : Inf α<VAR>toPartialOrder✝ : PartialOrder α<VAR>inf_le_left✝¹ : ∀ (a b : α), a ⊓ b ≤ a<VAR>inf_le_right✝¹ : ∀ (a b : α), a ⊓ b ≤ b<VAR>le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c<VAR>toInf✝ : Inf α<VAR>inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a<VAR>inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b<VAR>le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<VAR>ss : toInf = toInf<GOAL>mk inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf_le_left✝ inf_le_right✝ le_inf✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : Ring α<VAR>inst✝ : Ring β<VAR>h : Antiperiodic f c<VAR>n : ℤ<GOAL>f (x + ↑n * c) = ↑↑n.negOnePow * f x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>h e f : L<VAR>t : IsSl2Triple h e f<GOAL>⁅h, e⁆ = 2 • e
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp : (↑#ι - 1) * p ≤ 1<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Antitone fun s => T μ p (∫⋯∫⁻_sᶜ, f ∂μ) s
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp : (↑#ι - 1) * p ≤ 1<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∀ (s : Finset ι) ⦃a : ι⦄, a ∉ s → T μ p (∫⋯∫⁻_(insert a s)ᶜ, f ∂μ) (insert a s) ≤ T μ p (∫⋯∫⁻_sᶜ, f ∂μ) s
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp : (↑#ι - 1) * p ≤ 1<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∉ s<GOAL>T μ p (∫⋯∫⁻_(insert i s)ᶜ, f ∂μ) (insert i s) ≤ T μ p (∫⋯∫⁻_sᶜ, f ∂μ) s