ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : Nontrivial R<GOAL>W.polynomial ≠ 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : Nontrivial R<GOAL>{ a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly, d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly }.toPoly ≠ 0
<VAR>x : ↑I<GOAL>1 - ↑x ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s✝ t u : Set α<VAR>m : MeasurableSpace α<VAR>s : Set (Set α)<VAR>hs : s.Countable<VAR>h : ∀ t ∈ s, MeasurableSet t<GOAL>MeasurableSet (⋃₀ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s✝ t u : Set α<VAR>m : MeasurableSpace α<VAR>s : Set (Set α)<VAR>hs : s.Countable<VAR>h : ∀ t ∈ s, MeasurableSet t<GOAL>MeasurableSet (⋃ i ∈ s, i)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r : Rˣ<VAR>x : R<VAR>x_eq : x = r • r⁻¹ • x<GOAL>r • r⁻¹ • x ∈ σ (r • a) ↔ x ∈ r • σ a
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r : Rˣ<VAR>x : R<VAR>x_eq : x = r • r⁻¹ • x<GOAL>r⁻¹ • x ∈ σ a ↔ x ∈ r • σ a
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J J' I : Ideal S<VAR>h : I.IsPrime<GOAL>(⊤.prod I).IsPrime
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J J' I : Ideal S<VAR>h : I.IsPrime<VAR>this : (I.prod ⊤).IsPrime := isPrime_ideal_prod_top<GOAL>(⊤.prod I).IsPrime
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J J' I : Ideal S<VAR>h : I.IsPrime<VAR>this : (I.prod ⊤).IsPrime := isPrime_ideal_prod_top<GOAL>(map (↑RingEquiv.prodComm) (I.prod ⊤)).IsPrime
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K✝ : Type w<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Algebra F K✝<VAR>inst✝² : Algebra E K✝<VAR>inst✝¹ : IsScalarTower F E K✝<VAR>f : F[X]<VAR>hsep : f.Separable<VAR>hirr : Irreducible f<VAR>inst✝ : IsPurelyInseparable F E<VAR>K : Type v := AlgebraicClosure E<GOAL>Irreducible (Polynomial.map (algebraMap F E) f)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K✝ : Type w<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Algebra F K✝<VAR>inst✝² : Algebra E K✝<VAR>inst✝¹ : IsScalarTower F E K✝<VAR>f : F[X]<VAR>hsep : f.Separable<VAR>hirr : Irreducible f<VAR>inst✝ : IsPurelyInseparable F E<VAR>K : Type v := AlgebraicClosure E<VAR>x : K<VAR>hx : (aeval x) f = 0<GOAL>Irreducible (Polynomial.map (algebraMap F E) f)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K✝ : Type w<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Algebra F K✝<VAR>inst✝² : Algebra E K✝<VAR>inst✝¹ : IsScalarTower F E K✝<VAR>f : F[X]<VAR>hsep : f.Separable<VAR>hirr : Irreducible f<VAR>inst✝ : IsPurelyInseparable F E<VAR>K : Type v := AlgebraicClosure E<VAR>x : K<VAR>hx : (aeval x) f = 0<VAR>ha : Associated f (minpoly F x)<GOAL>Irreducible (Polynomial.map (algebraMap F E) f)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K✝ : Type w<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Algebra F K✝<VAR>inst✝² : Algebra E K✝<VAR>inst✝¹ : IsScalarTower F E K✝<VAR>f : F[X]<VAR>hsep : f.Separable<VAR>hirr : Irreducible f<VAR>inst✝ : IsPurelyInseparable F E<VAR>K : Type v := AlgebraicClosure E<VAR>x : K<VAR>hx : (aeval x) f = 0<VAR>ha : Associated f (minpoly F x)<VAR>ha' : Associated (Polynomial.map (algebraMap F E) f) (Polynomial.map (algebraMap F E) (minpoly F x))<GOAL>Irreducible (Polynomial.map (algebraMap F E) f)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K✝ : Type w<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Algebra F K✝<VAR>inst✝² : Algebra E K✝<VAR>inst✝¹ : IsScalarTower F E K✝<VAR>f : F[X]<VAR>hsep : f.Separable<VAR>hirr : Irreducible f<VAR>inst✝ : IsPurelyInseparable F E<VAR>K : Type v := AlgebraicClosure E<VAR>x : K<VAR>hx : (aeval x) f = 0<VAR>ha : Associated f (minpoly F x)<VAR>ha' : Associated (Polynomial.map (algebraMap F E) f) (Polynomial.map (algebraMap F E) (minpoly F x))<VAR>heq : Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x<GOAL>Irreducible (Polynomial.map (algebraMap F E) f)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K✝ : Type w<VAR>inst✝⁴ : Field K✝<VAR>inst✝³ : Algebra F K✝<VAR>inst✝² : Algebra E K✝<VAR>inst✝¹ : IsScalarTower F E K✝<VAR>f : F[X]<VAR>hsep : f.Separable<VAR>hirr : Irreducible f<VAR>inst✝ : IsPurelyInseparable F E<VAR>K : Type v := AlgebraicClosure E<VAR>x : K<VAR>hx : (aeval x) f = 0<VAR>ha : Associated f (minpoly F x)<VAR>ha' : Associated (Polynomial.map (algebraMap F E) f) (Polynomial.map (algebraMap F E) (minpoly F x))<VAR>heq : Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x<GOAL>Irreducible (minpoly E x)
<VAR>R : Type u_4<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>B : BilinForm S M<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>hB : B.Nondegenerate<VAR>b : Basis ι S M<GOAL>B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>h : s₁ ⊆ s₂<GOAL>(∏ x ∈ s₂ \ s₁, f x) * ∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x
<GOAL>RespectsIso fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f
<GOAL>∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), Function.Surjective ⇑e.toRingHom
<VAR>R✝ S✝ : Type u_1<VAR>inst✝¹ : CommRing R✝<VAR>inst✝ : CommRing S✝<VAR>e : R✝ ≃+* S✝<GOAL>Function.Surjective ⇑e.toRingHom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s✝ t : Set α<VAR>a b : α<VAR>f : β → α<VAR>s : Set β<VAR>H : BddAbove (f '' s)<VAR>Hne : s.Nonempty<GOAL>IsLUB (f '' s) (⨆ i, f ↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s✝ t : Set α<VAR>a b : α<VAR>f : β → α<VAR>s : Set β<VAR>H : BddAbove (f '' s)<VAR>Hne : s.Nonempty<GOAL>IsLUB (f '' s) (sSup (f '' s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>αs : ι → Type u_13<VAR>inst✝¹ : Zero M<VAR>l : (i : ι) × αs i →₀ M<VAR>inst✝ : AddCommMonoid N<VAR>f : (i : ι) × αs i → M → N<GOAL>l.sum f = ∑ i ∈ l.splitSupport, (l.split i).sum fun a b => f ⟨i, a⟩ b
<VAR>x y : ℂ<GOAL>sin (x * I) = sinh x * I
<VAR>x y : ℂ<VAR>h : I * sin (x * I) = -sinh x<GOAL>sin (x * I) = sinh x * I
<VAR>x y : ℂ<VAR>h : I * sin (x * I) = -sinh x<GOAL>sin (x * I) = -(I * sin (x * I)) * I
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c✝ d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>c : 𝔸<VAR>hd : HasDerivAt d d' x<GOAL>HasDerivAt (fun y => c * d y) (c * d') x
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c✝ d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>c : 𝔸<VAR>hd : HasDerivWithinAt d d' univ x<GOAL>HasDerivWithinAt (fun y => c * d y) (c * d') univ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>a ∈ Ico a b ↔ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>(bliminf u f fun x => False) = ⊤
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group H<VAR>inst✝¹ : MulAction G α<VAR>a : G<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x✝ : G<GOAL>x✝ ∈ stabilizer G ↑s ↔ x✝ ∈ stabilizer G s
<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>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x y : ↥M<GOAL>mk' S (↑x) y * mk' S (↑y) x = 1
<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>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x y : ↥M<GOAL>mk' S (↑y * ↑x) (y * x) = 1
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x✝ : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>i : ι<VAR>x : β i<VAR>j : ι<GOAL>(filter p (single i x)) j = (if p i then single i x else 0) j
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x✝ : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>i : ι<VAR>x : β i<VAR>j : ι<VAR>this : (if p i then single i x else 0) j = if p i then (single i x) j else 0 j<GOAL>(filter p (single i x)) j = (if p i then single i x else 0) j
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x✝ : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>i : ι<VAR>x : β i<VAR>j : ι<VAR>this : (if p i then single i x else 0) j = if p i then (single i x) j else 0<GOAL>(filter p (single i x)) j = (if p i then single i x else 0) j
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x✝ : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>i : ι<VAR>x : β i<VAR>j : ι<VAR>this : (if p i then single i x else 0) j = if p i then (single i x) j else 0<GOAL>(if p j then (single i x) j else 0) = if p i then (single i x) j else 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x✝ : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>i : ι<VAR>x : β i<VAR>this : (if p i then single i x else 0) i = if p i then (single i x) i else 0<GOAL>(if p i then (single i x) i else 0) = if p i then (single i x) i else 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x✝ : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>i : ι<VAR>x : β i<VAR>j : ι<VAR>this : (if p i then single i x else 0) j = if p i then (single i x) j else 0<VAR>hij : i ≠ j<GOAL>(if p j then (single i x) j else 0) = if p i then (single i x) j else 0
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>a : PresentedGroup M.relationsSet<GOAL>cs.mulEquiv (cs.mulEquiv.symm a) = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<GOAL>_root_.Disjoint (insert a t) s ↔ a ∉ s ∧ _root_.Disjoint s t
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<VAR>h : b = 0 → a = 0<GOAL>a * b / b = a
<VAR>d : ℕ<VAR>a b : ℤ√↑d<GOAL>a ≤ b ∨ b ≤ a
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>t : (b - a).Nonneg ∨ (-(b - a)).Nonneg<GOAL>a ≤ b ∨ b ≤ a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>inst✝ : Field k<VAR>φ : MvPowerSeries σ k<GOAL>(constantCoeff σ k) φ⁻¹ = ((constantCoeff σ k) φ)⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>H : LiftRel R s t<VAR>n : ℕ<GOAL>Computation.LiftRel (LiftRelO R (LiftRel R)) (s.drop (n + 1)).destruct (t.drop (n + 1)).destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>H : LiftRel R s t<VAR>n : ℕ<GOAL>Computation.LiftRel (LiftRelO R (LiftRel R)) ((s.drop n).destruct >>= tail.aux) ((t.drop n).destruct >>= tail.aux)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>H : LiftRel R s t<VAR>n : ℕ<GOAL>Computation.LiftRel ?R (s.drop n).destruct (t.drop n).destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>H : LiftRel R s t<VAR>n : ℕ<GOAL>∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, ?R a b → Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux a) (tail.aux b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>H : LiftRel R s t<VAR>n : ℕ<GOAL>Option (α × WSeq α) → Option (β × WSeq β) → Prop
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>H : LiftRel R s t<VAR>n : ℕ<GOAL>∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R (LiftRel R) a b → Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux a) (tail.aux b)
<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>vectorSpan ℝ (s.points '' ↑(univ.erase i)) ⟂ (s.altitude i).direction
<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>vectorSpan ℝ (s.points '' ↑(univ.erase i)) ⟂ (vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts : List α<VAR>r : List β<VAR>ys : List α<VAR>f : List α → β<GOAL>(permutationsAux2 t ts r ys f).2 = map (fun x => f (x ++ ts)) (permutationsAux2 t [] [] ys id).2 ++ r
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v r : ι → F<VAR>i : ι<VAR>x : F<VAR>hvs : Set.InjOn v ↑s<VAR>hs : s.Nonempty<VAR>hx : ∀ i ∈ s, x ≠ v i<GOAL>eval x ((interpolate s v) r) = (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v r : ι → F<VAR>i : ι<VAR>x : F<VAR>hvs : Set.InjOn v ↑s<VAR>hs : s.Nonempty<VAR>hx : ∀ i ∈ s, x ≠ v i<GOAL>(eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) / (eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * 1 i) = (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹
<VAR>α : Type u_1<VAR>inst✝ : CommSemigroup α<VAR>a c✝ c : α<GOAL>a ∣ c * a
<VAR>X : Type u_1<VAR>Y✝ : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace Y✝<VAR>inst✝⁴ : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝³ : TopologicalSpace X'<VAR>inst✝² : TopologicalSpace Y'<VAR>ι : Type u_6<VAR>p : ι → Prop<VAR>Y : ι → Type u_7<VAR>inst✝¹ : (i : ι) → TopologicalSpace (Y i)<VAR>inst✝ : DecidablePred p<GOAL>Continuous (Equiv.piEquivPiSubtypeProd p Y).toFun
<VAR>X : Type u_1<VAR>Y✝ : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace Y✝<VAR>inst✝⁴ : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝³ : TopologicalSpace X'<VAR>inst✝² : TopologicalSpace Y'<VAR>ι : Type u_6<VAR>p : ι → Prop<VAR>Y : ι → Type u_7<VAR>inst✝¹ : (i : ι) → TopologicalSpace (Y i)<VAR>inst✝ : DecidablePred p<VAR>j : ι<VAR>h✝ : p j<GOAL>Continuous fun a => a.1 ⟨j, h✝⟩
<VAR>X : Type u_1<VAR>Y✝ : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace Y✝<VAR>inst✝⁴ : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝³ : TopologicalSpace X'<VAR>inst✝² : TopologicalSpace Y'<VAR>ι : Type u_6<VAR>p : ι → Prop<VAR>Y : ι → Type u_7<VAR>inst✝¹ : (i : ι) → TopologicalSpace (Y i)<VAR>inst✝ : DecidablePred p<VAR>j : ι<VAR>h✝ : ¬p j<GOAL>Continuous fun a => a.2 ⟨j, h✝⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableEq m<VAR>i j : m<VAR>hij : b i ≤ b j<VAR>c : R<VAR>r s : m<VAR>hrs : b s < b r<GOAL>stdBasisMatrix i j c r s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableEq m<VAR>i j : m<VAR>hij : b i ≤ b j<VAR>c : R<VAR>r s : m<VAR>hrs : b s < b r<GOAL>¬(i = r ∧ j = s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableEq m<VAR>i j : m<VAR>hij : b i ≤ b j<VAR>c : R<VAR>hrs : b j < b i<GOAL>False
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>ι : Type u<VAR>s : ι → K[X]<VAR>t : Finset ι<GOAL>(∀ j ∈ t, Splits i (s j)) → Splits i (∏ x ∈ t, s x)
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>hI : IsClosed ↑I<GOAL>I.IsMaximal ↔ ∃ x, idealOfSet 𝕜 {x}ᶜ = I
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>hI : IsClosed ↑I<GOAL>I.IsMaximal → ∃ x, idealOfSet 𝕜 {x}ᶜ = I
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>hI : IsClosed ↑I<VAR>hI' : I.IsMaximal<GOAL>∃ x, idealOfSet 𝕜 {x}ᶜ = I
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>hI : IsClosed ↑I<VAR>hI' : I.IsMaximal<VAR>x : X<VAR>hx : setOfIdeal I = {x}ᶜ<GOAL>∃ x, idealOfSet 𝕜 {x}ᶜ = I
<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>FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 = ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3
<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>↑(η ^ 2 * FermatLastTheoremForThreeGen.Solution.u₁ S * (FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 + FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 = 0
<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>(↑(η ^ 2 * FermatLastTheoremForThreeGen.Solution.u₁ S * (FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 + FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3) * (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) = 0 * (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ 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<GOAL>↑(η ^ 2 * FermatLastTheoremForThreeGen.Solution.u₁ S * (FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 * (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) + FermatLastTheoremForThreeGen.Solution.Y S ^ 3 * (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) + ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 * (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) = 0
<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>↑(η ^ 2 * FermatLastTheoremForThreeGen.Solution.u₁ S * (FermatLastTheoremForThreeGen.Solution.u₂ S)⁻¹) * (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 * (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) + FermatLastTheoremForThreeGen.Solution.Y S ^ 3 * (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) + ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) * FermatLastTheoremForThreeGen.Solution.Z S ^ 3 * (λ * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * ↑η) = FermatLastTheoremForThreeGen.Solution.X S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₁ S) * λ ^ (3 * S.multiplicity - 2) + FermatLastTheoremForThreeGen.Solution.Y S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₂ S) * λ * ↑η + FermatLastTheoremForThreeGen.Solution.Z S ^ 3 * ↑(FermatLastTheoremForThreeGen.Solution.u₃ S) * λ * ↑η ^ 2
<VAR>a s n step : Nat<GOAL>map (fun x => a + x) (range' s (n + 1) step) = range' (a + s) (n + 1) step
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : Finite ι<VAR>e : Basis ι R M<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<GOAL>(Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : Finite ι<VAR>e : Basis ι R M<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<VAR>val✝ : Fintype ι<GOAL>(Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x