-- Mathlib/FieldTheory/IsAlgClosed/Basic.lean
theorem of_ringEquiv (k' : Type u) [Field k'] (e : k ≃+* k')
    [IsAlgClosed k] : IsAlgClosed k'

Proof state:
case H
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
⊢ ∃ x, eval x p = 0

Tactic:
rcases IsAlgClosed.exists_root (k := k) (p.map e.symm.toRingHom) hpe with ⟨x, hx⟩

Result:
case H.intro
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : (map e.symm.toRingHom p).IsRoot x
⊢ ∃ x, eval x p = 0

Proof state:
case h
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : (map e.symm.toRingHom p).IsRoot x
⊢ eval (e x) p = 0

Tactic:
rw [IsRoot] at hx

Result:
case h
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : eval x (map e.symm.toRingHom p) = 0
⊢ eval (e x) p = 0

Proof state:
case H
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
⊢ ∀ (p : k'[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0

Tactic:
intro p hmp hp

Result:
case H
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
⊢ ∃ x, eval x p = 0

Proof state:
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
⊢ p.degree ≠ 0

Tactic:
exact ne_of_gt (degree_pos_of_irreducible hp)

Result:
no goals

Proof state:
case h.a
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : eval x (map e.symm.toRingHom p) = 0
⊢ e.symm (eval (e x) p) = e.symm 0

Tactic:
rw [map_zero, ← hx]

Result:
case h.a
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : eval x (map e.symm.toRingHom p) = 0
⊢ e.symm (eval (e x) p) = eval x (map e.symm.toRingHom p)

Proof state:
case h.a
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : eval x (map e.symm.toRingHom p) = 0
⊢ e.symm (eval (e x) p) = eval x (map e.symm.toRingHom p)

Tactic:
clear hx hpe hp hmp

Result:
case h.a
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
x : k
⊢ e.symm (eval (e x) p) = eval x (map e.symm.toRingHom p)

Proof state:
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
⊢ (map e.symm.toRingHom p).degree ≠ 0

Tactic:
rw [degree_map]

Result:
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
⊢ p.degree ≠ 0

Proof state:
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
⊢ IsAlgClosed k'

Tactic:
apply IsAlgClosed.of_exists_root

Result:
case H
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
⊢ ∀ (p : k'[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0

Proof state:
case h.a
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
x : k
⊢ e.symm (eval (e x) p) = eval x (map e.symm.toRingHom p)

Tactic:
induction p using Polynomial.induction_on <;> simp_all

Result:
no goals

Proof state:
case H.intro
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : (map e.symm.toRingHom p).IsRoot x
⊢ ∃ x, eval x p = 0

Tactic:
use e x

Result:
case h
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : (map e.symm.toRingHom p).IsRoot x
⊢ eval (e x) p = 0

Proof state:
case h
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : eval x (map e.symm.toRingHom p) = 0
⊢ eval (e x) p = 0

Tactic:
apply e.symm.injective

Result:
case h.a
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
x : k
hx : eval x (map e.symm.toRingHom p) = 0
⊢ e.symm (eval (e x) p) = e.symm 0

Proof state:
case H
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
⊢ ∃ x, eval x p = 0

Tactic:
have hpe : degree (p.map e.symm.toRingHom) ≠ 0 := by
  rw [degree_map]
  exact ne_of_gt (degree_pos_of_irreducible hp)

Result:
case H
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
hmp : p.Monic
hp : Irreducible p
hpe : (map e.symm.toRingHom p).degree ≠ 0
⊢ ∃ x, eval x p = 0