ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>inst✝¹² : TopologicalSpace X<VAR>A D✝ E✝ : Type u<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : TopologicalSpace D✝<VAR>inst✝⁹ : TopologicalSpace E✝<VAR>inst✝⁸ : ExtremallyDisconnected A<VAR>inst✝⁷ : CompactSpace A<VAR>inst✝⁶ : T2Space A<VAR>B C : Type u<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace C<VAR>inst✝³ : CompactSpace B<VAR>inst✝² : T2Space B<VAR>inst✝¹ : CompactSpace C<VAR>inst✝ : T2Space C<VAR>φ : A → C<VAR>f : B → C<VAR>φ_cont : Continuous φ<VAR>f_cont : Continuous f<VAR>f_surj : Surjective f<VAR>D : Set (A × B) := {x | φ x.1 = f x.2}<VAR>D_comp : CompactSpace ↑D<VAR>π₁ : ↑D → A := Prod.fst ∘ Subtype.val<VAR>π₁_cont : Continuous π₁<VAR>π₁_surj : Surjective π₁<VAR>E : Set ↑D<VAR>left✝ : CompactSpace ↑E<VAR>E_onto : π₁ '' E = univ<VAR>E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ<VAR>ρ : ↑E → A := E.restrict π₁<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min<VAR>π₂ : ↑D → B := Prod.snd ∘ Subtype.val<GOAL>∃ h, Continuous h ∧ f ∘ h = φ
<VAR>X : Type u<VAR>inst✝¹² : TopologicalSpace X<VAR>A D✝ E✝ : Type u<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : TopologicalSpace D✝<VAR>inst✝⁹ : TopologicalSpace E✝<VAR>inst✝⁸ : ExtremallyDisconnected A<VAR>inst✝⁷ : CompactSpace A<VAR>inst✝⁶ : T2Space A<VAR>B C : Type u<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace C<VAR>inst✝³ : CompactSpace B<VAR>inst✝² : T2Space B<VAR>inst✝¹ : CompactSpace C<VAR>inst✝ : T2Space C<VAR>φ : A → C<VAR>f : B → C<VAR>φ_cont : Continuous φ<VAR>f_cont : Continuous f<VAR>f_surj : Surjective f<VAR>D : Set (A × B) := {x | φ x.1 = f x.2}<VAR>D_comp : CompactSpace ↑D<VAR>π₁ : ↑D → A := Prod.fst ∘ Subtype.val<VAR>π₁_cont : Continuous π₁<VAR>π₁_surj : Surjective π₁<VAR>E : Set ↑D<VAR>left✝ : CompactSpace ↑E<VAR>E_onto : π₁ '' E = univ<VAR>E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ<VAR>ρ : ↑E → A := E.restrict π₁<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min<VAR>π₂ : ↑D → B := Prod.snd ∘ Subtype.val<VAR>π₂_cont : Continuous π₂<GOAL>∃ h, Continuous h ∧ f ∘ h = φ
<VAR>X : Type u<VAR>inst✝¹² : TopologicalSpace X<VAR>A D✝ E✝ : Type u<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : TopologicalSpace D✝<VAR>inst✝⁹ : TopologicalSpace E✝<VAR>inst✝⁸ : ExtremallyDisconnected A<VAR>inst✝⁷ : CompactSpace A<VAR>inst✝⁶ : T2Space A<VAR>B C : Type u<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace C<VAR>inst✝³ : CompactSpace B<VAR>inst✝² : T2Space B<VAR>inst✝¹ : CompactSpace C<VAR>inst✝ : T2Space C<VAR>φ : A → C<VAR>f : B → C<VAR>φ_cont : Continuous φ<VAR>f_cont : Continuous f<VAR>f_surj : Surjective f<VAR>D : Set (A × B) := {x | φ x.1 = f x.2}<VAR>D_comp : CompactSpace ↑D<VAR>π₁ : ↑D → A := Prod.fst ∘ Subtype.val<VAR>π₁_cont : Continuous π₁<VAR>π₁_surj : Surjective π₁<VAR>E : Set ↑D<VAR>left✝ : CompactSpace ↑E<VAR>E_onto : π₁ '' E = univ<VAR>E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ<VAR>ρ : ↑E → A := E.restrict π₁<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min<VAR>π₂ : ↑D → B := Prod.snd ∘ Subtype.val<VAR>π₂_cont : Continuous π₂<GOAL>f ∘ E.restrict π₂ ∘ ⇑ρ'.symm = φ
<VAR>X : Type u<VAR>inst✝¹² : TopologicalSpace X<VAR>A D✝ E✝ : Type u<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : TopologicalSpace D✝<VAR>inst✝⁹ : TopologicalSpace E✝<VAR>inst✝⁸ : ExtremallyDisconnected A<VAR>inst✝⁷ : CompactSpace A<VAR>inst✝⁶ : T2Space A<VAR>B C : Type u<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace C<VAR>inst✝³ : CompactSpace B<VAR>inst✝² : T2Space B<VAR>inst✝¹ : CompactSpace C<VAR>inst✝ : T2Space C<VAR>φ : A → C<VAR>f : B → C<VAR>φ_cont : Continuous φ<VAR>f_cont : Continuous f<VAR>f_surj : Surjective f<VAR>D : Set (A × B) := {x | φ x.1 = f x.2}<VAR>D_comp : CompactSpace ↑D<VAR>π₁ : ↑D → A := Prod.fst ∘ Subtype.val<VAR>π₁_cont : Continuous π₁<VAR>π₁_surj : Surjective π₁<VAR>E : Set ↑D<VAR>left✝ : CompactSpace ↑E<VAR>E_onto : π₁ '' E = univ<VAR>E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ<VAR>ρ : ↑E → A := E.restrict π₁<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min<VAR>π₂ : ↑D → B := Prod.snd ∘ Subtype.val<VAR>π₂_cont : Continuous π₂<GOAL>f ∘ E.restrict π₂ = φ ∘ ⇑ρ'
<VAR>X : Type u<VAR>inst✝¹² : TopologicalSpace X<VAR>A D✝ E✝ : Type u<VAR>inst✝¹¹ : TopologicalSpace A<VAR>inst✝¹⁰ : TopologicalSpace D✝<VAR>inst✝⁹ : TopologicalSpace E✝<VAR>inst✝⁸ : ExtremallyDisconnected A<VAR>inst✝⁷ : CompactSpace A<VAR>inst✝⁶ : T2Space A<VAR>B C : Type u<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace C<VAR>inst✝³ : CompactSpace B<VAR>inst✝² : T2Space B<VAR>inst✝¹ : CompactSpace C<VAR>inst✝ : T2Space C<VAR>φ : A → C<VAR>f : B → C<VAR>φ_cont : Continuous φ<VAR>f_cont : Continuous f<VAR>f_surj : Surjective f<VAR>D : Set (A × B) := {x | φ x.1 = f x.2}<VAR>D_comp : CompactSpace ↑D<VAR>π₁ : ↑D → A := Prod.fst ∘ Subtype.val<VAR>π₁_cont : Continuous π₁<VAR>π₁_surj : Surjective π₁<VAR>E : Set ↑D<VAR>left✝ : CompactSpace ↑E<VAR>E_onto : π₁ '' E = univ<VAR>E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.restrict π₁ '' E₀ ≠ univ<VAR>ρ : ↑E → A := E.restrict π₁<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min<VAR>π₂ : ↑D → B := Prod.snd ∘ Subtype.val<VAR>π₂_cont : Continuous π₂<VAR>x : ↑E<GOAL>(f ∘ E.restrict π₂) x = (φ ∘ ⇑ρ') x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℕ<VAR>hn : chainLength α β < n<GOAL>rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℕ<VAR>hn : chainLength α β < n<VAR>e : ¬rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℕ<VAR>hn : chainLength α β < n<VAR>e : ¬rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥<VAR>W : Weight K (↥H) L := { toFun := -(n • ⇑α) + ⇑(chainTop (⇑α) β), weightSpace_ne_bot' := e }<VAR>hW : ⇑W = -(n • ⇑α) + ⇑(chainTop (⇑α) β)<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℕ<VAR>hn : chainLength α β < n<VAR>e : ¬rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥<VAR>W : Weight K (↥H) L := { toFun := -(n • ⇑α) + ⇑(chainTop (⇑α) β), weightSpace_ne_bot' := e }<VAR>hW : ⇑W = -(n • ⇑α) + ⇑(chainTop (⇑α) β)<VAR>H₁ : 1 + n + chainTopCoeff (⇑(-α)) W ≤ chainLength (-α) W<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℕ<VAR>hn : chainLength α β < n<VAR>e : ¬rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥<VAR>W : Weight K (↥H) L := { toFun := -(n • ⇑α) + ⇑(chainTop (⇑α) β), weightSpace_ne_bot' := e }<VAR>hW : ⇑W = -(n • ⇑α) + ⇑(chainTop (⇑α) β)<VAR>H₁ : 1 + n + chainTopCoeff (⇑(-α)) W ≤ chainLength (-α) W<VAR>H₂ : (1 + n + chainTopCoeff (⇑(-α)) W) • ⇑α + ⇑(chainTop (⇑(-α)) W) = (chainTopCoeff (⇑α) β + 1) • ⇑α + ⇑β<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℕ<VAR>hn : chainLength α β < n<VAR>e : ¬rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥<VAR>W : Weight K (↥H) L := { toFun := -(n • ⇑α) + ⇑(chainTop (⇑α) β), weightSpace_ne_bot' := e }<VAR>hW : ⇑W = -(n • ⇑α) + ⇑(chainTop (⇑α) β)<VAR>H₁ : 1 + n + chainTopCoeff (⇑(-α)) W ≤ chainLength (-α) W<VAR>H₂ : (1 + n + chainTopCoeff (⇑(-α)) W) • ⇑α + ⇑(chainTop (⇑(-α)) W) = (chainTopCoeff (⇑α) β + 1) • ⇑α + ⇑β<VAR>this : rootSpace H (-((1 + n + chainTopCoeff (⇑(-α)) W) • ⇑(-α)) + ⇑(chainTop (⇑(-α)) W)) ≠ ⊥<GOAL>False
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℕ<VAR>hn : chainLength α β < n<VAR>e : ¬rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥<VAR>W : Weight K (↥H) L := { toFun := -(n • ⇑α) + ⇑(chainTop (⇑α) β), weightSpace_ne_bot' := e }<VAR>hW : ⇑W = -(n • ⇑α) + ⇑(chainTop (⇑α) β)<VAR>H₁ : 1 + n + chainTopCoeff (⇑(-α)) W ≤ chainLength (-α) W<VAR>H₂ : (1 + n + chainTopCoeff (⇑(-α)) W) • ⇑α + ⇑(chainTop (⇑(-α)) W) = (chainTopCoeff (⇑α) β + 1) • ⇑α + ⇑β<VAR>this : rootSpace H ((chainTopCoeff (⇑α) β + 1) • ⇑α + ⇑β) ≠ ⊥<GOAL>False
<VAR>n : ℤ<VAR>z τ : ℂ<GOAL>π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
<VAR>n : ℤ<VAR>z τ : ℂ<VAR>this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖<GOAL>π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
<VAR>n : ℤ<VAR>z τ : ℂ<VAR>this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖<GOAL>π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖
<VAR>n : ℤ<VAR>z τ : ℂ<VAR>this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖<GOAL>‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * (π * ↑|n| ^ 2) ≤ ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * (‖↑π‖ * ‖I‖ * ‖↑n ^ 2‖)
<VAR>n : ℤ<VAR>z τ : ℂ<VAR>this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖<GOAL>π * ↑|n| ^ 2 = ‖↑π‖ * ‖I‖ * ‖↑n ^ 2‖
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F G : C ⥤ Discrete PUnit.{w + 1}<VAR>X : C<GOAL>F.obj X = G.obj X
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a b : ℕ<GOAL>(a ^ n).Coprime b ↔ a.Coprime b
<VAR>a b n : ℕ<VAR>hn : 0 < n.succ<GOAL>(a ^ n.succ).Coprime b ↔ a.Coprime b
<VAR>a b n : ℕ<VAR>hn : 0 < n.succ<GOAL>(a ^ n).Coprime b ∧ a.Coprime b ↔ a.Coprime b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a✝ a : α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<GOAL>s ∈ 𝓓 a (𝓓 a 𝒜) ↔ s ∈ 𝓓 a 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a✝ a : α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<GOAL>s ∈ 𝓓 a 𝒜 ∧ s.erase a ∈ 𝓓 a 𝒜 ∨ s ∉ 𝓓 a 𝒜 ∧ insert a s ∈ 𝓓 a 𝒜 → s ∈ 𝓓 a 𝒜
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>a b : α<VAR>m n : ℕ<GOAL>2 = 1 + 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : (nilradical R).IsPrime<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hm : f.Monic<VAR>hi : Irreducible (Polynomial.map φ f)<VAR>R' : Type u_1 := R ⧸ nilradical R<GOAL>Irreducible f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : (nilradical R).IsPrime<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hm : f.Monic<VAR>hi : Irreducible (Polynomial.map φ f)<VAR>R' : Type u_1 := R ⧸ nilradical R<VAR>ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯<GOAL>Irreducible f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : (nilradical R).IsPrime<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hm : f.Monic<VAR>hi : Irreducible (Polynomial.map φ f)<VAR>R' : Type u_1 := R ⧸ nilradical R<VAR>ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯<VAR>ι : R →+* R' := algebraMap R R'<GOAL>Irreducible f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : (nilradical R).IsPrime<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hm : f.Monic<VAR>R' : Type u_1 := R ⧸ nilradical R<VAR>ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯<VAR>ι : R →+* R' := algebraMap R R'<VAR>hi : Irreducible (Polynomial.map ψ (Polynomial.map ι f))<GOAL>Irreducible f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : (nilradical R).IsPrime<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hm : f.Monic<VAR>R' : Type u_1 := R ⧸ nilradical R<VAR>ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯<VAR>ι : R →+* R' := algebraMap R R'<VAR>hi : Irreducible (Polynomial.map ι f)<GOAL>Irreducible f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : (nilradical R).IsPrime<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hm : f.Monic<VAR>R' : Type u_1 := R ⧸ nilradical R<VAR>ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯<VAR>ι : R →+* R' := algebraMap R R'<VAR>hi : Irreducible (Polynomial.map ι f)<VAR>a b : R[X]<VAR>h : f = a * b<GOAL>IsUnit a ∨ IsUnit b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : (nilradical R).IsPrime<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hm : f.Monic<VAR>R' : Type u_1 := R ⧸ nilradical R<VAR>ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯<VAR>ι : R →+* R' := algebraMap R R'<VAR>hi : Irreducible (Polynomial.map ι f)<VAR>a b : R[X]<VAR>h : f = a * b<VAR>hb : IsUnit (Polynomial.map ι b)<GOAL>IsUnit a ∨ IsUnit b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : (nilradical R).IsPrime<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hm : f.Monic<VAR>R' : Type u_1 := R ⧸ nilradical R<VAR>ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯<VAR>ι : R →+* R' := algebraMap R R'<VAR>hi : Irreducible (Polynomial.map ι f)<VAR>a b : R[X]<VAR>h : f = a * b<VAR>hb : IsUnit (Polynomial.map ι b)<VAR>hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)<GOAL>IsUnit a ∨ IsUnit b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : (nilradical R).IsPrime<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hm : f.Monic<VAR>R' : Type u_1 := R ⧸ nilradical R<VAR>ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯<VAR>ι : R →+* R' := algebraMap R R'<VAR>hi : Irreducible (Polynomial.map ι f)<VAR>a b : R[X]<VAR>h : f = a * b<VAR>hb : IsUnit (Polynomial.map ι b)<VAR>hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)<GOAL>IsUnit (-(a.coeff f.natDegree * b.coeff 0))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : (nilradical R).IsPrime<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hm : f.Monic<VAR>R' : Type u_1 := R ⧸ nilradical R<VAR>ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯<VAR>ι : R →+* R' := algebraMap R R'<VAR>hi : Irreducible (Polynomial.map ι f)<VAR>a b : R[X]<VAR>h : f = a * b<VAR>hb : IsUnit (Polynomial.map ι b)<VAR>hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)<VAR>hc : f.leadingCoeff = (a * b).coeff f.natDegree<GOAL>IsUnit (-(a.coeff f.natDegree * b.coeff 0))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : (nilradical R).IsPrime<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hm : f.Monic<VAR>R' : Type u_1 := R ⧸ nilradical R<VAR>ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯<VAR>ι : R →+* R' := algebraMap R R'<VAR>hi : Irreducible (Polynomial.map ι f)<VAR>a b : R[X]<VAR>h : f = a * b<VAR>hb : IsUnit (Polynomial.map ι b)<VAR>hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)<VAR>hc : 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)<GOAL>IsUnit (-(a.coeff f.natDegree * b.coeff 0))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : (nilradical R).IsPrime<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hm : f.Monic<VAR>R' : Type u_1 := R ⧸ nilradical R<VAR>ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯<VAR>ι : R →+* R' := algebraMap R R'<VAR>hi : Irreducible (Polynomial.map ι f)<VAR>a b : R[X]<VAR>h : f = a * b<VAR>hb : IsUnit (Polynomial.map ι b)<VAR>hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)<VAR>hc : 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)<GOAL>IsUnit (∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x) - 1)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>¬eval (↑(n - (ν - 1))) (ascPochhammer R ν) = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>¬↑(eval (n - (ν - 1)) (ascPochhammer ℕ ν)) = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>¬eval (n - (ν - 1)) (ascPochhammer ℕ ν) = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<VAR>n : ℕ<VAR>h : 0 ≤ n<GOAL>0 < eval (n - (0 - 1)) (ascPochhammer ℕ 0)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<VAR>n ν : ℕ<VAR>h : ν ≤ n<VAR>h' : ν > 0<GOAL>0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)
<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>α : ↥(solvableByRad F E)<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hα : P (α ^ n)<VAR>p : F[X] := minpoly F (α ^ n)<VAR>hp : p.comp (X ^ n) ≠ 0<GOAL>P α
<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>α : ↥(solvableByRad F E)<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hα : P (α ^ n)<VAR>p : F[X] := minpoly F (α ^ n)<VAR>hp : p.comp (X ^ n) ≠ 0<GOAL>Fact (Splits (algebraMap F ?q.SplittingField) (minpoly F α))
<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>α : ↥(solvableByRad F E)<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hα : P (α ^ n)<VAR>p : F[X] := minpoly F (α ^ n)<VAR>hp : p.comp (X ^ n) ≠ 0<GOAL>IsSolvable ?q.Gal
<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>α : ↥(solvableByRad F E)<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hα : P (α ^ n)<VAR>p : F[X] := minpoly F (α ^ n)<VAR>hp : p.comp (X ^ n) ≠ 0<GOAL>F[X]
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>ofFn f = [] ↔ n = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>a✝ : Nontrivial A<GOAL>pb.minpolyGen.Monic
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>a✝ : Nontrivial A<GOAL>(∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree < (X ^ pb.dim).degree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>a✝ : Nontrivial A<GOAL>(∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree < ↑pb.dim
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a ≤ b / c<GOAL>a * c ≤ b
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a ≤ b / c<GOAL>a * c⁻¹⁻¹ ≤ b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f✝ : β → α<VAR>inst✝ : DecidableEq β<VAR>s₁ s₂ : Finset β<VAR>h₁ : s₁.Nonempty<VAR>h₂ : s₂.Nonempty<VAR>f : β → α<VAR>a : α<GOAL>(s₁ ∪ s₂).sup' ⋯ f ≤ a ↔ s₁.sup' h₁ f ⊔ s₂.sup' h₂ f ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : Zero α<VAR>inst✝ : LocallyFiniteOrder α<VAR>f g : ι →₀ α<GOAL>(Ioc f g).card = ∏ i ∈ f.support ∪ g.support, (Icc (f i) (g i)).card - 1
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A✝ B A : Matrix n n α<VAR>b : n → α<VAR>h : IsUnit A.det<GOAL>A.det • A⁻¹ *ᵥ b = A.cramer b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>m : MeasurableSpace α<VAR>f : α → β<GOAL>HasFiniteIntegral f 0
<VAR>m n a b c d : ℕ<VAR>h : a ≡ b [MOD m]<VAR>h2 : |↑b - ↑a| < ↑m<GOAL>Int.ofNat a = Int.ofNat b
<VAR>m n a b c d : ℕ<VAR>h : a ≡ b [MOD m]<VAR>h2 : |↑b - ↑a| < ↑m<GOAL>Int.ofNat b - Int.ofNat a = 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>X Y : R<GOAL>W.Nonsingular ![X, Y, 1] ↔ W.toAffine.Nonsingular X Y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>X Y : R<GOAL>W.Equation ![X, Y, 1] ∧ (W.a₁ * ![X, Y, 1] 1 * ![X, Y, 1] 2 ≠ 3 * ![X, Y, 1] 0 ^ 2 + 2 * W.a₂ * ![X, Y, 1] 0 * ![X, Y, 1] 2 + W.a₄ * ![X, Y, 1] 2 ^ 2 ∨ ![X, Y, 1] 1 * ![X, Y, 1] 2 ≠ -![X, Y, 1] 1 * ![X, Y, 1] 2 - W.a₁ * ![X, Y, 1] 0 * ![X, Y, 1] 2 - W.a₃ * ![X, Y, 1] 2 ^ 2 ∨ ![X, Y, 1] 1 ^ 2 + W.a₁ * ![X, Y, 1] 0 * ![X, Y, 1] 1 + 2 * W.a₃ * ![X, Y, 1] 1 * ![X, Y, 1] 2 ≠ W.a₂ * ![X, Y, 1] 0 ^ 2 + 2 * W.a₄ * ![X, Y, 1] 0 * ![X, Y, 1] 2 + 3 * W.a₆ * ![X, Y, 1] 2 ^ 2) ↔ W.toAffine.Nonsingular X Y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>X Y : R<GOAL>W.Equation ![X, Y, 1] ∧ (W.a₁ * Y * 1 ≠ 3 * X ^ 2 + 2 * W.a₂ * X * 1 + W.a₄ * 1 ^ 2 ∨ Y * 1 ≠ -Y * 1 - W.a₁ * X * 1 - W.a₃ * 1 ^ 2 ∨ Y ^ 2 + W.a₁ * X * Y + 2 * W.a₃ * Y * 1 ≠ W.a₂ * X ^ 2 + 2 * W.a₄ * X * 1 + 3 * W.a₆ * 1 ^ 2) ↔ W.toAffine.Nonsingular X Y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>X Y : R<GOAL>Y ^ 2 + W.toAffine.a₁ * X * Y + W.toAffine.a₃ * Y = X ^ 3 + W.toAffine.a₂ * X ^ 2 + W.toAffine.a₄ * X + W.toAffine.a₆ → W.toAffine.a₁ * Y = 3 * X ^ 2 + 2 * W.toAffine.a₂ * X + W.toAffine.a₄ → Y = -Y - W.toAffine.a₁ * X - W.toAffine.a₃ → Y ^ 2 + W.a₁ * X * Y + 2 * W.a₃ * Y = W.a₂ * X ^ 2 + 2 * W.a₄ * X + 3 * W.a₆