ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℕ<VAR>h : x * x = d * y * y<VAR>g : ℕ := x.gcd y<VAR>gpos : g > 0<GOAL>False
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℕ<VAR>h : x * x = d * y * y<VAR>g : ℕ := x.gcd y<VAR>gpos : g > 0<VAR>m n : ℕ<VAR>co : m.Coprime n<VAR>hx : x = m * g<VAR>hy : y = n * g<GOAL>False
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℕ<VAR>g : ℕ := x.gcd y<VAR>gpos : g > 0<VAR>m n : ℕ<VAR>h : m * g * (m * g) = d * (n * g) * (n * g)<VAR>co : m.Coprime n<VAR>hx : x = m * g<VAR>hy : y = n * g<GOAL>False
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℕ<VAR>g : ℕ := x.gcd y<VAR>gpos : g > 0<VAR>m n : ℕ<VAR>h : m * g * (m * g) = d * (n * g) * (n * g)<VAR>co : m.Coprime n<VAR>hx : x = m * g<VAR>hy : y = n * g<VAR>this : m * m = d * (n * n)<GOAL>False
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y : ℕ<VAR>g : ℕ := x.gcd y<VAR>gpos : g > 0<VAR>m n : ℕ<VAR>h : m * g * (m * g) = d * (n * g) * (n * g)<VAR>co : m.Coprime n<VAR>hx : x = m * g<VAR>hy : y = n * g<VAR>this : m * m = d * (n * n)<VAR>co2 : (m * m).Coprime (n * n)<GOAL>False
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>x : M ⊗[R] N<GOAL>∃ S, x = S.sum fun m n => m ⊗ₜ[R] n
<VAR>b✝ x y a b : ℝ<VAR>h₁ : a ≠ 0<VAR>h₂ : b ≠ 0<VAR>c : ℝ<GOAL>logb (a / b) c = ((logb a c)⁻¹ - (logb b c)⁻¹)⁻¹
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>v₁ v₂ : G<VAR>p₁ p₂ : P<GOAL>v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
<VAR>n : ℕ<VAR>i j : Fin (n + 2)<VAR>h : j ≠ i<GOAL>Set.range ⇑(asOrderHom ((standardSimplex.objEquiv [n + 1] (op [n])).symm (δ j))) ∪ {i} ≠ Set.univ
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>a b : A<VAR>n : ℕ<GOAL>(coeff A n) ((rescale a) (exp A) * (rescale b) (exp A)) = (coeff A n) ((rescale (a + b)) (exp A))
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>a b : A<VAR>n : ℕ<GOAL>∑ x ∈ Finset.range n.succ, a ^ x * (algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * (algebraMap ℚ A) (1 / ↑(n - x)!)) = ∑ x ∈ Finset.range (n + 1), a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>a b : A<VAR>n : ℕ<GOAL>∀ x ∈ Finset.range n.succ, a ^ x * (algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * (algebraMap ℚ A) (1 / ↑(n - x)!)) = a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>a b : A<VAR>n x : ℕ<VAR>hx : x ∈ Finset.range n.succ<GOAL>(algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!) = ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>a b : A<VAR>n x : ℕ<VAR>hx : x ∈ Finset.range n.succ<GOAL>(algebraMap ℚ A) (1 / ↑x ! * (1 / ↑(n - x)!)) = (algebraMap ℚ A) (↑(n.choose x) * (1 / ↑n !))
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>a b : A<VAR>n x : ℕ<VAR>hx : x ∈ Finset.range n.succ<GOAL>1 / ↑x ! * (1 / ↑(n - x)!) = ↑(n.choose x) * (1 / ↑n !)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>a b : A<VAR>n x : ℕ<VAR>hx : x ∈ Finset.range n.succ<GOAL>1 / (↑x ! * ↑(n - x)!) = ↑(n.choose x) / ↑n !
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>a b : A<VAR>n x : ℕ<VAR>hx : x ∈ Finset.range n.succ<GOAL>↑(n.choose x) / ↑n ! = 1 / (↑x ! * ↑(n - x)!)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>a b : A<VAR>n x : ℕ<VAR>hx : x ∈ Finset.range n.succ<GOAL>↑(n ! / (x ! * (n - x)!)) = ↑n ! / (↑x ! * ↑(n - x)!)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>a b : A<VAR>n x : ℕ<VAR>hx : x ∈ Finset.range n.succ<GOAL>x ≤ n
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>a b : A<VAR>n x : ℕ<VAR>hx : x ∈ Finset.range n.succ<GOAL>↑n ! ≠ 0
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hapc : ∠ a p c = π<VAR>hbpd : ∠ b p d = π<GOAL>dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hapc : ∠ a p c = π<VAR>hbpd : ∠ b p d = π<VAR>h' : Cospherical {a, c, b, d}<GOAL>dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hapc : ∠ a p c = π<VAR>hbpd : ∠ b p d = π<VAR>h' : Cospherical {a, c, b, d}<VAR>hmul : dist a p * dist c p = dist b p * dist d p<GOAL>dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hapc : ∠ a p c = π<VAR>hbpd : ∠ b p d = π<VAR>h' : Cospherical {a, c, b, d}<VAR>hmul : dist a p * dist c p = dist b p * dist d p<VAR>hbp : dist b p ≠ 0<GOAL>dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hapc : ∠ a p c = π<VAR>hbpd : ∠ b p d = π<VAR>h' : Cospherical {a, c, b, d}<VAR>hmul : dist a p * dist c p = dist b p * dist d p<VAR>hbp : dist b p ≠ 0<VAR>h₁ : dist c d = dist c p / dist b p * dist a b<VAR>h₂ : dist d a = dist a p / dist b p * dist b c<GOAL>dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hapc : ∠ a p c = π<VAR>hbpd : ∠ b p d = π<VAR>h' : Cospherical {a, c, b, d}<VAR>hmul : dist a p * dist c p = dist b p * dist d p<VAR>hbp : dist b p ≠ 0<VAR>h₁ : dist c d = dist c p / dist b p * dist a b<VAR>h₂ : dist d a = dist a p / dist b p * dist b c<VAR>h₃ : dist d p = dist a p * dist c p / dist b p<GOAL>dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
<VAR>V : Type u_1<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : Cospherical {a, b, c, d}<VAR>hapc : ∠ a p c = π<VAR>hbpd : ∠ b p d = π<VAR>h' : Cospherical {a, c, b, d}<VAR>hmul : dist a p * dist c p = dist b p * dist d p<VAR>hbp : dist b p ≠ 0<VAR>h₁ : dist c d = dist c p / dist b p * dist a b<VAR>h₂ : dist d a = dist a p / dist b p * dist b c<VAR>h₃ : dist d p = dist a p * dist c p / dist b p<VAR>h₄ : ∀ (x y : ℝ), x * (y * x) = x * x * y<GOAL>dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<GOAL>Ex ≤ Ey
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<GOAL>Ex ≤ Ey
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hxU : 0 ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K 0, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K 0; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<GOAL>Ex ≤ Ey
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<GOAL>Ex ≤ Ey
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<GOAL>Ex ≤ Ey
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r = finrank K L<GOAL>Ex ≤ Ey
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<GOAL>Ex ≤ Ey
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<GOAL>Ex ≤ Ey
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<GOAL>χ = X ^ r
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<GOAL>∀ i < r, χ.coeff i = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>i : ℕ<VAR>hi : i < r<GOAL>χ.coeff i = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>hi : 0 < r<GOAL>χ.coeff 0 = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>i : ℕ<VAR>hi : i < r<VAR>hi0 : i ≠ 0<GOAL>χ.coeff i = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>i : ℕ<VAR>hi : i < r<VAR>hi0 : i ≠ 0<VAR>hψ : constantCoeff ψ ≠ 0<GOAL>χ.coeff i = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>i : ℕ<VAR>hi : i < r<VAR>hi0 : i ≠ 0<VAR>hψ : constantCoeff ψ ≠ 0<VAR>s : Finset K<VAR>hs : r ≤ s.card<VAR>hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0<GOAL>χ.coeff i = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>i : ℕ<VAR>hi : i < r<VAR>hi0 : i ≠ 0<VAR>hψ : constantCoeff ψ ≠ 0<VAR>s : Finset K<VAR>hs : r ≤ s.card<VAR>hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0<GOAL>∀ i_1 ∈ s, eval i_1 (χ.coeff i) = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>i : ℕ<VAR>hi : i < r<VAR>hi0 : i ≠ 0<VAR>hψ : constantCoeff ψ ≠ 0<VAR>s : Finset K<VAR>hs : r ≤ s.card<VAR>hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0<GOAL>(χ.coeff i).natDegree < s.card
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>i : ℕ<VAR>hi : i < r<VAR>hi0 : i ≠ 0<VAR>hψ : constantCoeff ψ ≠ 0<VAR>s : Finset K<VAR>hs : r ≤ s.card<VAR>hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0<VAR>α : K<VAR>hα : α ∈ s<GOAL>eval α (χ.coeff i) = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>i : ℕ<VAR>hi : i < r<VAR>hi0 : i ≠ 0<VAR>hψ : constantCoeff ψ ≠ 0<VAR>s : Finset K<VAR>hs : r ≤ s.card<VAR>hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0<VAR>α : K<VAR>hα : α ∈ s<GOAL>∀ (m : ↥↑E), ∃ n, ((toEnd K ↥U ↥↑E) (α • u + x') ^ n) m = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>i : ℕ<VAR>hi : i < r<VAR>hi0 : i ≠ 0<VAR>hψ : constantCoeff ψ ≠ 0<VAR>s : Finset K<VAR>hs : r ≤ s.card<VAR>hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0<VAR>α : K<VAR>hα : α ∈ s<VAR>v : ↥U := α • u + x'<GOAL>∀ (m : ↥↑E), ∃ n, ((toEnd K ↥U ↥↑E) (α • u + x') ^ n) m = 0