ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<VAR>h : (minpoly K f).IsRoot μ<VAR>p : K[X]<VAR>hp : minpoly K f = (X - C μ) * p<VAR>con : LinearMap.ker (f - (algebraMap K (End K V)) μ) = ⊥<VAR>u : (V →ₗ[K] V)ˣ<VAR>hu : ↑u = f - (algebraMap K (End K V)) μ<VAR>p_ne_0 : p ≠ 0<VAR>this : (aeval f) p = 0<VAR>h_deg : (minpoly K f).degree ≤ p.degree<GOAL>False
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<VAR>h : (minpoly K f).IsRoot μ<VAR>p : K[X]<VAR>hp : minpoly K f = (X - C μ) * p<VAR>con : LinearMap.ker (f - (algebraMap K (End K V)) μ) = ⊥<VAR>u : (V →ₗ[K] V)ˣ<VAR>hu : ↑u = f - (algebraMap K (End K V)) μ<VAR>p_ne_0 : p ≠ 0<VAR>this : (aeval f) p = 0<VAR>h_deg : 1 + ↑p.natDegree ≤ ↑p.natDegree<GOAL>False
<VAR>Ω : Type u_1<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁴ : SMul R ℝ≥0<VAR>inst✝³ : SMul R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝ : TopologicalSpace Ω<GOAL>testAgainstNN 0 = 0
<VAR>Ω : Type u_1<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁴ : SMul R ℝ≥0<VAR>inst✝³ : SMul R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝ : TopologicalSpace Ω<VAR>x✝ : Ω →ᵇ ℝ≥0<GOAL>testAgainstNN 0 x✝ = 0 x✝
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>W.Nonsingular x y ↔ W.Equation x y ∧ (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>inst✝ : F.IsEquivalence<VAR>h : HasStrongEpiMonoFactorisations C<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>Nonempty (StrongEpiMonoFactorisation f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>inst✝ : F.IsEquivalence<VAR>h : HasStrongEpiMonoFactorisations C<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some<GOAL>Nonempty (StrongEpiMonoFactorisation f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>inst✝ : F.IsEquivalence<VAR>h : HasStrongEpiMonoFactorisations C<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some<VAR>this : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)<GOAL>Nonempty (StrongEpiMonoFactorisation f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>inst✝ : F.IsEquivalence<VAR>h : HasStrongEpiMonoFactorisations C<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some<VAR>this✝ : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)<VAR>this : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e)<GOAL>Nonempty (StrongEpiMonoFactorisation f)
<VAR>p : ℝ × ℝ<GOAL>HasFDerivAt (↑polarCoord.symm) (LinearMap.toContinuousLinearMap ((Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)) !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2])) p
<VAR>p : ℝ × ℝ<GOAL>HasFDerivAt (↑polarCoord.symm) ((cos p.2 • ContinuousLinearMap.fst ℝ ℝ ℝ + (-p.1 * sin p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ).prod (sin p.2 • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 * cos p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ)) p
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>hp : p ≠ 0<GOAL>∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>hp : Nat.Prime p<GOAL>∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>hp : Nat.Prime p<VAR>N : ℕ<VAR>ih : ∀ m < N, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>hn : f.natDegree = N<GOAL>∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>hp : Nat.Prime p<VAR>N : ℕ<VAR>ih : ∀ m < N, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>hn : f.natDegree = N<VAR>h : f.Separable<GOAL>∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>hp : Nat.Prime p<VAR>N : ℕ<VAR>ih : ∀ m < N, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>hn : f.natDegree = N<VAR>h1 : ¬f.Separable<VAR>g : F[X]<VAR>hg : Irreducible g<VAR>hgf : (expand F p) g = f<GOAL>∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : DivisionSemiring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module Rᵐᵒᵖ M<VAR>inst✝¹ : Module R M<VAR>inst✝ : SMulCommClass R Rᵐᵒᵖ M<GOAL>1⁻¹ = 1
<VAR>α : Type u<VAR>i l p : Nat<VAR>a : Array α<VAR>h : a.size ≤ l<GOAL>a.extract p l = a.extract p a.size
<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<VAR>s : Set E<GOAL>(convexHull R) s = ⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t
<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<VAR>s : Set E<GOAL>(convexHull R) s ⊆ ⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t
<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<VAR>s : Set E<GOAL>⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t ⊆ (convexHull R) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>ha hb : 1 ≤ 1<GOAL>1 * 1 = 1
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>x : X<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : Nonempty N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<GOAL>(fun x_1 x_2 => x_1 * x_2) ⟦p⟧ ⟦q⟧ = ⟦transAt i q p⟧
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>x : X<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : Nonempty N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<GOAL>(fun x_1 x_2 => x_1 * x_2) ⟦p⟧ ⟦q⟧ = ⟦fromLoop (Classical.arbitrary N) (Path.trans (toLoop (Classical.arbitrary N) q) (toLoop (Classical.arbitrary N) p))⟧
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>x : X<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : Nonempty N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<GOAL>(loopHomeo (Classical.arbitrary N)).symm (Path.trans ((loopHomeo (Classical.arbitrary N)).toEquiv q) ((loopHomeo (Classical.arbitrary N)).toEquiv p)) ≈ fromLoop (Classical.arbitrary N) (Path.trans (toLoop (Classical.arbitrary N) q) (toLoop (Classical.arbitrary N) p))
<VAR>m n : ℕ<VAR>hc : m.Coprime n<VAR>hm : IsSquare (-1)<VAR>hn : IsSquare (-1)<VAR>this : IsSquare (-1)<GOAL>IsSquare (-1)
<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 - p) b = toIcoMod hp a b - p
<VAR>k m n : Nat<GOAL>k.Coprime (m * n) ↔ k.Coprime m ∧ k.Coprime n
<VAR>α : Sort u_1<VAR>inst✝ : DecidableEq α<VAR>a b x : α<GOAL>x ≠ a → x ≠ b → (swap a b) x = x
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₁₂ : Type u_3<VAR>C₂₃ : Type u_4<VAR>C₃ : Type u_5<VAR>C₄ : Type u_6<VAR>inst✝⁹ : Category.{u_15, u_1} C₁<VAR>inst✝⁸ : Category.{u_14, u_2} C₂<VAR>inst✝⁷ : Category.{u_12, u_5} C₃<VAR>inst✝⁶ : Category.{u_11, u_6} C₄<VAR>inst✝⁵ : Category.{u_13, u_3} C₁₂<VAR>inst✝⁴ : Category.{u_17, u_4} C₂₃<VAR>F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂<VAR>G : C₁₂ ⥤ C₃ ⥤ C₄<VAR>F : C₁ ⥤ C₂₃ ⥤ C₄<VAR>G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃<VAR>associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : BifunctorComp₁₂IndexData r<VAR>ρ₂₃ : BifunctorComp₂₃IndexData r<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<VAR>H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<GOAL>ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ (mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j = ((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₁₂ : Type u_3<VAR>C₂₃ : Type u_4<VAR>C₃ : Type u_5<VAR>C₄ : Type u_6<VAR>inst✝⁹ : Category.{u_15, u_1} C₁<VAR>inst✝⁸ : Category.{u_14, u_2} C₂<VAR>inst✝⁷ : Category.{u_12, u_5} C₃<VAR>inst✝⁶ : Category.{u_11, u_6} C₄<VAR>inst✝⁵ : Category.{u_13, u_3} C₁₂<VAR>inst✝⁴ : Category.{u_17, u_4} C₂₃<VAR>F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂<VAR>G : C₁₂ ⥤ C₃ ⥤ C₄<VAR>F : C₁ ⥤ C₂₃ ⥤ C₄<VAR>G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃<VAR>associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : BifunctorComp₁₂IndexData r<VAR>ρ₂₃ : BifunctorComp₂₃IndexData r<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<VAR>H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<VAR>this : ((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<GOAL>ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ (mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j = ((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₁₂ : Type u_3<VAR>C₂₃ : Type u_4<VAR>C₃ : Type u_5<VAR>C₄ : Type u_6<VAR>inst✝⁹ : Category.{u_15, u_1} C₁<VAR>inst✝⁸ : Category.{u_14, u_2} C₂<VAR>inst✝⁷ : Category.{u_12, u_5} C₃<VAR>inst✝⁶ : Category.{u_11, u_6} C₄<VAR>inst✝⁵ : Category.{u_13, u_3} C₁₂<VAR>inst✝⁴ : Category.{u_17, u_4} C₂₃<VAR>F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂<VAR>G : C₁₂ ⥤ C₃ ⥤ C₄<VAR>F : C₁ ⥤ C₂₃ ⥤ C₄<VAR>G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃<VAR>associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : BifunctorComp₁₂IndexData r<VAR>ρ₂₃ : BifunctorComp₂₃IndexData r<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<VAR>H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<VAR>this✝ : ((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<VAR>this : ((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<GOAL>ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ (mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j = ((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₁₂ : Type u_3<VAR>C₂₃ : Type u_4<VAR>C₃ : Type u_5<VAR>C₄ : Type u_6<VAR>inst✝⁹ : Category.{u_15, u_1} C₁<VAR>inst✝⁸ : Category.{u_14, u_2} C₂<VAR>inst✝⁷ : Category.{u_12, u_5} C₃<VAR>inst✝⁶ : Category.{u_11, u_6} C₄<VAR>inst✝⁵ : Category.{u_13, u_3} C₁₂<VAR>inst✝⁴ : Category.{u_17, u_4} C₂₃<VAR>F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂<VAR>G : C₁₂ ⥤ C₃ ⥤ C₄<VAR>F : C₁ ⥤ C₂₃ ⥤ C₄<VAR>G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃<VAR>associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : BifunctorComp₁₂IndexData r<VAR>ρ₂₃ : BifunctorComp₂₃IndexData r<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<VAR>H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<VAR>this✝ : ((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<VAR>this : ((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<GOAL>ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ (mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).inv j ≫ mapMap ((((mapTrifunctorMapNatTrans associator.hom I₁ I₂ I₃).app X₁).app X₂).app X₃) r j ≫ (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j = ((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₁₂ : Type u_3<VAR>C₂₃ : Type u_4<VAR>C₃ : Type u_5<VAR>C₄ : Type u_6<VAR>inst✝⁹ : Category.{u_15, u_1} C₁<VAR>inst✝⁸ : Category.{u_14, u_2} C₂<VAR>inst✝⁷ : Category.{u_12, u_5} C₃<VAR>inst✝⁶ : Category.{u_11, u_6} C₄<VAR>inst✝⁵ : Category.{u_13, u_3} C₁₂<VAR>inst✝⁴ : Category.{u_17, u_4} C₂₃<VAR>F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂<VAR>G : C₁₂ ⥤ C₃ ⥤ C₄<VAR>F : C₁ ⥤ C₂₃ ⥤ C₄<VAR>G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃<VAR>associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : BifunctorComp₁₂IndexData r<VAR>ρ₂₃ : BifunctorComp₂₃IndexData r<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<VAR>H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<VAR>this✝ : ((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<VAR>this : ((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<GOAL>((associator.hom.app (X₁ (i₁, i₂, i₃).1)).app (X₂ (i₁, i₂, i₃).2.1)).app (X₃ (i₁, i₂, i₃).2.2) ≫ (((mapTrifunctorObj (bifunctorComp₂₃ F G₂₃) X₁ I₂ I₃).obj X₂).obj X₃).ιMapObj r (i₁, i₂, i₃) j h ≫ (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j = ((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫ ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k✝ : ℕ<VAR>N N₁ N₂ : LieSubmodule R L M<VAR>k : ℕ<GOAL>ucs k N = ⊤ ↔ LieModule.lowerCentralSeries R L M k ≤ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k✝ : ℕ<VAR>N N₁ N₂ : LieSubmodule R L M<VAR>k : ℕ<GOAL>lcs k ⊤ ≤ N ↔ LieModule.lowerCentralSeries R L M k ≤ N
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>h : Coplanar k s<GOAL>FiniteDimensional k ↥(vectorSpan k s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>h : Coplanar k s<GOAL>2 < Cardinal.aleph0
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>φ : k⟦X⟧<GOAL>(coeff k n) φ⁻¹ = if n = 0 then ((constantCoeff k) φ)⁻¹ else -((constantCoeff k) φ)⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff k x.1) φ * (coeff k x.2) φ⁻¹ else 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Countable ι<VAR>inst✝ : T2Space α<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), AnalyticSet (s n)<VAR>i₀ : ι<GOAL>AnalyticSet (⋂ n, s n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Countable ι<VAR>inst✝ : T2Space α<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), AnalyticSet (s n)<VAR>i₀ : ι<VAR>β : ι → Type<VAR>hβ : (n : ι) → TopologicalSpace (β n)<VAR>h'β : ∀ (n : ι), PolishSpace (β n)<VAR>f : (n : ι) → β n → α<VAR>f_cont : ∀ (n : ι), Continuous (f n)<VAR>f_range : ∀ (n : ι), range (f n) = s n<GOAL>AnalyticSet (⋂ n, s n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Countable ι<VAR>inst✝ : T2Space α<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), AnalyticSet (s n)<VAR>i₀ : ι<VAR>β : ι → Type<VAR>hβ : (n : ι) → TopologicalSpace (β n)<VAR>h'β : ∀ (n : ι), PolishSpace (β n)<VAR>f : (n : ι) → β n → α<VAR>f_cont : ∀ (n : ι), Continuous (f n)<VAR>f_range : ∀ (n : ι), range (f n) = s n<VAR>γ : Type u_2 := (n : ι) → β n<VAR>t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}<GOAL>AnalyticSet (⋂ n, s n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Countable ι<VAR>inst✝ : T2Space α<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), AnalyticSet (s n)<VAR>i₀ : ι<VAR>β : ι → Type<VAR>hβ : (n : ι) → TopologicalSpace (β n)<VAR>h'β : ∀ (n : ι), PolishSpace (β n)<VAR>f : (n : ι) → β n → α<VAR>f_cont : ∀ (n : ι), Continuous (f n)<VAR>f_range : ∀ (n : ι), range (f n) = s n<VAR>γ : Type u_2 := (n : ι) → β n<VAR>t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}<VAR>t_closed : IsClosed t<GOAL>AnalyticSet (⋂ n, s n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Countable ι<VAR>inst✝ : T2Space α<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), AnalyticSet (s n)<VAR>i₀ : ι<VAR>β : ι → Type<VAR>hβ : (n : ι) → TopologicalSpace (β n)<VAR>h'β : ∀ (n : ι), PolishSpace (β n)<VAR>f : (n : ι) → β n → α<VAR>f_cont : ∀ (n : ι), Continuous (f n)<VAR>f_range : ∀ (n : ι), range (f n) = s n<VAR>γ : Type u_2 := (n : ι) → β n<VAR>t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}<VAR>t_closed : IsClosed t<VAR>this : PolishSpace ↑t<GOAL>AnalyticSet (⋂ n, s n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Countable ι<VAR>inst✝ : T2Space α<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), AnalyticSet (s n)<VAR>i₀ : ι<VAR>β : ι → Type<VAR>hβ : (n : ι) → TopologicalSpace (β n)<VAR>h'β : ∀ (n : ι), PolishSpace (β n)<VAR>f : (n : ι) → β n → α<VAR>f_cont : ∀ (n : ι), Continuous (f n)<VAR>f_range : ∀ (n : ι), range (f n) = s n<VAR>γ : Type u_2 := (n : ι) → β n<VAR>t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}<VAR>t_closed : IsClosed t<VAR>this : PolishSpace ↑t<VAR>F : ↑t → α := fun x => f i₀ (↑x i₀)<GOAL>AnalyticSet (⋂ n, s n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Countable ι<VAR>inst✝ : T2Space α<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), AnalyticSet (s n)<VAR>i₀ : ι<VAR>β : ι → Type<VAR>hβ : (n : ι) → TopologicalSpace (β n)<VAR>h'β : ∀ (n : ι), PolishSpace (β n)<VAR>f : (n : ι) → β n → α<VAR>f_cont : ∀ (n : ι), Continuous (f n)<VAR>f_range : ∀ (n : ι), range (f n) = s n<VAR>γ : Type u_2 := (n : ι) → β n<VAR>t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}<VAR>t_closed : IsClosed t<VAR>this : PolishSpace ↑t<VAR>F : ↑t → α := fun x => f i₀ (↑x i₀)<VAR>F_cont : Continuous F<GOAL>AnalyticSet (⋂ n, s n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Countable ι<VAR>inst✝ : T2Space α<VAR>s : ι → Set α<VAR>hs : ∀ (n : ι), AnalyticSet (s n)<VAR>i₀ : ι<VAR>β : ι → Type<VAR>hβ : (n : ι) → TopologicalSpace (β n)<VAR>h'β : ∀ (n : ι), PolishSpace (β n)<VAR>f : (n : ι) → β n → α<VAR>f_cont : ∀ (n : ι), Continuous (f n)<VAR>f_range : ∀ (n : ι), range (f n) = s n<VAR>γ : Type u_2 := (n : ι) → β n<VAR>t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}<VAR>t_closed : IsClosed t<VAR>this : PolishSpace ↑t<VAR>F : ↑t → α := fun x => f i₀ (↑x i₀)<VAR>F_cont : Continuous F<VAR>F_range : range F = ⋂ n, s n<GOAL>AnalyticSet (range F)
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>β : Type u_1<VAR>n : ℕ<VAR>s✝ : Finset β<VAR>f : β → Holor α ds<VAR>this : DecidableEq β := Classical.decEq β<VAR>x : β<VAR>s : Finset β<VAR>h_x_notin_s : x ∉ s<VAR>ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)<VAR>h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)<GOAL>CPRankMax ((insert x s).card * n) (∑ x ∈ insert x s, f x)
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>β : Type u_1<VAR>n : ℕ<VAR>s✝ : Finset β<VAR>f : β → Holor α ds<VAR>this : DecidableEq β := Classical.decEq β<VAR>x : β<VAR>s : Finset β<VAR>h_x_notin_s : x ∉ s<VAR>ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)<VAR>h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)<GOAL>CPRankMax ((s.card + 1) * n) (f x + ∑ x ∈ s, f x)
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>β : Type u_1<VAR>n : ℕ<VAR>s✝ : Finset β<VAR>f : β → Holor α ds<VAR>this : DecidableEq β := Classical.decEq β<VAR>x : β<VAR>s : Finset β<VAR>h_x_notin_s : x ∉ s<VAR>ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)<VAR>h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)<GOAL>CPRankMax (s.card * n + 1 * n) (f x + ∑ x ∈ s, f x)