ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.39294, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.39346, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : D<VAR>x : ℱ.obj (op X)<GOAL>(pushforwardFamily α x).Compatible
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.39294, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.39346, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : D<VAR>x : ℱ.obj (op X)<GOAL>∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂), iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ → ℱ'.val.map iZW₁.op (α.app (op W₁) (ℱ.map iWX₁.op x)) = ℱ'.val.map iZW₂.op (α.app (op W₂) (ℱ.map iWX₂.op x))
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.39294, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.39346, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : D<VAR>x : ℱ.obj (op X)<VAR>Z : D<VAR>W₁ W₂ : C<VAR>iWX₁ : G.obj W₁ ⟶ X<VAR>iWX₂ : G.obj W₂ ⟶ X<VAR>iZW₁ : Z ⟶ G.obj W₁<VAR>iZW₂ : Z ⟶ G.obj W₂<VAR>e : iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂<GOAL>ℱ'.val.map iZW₁.op (α.app (op W₁) (ℱ.map iWX₁.op x)) = ℱ'.val.map iZW₂.op (α.app (op W₂) (ℱ.map iWX₂.op x))
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.39294, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.39346, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : D<VAR>x : ℱ.obj (op X)<VAR>Z : D<VAR>W₁ W₂ : C<VAR>iWX₁ : G.obj W₁ ⟶ X<VAR>iWX₂ : G.obj W₂ ⟶ X<VAR>iZW₁ : Z ⟶ G.obj W₁<VAR>iZW₂ : Z ⟶ G.obj W₂<VAR>e : iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂<VAR>V : C<VAR>iVZ : G.obj V ⟶ Z<GOAL>ℱ'.val.map iVZ.op (ℱ'.val.map iZW₁.op (α.app (op W₁) (ℱ.map iWX₁.op x))) = ℱ'.val.map iVZ.op (ℱ'.val.map iZW₂.op (α.app (op W₂) (ℱ.map iWX₂.op x)))
<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>inst✝ : IsLocalization M S<VAR>I : Ideal R<VAR>hp : I.IsPrime<VAR>hd : Disjoint ↑M ↑I<GOAL>(Ideal.map (algebraMap R S) I).IsPrime
<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>inst✝ : IsLocalization M S<VAR>I : Ideal R<VAR>hp : I.IsPrime<VAR>hd : Disjoint ↑M ↑I<GOAL>I.IsPrime ∧ Disjoint ↑M ↑I
<VAR>fs : Code<VAR>k : Cont'<GOAL>contSupp (Cont'.cons₁ fs k) = trStmts₁ (move₂ (fun x => false) main aux (move₂ (fun s => decide (s = Γ'.consₗ)) stack main (move₂ (fun x => false) aux stack (trNormal fs k.cons₂)))) ∪ codeSupp fs k.cons₂
<VAR>m n✝ k n : ℕ<VAR>h✝ : k = n + 1<VAR>x : ZMod (namedPattern k (n + 1) h✝)<GOAL>↑x.valMinAbs = x
<VAR>m n✝ k n : ℕ<VAR>h✝ : k = n + 1<VAR>x : ZMod (namedPattern k (n + 1) h✝)<GOAL>↑(if x.val ≤ namedPattern k (n + 1) h✝ / 2 then ↑x.val else ↑x.val - ↑(namedPattern k (n + 1) h✝)) = x
<VAR>P : TopCat → Prop<VAR>X✝ : Type u<VAR>inst✝³ : TopologicalSpace X✝<VAR>inst✝² : CompactSpace X✝<VAR>inst✝¹ : T2Space X✝<VAR>inst✝ : HasProp P X✝<VAR>X Y : CompHausLike P<VAR>f : X ⟶ Y<VAR>hf : Function.Surjective ⇑f<GOAL>Epi f
<VAR>P : TopCat → Prop<VAR>X✝ : Type u<VAR>inst✝³ : TopologicalSpace X✝<VAR>inst✝² : CompactSpace X✝<VAR>inst✝¹ : T2Space X✝<VAR>inst✝ : HasProp P X✝<VAR>X Y : CompHausLike P<VAR>f : X ⟶ Y<VAR>hf : Epi ⇑f<GOAL>Epi f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>n : ℕ<GOAL>derivative (X ^ n) = C ↑n * X ^ (n - 1)
<VAR>C : FloatCfg<GOAL>emin ≤ emin + ↑prec - 1
<VAR>C : FloatCfg<GOAL>emin ≤ emin + (↑prec - 1)
<VAR>C : FloatCfg<GOAL>0 ≤ ↑prec - 1
<VAR>C : FloatCfg<GOAL>1 ≤ prec
<VAR>C : FloatCfg<VAR>this : prec ≤ 2 * emax<GOAL>emin + ↑prec - 1 ≤ ↑emax
<VAR>C : FloatCfg<VAR>this : ↑prec ≤ ↑(2 * emax)<GOAL>emin + ↑prec - 1 ≤ ↑emax
<VAR>C : FloatCfg<VAR>this : 0 ≤ ↑(2 * emax) - ↑prec<GOAL>0 ≤ ↑emax - (emin + ↑prec - 1)
<VAR>C : FloatCfg<VAR>this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec<GOAL>0 ≤ ↑FloatCfg.emax * 2 - ↑prec
<VAR>C : FloatCfg<VAR>this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec<GOAL>0 ≤ 2 * ↑FloatCfg.emax - ↑prec
<VAR>C : FloatCfg<GOAL>emin = max (emin + ↑(Nat.size 0) - ↑prec) emin
<VAR>q : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (x / ↑m) ↔ m ≠ 0 ∧ Irrational x
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M✝ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R M✝<VAR>M : Type u_9<VAR>inst✝² : AddCommMonoidWithOne M<VAR>inst✝¹ : CharZero M<VAR>inst✝ : Module R M<GOAL>CharZero R
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M✝ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R M✝<VAR>M : Type u_9<VAR>inst✝² : AddCommMonoidWithOne M<VAR>inst✝¹ : CharZero M<VAR>inst✝ : Module R M<VAR>m n : ℕ<VAR>h : ↑m = ↑n<GOAL>↑m = ↑n
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>f : P →ₗ[R] Q →ₗ[R] M<VAR>p : Submodule R P<VAR>q : Submodule R Q<GOAL>Submodule.map₂ f p q = range (lift f ∘ₗ mapIncl p q)
<VAR>M : Type u_1<VAR>N✝ : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S N N' : Submonoid M<GOAL>N ⊔ N' = closure (↑N ∪ ↑N')
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>a t : ℝ<VAR>ht : t ∈ {t | t * a ∈ s}<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I (γ ∘ fun x => x * a) t (ContinuousLinearMap.smulRight 1 ((a • v) ((γ ∘ fun x => x * a) t)))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>a t : ℝ<VAR>ht : t ∈ {t | t * a ∈ s}<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I (γ ∘ fun x => x * a) t ((ContinuousLinearMap.smulRight 1 (v (γ (t * a)))).comp (ContinuousLinearMap.smulRight 1 a))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>a t : ℝ<VAR>ht : t ∈ {t | t * a ∈ s}<GOAL>HasFDerivWithinAt (writtenInExtChartAt 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) t fun x => x * a) (ContinuousLinearMap.smulRight 1 a) (range ↑𝓘(ℝ, ℝ)) (↑(extChartAt 𝓘(ℝ, ℝ) t) t)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>a t : ℝ<VAR>ht : t ∈ {t | t * a ∈ s}<GOAL>HasFDerivAt (fun x => x * a) (ContinuousLinearMap.smulRight 1 a) t
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹² : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹¹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝¹⁰ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>E : Type u_9<VAR>inst✝⁷ : AddCommMonoid E<VAR>inst✝⁶ : Module R E<VAR>F : Type u_10<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : DecidableEq ι<VAR>z : R<VAR>f : (i : ι) → s i<VAR>i : ι<VAR>r : R₁<VAR>inst✝³ : SMul R₁ R<VAR>inst✝² : IsScalarTower R₁ R R<VAR>inst✝¹ : SMul R₁ (s i)<VAR>inst✝ : IsScalarTower R₁ R (s i)<GOAL>tprodCoeff R z (update f i (r • f i)) = tprodCoeff R (r • z) f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹² : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹¹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝¹⁰ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>E : Type u_9<VAR>inst✝⁷ : AddCommMonoid E<VAR>inst✝⁶ : Module R E<VAR>F : Type u_10<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : DecidableEq ι<VAR>z : R<VAR>f : (i : ι) → s i<VAR>i : ι<VAR>r : R₁<VAR>inst✝³ : SMul R₁ R<VAR>inst✝² : IsScalarTower R₁ R R<VAR>inst✝¹ : SMul R₁ (s i)<VAR>inst✝ : IsScalarTower R₁ R (s i)<VAR>h₁ : r • z = r • 1 * z<GOAL>tprodCoeff R z (update f i (r • f i)) = tprodCoeff R (r • z) f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹² : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹¹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝¹⁰ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>E : Type u_9<VAR>inst✝⁷ : AddCommMonoid E<VAR>inst✝⁶ : Module R E<VAR>F : Type u_10<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : DecidableEq ι<VAR>z : R<VAR>f : (i : ι) → s i<VAR>i : ι<VAR>r : R₁<VAR>inst✝³ : SMul R₁ R<VAR>inst✝² : IsScalarTower R₁ R R<VAR>inst✝¹ : SMul R₁ (s i)<VAR>inst✝ : IsScalarTower R₁ R (s i)<VAR>h₁ : r • z = r • 1 * z<VAR>h₂ : r • f i = (r • 1) • f i<GOAL>tprodCoeff R z (update f i (r • f i)) = tprodCoeff R (r • z) f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹² : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹¹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝¹⁰ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>E : Type u_9<VAR>inst✝⁷ : AddCommMonoid E<VAR>inst✝⁶ : Module R E<VAR>F : Type u_10<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : DecidableEq ι<VAR>z : R<VAR>f : (i : ι) → s i<VAR>i : ι<VAR>r : R₁<VAR>inst✝³ : SMul R₁ R<VAR>inst✝² : IsScalarTower R₁ R R<VAR>inst✝¹ : SMul R₁ (s i)<VAR>inst✝ : IsScalarTower R₁ R (s i)<VAR>h₁ : r • z = r • 1 * z<VAR>h₂ : r • f i = (r • 1) • f i<GOAL>tprodCoeff R z (update f i ((r • 1) • f i)) = tprodCoeff R (r • 1 * z) f
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>L₃ : Type w₁<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L₁<VAR>inst✝⁴ : LieRing L₂<VAR>inst✝³ : LieRing L₃<VAR>inst✝² : LieAlgebra R L₁<VAR>inst✝¹ : LieAlgebra R L₂<VAR>inst✝ : LieAlgebra R L₃<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>h : Bijective ⇑f<VAR>x y : L₁<GOAL>{ toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯ }.toFun ⁅x, y⁆ = ⁅{ toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯ }.toFun x, { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯ }.toFun y⁆
<VAR>a b x : PGame<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<GOAL>(mk xl xr xL xR + mk yl yr yL yR).birthday = (mk xl xr xL xR).birthday ♯ (mk yl yr yL yR).birthday
<VAR>a b x : PGame<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<GOAL>max (lsub fun i => ((mk xl xr xL xR + mk yl yr yL yR).moveLeft i).birthday) (lsub fun i => ((mk xl xr xL xR + mk yl yr yL yR).moveRight i).birthday) = max ((mk xl xr xL xR).birthday.blsub fun a' x => a' ♯ (mk yl yr yL yR).birthday) ((mk yl yr yL yR).birthday.blsub fun b' x => (mk xl xr xL xR).birthday ♯ b')
<VAR>a b x : PGame<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<GOAL>max (max (lsub fun a => ((mk xl xr xL xR + mk yl yr yL yR).moveLeft (Sum.inl a)).birthday) (lsub fun b => ((mk xl xr xL xR + mk yl yr yL yR).moveLeft (Sum.inr b)).birthday)) (max (lsub fun a => ((mk xl xr xL xR + mk yl yr yL yR).moveRight (Sum.inl a)).birthday) (lsub fun b => ((mk xl xr xL xR + mk yl yr yL yR).moveRight (Sum.inr b)).birthday)) = max ((mk xl xr xL xR).birthday.blsub fun a' x => a' ♯ (mk yl yr yL yR).birthday) ((mk yl yr yL yR).birthday.blsub fun b' x => (mk xl xr xL xR).birthday ♯ b')
<VAR>a b x : PGame<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<GOAL>max (max (lsub fun a => (xL a + mk yl yr yL yR).birthday) (lsub fun b => (mk xl xr xL xR + yL b).birthday)) (max (lsub fun a => (xR a + mk yl yr yL yR).birthday) (lsub fun b => (mk xl xr xL xR + yR b).birthday)) = max ((mk xl xr xL xR).birthday.blsub fun a' x => a' ♯ (mk yl yr yL yR).birthday) ((mk yl yr yL yR).birthday.blsub fun b' x => (mk xl xr xL xR).birthday ♯ b')
<VAR>a b x : PGame<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<GOAL>max (max (lsub fun a => (xL a).birthday ♯ (mk yl yr yL yR).birthday) (lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday)) (max (lsub fun a => (xR a).birthday ♯ (mk yl yr yL yR).birthday) (lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday)) = max ((mk xl xr xL xR).birthday.blsub fun a' x => a' ♯ (mk yl yr yL yR).birthday) ((mk yl yr yL yR).birthday.blsub fun b' x => (mk xl xr xL xR).birthday ♯ b')
<VAR>a b x : PGame<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<GOAL>max (max (lsub fun a => (xL a).birthday ♯ (mk yl yr yL yR).birthday) (lsub fun a => (xR a).birthday ♯ (mk yl yr yL yR).birthday)) (max (lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) (lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday)) = max ((mk xl xr xL xR).birthday.blsub fun a' x => a' ♯ (mk yl yr yL yR).birthday) ((mk yl yr yL yR).birthday.blsub fun b' x => (mk xl xr xL xR).birthday ♯ b')
<VAR>a b x : PGame<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<GOAL>max (lsub fun a => (xL a).birthday ♯ (mk yl yr yL yR).birthday) (lsub fun a => (xR a).birthday ♯ (mk yl yr yL yR).birthday) ≤ (mk xl xr xL xR).birthday.blsub fun a' x => a' ♯ (mk yl yr yL yR).birthday
<VAR>a b x : PGame<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<GOAL>((mk xl xr xL xR).birthday.blsub fun a' x => a' ♯ (mk yl yr yL yR).birthday) ≤ max (lsub fun a => (xL a).birthday ♯ (mk yl yr yL yR).birthday) (lsub fun a => (xR a).birthday ♯ (mk yl yr yL yR).birthday)
<VAR>a b x : PGame<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<GOAL>max (lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) (lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday) ≤ (mk yl yr yL yR).birthday.blsub fun b' x => (mk xl xr xL xR).birthday ♯ b'
<VAR>a b x : PGame<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<GOAL>((mk yl yr yL yR).birthday.blsub fun b' x => (mk xl xr xL xR).birthday ♯ b') ≤ max (lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) (lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday)
<VAR>a b x : PGame<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>i : Ordinal.{u}<VAR>hi : i < (mk xl xr xL xR).birthday<VAR>j : (mk xl xr xL xR).LeftMoves<VAR>hj : i ≤ ((mk xl xr xL xR).moveLeft j).birthday<GOAL>i ♯ (mk yl yr yL yR).birthday < max (lsub fun a => (xL a).birthday ♯ (mk yl yr yL yR).birthday) (lsub fun a => (xR a).birthday ♯ (mk yl yr yL yR).birthday)
<VAR>a b x : PGame<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>i : Ordinal.{u}<VAR>hi : i < (mk xl xr xL xR).birthday<VAR>j : (mk xl xr xL xR).RightMoves<VAR>hj : i ≤ ((mk xl xr xL xR).moveRight j).birthday<GOAL>i ♯ (mk yl yr yL yR).birthday < max (lsub fun a => (xL a).birthday ♯ (mk yl yr yL yR).birthday) (lsub fun a => (xR a).birthday ♯ (mk yl yr yL yR).birthday)
<VAR>a b x : PGame<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>i : Ordinal.{u}<VAR>hi : i < (mk yl yr yL yR).birthday<VAR>j : (mk yl yr yL yR).LeftMoves<VAR>hj : i ≤ ((mk yl yr yL yR).moveLeft j).birthday<GOAL>(mk xl xr xL xR).birthday ♯ i < max (lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) (lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday)
<VAR>a b x : PGame<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>i : Ordinal.{u}<VAR>hi : i < (mk yl yr yL yR).birthday<VAR>j : (mk yl yr yL yR).RightMoves<VAR>hj : i ≤ ((mk yl yr yL yR).moveRight j).birthday<GOAL>(mk xl xr xL xR).birthday ♯ i < max (lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) (lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>w x y z : V<VAR>hw : w ≠ 0<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<VAR>hs : (o.oangle w x).sign = (o.oangle y z).sign<GOAL>InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle y z
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>w x y z : V<VAR>hw : w ≠ 0<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<VAR>hs : (o.oangle w x).sign = (o.oangle y z).sign<VAR>h : o.oangle w x = o.oangle y z<GOAL>InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>p : α → Bool<VAR>l : List α<GOAL>l.Nodup → (List.filter p l).Nodup
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝³ : CommRing T<VAR>p : T[X]<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra T S<VAR>a : S<GOAL>a ∈ p.rootSet S ↔ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>a b : α<GOAL>Ioo a b ⊆ closure (interior (Ioo a b))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<GOAL>∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n<GOAL>∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<VAR>n : ℕ<GOAL>‖f (x + y) - p.partialSum n y‖ ≤ C / (1 - a) * (a * (‖y‖ / ↑r')) ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<VAR>n : ℕ<VAR>yr' : ‖y‖ < ↑r'<GOAL>‖f (x + y) - p.partialSum n y‖ ≤ C / (1 - a) * (a * (‖y‖ / ↑r')) ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<VAR>n : ℕ<VAR>yr' : ‖y‖ < ↑r'<VAR>hr'0 : 0 < ↑r'<GOAL>‖f (x + y) - p.partialSum n y‖ ≤ C / (1 - a) * (a * (‖y‖ / ↑r')) ^ n