[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0) (_ : _root_.IsAlgebraic R x)
⊢ x ∈ {x_1 | x_1 ∈ Polynomial.roots (Polynomial.map (algebraMap R L) ↑p)}
[PROOFSTEP]
dsimp
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0) (_ : _root_.IsAlgebraic R x)
⊢ x ∈
    Polynomial.roots
      (Polynomial.map (algebraMap R L)
        ↑(Classical.indefiniteDescription (fun x_1 => ¬x_1 = 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
            (_ : _root_.IsAlgebraic R x)))
[PROOFSTEP]
have h : p.1.map (algebraMap R L) ≠ 0 :=
  by
  rw [Ne.def, ← Polynomial.degree_eq_bot,
    Polynomial.degree_map_eq_of_injective (NoZeroSMulDivisors.algebraMap_injective R L), Polynomial.degree_eq_bot]
  exact p.2.1
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0) (_ : _root_.IsAlgebraic R x)
⊢ Polynomial.map (algebraMap R L) ↑p ≠ 0
[PROOFSTEP]
rw [Ne.def, ← Polynomial.degree_eq_bot,
  Polynomial.degree_map_eq_of_injective (NoZeroSMulDivisors.algebraMap_injective R L), Polynomial.degree_eq_bot]
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0) (_ : _root_.IsAlgebraic R x)
⊢ ¬↑p = 0
[PROOFSTEP]
exact p.2.1
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0) (_ : _root_.IsAlgebraic R x)
h : Polynomial.map (algebraMap R L) ↑p ≠ 0
⊢ x ∈
    Polynomial.roots
      (Polynomial.map (algebraMap R L)
        ↑(Classical.indefiniteDescription (fun x_1 => ¬x_1 = 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
            (_ : _root_.IsAlgebraic R x)))
[PROOFSTEP]
erw [Polynomial.mem_roots h, Polynomial.IsRoot, Polynomial.eval_map, ← Polynomial.aeval_def, p.2.2]
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x y : L
⊢ (fun x =>
          let p :=
            Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
              (_ : _root_.IsAlgebraic R x);
          { fst := ↑p,
            snd :=
              { val := x, property := (_ : x ∈ {x_1 | x_1 ∈ Polynomial.roots (Polynomial.map (algebraMap R L) ↑p)}) } })
        x =
      (fun x =>
          let p :=
            Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
              (_ : _root_.IsAlgebraic R x);
          { fst := ↑p,
            snd :=
              { val := x, property := (_ : x ∈ {x_1 | x_1 ∈ Polynomial.roots (Polynomial.map (algebraMap R L) ↑p)}) } })
        y →
    x = y
[PROOFSTEP]
intro h
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x y : L
h :
  (fun x =>
        let p :=
          Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
            (_ : _root_.IsAlgebraic R x);
        { fst := ↑p,
          snd :=
            { val := x, property := (_ : x ∈ {x_1 | x_1 ∈ Polynomial.roots (Polynomial.map (algebraMap R L) ↑p)}) } })
      x =
    (fun x =>
        let p :=
          Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
            (_ : _root_.IsAlgebraic R x);
        { fst := ↑p,
          snd :=
            { val := x, property := (_ : x ∈ {x_1 | x_1 ∈ Polynomial.roots (Polynomial.map (algebraMap R L) ↑p)}) } })
      y
⊢ x = y
[PROOFSTEP]
simp at h 
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x y : L
h :
  ↑(Classical.indefiniteDescription (fun x_1 => ¬x_1 = 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
          (_ : _root_.IsAlgebraic R x)) =
      ↑(Classical.indefiniteDescription (fun x => ¬x = 0 ∧ ↑(Polynomial.aeval y) x = 0) (_ : _root_.IsAlgebraic R y)) ∧
    HEq
      { val := x,
        property :=
          (_ :
            x ∈
              {x_1 |
                x_1 ∈
                  Polynomial.roots
                    (Polynomial.map (algebraMap R L)
                      ↑(Classical.indefiniteDescription (fun x_2 => x_2 ≠ 0 ∧ ↑(Polynomial.aeval x) x_2 = 0)
                          (_ : _root_.IsAlgebraic R x)))}) }
      { val := y,
        property :=
          (_ :
            y ∈
              {x |
                x ∈
                  Polynomial.roots
                    (Polynomial.map (algebraMap R L)
                      ↑(Classical.indefiniteDescription (fun x => x ≠ 0 ∧ ↑(Polynomial.aeval y) x = 0)
                          (_ : _root_.IsAlgebraic R y)))}) }
⊢ x = y
[PROOFSTEP]
refine' (Subtype.heq_iff_coe_eq _).1 h.2
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x y : L
h :
  ↑(Classical.indefiniteDescription (fun x_1 => ¬x_1 = 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
          (_ : _root_.IsAlgebraic R x)) =
      ↑(Classical.indefiniteDescription (fun x => ¬x = 0 ∧ ↑(Polynomial.aeval y) x = 0) (_ : _root_.IsAlgebraic R y)) ∧
    HEq
      { val := x,
        property :=
          (_ :
            x ∈
              {x_1 |
                x_1 ∈
                  Polynomial.roots
                    (Polynomial.map (algebraMap R L)
                      ↑(Classical.indefiniteDescription (fun x_2 => x_2 ≠ 0 ∧ ↑(Polynomial.aeval x) x_2 = 0)
                          (_ : _root_.IsAlgebraic R x)))}) }
      { val := y,
        property :=
          (_ :
            y ∈
              {x |
                x ∈
                  Polynomial.roots
                    (Polynomial.map (algebraMap R L)
                      ↑(Classical.indefiniteDescription (fun x => x ≠ 0 ∧ ↑(Polynomial.aeval y) x = 0)
                          (_ : _root_.IsAlgebraic R y)))}) }
⊢ ∀ (x_1 : L),
    x_1 ∈
        {x_2 |
          x_2 ∈
            Polynomial.roots
              (Polynomial.map (algebraMap R L)
                ↑(Classical.indefiniteDescription (fun x_3 => x_3 ≠ 0 ∧ ↑(Polynomial.aeval x) x_3 = 0)
                    (_ : _root_.IsAlgebraic R x)))} ↔
      x_1 ∈
        {x |
          x ∈
            Polynomial.roots
              (Polynomial.map (algebraMap R L)
                ↑(Classical.indefiniteDescription (fun x => x ≠ 0 ∧ ↑(Polynomial.aeval y) x = 0)
                    (_ : _root_.IsAlgebraic R y)))}
[PROOFSTEP]
simp only [h.1, iff_self_iff, forall_true_iff]
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
⊢ #((p : R[X]) × { x // x ∈ Polynomial.roots (Polynomial.map (algebraMap R L) p) }) =
    sum fun p => #↑{x | x ∈ Polynomial.roots (Polynomial.map (algebraMap R L) p)}
[PROOFSTEP]
rw [← mk_sigma]
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
⊢ #((p : R[X]) × { x // x ∈ Polynomial.roots (Polynomial.map (algebraMap R L) p) }) =
    #((i : R[X]) × ↑{x | x ∈ Polynomial.roots (Polynomial.map (algebraMap R L) i)})
[PROOFSTEP]
rfl
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
⊢ max (max (max #R ℵ₀) ℵ₀) ℵ₀ = max #R ℵ₀
[PROOFSTEP]
simp only [max_assoc, max_comm ℵ₀, max_left_comm ℵ₀, max_self]
[GOAL]
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : Field L
inst✝¹ : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
inst✝ : IsAlgClosed K
hv : IsTranscendenceBasis R v
this : Nontrivial R := RingHom.domain_nontrivial (algebraMap R K)
⊢ IsAlgClosed K
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
⊢ K ≃+* L
[PROOFSTEP]
letI := isAlgClosure_of_transcendence_basis v hv
[GOAL]
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
⊢ K ≃+* L
[PROOFSTEP]
letI := isAlgClosure_of_transcendence_basis w hw
[GOAL]
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
⊢ K ≃+* L
[PROOFSTEP]
have e : Algebra.adjoin R (Set.range v) ≃+* Algebra.adjoin R (Set.range w)
[GOAL]
case e
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
⊢ { x // x ∈ Algebra.adjoin R (Set.range v) } ≃+* { x // x ∈ Algebra.adjoin R (Set.range w) }
[PROOFSTEP]
refine' hv.1.aevalEquiv.symm.toRingEquiv.trans _
[GOAL]
case e
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
⊢ MvPolynomial ι R ≃+* { x // x ∈ Algebra.adjoin R (Set.range w) }
[PROOFSTEP]
refine' (AlgEquiv.ofAlgHom (MvPolynomial.rename e) (MvPolynomial.rename e.symm) _ _).toRingEquiv.trans _
[GOAL]
case e.refine'_1
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
⊢ AlgHom.comp (MvPolynomial.rename ↑e) (MvPolynomial.rename ↑e.symm) = AlgHom.id R (MvPolynomial κ R)
[PROOFSTEP]
ext
[GOAL]
case e.refine'_1.hf.a
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
i✝ : κ
m✝ : κ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑(AlgHom.comp (MvPolynomial.rename ↑e) (MvPolynomial.rename ↑e.symm)) (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ (↑(AlgHom.id R (MvPolynomial κ R)) (MvPolynomial.X i✝))
[PROOFSTEP]
simp
[GOAL]
case e.refine'_2
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
⊢ AlgHom.comp (MvPolynomial.rename ↑e.symm) (MvPolynomial.rename ↑e) = AlgHom.id R (MvPolynomial ι R)
[PROOFSTEP]
ext
[GOAL]
case e.refine'_2.hf.a
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
i✝ : ι
m✝ : ι →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑(AlgHom.comp (MvPolynomial.rename ↑e.symm) (MvPolynomial.rename ↑e)) (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ (↑(AlgHom.id R (MvPolynomial ι R)) (MvPolynomial.X i✝))
[PROOFSTEP]
simp
[GOAL]
case e.refine'_3
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
⊢ MvPolynomial κ R ≃+* { x // x ∈ Algebra.adjoin R (Set.range w) }
[PROOFSTEP]
exact hw.1.aevalEquiv.toRingEquiv
[GOAL]
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e✝ : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
e : { x // x ∈ Algebra.adjoin R (Set.range v) } ≃+* { x // x ∈ Algebra.adjoin R (Set.range w) }
⊢ K ≃+* L
[PROOFSTEP]
exact IsAlgClosure.equivOfEquiv K L e
[GOAL]
R L K : Type u
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ hv : IsTranscendenceBasis R v
⊢ max #{ x // x ∈ Algebra.adjoin R (Set.range v) } ℵ₀ = max #(MvPolynomial ι R) ℵ₀
[PROOFSTEP]
rw [Cardinal.eq.2 ⟨hv.1.aevalEquiv.toEquiv⟩]
[GOAL]
R L K : Type u
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ hv : IsTranscendenceBasis R v
⊢ max (max (max #R #ι) ℵ₀) ℵ₀ = max (max #R #ι) ℵ₀
[PROOFSTEP]
simp [max_assoc]
[GOAL]
R L K : Type u
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ : IsTranscendenceBasis R v
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ #ι
⊢ max (max #R #ι) ℵ₀ = #ι
[PROOFSTEP]
rw [max_eq_left, max_eq_right]
[GOAL]
R L K : Type u
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ : IsTranscendenceBasis R v
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ #ι
⊢ #R ≤ #ι
[PROOFSTEP]
exact le_trans hR this
[GOAL]
R L K : Type u
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ : IsTranscendenceBasis R v
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ #ι
⊢ ℵ₀ ≤ max #R #ι
[PROOFSTEP]
exact le_max_of_le_right this
[GOAL]
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : #K = #L
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
cases' exists_isTranscendenceBasis ℤ (show Function.Injective (algebraMap ℤ K) from Int.cast_injective) with s hs
[GOAL]
case intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : #K = #L
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
cases' exists_isTranscendenceBasis ℤ (show Function.Injective (algebraMap ℤ L) from Int.cast_injective) with t ht
[GOAL]
case intro.intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : #K = #L
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
have : #s = #t :=
  by
  rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs (le_of_eq mk_int) hK, ←
    cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht (le_of_eq mk_int), hKL]
  rwa [← hKL]
[GOAL]
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : #K = #L
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ #↑s = #↑t
[PROOFSTEP]
rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs (le_of_eq mk_int) hK, ←
  cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht (le_of_eq mk_int), hKL]
[GOAL]
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : #K = #L
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ ℵ₀ < #L
[PROOFSTEP]
rwa [← hKL]
[GOAL]
case intro.intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : #K = #L
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
this : #↑s = #↑t
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
cases' Cardinal.eq.1 this with e
[GOAL]
case intro.intro.intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : #K = #L
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
this : #↑s = #↑t
e : ↑s ≃ ↑t
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
exact ⟨equivOfTranscendenceBasis _ _ e hs ht⟩
[GOAL]
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
letI : Algebra (ZMod p) K := ZMod.algebra _ _
[GOAL]
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this : Algebra (ZMod p) K := ZMod.algebra K p
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
letI : Algebra (ZMod p) L := ZMod.algebra _ _
[GOAL]
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
cases'
  exists_isTranscendenceBasis (ZMod p) (show Function.Injective (algebraMap (ZMod p) K) from RingHom.injective _) with s
  hs
[GOAL]
case intro
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
cases'
  exists_isTranscendenceBasis (ZMod p) (show Function.Injective (algebraMap (ZMod p) L) from RingHom.injective _) with t
  ht
[GOAL]
case intro.intro
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
have : #s = #t :=
  by
  rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs (lt_aleph0_of_finite (ZMod p)).le hK, ←
    cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht (lt_aleph0_of_finite (ZMod p)).le, hKL]
  rwa [← hKL]
[GOAL]
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ #↑s = #↑t
[PROOFSTEP]
rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs (lt_aleph0_of_finite (ZMod p)).le hK, ←
  cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht (lt_aleph0_of_finite (ZMod p)).le, hKL]
[GOAL]
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ ℵ₀ < #L
[PROOFSTEP]
rwa [← hKL]
[GOAL]
case intro.intro
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this✝¹ : Algebra (ZMod p) K := ZMod.algebra K p
this✝ : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
this : #↑s = #↑t
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
cases' Cardinal.eq.1 this with e
[GOAL]
case intro.intro.intro
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this✝¹ : Algebra (ZMod p) K := ZMod.algebra K p
this✝ : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
this : #↑s = #↑t
e : ↑s ≃ ↑t
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
exact ⟨equivOfTranscendenceBasis _ _ e hs ht⟩
[GOAL]
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
rcases CharP.char_is_prime_or_zero K p with (hp | hp)
[GOAL]
case inl
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
hp : Nat.Prime p
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
haveI : Fact p.Prime := ⟨hp⟩
[GOAL]
case inl
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
exact ringEquivOfCardinalEqOfCharP p hK hKL
[GOAL]
case inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
hp : p = 0
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
simp only [hp] at *
[GOAL]
case inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
hK : ℵ₀ < #K
hKL : #K = #L
inst✝¹ : CharP K 0
inst✝ : CharP L 0
hp : True
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
letI : CharZero K := CharP.charP_to_charZero K
[GOAL]
case inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
hK : ℵ₀ < #K
hKL : #K = #L
inst✝¹ : CharP K 0
inst✝ : CharP L 0
hp : True
this : CharZero K := CharP.charP_to_charZero K
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
letI : CharZero L := CharP.charP_to_charZero L
[GOAL]
case inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
hK : ℵ₀ < #K
hKL : #K = #L
inst✝¹ : CharP K 0
inst✝ : CharP L 0
hp : True
this✝ : CharZero K := CharP.charP_to_charZero K
this : CharZero L := CharP.charP_to_charZero L
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
exact ringEquivOfCardinalEqOfCharZero hK hKL
