ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝ : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N : LieSubmodule R L M<GOAL>(∃ k, lowerCentralSeries R L (↥↑N) k = ⊥) ↔ ∃ k, LieSubmodule.lcs 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✝ : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N : LieSubmodule R L M<VAR>k : ℕ<GOAL>lowerCentralSeries R L (↥↑N) k = ⊥ ↔ LieSubmodule.lcs k N = ⊥
<VAR>x y : ℝ<GOAL>↑(cos (2 * x)) = ↑(cos x ^ 2 - sin x ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>a : ℝ≥0<GOAL>Tendsto ENNReal.toNNReal (𝓝 ↑a) (𝓝 (↑a).toNNReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>a : ℝ≥0<GOAL>Tendsto (ENNReal.toNNReal ∘ ofNNReal) (𝓝 a) (𝓝 (↑a).toNNReal)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f✝ g✝ : α → ℝ<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>f_mble : AEMeasurable f μ<VAR>g_mble : AEMeasurable g μ<VAR>s : Set α<VAR>s_mble : NullMeasurableSet s μ<GOAL>NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Icc (f p.1) (g p.1)} (μ.prod volume)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f✝ g✝ : α → ℝ<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>f_mble : AEMeasurable f μ<VAR>g_mble : AEMeasurable g μ<VAR>s : Set α<VAR>s_mble : NullMeasurableSet s μ<GOAL>NullMeasurableSet (fun p => f p.1 ≤ p.2) (μ.prod volume)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f✝ g✝ : α → ℝ<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>f_mble : AEMeasurable f μ<VAR>g_mble : AEMeasurable g μ<VAR>s : Set α<VAR>s_mble : NullMeasurableSet s μ<GOAL>NullMeasurableSet (fun p => p.2 ≤ g p.1) (μ.prod volume)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>a : A<VAR>h : ¬IsUnit ((aeval a) (Multiset.map (fun x => X - C x) p.roots).prod)<GOAL>∃ k ∈ σ a, eval k p = 0
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>a : A<VAR>h : ¬IsUnit (List.map (⇑(aeval a)) (Multiset.map (fun x => X - C x) p.roots).toList).prod<GOAL>∃ k ∈ σ a, eval k p = 0
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>a : A<VAR>h : ¬∀ m ∈ List.map (⇑(aeval a)) (Multiset.map (fun x => X - C x) p.roots).toList, IsUnit m<GOAL>∃ k ∈ σ a, eval k p = 0
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>a : A<VAR>h : ∃ a_1 ∈ p.roots, ¬IsUnit (a - ↑ₐ a_1)<GOAL>∃ k ∈ σ a, eval k p = 0
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>a : A<VAR>r : R<VAR>r_mem : r ∈ p.roots<VAR>r_nu : ¬IsUnit (a - ↑ₐ r)<GOAL>∃ k ∈ σ a, eval k p = 0
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : StarRing R<VAR>inst✝¹¹ : NonUnitalSemiring A<VAR>inst✝¹⁰ : StarRing A<VAR>inst✝⁹ : Module R A<VAR>inst✝⁸ : IsScalarTower R A A<VAR>inst✝⁷ : SMulCommClass R A A<VAR>inst✝⁶ : StarModule R A<VAR>inst✝⁵ : NonUnitalSemiring B<VAR>inst✝⁴ : StarRing B<VAR>inst✝³ : Module R B<VAR>inst✝² : IsScalarTower R B B<VAR>inst✝¹ : SMulCommClass R B B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>this : ∀ (t : Set A), NonUnitalAlgebra.adjoin R (star t) ≤ star (NonUnitalAlgebra.adjoin R t)<GOAL>star (NonUnitalAlgebra.adjoin R s) ≤ NonUnitalAlgebra.adjoin R (star s)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝⁵ : Monoid β<VAR>inst✝⁴ : Monoid γ<VAR>inst✝³ : FunLike F β γ<VAR>M : ι → Type u_6<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : DecidableEq ι<VAR>f g : ((i : ι) → M i) →* γ<VAR>h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)<GOAL>f = g
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝⁵ : Monoid β<VAR>inst✝⁴ : Monoid γ<VAR>inst✝³ : FunLike F β γ<VAR>M : ι → Type u_6<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : DecidableEq ι<VAR>f g : ((i : ι) → M i) →* γ<VAR>h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)<VAR>val✝ : Fintype ι<GOAL>f = g
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝⁵ : Monoid β<VAR>inst✝⁴ : Monoid γ<VAR>inst✝³ : FunLike F β γ<VAR>M : ι → Type u_6<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : DecidableEq ι<VAR>f g : ((i : ι) → M i) →* γ<VAR>h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)<VAR>val✝ : Fintype ι<VAR>x : (i : ι) → M i<GOAL>f x = g x
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝⁵ : Monoid β<VAR>inst✝⁴ : Monoid γ<VAR>inst✝³ : FunLike F β γ<VAR>M : ι → Type u_6<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>inst✝¹ : Finite ι<VAR>inst✝ : DecidableEq ι<VAR>f g : ((i : ι) → M i) →* γ<VAR>h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)<VAR>val✝ : Fintype ι<VAR>x : (i : ι) → M i<GOAL>univ.noncommProd (fun i => f (Pi.mulSingle i (x i))) ⋯ = univ.noncommProd (fun i => g (Pi.mulSingle i (x i))) ⋯
<VAR>α β : Type u<VAR>c : Cardinal.{?u.232884}<GOAL>2 ≤ #α ↔ ∃ x y, x ≠ y
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>c : Cofan Z<VAR>f : Fan fun x => op (Z x)<VAR>hc : IsColimit c<VAR>hf : IsLimit f<VAR>c' : Cofan Z<GOAL>(hc.desc c').op ≫ (opCoproductIsoProduct' hc hf).hom = hf.lift c'.op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>c : Cofan Z<VAR>f : Fan fun x => op (Z x)<VAR>hc : IsColimit c<VAR>hf : IsLimit f<VAR>c' : Cofan Z<VAR>x✝ : Discrete α<VAR>j : α<GOAL>(c.ι.app { as := j } ≫ (hc.desc c').op.unop).op = (c.ι.app { as := j } ≫ (hf.lift c'.op ≫ (opCoproductIsoProduct' hc hf).inv).unop).op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>c : Cofan Z<VAR>f : Fan fun x => op (Z x)<VAR>hc : IsColimit c<VAR>hf : IsLimit f<VAR>c' : Cofan Z<VAR>x✝ : Discrete α<VAR>j : α<GOAL>(c'.ι.app { as := j }).op = hf.lift (Fan.mk (op c'.pt) fun a => (c'.inj a).op) ≫ (opCoproductIsoProduct' hc hf).inv ≫ (c.ι.app { as := j }).op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>c : Cofan Z<VAR>f : Fan fun x => op (Z x)<VAR>hc : IsColimit c<VAR>hf : IsLimit f<VAR>c' : Cofan Z<VAR>x✝ : Discrete α<VAR>j : α<GOAL>(c'.ι.app { as := j }).op = (Fan.mk (op c'.pt) fun a => (c'.inj a).op).π.app { as := j }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<GOAL>Icc a b \ {a, b} = Ioo a b
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : Filter X<VAR>ht : IsCompact t<VAR>hf : Disjoint f (cocompact X)<GOAL>f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (univ ×ˢ t)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : Filter X<VAR>ht : IsCompact t<VAR>hf : Disjoint f (cocompact X)<VAR>K : Set X<VAR>hKf : K ∈ f<VAR>hK : IsCompact K<GOAL>f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (univ ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Div α<VAR>a b : α<GOAL>some a / some b = some (a / b)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>q n : ℕ<GOAL>(Q q ≫ Q q).f n = (Q q).f n
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>x : E<GOAL>x ∈ Submodule.map (LinearMap.fst R E F) f.graph ↔ x ∈ f.domain
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>x : E<GOAL>(∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1) ↔ x ∈ f.domain
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n : ℕ+<VAR>g : L ≃+* L<GOAL>∃ m, ∀ t ∈ rootsOfUnity n L, g ↑t = ↑(t ^ m)
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : Semiring R✝<VAR>inst✝¹⁰ : AddCommMonoid M✝<VAR>inst✝⁹ : Module R✝ M✝<VAR>P : Type u_3<VAR>inst✝⁸ : AddCommMonoid P<VAR>inst✝⁷ : Module R✝ P<VAR>f : M✝ →ₗ[R✝] P<VAR>R : Type u_4<VAR>S : Type u_5<VAR>M : Type u_6<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module S M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R S M<VAR>h : Surjective ⇑(algebraMap R S)<VAR>X : Finset M<GOAL>(restrictScalars R (span S ↑X)).FG
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹¹ : Semiring R✝<VAR>inst✝¹⁰ : AddCommMonoid M✝<VAR>inst✝⁹ : Module R✝ M✝<VAR>P : Type u_3<VAR>inst✝⁸ : AddCommMonoid P<VAR>inst✝⁷ : Module R✝ P<VAR>f : M✝ →ₗ[R✝] P<VAR>R : Type u_4<VAR>S : Type u_5<VAR>M : Type u_6<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module S M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R S M<VAR>h : Surjective ⇑(algebraMap R S)<VAR>X : Finset M<GOAL>span R ↑X = restrictScalars R (span S ↑X)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<GOAL>LiouvilleWith p (↑n - x) ↔ LiouvilleWith p x
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>h : x ∈ s<GOAL>infEdist x t ≤ hausdorffEdist s t
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>h : x ∈ s<GOAL>infEdist x t ≤ (⨆ x ∈ s, infEdist x t) ⊔ ⨆ y ∈ t, infEdist y s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>h : x ∈ s<GOAL>infEdist x t ≤ ⨆ x ∈ s, infEdist x t
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>(∃ X, Associated (X ^ 3) (FermatLastTheoremForThreeGen.Solution.x S)) ∧ (∃ Y, Associated (Y ^ 3) (FermatLastTheoremForThreeGen.Solution.y S)) ∧ ∃ Z, Associated (Z ^ 3) (FermatLastTheoremForThreeGen.Solution.z S)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h₁ : IsCoprime (FermatLastTheoremForThreeGen.Solution.x S * FermatLastTheoremForThreeGen.Solution.y S) (FermatLastTheoremForThreeGen.Solution.z S)<GOAL>(∃ X, Associated (X ^ 3) (FermatLastTheoremForThreeGen.Solution.x S)) ∧ (∃ Y, Associated (Y ^ 3) (FermatLastTheoremForThreeGen.Solution.y S)) ∧ ∃ Z, Associated (Z ^ 3) (FermatLastTheoremForThreeGen.Solution.z S)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h₁ : IsCoprime (FermatLastTheoremForThreeGen.Solution.x S * FermatLastTheoremForThreeGen.Solution.y S) (FermatLastTheoremForThreeGen.Solution.z S)<VAR>h₂ : Associated (FermatLastTheoremForThreeGen.Solution.w S ^ 3) (FermatLastTheoremForThreeGen.Solution.x S * FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S)<GOAL>(∃ X, Associated (X ^ 3) (FermatLastTheoremForThreeGen.Solution.x S)) ∧ (∃ Y, Associated (Y ^ 3) (FermatLastTheoremForThreeGen.Solution.y S)) ∧ ∃ Z, Associated (Z ^ 3) (FermatLastTheoremForThreeGen.Solution.z S)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h₁ : IsCoprime (FermatLastTheoremForThreeGen.Solution.x S * FermatLastTheoremForThreeGen.Solution.y S) (FermatLastTheoremForThreeGen.Solution.z S)<VAR>h₂ : Associated (FermatLastTheoremForThreeGen.Solution.w S ^ 3) (FermatLastTheoremForThreeGen.Solution.x S * FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S)<VAR>T : 𝓞 K<VAR>h₃ : Associated (T ^ 3) (FermatLastTheoremForThreeGen.Solution.x S * FermatLastTheoremForThreeGen.Solution.y S)<GOAL>(∃ X, Associated (X ^ 3) (FermatLastTheoremForThreeGen.Solution.x S)) ∧ (∃ Y, Associated (Y ^ 3) (FermatLastTheoremForThreeGen.Solution.y S)) ∧ ∃ Z, Associated (Z ^ 3) (FermatLastTheoremForThreeGen.Solution.z S)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Group α<VAR>inst✝ : Group β<VAR>f : α → β<VAR>hf✝ hf : IsGroupHom f<VAR>a b : α<GOAL>f (a / b) = f a / f b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Monoid M<VAR>S : Set (MonoidAlgebra R M)<VAR>hS : adjoin R S = ⊤<GOAL>adjoin R (⇑(of R M) '' ⋃ f ∈ S, ↑f.support) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Monoid M<VAR>S : Set (MonoidAlgebra R M)<VAR>hS : adjoin R S = ⊤<GOAL>⇑(of R M) '' ⋃ f ∈ S, ↑f.support = ⋃ f ∈ S, ⇑(of R M) '' ↑f.support
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P✝ Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>P : Cubic R<GOAL>(fun f => { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) ((fun P => ⟨P.toPoly, ⋯⟩) P) = P
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>f : { p // p.degree ≤ 3 }<GOAL>(fun P => ⟨P.toPoly, ⋯⟩) ((fun f => { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f) = f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>f : { p // p.degree ≤ 3 }<VAR>n : ℕ<GOAL>{ a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff (4 + n) = (↑f).coeff (4 + n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>f : { p // p.degree ≤ 3 }<VAR>n : ℕ<VAR>h3 : 3 < 4 + n<GOAL>{ a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff (4 + n) = (↑f).coeff (4 + n)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : X.Opens<VAR>r : ↑Γ(X, U)<GOAL>f ''ᵁ X.basicOpen r = Y.basicOpen ((Hom.appIso f U).inv r)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : X.Opens<VAR>r : ↑Γ(X, U)<VAR>e : f ⁻¹ᵁ Y.basicOpen ((Hom.appIso f U).inv r) = X.basicOpen ((Hom.app f (f ''ᵁ U)) ((Hom.appIso f U).inv r))<GOAL>f ''ᵁ X.basicOpen r = Y.basicOpen ((Hom.appIso f U).inv r)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : X.Opens<VAR>r : ↑Γ(X, U)<VAR>e : f ⁻¹ᵁ Y.basicOpen ((Hom.appIso f U).inv r) = X.basicOpen r<GOAL>f ''ᵁ X.basicOpen r = Y.basicOpen ((Hom.appIso f U).inv r)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : X.Opens<VAR>r : ↑Γ(X, U)<VAR>e : f ⁻¹ᵁ Y.basicOpen ((Hom.appIso f U).inv r) = f ⁻¹ᵁ f ''ᵁ U ⊓ X.basicOpen r<GOAL>X.basicOpen r ≤ f ⁻¹ᵁ f ''ᵁ U
<VAR>μ ν : YoungDiagram<GOAL>μ.transpose = ν.transpose ↔ μ = ν
<VAR>μ ν : YoungDiagram<GOAL>μ = ν.transpose.transpose ↔ μ = ν
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : [n] ⟶ Δ'<VAR>hθ : ¬Mono θ<GOAL>X.map θ.op ≫ PInfty.f n = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : [n] ⟶ Δ'<VAR>hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)<GOAL>X.map θ.op ≫ PInfty.f n = 0
<VAR>C✝ : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C✝<VAR>inst✝⁹ : MonoidalCategory C✝<VAR>inst✝⁸ : BraidedCategory C✝<VAR>D : Type u₂<VAR>inst✝⁷ : Category.{v₂, u₂} D<VAR>inst✝⁶ : MonoidalCategory D<VAR>inst✝⁵ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} E<VAR>inst✝³ : MonoidalCategory E<VAR>inst✝² : BraidedCategory E<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>i : SymmetricCategory C<GOAL>(fun X Y => (β_ Y X).symm) = β_
<VAR>C✝ : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C✝<VAR>inst✝⁹ : MonoidalCategory C✝<VAR>inst✝⁸ : BraidedCategory C✝<VAR>D : Type u₂<VAR>inst✝⁷ : Category.{v₂, u₂} D<VAR>inst✝⁶ : MonoidalCategory D<VAR>inst✝⁵ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} E<VAR>inst✝³ : MonoidalCategory E<VAR>inst✝² : BraidedCategory E<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>i : SymmetricCategory C<VAR>X Y : C<GOAL>(β_ Y X).symm = β_ X Y
<VAR>α : Type u_1<VAR>R✝ : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>F : Type u_5<VAR>inst✝⁵ : FunLike F M M₂<VAR>inst✝⁴ : AddMonoidHomClass F M M₂<VAR>f : F<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : DivisionRing R<VAR>inst✝² : DivisionRing S<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module S M₂<VAR>z : ℤ<VAR>x : M<GOAL>f ((↑z)⁻¹ • x) = (↑z)⁻¹ • f x
<VAR>α : Type u_1<VAR>R✝ : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>F : Type u_5<VAR>inst✝⁵ : FunLike F M M₂<VAR>inst✝⁴ : AddMonoidHomClass F M M₂<VAR>f : F<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : DivisionRing R<VAR>inst✝² : DivisionRing S<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module S M₂<VAR>x : M<VAR>n : ℕ<GOAL>f ((↑↑n)⁻¹ • x) = (↑↑n)⁻¹ • f x
<VAR>α : Type u_1<VAR>R✝ : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>F : Type u_5<VAR>inst✝⁵ : FunLike F M M₂<VAR>inst✝⁴ : AddMonoidHomClass F M M₂<VAR>f : F<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : DivisionRing R<VAR>inst✝² : DivisionRing S<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module S M₂<VAR>x : M<VAR>n : ℕ<GOAL>f ((↑(-↑n))⁻¹ • x) = (↑(-↑n))⁻¹ • f x
<VAR>𝕜 : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E✝<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : InnerProductSpace 𝕜 E✝<VAR>inst✝⁶ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E✝<VAR>inst✝⁵ : HasOrthogonalProjection K<VAR>E : Type u_4<VAR>E' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace 𝕜 E'<VAR>f : E ≃ₗᵢ[𝕜] E'<VAR>p : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection p<VAR>x : E'<GOAL>↑((orthogonalProjection (Submodule.map (↑f.toLinearEquiv) p)) x) = f ↑((orthogonalProjection p) (f.symm x))
<VAR>f : StieltjesFunction<GOAL>f.outer.trim = f.outer
<VAR>f : StieltjesFunction<VAR>s : Set ℝ<GOAL>f.outer.trim s ≤ f.outer s
<VAR>f : StieltjesFunction<VAR>s : Set ℝ<GOAL>⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), f.outer t ≤ f.outer s
<VAR>f : StieltjesFunction<VAR>s : Set ℝ<VAR>t : ℕ → Set ℝ<VAR>ht : s ⊆ ⋃ i, t i<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (t i) < ⊤<GOAL>⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), f.outer t ≤ ∑' (i : ℕ), f.length (t i) + ↑ε
<VAR>f : StieltjesFunction<VAR>s : Set ℝ<VAR>t : ℕ → Set ℝ<VAR>ht : s ⊆ ⋃ i, t i<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (t i) < ⊤<VAR>ε' : ℕ → ℝ≥0<VAR>ε'0 : ∀ (i : ℕ), 0 < ε' i<VAR>hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε<GOAL>⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), f.outer t ≤ ∑' (i : ℕ), f.length (t i) + ↑ε
<VAR>f : StieltjesFunction<VAR>s : Set ℝ<VAR>t : ℕ → Set ℝ<VAR>ht : s ⊆ ⋃ i, t i<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (t i) < ⊤<VAR>ε' : ℕ → ℝ≥0<VAR>ε'0 : ∀ (i : ℕ), 0 < ε' i<VAR>hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε<GOAL>⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), f.outer t ≤ ∑' (i : ℕ), f.length (t i) + ∑' (i : ℕ), ↑(ε' i)
<VAR>f : StieltjesFunction<VAR>s : Set ℝ<VAR>t : ℕ → Set ℝ<VAR>ht : s ⊆ ⋃ i, t i<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (t i) < ⊤<VAR>ε' : ℕ → ℝ≥0<VAR>ε'0 : ∀ (i : ℕ), 0 < ε' i<VAR>hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε<GOAL>⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), f.outer t ≤ ∑' (a : ℕ), (f.length (t a) + ↑(ε' a))
<VAR>f : StieltjesFunction<VAR>s : Set ℝ<VAR>t : ℕ → Set ℝ<VAR>ht : s ⊆ ⋃ i, t i<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (t i) < ⊤<VAR>ε' : ℕ → ℝ≥0<VAR>ε'0 : ∀ (i : ℕ), 0 < ε' i<VAR>hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε<VAR>g : ℕ → Set ℝ<VAR>hg : ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ f.outer (g i) ≤ f.length (t i) + ofReal ↑(ε' i)<GOAL>⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), f.outer t ≤ ∑' (a : ℕ), (f.length (t a) + ↑(ε' a))
<VAR>f : StieltjesFunction<VAR>s : Set ℝ<VAR>t : ℕ → Set ℝ<VAR>ht : s ⊆ ⋃ i, t i<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (t i) < ⊤<VAR>ε' : ℕ → ℝ≥0<VAR>ε'0 : ∀ (i : ℕ), 0 < ε' i<VAR>hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε<VAR>g : ℕ → Set ℝ<VAR>hg : ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ f.outer (g i) ≤ f.length (t i) + ↑(ε' i)<GOAL>⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), f.outer t ≤ ∑' (a : ℕ), (f.length (t a) + ↑(ε' a))
<VAR>f : StieltjesFunction<VAR>s : Set ℝ<VAR>t : ℕ → Set ℝ<VAR>ht : s ⊆ ⋃ i, t i<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (t i) < ⊤<VAR>ε' : ℕ → ℝ≥0<VAR>ε'0 : ∀ (i : ℕ), 0 < ε' i<VAR>hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε<VAR>g : ℕ → Set ℝ<VAR>hg : ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ f.outer (g i) ≤ f.length (t i) + ↑(ε' i)<GOAL>⨅ (_ : s ⊆ iUnion g), ⨅ (_ : MeasurableSet (iUnion g)), f.outer (iUnion g) ≤ ∑' (a : ℕ), (f.length (t a) + ↑(ε' a))
<VAR>f : StieltjesFunction<VAR>s : Set ℝ<VAR>t : ℕ → Set ℝ<VAR>ht : s ⊆ ⋃ i, t i<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (t i) < ⊤<VAR>ε' : ℕ → ℝ≥0<VAR>ε'0 : ∀ (i : ℕ), 0 < ε' i<VAR>hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε<VAR>g : ℕ → Set ℝ<VAR>hg : ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ f.outer (g i) ≤ f.length (t i) + ↑(ε' i)<GOAL>⨅ (_ : MeasurableSet (iUnion g)), f.outer (iUnion g) ≤ ∑' (a : ℕ), (f.length (t a) + ↑(ε' a))
<VAR>f : StieltjesFunction<VAR>s : Set ℝ<VAR>t : ℕ → Set ℝ<VAR>ht : s ⊆ ⋃ i, t i<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (t i) < ⊤<VAR>ε' : ℕ → ℝ≥0<VAR>ε'0 : ∀ (i : ℕ), 0 < ε' i<VAR>hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε<VAR>g : ℕ → Set ℝ<VAR>hg : ∀ (i : ℕ), t i ⊆ g i ∧ MeasurableSet (g i) ∧ f.outer (g i) ≤ f.length (t i) + ↑(ε' i)<GOAL>f.outer (iUnion g) ≤ ∑' (a : ℕ), (f.length (t a) + ↑(ε' a))
<VAR>K : Type u<VAR>inst✝ : Field K<GOAL>num 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>n : ℕ<VAR>hs : autoParam s.Finite _auto✝<GOAL>s.ncard = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n