ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n✝ n : ℕ<GOAL>f n - ∑ i ∈ Finset.range n, μ[f (i + 1) - f i|↑ℱ i] = f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i|↑ℱ i])
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.snd (𝒰.map i ≫ f) g = pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.snd (𝒰.map i ≫ f) g
<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>h : NullMeasurableSet s μ<VAR>hs : μ s ≠ ⊤<GOAL>μ sᶜ = μ univ - μ s
<VAR>J : Type u'<VAR>inst✝² : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ PresheafedSpace C<VAR>inst✝ : HasColimit F<VAR>U : Opens ↑↑(colimit F)<VAR>j k : Jᵒᵖ<VAR>f : j ⟶ k<GOAL>(Opens.map (F.map f.unop).base).op.obj (op ((Opens.map (colimit.ι F (unop j)).base).obj U)) = op ((Opens.map (colimit.ι F (unop k)).base).obj U)
<VAR>J : Type u'<VAR>inst✝² : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ PresheafedSpace C<VAR>inst✝ : HasColimit F<VAR>U : Opens ↑↑(colimit F)<VAR>j k : Jᵒᵖ<VAR>f : j ⟶ k<GOAL>(Opens.map (F.map f.unop).base).op.obj (op ((Opens.map (colimit.ι F (unop j)).base).obj U)) = op ((Opens.map ((F.map f.unop).base ≫ (colimit.ι F (unop j)).base)).obj U)
<VAR>J : Type u'<VAR>inst✝² : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ PresheafedSpace C<VAR>inst✝ : HasColimit F<VAR>U : Opens ↑↑(colimit F)<VAR>i j k : Jᵒᵖ<VAR>f : i ⟶ j<VAR>g : j ⟶ k<GOAL>(F.map (g.unop ≫ f.unop)).c.app (op ((Opens.map (colimit.ι F (unop i)).base).obj U)) ≫ (F.obj (unop k)).presheaf.map (eqToHom ⋯) = ((F.map f.unop).c.app (op ((Opens.map (colimit.ι F (unop i)).base).obj U)) ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫ (F.map g.unop).c.app (op ((Opens.map (colimit.ι F (unop j)).base).obj U)) ≫ (F.obj (unop k)).presheaf.map (eqToHom ⋯)
<VAR>J : Type u'<VAR>inst✝² : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ PresheafedSpace C<VAR>inst✝ : HasColimit F<VAR>U : Opens ↑↑(colimit F)<VAR>i j k : Jᵒᵖ<VAR>f : i ⟶ j<VAR>g : j ⟶ k<GOAL>(F.map (g.unop ≫ f.unop)).c.app (op ((Opens.map (colimit.ι F (unop i)).base).obj U)) ≫ (F.obj (unop k)).presheaf.map (eqToHom ⋯) = (F.map f.unop).c.app (op ((Opens.map (colimit.ι F (unop i)).base).obj U)) ≫ (F.map g.unop).c.app (op ((Opens.map (F.map f.unop).base).obj ((Opens.map (colimit.ι F (unop i)).base).obj U))) ≫ ((pushforward C (F.map g.unop).base).obj (F.obj (unop k)).presheaf).map (eqToHom ⋯) ≫ (F.obj (unop k)).presheaf.map (eqToHom ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>x y : α<GOAL>cmp x x = eq
<VAR>m n : ℕ∞<VAR>hm : m ≠ ⊤<GOAL>¬IsMax m
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : D ⥤ C<VAR>Z : D<VAR>T : Presieve (F.obj Z)<VAR>x : FamilyOfElements P T<VAR>h : x.Compatible<VAR>Z₁ Z₂ W : D<VAR>g₁ : W ⟶ Z₁<VAR>g₂ : W ⟶ Z₂<VAR>f₁ : Z₁ ⟶ Z<VAR>f₂ : Z₂ ⟶ Z<VAR>h₁ : Presieve.functorPullback F T f₁<VAR>h₂ : Presieve.functorPullback F T f₂<VAR>eq : g₁ ≫ f₁ = g₂ ≫ f₂<GOAL>(F.op ⋙ P).map g₁.op (FamilyOfElements.functorPullback F x f₁ h₁) = (F.op ⋙ P).map g₂.op (FamilyOfElements.functorPullback F x f₂ h₂)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : IsWellOrder α fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : a < b<GOAL>(if h : ∃ y, a < y then ⋯.min {y | a < y} h else a) ≤ b
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : IsWellOrder α fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : a < b<GOAL>⋯.min {y | a < y} ⋯ ≤ b
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>B : Type u<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R B<VAR>I : Ideal B<VAR>C : Type u<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : FormallySmooth R A<VAR>f : A →ₐ[R] C<VAR>g : B →ₐ[R] C<VAR>hg : Function.Surjective ⇑g<VAR>hg' : IsNilpotent (RingHom.ker ↑g)<VAR>x : A<GOAL>g ((liftOfSurjective f g hg hg') x) = f x
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>B : Type u<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R B<VAR>I : Ideal B<VAR>C : Type u<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : FormallySmooth R A<VAR>f : A →ₐ[R] C<VAR>g : B →ₐ[R] C<VAR>hg : Function.Surjective ⇑g<VAR>hg' : IsNilpotent (RingHom.ker ↑g)<VAR>x : A<GOAL>(Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x)) = (Ideal.quotientKerAlgEquivOfSurjective hg).symm (f x)
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>B : Type u<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R B<VAR>I : Ideal B<VAR>C : Type u<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : FormallySmooth R A<VAR>f : A →ₐ[R] C<VAR>g : B →ₐ[R] C<VAR>hg : Function.Surjective ⇑g<VAR>hg' : IsNilpotent (RingHom.ker ↑g)<VAR>x : A<GOAL>(Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x)) = ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f) x
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>B : Type u<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R B<VAR>I : Ideal B<VAR>C : Type u<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : FormallySmooth R A<VAR>f : A →ₐ[R] C<VAR>g : B →ₐ[R] C<VAR>hg : Function.Surjective ⇑g<VAR>hg' : IsNilpotent (RingHom.ker ↑g)<VAR>x : A<GOAL>(Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x)) = (Ideal.Quotient.mk (RingHom.ker ↑g)) ((lift (RingHom.ker ↑g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f)) x)
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>B : Type u<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R B<VAR>I : Ideal B<VAR>C : Type u<VAR>inst✝² : CommRing C<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : FormallySmooth R A<VAR>f : A →ₐ[R] C<VAR>g : B →ₐ[R] C<VAR>hg : Function.Surjective ⇑g<VAR>hg' : IsNilpotent (RingHom.ker ↑g)<VAR>x : A<GOAL>(Ideal.quotientKerAlgEquivOfSurjective hg) ((Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x))) = (Ideal.quotientKerAlgEquivOfSurjective hg) ((Ideal.Quotient.mk (RingHom.ker ↑g)) ((lift (RingHom.ker ↑g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f)) x))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>inst✝¹ : Category.{?u.101120, u_3} E<VAR>inst✝ : IsIdempotentComplete D<VAR>F G : Karoubi C ⥤ D<VAR>τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G<VAR>P : Karoubi C<GOAL>(((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app P = F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>inst✝¹ : Category.{?u.101120, u_3} E<VAR>inst✝ : IsIdempotentComplete D<VAR>F G : Karoubi C ⥤ D<VAR>τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G<VAR>P : Karoubi C<GOAL>F.map P.decompId_i ≫ (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app { X := P.X, p := 𝟙 P.X, idem := ⋯ } ≫ G.map P.decompId_p = F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>inst✝¹ : Category.{?u.101120, u_3} E<VAR>inst✝ : IsIdempotentComplete D<VAR>F G : Karoubi C ⥤ D<VAR>τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G<VAR>P : Karoubi C<GOAL>(((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app { X := P.X, p := 𝟙 P.X, idem := ⋯ } = τ.app P.X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>inst✝¹ : Category.{?u.101120, u_3} E<VAR>inst✝ : IsIdempotentComplete D<VAR>F G : Karoubi C ⥤ D<VAR>τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G<VAR>P : Karoubi C<GOAL>(((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app { X := P.X, p := 𝟙 P.X, idem := ⋯ } = (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ)).app P.X
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<VAR>x : F<VAR>f : Polynomial ↥(subfield G F)<VAR>hf : Polynomial.eval₂ (subfield G F).subtype x f = 0<VAR>this : (subfield G F).subtype = (subfield G F).subtype<VAR>h : Polynomial.map (IsInvariantSubring.subtypeHom G (subfield G F).toSubring).toRingHom f = Polynomial.map (↑(IsInvariantSubring.subtypeHom G (subfield G F).toSubring)) f<GOAL>minpoly G F x ∣ f
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<VAR>x : F<VAR>f : Polynomial ↥(subfield G F)<VAR>hf : Polynomial.eval₂ (subfield G F).subtype x f = 0<VAR>this : (subfield G F).subtype = (subfield G F).subtype<VAR>h : Polynomial.map (IsInvariantSubring.subtypeHom G (subfield G F).toSubring).toRingHom f = Polynomial.map (↑(IsInvariantSubring.subtypeHom G (subfield G F).toSubring)) f<GOAL>∏ g : G ⧸ stabilizer G x, (Polynomial.X - Polynomial.C (ofQuotientStabilizer G x g)) ∣ Polynomial.map (subfield G F).subtype f
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<VAR>x : F<VAR>f : Polynomial ↥(subfield G F)<VAR>hf : Polynomial.eval₂ (subfield G F).subtype x f = 0<VAR>this : (subfield G F).subtype = (subfield G F).subtype<VAR>h : Polynomial.map (IsInvariantSubring.subtypeHom G (subfield G F).toSubring).toRingHom f = Polynomial.map (↑(IsInvariantSubring.subtypeHom G (subfield G F).toSubring)) f<VAR>y : G ⧸ stabilizer G x<VAR>g : G<GOAL>Polynomial.X - Polynomial.C (ofQuotientStabilizer G x ↑g) ∣ Polynomial.map (subfield G F).subtype f
<VAR>r n : ℕ<GOAL>(2 * n).choose (2 * n / 2) = (2 * n).choose n
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>C : ℝ<VAR>hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>LiouvilleWith p (-x)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>C : ℝ<VAR>hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>∀ (x_1 : ℕ), (∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) → ∃ m, -x ≠ ↑m / ↑x_1 ∧ |-x - ↑m / ↑x_1| < C / ↑x_1 ^ p
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>C : ℝ<VAR>hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>n : ℕ<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>∃ m, -x ≠ ↑m / ↑n ∧ |-x - ↑m / ↑n| < C / ↑n ^ p
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>C : ℝ<VAR>hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>n : ℕ<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>|-x - ↑(-m) / ↑n| < C / ↑n ^ p
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>C : ℝ<VAR>hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>n : ℕ<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>|-x - ↑(-m) / ↑n| = |x - ↑m / ↑n|
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>C : ℝ<VAR>hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>n : ℕ<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>|↑(-m) / ↑n - -x| = |x - ↑m / ↑n|
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>n k : ℕ<VAR>hkn : k ≤ n<GOAL>n.choose k • choose r n = choose r k * choose (r - ↑k) (n - k)
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>n k : ℕ<VAR>hkn : k ≤ n<GOAL>(fun x => n.factorial • x) (n.choose k • choose r n) = (fun x => n.factorial • x) (choose r k * choose (r - ↑k) (n - k))
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>n k : ℕ<VAR>hkn : k ≤ n<GOAL>n.factorial • n.choose k • choose r n = n.factorial • (choose r k * choose (r - ↑k) (n - k))
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>n k : ℕ<VAR>hkn : k ≤ n<GOAL>n.choose k • (descPochhammer ℤ n).smeval r = n.choose k • ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k))
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>n k : ℕ<VAR>hkn : k ≤ n<GOAL>n.choose k • (descPochhammer ℤ (n - k + k)).smeval r = n.choose k • ((descPochhammer ℤ k).smeval r * (descPochhammer ℤ (n - k)).smeval (r - ↑k))
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ x y p : R<VAR>h : p ∣ x - y<GOAL>p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * x ^ (n - 1)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>a b x✝ y✝ x y p : R<VAR>h : p ∣ x - y<GOAL>p ∣ y - x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : CompleteLattice α<VAR>S : Set α<VAR>c : α<GOAL>c ∈ Ici (sSup S) ↔ c ∈ ⨆ a ∈ S, Ici a
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f✝ : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>f : X ⟶ Z<GOAL>f ≫ 𝟙 Z = 𝟙 X ≫ f
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : Preorder α<VAR>a b c d : α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : PosMulMono α<VAR>H : 0 ≤ a<GOAL>0 ≤ a ^ 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : Preorder α<VAR>a b c d : α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : PosMulMono α<VAR>H : 0 ≤ a<GOAL>0 ≤ 1
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : Preorder α<VAR>a b c d : α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : PosMulMono α<VAR>H : 0 ≤ a<VAR>n : ℕ<GOAL>0 ≤ a ^ (n + 1)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : Preorder α<VAR>a b c d : α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : PosMulMono α<VAR>H : 0 ≤ a<VAR>n : ℕ<GOAL>0 ≤ a ^ n * a
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<GOAL>(t.centerMass w fun i => c • z i) = c • t.centerMass w z
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>F : C ⥤ C'<VAR>H : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F<VAR>i : D.J<GOAL>(fun i j => F.map (D.t i j)) i i = 𝟙 ((fun i => F.obj (D.V i)) (i, i))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>F : C ⥤ C'<VAR>H : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F<VAR>i j k : D.J<GOAL>(fun i j k => (PreservesPullback.iso F (D.f i j) (D.f i k)).inv ≫ F.map (D.t' i j k) ≫ (PreservesPullback.iso F (D.f j k) (D.f j i)).hom) i j k ≫ pullback.snd ((fun i j => F.map (D.f i j)) j k) ((fun i j => F.map (D.f i j)) j i) = pullback.fst ((fun i j => F.map (D.f i j)) i j) ((fun i j => F.map (D.f i j)) i k) ≫ (fun i j => F.map (D.t i j)) i j
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>F : C ⥤ C'<VAR>H : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F<VAR>i j k : D.J<GOAL>(fun i j k => (PreservesPullback.iso F (D.f i j) (D.f i k)).inv ≫ F.map (D.t' i j k) ≫ (PreservesPullback.iso F (D.f j k) (D.f j i)).hom) i j k ≫ (fun i j k => (PreservesPullback.iso F (D.f i j) (D.f i k)).inv ≫ F.map (D.t' i j k) ≫ (PreservesPullback.iso F (D.f j k) (D.f j i)).hom) j k i ≫ (fun i j k => (PreservesPullback.iso F (D.f i j) (D.f i k)).inv ≫ F.map (D.t' i j k) ≫ (PreservesPullback.iso F (D.f j k) (D.f j i)).hom) k i j = 𝟙 (pullback ((fun i j => F.map (D.f i j)) i j) ((fun i j => F.map (D.f i j)) i k))
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J K L I : Ideal R<VAR>h : I = ⊤<GOAL>⊤ = I * ⊤
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hba : ¬b ∣ a + 1<GOAL>(a + 1) / b = a / b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : SemilatticeInf α<VAR>inst✝⁴ : BoundedOrder α<VAR>inst✝³ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝² : SemilatticeInf β<VAR>inst✝¹ : BoundedOrder β<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a✝ b a : α<GOAL>{b}.truncatedInf a = if b ≤ a then b else ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : SemilatticeInf α<VAR>inst✝⁴ : BoundedOrder α<VAR>inst✝³ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝² : SemilatticeInf β<VAR>inst✝¹ : BoundedOrder β<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a✝ b a : α<GOAL>(if h : b ≤ a then (filter (fun x => x ≤ a) {b}).inf' ⋯ fun x => x else ⊥) = if b ≤ a then b else ⊥
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝ : DecidableEq ι<GOAL>derivative (nodal s v) = ∑ i ∈ s, nodal (s.erase i) v
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝ : DecidableEq ι<GOAL>derivative (nodal ∅ v) = ∑ i ∈ ∅, nodal (∅.erase i) v
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>t : Finset ι<VAR>hit : i ∉ t<VAR>IH : derivative (nodal t v) = ∑ i ∈ t, nodal (t.erase i) v<GOAL>derivative (nodal (insert i t) v) = ∑ i_1 ∈ insert i t, nodal ((insert i t).erase i_1) v
<VAR>a b : ℝ<GOAL>frontier {z | a ≤ z.re ∧ b ≤ z.im} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ b ≤ z.im}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<GOAL>a / b = c ↔ a = c * b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s : Multiset ι<VAR>f g : ι → α<VAR>hs : s ≠ ∅<VAR>hfg : ∀ i ∈ s, f i < g i<GOAL>(map f s).prod < (map g s).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s : Multiset ι<VAR>f g : ι → α<VAR>hs : s ≠ ∅<VAR>hfg : ∀ i ∈ s, f i < g i<VAR>i : ι<VAR>hi : i ∈ s<GOAL>(map f s).prod < (map g s).prod
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>w : σ → M<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : NoZeroSMulDivisors ℕ M<VAR>hw : ∀ (i : σ), w i ≠ 0<VAR>n : ℕ<VAR>s : σ<VAR>h : n • w s = 0<GOAL>n = 0
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>w : σ → M<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : NoZeroSMulDivisors ℕ M<VAR>hw : ∀ (i : σ), w i ≠ 0<VAR>n : ℕ<VAR>s : σ<VAR>h : ¬w s = 0 → n = 0<GOAL>n = 0
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : SeminormedCommRing S<VAR>inst✝¹² : SeminormedRing R<VAR>inst✝¹¹ : SeminormedAddCommGroup M<VAR>inst✝¹⁰ : Algebra S R<VAR>inst✝⁹ : Module S M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module Rᵐᵒᵖ M<VAR>inst✝⁶ : BoundedSMul S R<VAR>inst✝⁵ : BoundedSMul S M<VAR>inst✝⁴ : BoundedSMul R M<VAR>inst✝³ : BoundedSMul Rᵐᵒᵖ M<VAR>inst✝² : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹ : IsScalarTower S R M<VAR>inst✝ : IsScalarTower S Rᵐᵒᵖ M<VAR>x : tsze R M<GOAL>‖x‖ = ‖x.fst‖ + ‖x.snd‖
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : SeminormedCommRing S<VAR>inst✝¹² : SeminormedRing R<VAR>inst✝¹¹ : SeminormedAddCommGroup M<VAR>inst✝¹⁰ : Algebra S R<VAR>inst✝⁹ : Module S M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module Rᵐᵒᵖ M<VAR>inst✝⁶ : BoundedSMul S R<VAR>inst✝⁵ : BoundedSMul S M<VAR>inst✝⁴ : BoundedSMul R M<VAR>inst✝³ : BoundedSMul Rᵐᵒᵖ M<VAR>inst✝² : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹ : IsScalarTower S R M<VAR>inst✝ : IsScalarTower S Rᵐᵒᵖ M<VAR>x : tsze R M<GOAL>(‖x.1‖ ^ ENNReal.toReal 1 + ‖x.2‖ ^ ENNReal.toReal 1) ^ (1 / ENNReal.toReal 1) = ‖x.fst‖ + ‖x.snd‖
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : SeminormedCommRing S<VAR>inst✝¹² : SeminormedRing R<VAR>inst✝¹¹ : SeminormedAddCommGroup M<VAR>inst✝¹⁰ : Algebra S R<VAR>inst✝⁹ : Module S M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module Rᵐᵒᵖ M<VAR>inst✝⁶ : BoundedSMul S R<VAR>inst✝⁵ : BoundedSMul S M<VAR>inst✝⁴ : BoundedSMul R M<VAR>inst✝³ : BoundedSMul Rᵐᵒᵖ M<VAR>inst✝² : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹ : IsScalarTower S R M<VAR>inst✝ : IsScalarTower S Rᵐᵒᵖ M<VAR>x : tsze R M<GOAL>‖x.1‖ + ‖x.2‖ = ‖x.fst‖ + ‖x.snd‖
<VAR>w x✝ y z : ℝ<VAR>x : ℝ≥0<VAR>hw : w ≠ 0<VAR>h : y + z = w<GOAL>x ^ w = x ^ y * x ^ z
<VAR>w x✝ y z : ℝ<VAR>x : ℝ≥0<VAR>hw : w ≠ 0<VAR>h : y + z = w<GOAL>y + z ≠ 0
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x a : M<VAR>ha : 1 < a<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>1 < a ^ k
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x a : M<VAR>ha : 1 < a<VAR>l : ℕ<VAR>hk : l.succ ≠ 0<GOAL>1 < a ^ l.succ
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>p : α<VAR>hp : Irreducible p<VAR>k : ℕ<GOAL>normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)
<VAR>z : ℂ<GOAL>(trace ℝ ℂ) z = 2 * z.re
<VAR>z : ℂ<GOAL>!![z.re, -z.im; z.im, z.re] 0 0 + !![z.re, -z.im; z.im, z.re] 1 1 = 2 * z.re
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>f : Filter α<VAR>inst✝⁴ : f.NeBot<VAR>R : Type u_7<VAR>inst✝³ : Preorder R<VAR>κ : Type u_8<VAR>inst✝² : AddCommMonoid R<VAR>inst✝¹ : CovariantClass R R (fun a b => a + b) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass R R (fun a b => b + a) fun x x_1 => x ≤ x_1<VAR>u : κ → α → R<VAR>s : Finset κ<VAR>aux : CovariantClass R R (fun a b => a + b) fun x x_1 => x ≥ x_1<GOAL>(∀ k ∈ s, IsBoundedUnder (fun x x_1 => x ≥ x_1) f (u k)) → IsBoundedUnder (fun x x_1 => x ≥ x_1) f (∑ k ∈ s, u k)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsAffine Y<GOAL>P f ↔ Q f
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsAffine Y<VAR>this : Q.IsLocal := isLocal_affineProperty P<GOAL>P f ↔ Q f
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsAffine Y<VAR>this✝ : Q.IsLocal := isLocal_affineProperty P<VAR>this : ∀ (i : (Scheme.openCoverOfIsIso (𝟙 Y)).J), IsAffine ((Scheme.openCoverOfIsIso (𝟙 Y)).obj i)<GOAL>P f ↔ Q f
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsAffine Y<VAR>this✝ : Q.IsLocal := isLocal_affineProperty P<VAR>this : ∀ (i : (Scheme.openCoverOfIsIso (𝟙 Y)).J), IsAffine ((Scheme.openCoverOfIsIso (𝟙 Y)).obj i)<GOAL>(∀ (i : ((Scheme.openCoverOfIsIso (𝟙 Y)).pullbackCover f).J), Q ((Scheme.openCoverOfIsIso (𝟙 Y)).pullbackHom f i)) ↔ Q f