ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x✝ : M<VAR>hs : UniqueMDiffOn I s<VAR>x : M<VAR>y : M'<VAR>f : M → M'<VAR>hf : ContinuousOn f s<VAR>z : M<VAR>hz : z ∈ s ∩ f ⁻¹' (extChartAt I' y).source<GOAL>UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' y).source) z
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x✝ : M<VAR>hs : UniqueMDiffOn I s<VAR>x : M<VAR>y : M'<VAR>f : M → M'<VAR>hf : ContinuousOn f s<VAR>z : M<VAR>hz : z ∈ s ∩ f ⁻¹' (extChartAt I' y).source<GOAL>f ⁻¹' (extChartAt I' y).source ∈ nhdsWithin z s
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x✝ : M<VAR>hs : UniqueMDiffOn I s<VAR>x : M<VAR>y : M'<VAR>f : M → M'<VAR>hf : ContinuousOn f s<VAR>z : M<VAR>hz : z ∈ s ∩ f ⁻¹' (extChartAt I' y).source<GOAL>(extChartAt I' y).source ∈ nhds (f z)
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>f : R →+* S<VAR>z : S<VAR>hz : eval₂ f z p = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<VAR>hlt : 0 ≥ p.natDegree<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>f : R →+* S<VAR>z : S<VAR>hz : eval₂ f z p = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<VAR>hlt : 0 ≥ p.natDegree<VAR>A : p = C (p.coeff 0)<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>f : R →+* S<VAR>z : S<VAR>hz : f (p.coeff 0) = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<VAR>hlt : 0 ≥ p.natDegree<VAR>A : p = C (p.coeff 0)<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>f : R →+* S<VAR>z : S<VAR>hz : f (p.coeff 0) = 0<VAR>inj : ∀ (x : R), f x = 0 → x = 0<VAR>hlt : 0 ≥ p.natDegree<VAR>A : p = 0<GOAL>False
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E✝ : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E✝<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E✝<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E✝<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>E : Type v := AlgebraicClosure L<VAR>this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)<GOAL>discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E✝ : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E✝<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E✝<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E✝<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>E : Type v := AlgebraicClosure L<VAR>this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<GOAL>discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E✝ : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E✝<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E✝<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E✝<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>E : Type v := AlgebraicClosure L<VAR>this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>hnodup : ((minpoly K pb.gen).aroots E).Nodup<GOAL>discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E✝ : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E✝<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E✝<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E✝<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>E : Type v := AlgebraicClosure L<VAR>this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>hnodup : ((minpoly K pb.gen).aroots E).Nodup<VAR>hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E<GOAL>discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E✝ : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E✝<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E✝<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E✝<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>E : Type v := AlgebraicClosure L<VAR>this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>hnodup : ((minpoly K pb.gen).aroots E).Nodup<VAR>hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E<GOAL>(algebraMap K E) (discr K ⇑pb.basis) = (algebraMap K E) ((-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen))))
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E✝ : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E✝<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E✝<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E✝<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>E : Type v := AlgebraicClosure L<VAR>this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>hnodup : ((minpoly K pb.gen).aroots E).Nodup<VAR>hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E<GOAL>(-1) ^ (n * (n - 1) / 2) * ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen) = (-1) ^ (n * (n - 1) / 2) * (algebraMap K E) ((norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen))))
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E✝ : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E✝<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E✝<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E✝<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>E : Type v := AlgebraicClosure L<VAR>this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>hnodup : ((minpoly K pb.gen).aroots E).Nodup<VAR>hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E<GOAL>∏ i : Fin pb.dim, ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen) = (algebraMap K E) ((norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen))))
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E✝ : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E✝<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E✝<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E✝<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>E : Type v := AlgebraicClosure L<VAR>this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>hnodup : ((minpoly K pb.gen).aroots E).Nodup<VAR>hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E<GOAL>∏ i : Fin pb.dim, ∏ j ∈ {i}ᶜ, ((e j) pb.gen - (e i) pb.gen) = ∏ σ : L →ₐ[K] E, σ ((aeval pb.gen) (derivative (minpoly K pb.gen)))
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E✝ : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E✝<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E✝<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E✝<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>E : Type v := AlgebraicClosure L<VAR>this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>hnodup : ((minpoly K pb.gen).aroots E).Nodup<VAR>hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E<GOAL>∏ i : Fin pb.dim, ∏ j ∈ {i}ᶜ, ((e j) pb.gen - (e i) pb.gen) = ∏ σ : L →ₐ[K] E, ∏ a ∈ { val := ((minpoly K pb.gen).aroots E).erase (σ pb.gen), nodup := ⋯ }, (σ pb.gen - a)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E✝ : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E✝<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E✝<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E✝<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>E : Type v := AlgebraicClosure L<VAR>this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>hnodup : ((minpoly K pb.gen).aroots E).Nodup<VAR>hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E<GOAL>∏ x ∈ univ.sigma fun i => {i}ᶜ, ((e x.snd) pb.gen - (e x.fst) pb.gen) = ∏ x ∈ univ.sigma fun σ => { val := ((minpoly K pb.gen).aroots E).erase (σ pb.gen), nodup := ⋯ }, (x.fst pb.gen - x.snd)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E✝ : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E✝<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E✝<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E✝<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>E : Type v := AlgebraicClosure L<VAR>this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>hnodup : ((minpoly K pb.gen).aroots E).Nodup<VAR>σ : (_ : L →ₐ[K] E) × E<VAR>hroots : ∀ (σ : L →ₐ[K] E), Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧ eval (σ pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0<VAR>hσ : σ.snd ≠ σ.fst pb.gen ∧ Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧ eval σ.snd (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0<GOAL>(aeval σ.snd) (minpoly K pb.gen) = 0
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E✝ : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E✝<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E✝<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E✝<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>E : Type v := AlgebraicClosure L<VAR>this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>hnodup : ((minpoly K pb.gen).aroots E).Nodup<VAR>hroots : ∀ (σ : L →ₐ[K] E), Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧ eval (σ pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0<GOAL>∀ (a b : Fin pb.dim), ¬b = a → (e a) pb.gen ≠ (e b) pb.gen ∧ Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧ eval ((e a) pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E✝ : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E✝<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E✝<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E✝<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>E : Type v := AlgebraicClosure L<VAR>this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>hnodup : ((minpoly K pb.gen).aroots E).Nodup<VAR>hroots✝ : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E<VAR>hroots : ∀ (σ : L →ₐ[K] E), Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧ eval (σ pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0<GOAL>∀ (a : L →ₐ[K] E) (b : E) (ha : b ≠ a pb.gen ∧ Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧ eval b (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0), ¬a = pb.lift b ⋯
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E✝ : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E✝<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E✝<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E✝<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>E : Type v := AlgebraicClosure L<VAR>this : (a b : E) → Decidable (a = b) := fun a b => Classical.propDecidable (a = b)<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>hnodup : ((minpoly K pb.gen).aroots E).Nodup<VAR>hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E<GOAL>∀ (a b : Fin pb.dim) (ha : ¬b = a), pb.lift ((e a) pb.gen) ⋯ = e a
<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>M' : Submodule R M<VAR>N : ℕ →o Submodule R M<VAR>H : iSup ⇑N = M'<VAR>S : Finset M<VAR>hS : span R ↑S = M'<GOAL>∃ n, M' = N n
<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>M' : Submodule R M<VAR>N : ℕ →o Submodule R M<VAR>H : iSup ⇑N = M'<VAR>S : Finset M<VAR>hS : span R ↑S = M'<VAR>this : ∀ (s : { x // x ∈ S }), ∃ n, ↑s ∈ N n<GOAL>∃ n, M' = N n
<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>M' : Submodule R M<VAR>N : ℕ →o Submodule R M<VAR>H : iSup ⇑N = M'<VAR>S : Finset M<VAR>hS : span R ↑S = M'<VAR>f : { x // x ∈ S } → ℕ<VAR>hf : ∀ (s : { x // x ∈ S }), ↑s ∈ N (f s)<GOAL>∃ n, M' = N n
<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>M' : Submodule R M<VAR>N : ℕ →o Submodule R M<VAR>H : iSup ⇑N = M'<VAR>S : Finset M<VAR>hS : span R ↑S = M'<VAR>f : { x // x ∈ S } → ℕ<VAR>hf : ∀ (s : { x // x ∈ S }), ↑s ∈ N (f s)<GOAL>M' = N (S.attach.sup f)
<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>M' : Submodule R M<VAR>N : ℕ →o Submodule R M<VAR>H : iSup ⇑N = M'<VAR>S : Finset M<VAR>hS : span R ↑S = M'<VAR>f : { x // x ∈ S } → ℕ<VAR>hf : ∀ (s : { x // x ∈ S }), ↑s ∈ N (f s)<GOAL>M' ≤ N (S.attach.sup f)
<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>M' : Submodule R M<VAR>N : ℕ →o Submodule R M<VAR>H : iSup ⇑N = M'<VAR>S : Finset M<VAR>hS : span R ↑S = M'<VAR>f : { x // x ∈ S } → ℕ<VAR>hf : ∀ (s : { x // x ∈ S }), ↑s ∈ N (f s)<GOAL>N (S.attach.sup f) ≤ M'
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>s : Submonoid N<VAR>x : M × N<GOAL>x ∈ ⊤.prod s ↔ x ∈ comap (MonoidHom.snd M N) s
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>f : r ≼i s<VAR>a : α<VAR>x✝ : ↑{b | r b a}<VAR>x : α<VAR>h : x ∈ {b | r b a}<GOAL>((Subrel.relEmbedding r {b | r b a}).trans f.toRelEmbedding) ⟨x, h⟩ ∈ {b | s b (f a)}
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>f : r ≼i s<VAR>a : α<VAR>x✝ : ↑{b | r b a}<VAR>x : α<VAR>h : x ∈ {b | r b a}<GOAL>f.toRelEmbedding ((Subrel.relEmbedding r {b | r b a}) ⟨x, h⟩) ∈ {b | s b (f a)}
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>f : r ≼i s<VAR>a : α<VAR>x✝ : ↑{b | s b (f a)}<VAR>y : β<VAR>h : y ∈ {b | s b (f a)}<GOAL>∃ a_1, (RelEmbedding.codRestrict {b | s b (f a)} ((Subrel.relEmbedding r {b | r b a}).trans f.toRelEmbedding) ⋯) a_1 = ⟨y, h⟩
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>f : r ≼i s<VAR>a✝ : α<VAR>x✝ : ↑{b | s b (f a✝)}<VAR>a : α<VAR>h : f a ∈ {b | s b (f a✝)}<GOAL>∃ a_1, (RelEmbedding.codRestrict {b | s b (f a✝)} ((Subrel.relEmbedding r {b | r b a✝}).trans f.toRelEmbedding) ⋯) a_1 = ⟨f a, h⟩
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>s : Fin n → R<VAR>y : R<VAR>f : MvPolynomial (Fin (n + 1)) R<GOAL>(eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) ((finSuccEquiv R n) f))
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>s : Fin n → R<VAR>y : R<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] := let __src := mapRingHom (eval s); { toRingHom := __src, commutes' := ⋯ }<GOAL>(eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) ((finSuccEquiv R n) f))
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>s : Fin n → R<VAR>y : R<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] := let __src := mapRingHom (eval s); { toRingHom := __src, commutes' := ⋯ }<GOAL>aeval (Fin.cons y s) = (Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>s : Fin n → R<VAR>y : R<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] := let __src := mapRingHom (eval s); { toRingHom := __src, commutes' := ⋯ }<GOAL>∀ (i : Fin (n + 1)), (aeval (Fin.cons y s)) (X i) = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) (X i)