ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingLeft<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>j : n<VAR>hij : i ≠ j<GOAL>(B (v i)) (v j) = 0
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>X Y Z : C<VAR>inst✝⁴ : HasPullbacks C<VAR>S T : C<VAR>f : X ⟶ T<VAR>g : Y ⟶ T<VAR>i : T ⟶ S<VAR>inst✝³ : HasPullback i i<VAR>inst✝² : HasPullback f g<VAR>inst✝¹ : HasPullback (f ≫ i) (g ≫ i)<VAR>inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)<GOAL>(pullbackDiagonalMapIdIso f g i).inv ≫ snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i) = fst f g
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>X Y Z : C<VAR>inst✝⁴ : HasPullbacks C<VAR>S T : C<VAR>f : X ⟶ T<VAR>g : Y ⟶ T<VAR>i : T ⟶ S<VAR>inst✝³ : HasPullback i i<VAR>inst✝² : HasPullback f g<VAR>inst✝¹ : HasPullback (f ≫ i) (g ≫ i)<VAR>inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)<GOAL>snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i) = (pullbackDiagonalMapIdIso f g i).hom ≫ fst f g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : IsOpenMap f<VAR>s : Set Y<GOAL>f ⁻¹' closure s ⊆ closure (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : IsOpenMap f<VAR>s : Set Y<GOAL>(closure (f ⁻¹' s))ᶜ ⊆ (f ⁻¹' closure s)ᶜ
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting<VAR>inst✝ : HasBinaryBiproducts C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>p : ℤ<GOAL>(↑(cocycleOfDegreewiseSplit (triangleRotateShortComplex φ) (triangleRotateShortComplexSplitting φ))).v p (p + 1) ⋯ = -φ.f (p + { as := 1 }.as)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a b : WithBot α<VAR>hb : b ≠ 0<GOAL>⊥ * b = ⊥
<VAR>n : ℕ+<VAR>x : ℂˣ<GOAL>x ∈ rootsOfUnity n ℂ ↔ ∃ i < ↑n, cexp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
<VAR>n : ℕ+<VAR>x : ℂˣ<GOAL>↑x ^ ↑n = 1 ↔ ∃ i < ↑n, cexp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
<VAR>n : ℕ+<VAR>x : ℂˣ<VAR>hn0 : ↑↑n ≠ 0<GOAL>↑x ^ ↑n = 1 ↔ ∃ i < ↑n, cexp (2 * ↑π * I * (↑i / ↑↑n)) = ↑x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<GOAL>B.SeparatingRight
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.flip.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<GOAL>B.SeparatingRight
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.flip.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<GOAL>B.flip.SeparatingLeft
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.flip.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>i : n<GOAL>¬B.flip.IsOrtho (v i) (v i)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : 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>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.flip.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>i : n<GOAL>¬B.flip.flip.IsOrtho (v i) (v i)
<VAR>α : Type u_1<VAR>inst✝⁴ : Semifield α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : PosMulReflectLT α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>a b : α<VAR>inst✝ : MulPosMono α<VAR>ha : a ≤ 0<VAR>hb : 0 ≤ b<GOAL>a / b ≤ 0
<VAR>α : Type u_1<VAR>inst✝⁴ : Semifield α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : PosMulReflectLT α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>a b : α<VAR>inst✝ : MulPosMono α<VAR>ha : a ≤ 0<VAR>hb : 0 ≤ b<GOAL>a * b⁻¹ ≤ 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<VAR>a b : CliffordAlgebra Q<GOAL>((foldl Q f hf) n) (a * b) = ((foldl Q f hf) (((foldl Q f hf) n) a)) b
<VAR>M : Type u_1<VAR>m₁ m₂ : DivInvMonoid M<VAR>h_mul : HMul.hMul = HMul.hMul<VAR>h_inv : Inv.inv = Inv.inv<GOAL>m₁ = m₂
<VAR>M : Type u_1<VAR>m₁ m₂ : DivInvMonoid M<VAR>h_mul : HMul.hMul = HMul.hMul<VAR>h_inv : Inv.inv = Inv.inv<VAR>h_mon : toMonoid = toMonoid<GOAL>m₁ = m₂
<VAR>M : Type u_1<VAR>m₁ m₂ : DivInvMonoid M<VAR>h_mul : HMul.hMul = HMul.hMul<VAR>h_inv : Inv.inv = Inv.inv<VAR>h_mon : toMonoid = toMonoid<VAR>h₁ : One.one = One.one<VAR>f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }<VAR>this : Monoid.npow = Monoid.npow<GOAL>m₁ = m₂
<VAR>M : Type u_1<VAR>m₁ m₂ : DivInvMonoid M<VAR>h_mul : HMul.hMul = HMul.hMul<VAR>h_inv : Inv.inv = Inv.inv<VAR>h_mon : toMonoid = toMonoid<VAR>h₁ : One.one = One.one<VAR>f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }<VAR>this✝ : Monoid.npow = Monoid.npow<VAR>this : DivInvMonoid.zpow = DivInvMonoid.zpow<GOAL>m₁ = m₂
<VAR>M : Type u_1<VAR>m₁ m₂ : DivInvMonoid M<VAR>h_mul : HMul.hMul = HMul.hMul<VAR>h_inv : Inv.inv = Inv.inv<VAR>h_mon : toMonoid = toMonoid<VAR>h₁ : One.one = One.one<VAR>f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }<VAR>this✝¹ : Monoid.npow = Monoid.npow<VAR>this✝ : DivInvMonoid.zpow = DivInvMonoid.zpow<VAR>this : Div.div = Div.div<GOAL>m₁ = m₂
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Group α<VAR>a b : α<VAR>n : ℕ<VAR>x✝ : α<GOAL>(Equiv.mulLeft a ^ n) x✝ = (Equiv.mulLeft (a ^ n)) x✝
<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>n : ℕ<VAR>s : Simplex ℝ P (n + 1)<VAR>i : Fin (n + 2)<GOAL>(s.altitude i).direction = (vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<GOAL>(⇑(Linear_CC' C hsC ho) ∘ fun l => Products.eval C ↑l) l = Products.eval (C' C ho) (↑l).Tail
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<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>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>f.range = ⊤ ↔ Function.Surjective ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<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>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>LinearMap.range ↑f = ⊤ ↔ Function.Surjective ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : s =ᶠ[ae μ] univ<GOAL>s ∩ t =ᶠ[ae μ] t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : s =ᶠ[ae μ] univ<GOAL>t = univ ∩ t
<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>f : ((i : ι) → A i) → ℝ≥0∞<VAR>x : (i : ι) → A i<GOAL>T μ p f Finset.univ x = ∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (t : A i), f (update x i t) ∂μ i) ^ p ∂Measure.pi μ
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>S : Set E<VAR>n : ℤ<GOAL>F⟮↑n⟯ = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CommSemiring A<VAR>z : E<VAR>s : Set E<VAR>inst✝² : NormedRing B<VAR>inst✝¹ : NormedAlgebra 𝕜 B<VAR>inst✝ : Algebra A B<VAR>f : E → B<VAR>hf : AnalyticAt 𝕜 f z<VAR>p : A[X]<GOAL>AnalyticAt 𝕜 (fun x => (aeval (f x)) p) z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CommSemiring A<VAR>z : E<VAR>s : Set E<VAR>inst✝² : NormedRing B<VAR>inst✝¹ : NormedAlgebra 𝕜 B<VAR>inst✝ : Algebra A B<VAR>f : E → B<VAR>hf : AnalyticAt 𝕜 f z<VAR>p : A[X]<VAR>k : A<GOAL>AnalyticAt 𝕜 (fun x => (aeval (f x)) (C k)) z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CommSemiring A<VAR>z : E<VAR>s : Set E<VAR>inst✝² : NormedRing B<VAR>inst✝¹ : NormedAlgebra 𝕜 B<VAR>inst✝ : Algebra A B<VAR>f : E → B<VAR>hf : AnalyticAt 𝕜 f z<VAR>p✝ p q : A[X]<VAR>hp : AnalyticAt 𝕜 (fun x => (aeval (f x)) p) z<VAR>hq : AnalyticAt 𝕜 (fun x => (aeval (f x)) q) z<GOAL>AnalyticAt 𝕜 (fun x => (aeval (f x)) (p + q)) z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CommSemiring A<VAR>z : E<VAR>s : Set E<VAR>inst✝² : NormedRing B<VAR>inst✝¹ : NormedAlgebra 𝕜 B<VAR>inst✝ : Algebra A B<VAR>f : E → B<VAR>hf : AnalyticAt 𝕜 f z<VAR>p✝ : A[X]<VAR>p : ℕ<VAR>i : A<VAR>hp : AnalyticAt 𝕜 (fun x => (aeval (f x)) (C i * X ^ p)) z<GOAL>AnalyticAt 𝕜 (fun x => (aeval (f x)) (C i * X ^ (p + 1))) z
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : Filter X<GOAL>f ≤ 𝓝 x ↔ ∀ (s : Set X), x ∈ s → IsOpen s → s ∈ f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : Fork f g<GOAL>t.ι ≫ f = t.ι ≫ g
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>W✝ X✝ Y Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g : W✝ ⟶ Y<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y ⟶ Z✝<VAR>W E X Z : C<VAR>c : BinaryCofan W E<VAR>inst✝¹ : FinitaryExtensive C<VAR>inst✝ : HasPullbacks C<VAR>hc : IsColimit c<VAR>f : W ⟶ X<VAR>h : X ⟶ Z<VAR>i : c.pt ⟶ Z<VAR>H : IsPushout f c.inl h i<GOAL>H.IsVanKampen
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>W✝ X✝ Y Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g : W✝ ⟶ Y<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y ⟶ Z✝<VAR>W E X Z : C<VAR>c : BinaryCofan W E<VAR>inst✝¹ : FinitaryExtensive C<VAR>inst✝ : HasPullbacks C<VAR>hc : IsColimit c<VAR>f : W ⟶ X<VAR>h : X ⟶ Z<VAR>i : c.pt ⟶ Z<VAR>H : IsPushout f c.inl h i<VAR>hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)<GOAL>H.IsVanKampen
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>W✝ X✝ Y Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g : W✝ ⟶ Y<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y ⟶ Z✝<VAR>W E X Z : C<VAR>c : BinaryCofan W E<VAR>inst✝¹ : FinitaryExtensive C<VAR>inst✝ : HasPullbacks C<VAR>hc : IsColimit c<VAR>f : W ⟶ X<VAR>h : X ⟶ Z<VAR>i : c.pt ⟶ Z<VAR>H : IsPushout f c.inl h i<VAR>hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)<VAR>W' X' Y' Z' : C<VAR>f' : W' ⟶ X'<VAR>g' : W' ⟶ Y'<VAR>h' : X' ⟶ Z'<VAR>i' : Y' ⟶ Z'<VAR>αW : W' ⟶ W<VAR>αX : X' ⟶ X<VAR>αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }<VAR>αZ : Z' ⟶ Z<VAR>hf : IsPullback f' αW αX f<VAR>hg : IsPullback g' αW αY c.inl<VAR>hh : CommSq h' αX αZ h<VAR>hi : CommSq i' αY αZ i<VAR>w : CommSq f' g' h' i'<GOAL>IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>W✝ X✝ Y Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g : W✝ ⟶ Y<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y ⟶ Z✝<VAR>W E X Z : C<VAR>c : BinaryCofan W E<VAR>inst✝¹ : FinitaryExtensive C<VAR>inst✝ : HasPullbacks C<VAR>hc : IsColimit c<VAR>f : W ⟶ X<VAR>h : X ⟶ Z<VAR>i : c.pt ⟶ Z<VAR>H : IsPushout f c.inl h i<VAR>hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)<VAR>W' X' Y' Z' : C<VAR>f' : W' ⟶ X'<VAR>g' : W' ⟶ Y'<VAR>h' : X' ⟶ Z'<VAR>i' : Y' ⟶ Z'<VAR>αW : W' ⟶ W<VAR>αX : X' ⟶ X<VAR>αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }<VAR>αZ : Z' ⟶ Z<VAR>hf : IsPullback f' αW αX f<VAR>hg : IsPullback g' αW αY c.inl<VAR>hh : CommSq h' αX αZ h<VAR>hi : CommSq i' αY αZ i<VAR>w : CommSq f' g' h' i'<VAR>hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))<GOAL>IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>W✝ X✝ Y Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g : W✝ ⟶ Y<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y ⟶ Z✝<VAR>W E X Z : C<VAR>c : BinaryCofan W E<VAR>inst✝¹ : FinitaryExtensive C<VAR>inst✝ : HasPullbacks C<VAR>hc : IsColimit c<VAR>f : W ⟶ X<VAR>h : X ⟶ Z<VAR>i : c.pt ⟶ Z<VAR>H : IsPushout f c.inl h i<VAR>hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)<VAR>W' X' Y' Z' : C<VAR>f' : W' ⟶ X'<VAR>g' : W' ⟶ Y'<VAR>h' : X' ⟶ Z'<VAR>i' : Y' ⟶ Z'<VAR>αW : W' ⟶ W<VAR>αX : X' ⟶ X<VAR>αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }<VAR>αZ : Z' ⟶ Z<VAR>hf : IsPullback f' αW αX f<VAR>hg : IsPullback g' αW αY c.inl<VAR>hh : CommSq h' αX αZ h<VAR>hi : CommSq i' αY αZ i<VAR>w : CommSq f' g' h' i'<VAR>hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))<GOAL>Nonempty (IsColimit (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h')) ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>W✝ X✝ Y Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g : W✝ ⟶ Y<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y ⟶ Z✝<VAR>W E X Z : C<VAR>c : BinaryCofan W E<VAR>inst✝¹ : FinitaryExtensive C<VAR>inst✝ : HasPullbacks C<VAR>hc : IsColimit c<VAR>f : W ⟶ X<VAR>h : X ⟶ Z<VAR>i : c.pt ⟶ Z<VAR>H : IsPushout f c.inl h i<VAR>hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)<VAR>W' X' Y' Z' : C<VAR>f' : W' ⟶ X'<VAR>g' : W' ⟶ Y'<VAR>h' : X' ⟶ Z'<VAR>i' : Y' ⟶ Z'<VAR>αW : W' ⟶ W<VAR>αX : X' ⟶ X<VAR>αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }<VAR>αZ : Z' ⟶ Z<VAR>hf : IsPullback f' αW αX f<VAR>hg : IsPullback g' αW αY c.inl<VAR>hh : CommSq h' αX αZ h<VAR>hi : CommSq i' αY αZ i<VAR>w : CommSq f' g' h' i'<VAR>hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))<GOAL>pullback.snd αY c.inr ≫ (BinaryCofan.mk (c.inr ≫ i) h).inl = (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl ≫ αZ
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>W✝ X✝ Y Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g : W✝ ⟶ Y<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y ⟶ Z✝<VAR>W E X Z : C<VAR>c : BinaryCofan W E<VAR>inst✝¹ : FinitaryExtensive C<VAR>inst✝ : HasPullbacks C<VAR>hc : IsColimit c<VAR>f : W ⟶ X<VAR>h : X ⟶ Z<VAR>i : c.pt ⟶ Z<VAR>H : IsPushout f c.inl h i<VAR>hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)<VAR>W' X' Y' Z' : C<VAR>f' : W' ⟶ X'<VAR>g' : W' ⟶ Y'<VAR>h' : X' ⟶ Z'<VAR>i' : Y' ⟶ Z'<VAR>αW : W' ⟶ W<VAR>αX : X' ⟶ X<VAR>αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }<VAR>αZ : Z' ⟶ Z<VAR>hf : IsPullback f' αW αX f<VAR>hg : IsPullback g' αW αY c.inl<VAR>hh : CommSq h' αX αZ h<VAR>hi : CommSq i' αY αZ i<VAR>w : CommSq f' g' h' i'<VAR>hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))<GOAL>IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ (BinaryCofan.mk (c.inr ≫ i) h).inl ∧ IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ (BinaryCofan.mk (c.inr ≫ i) h).inr ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<GOAL>(M ↾ X).Base I ↔ M.Basis' I X
<VAR>p q : ℕ+ → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h : ∃ n, p n<VAR>n✝ m n : ℕ+<GOAL>n ≤ PNat.find h ↔ ∀ m < n, ¬p m
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>a : α<VAR>b : β<GOAL>LiftRel R (pure a) (pure b) ↔ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>a : α<VAR>b : β<GOAL>(∃ b_1, b_1 ∈ pure b ∧ R a b_1) ↔ R a b
<VAR>α : Type u_1<VAR>s : Set α<VAR>t : Set Bool<GOAL>s.boolIndicator ⁻¹' t = univ ∨ s.boolIndicator ⁻¹' t = s ∨ s.boolIndicator ⁻¹' t = sᶜ ∨ s.boolIndicator ⁻¹' t = ∅
<VAR>α : Type u_1<VAR>s : Set α<VAR>t : Set Bool<GOAL>((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = univ ∨ ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = s ∨ ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = sᶜ ∨ ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = ∅
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : Ring S<VAR>M : Type u_4<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsSemisimpleModule R M<GOAL>sSup {m | IsSimpleModule R ↥m} = ⊤
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>g : R →+* ℤ_[p]<VAR>hg : ∀ (n : ℕ), (toZModPow n).comp g = f n<VAR>r : R<GOAL>(lift f_compat) r = g r
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>g : R →+* ℤ_[p]<VAR>hg : ∀ (n : ℕ), (toZModPow n).comp g = f n<VAR>r : R<GOAL>∀ ε > 0, dist ((lift f_compat) r) (g r) ≤ ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>g : R →+* ℤ_[p]<VAR>hg : ∀ (n : ℕ), (toZModPow n).comp g = f n<VAR>r : R<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>dist ((lift f_compat) r) (g r) ≤ ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>g : R →+* ℤ_[p]<VAR>hg : ∀ (n : ℕ), (toZModPow n).comp g = f n<VAR>r : R<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<GOAL>dist ((lift f_compat) r) (g r) ≤ ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>g : R →+* ℤ_[p]<VAR>hg : ∀ (n : ℕ), (toZModPow n).comp g = f n<VAR>r : R<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<GOAL>dist ((lift f_compat) r) (g r) ≤ ↑p ^ (-↑n)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g✝ : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<VAR>g : E → G := fun y => f y - φ y<GOAL>‖f y - f x - φ (y - x)‖ ≤ C * ‖y - x‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g✝ : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<VAR>g : E → G := fun y => f y - φ y<VAR>hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x<GOAL>‖f y - f x - φ (y - x)‖ ≤ C * ‖y - x‖
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f : Filter α<VAR>p : α → Prop<VAR>q : Prop<GOAL>(∃ᶠ (x : α) in f, p x ∧ q) ↔ (∃ᶠ (x : α) in f, p x) ∧ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : InvolutiveNeg β<VAR>h1 : Antiperiodic f c₁<VAR>h2 : Antiperiodic f c₂<GOAL>Periodic f (c₁ - c₂)