[GOAL]
k : Type u
inst✝ : Field k
s : Finset (MonicIrreducible k)
f : MonicIrreducible k
hf : f ∈ s
⊢ ↑(toSplittingField k s) (evalXSelf k f) = 0
[PROOFSTEP]
rw [toSplittingField, evalXSelf, ← AlgHom.coe_toRingHom, hom_eval₂, AlgHom.coe_toRingHom, MvPolynomial.aeval_X,
  dif_pos hf, ← algebraMap_eq, AlgHom.comp_algebraMap]
[GOAL]
k : Type u
inst✝ : Field k
s : Finset (MonicIrreducible k)
f : MonicIrreducible k
hf : f ∈ s
⊢ Polynomial.eval₂ (algebraMap k (SplittingField (∏ x in s, ↑x)))
      (rootOfSplits (algebraMap k (SplittingField (∏ x in s, ↑x)))
        (_ : Splits (algebraMap k (SplittingField (∏ x in s, ↑x))) ↑f) (_ : ¬degree ↑f = 0))
      ↑f =
    0
[PROOFSTEP]
exact map_rootOfSplits _ _ _
[GOAL]
k : Type u
inst✝ : Field k
⊢ spanEval k ≠ ⊤
[PROOFSTEP]
rw [Ideal.ne_top_iff_one, spanEval, Ideal.span, ← Set.image_univ, Finsupp.mem_span_image_iff_total]
[GOAL]
k : Type u
inst✝ : Field k
⊢ ¬∃ l,
      l ∈ Finsupp.supported (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k) Set.univ ∧
        ↑(Finsupp.total (MonicIrreducible k) (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k)
                (evalXSelf k))
            l =
          1
[PROOFSTEP]
rintro ⟨v, _, hv⟩
[GOAL]
case intro.intro
k : Type u
inst✝ : Field k
v : MonicIrreducible k →₀ MvPolynomial (MonicIrreducible k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k) Set.univ
hv :
  ↑(Finsupp.total (MonicIrreducible k) (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k)
          (evalXSelf k))
      v =
    1
⊢ False
[PROOFSTEP]
replace hv := congr_arg (toSplittingField k v.support) hv
[GOAL]
case intro.intro
k : Type u
inst✝ : Field k
v : MonicIrreducible k →₀ MvPolynomial (MonicIrreducible k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k) Set.univ
hv :
  ↑(toSplittingField k v.support)
      (↑(Finsupp.total (MonicIrreducible k) (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k)
            (evalXSelf k))
        v) =
    ↑(toSplittingField k v.support) 1
⊢ False
[PROOFSTEP]
rw [AlgHom.map_one, Finsupp.total_apply, Finsupp.sum, AlgHom.map_sum, Finset.sum_eq_zero] at hv
[GOAL]
case intro.intro
k : Type u
inst✝ : Field k
v : MonicIrreducible k →₀ MvPolynomial (MonicIrreducible k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k) Set.univ
hv : 0 = 1
⊢ False
[PROOFSTEP]
exact zero_ne_one hv
[GOAL]
case intro.intro
k : Type u
inst✝ : Field k
v : MonicIrreducible k →₀ MvPolynomial (MonicIrreducible k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k) Set.univ
hv : ∑ x in v.support, ↑(toSplittingField k v.support) (↑v x • evalXSelf k x) = 1
⊢ ∀ (x : MonicIrreducible k), x ∈ v.support → ↑(toSplittingField k v.support) (↑v x • evalXSelf k x) = 0
[PROOFSTEP]
intro j hj
[GOAL]
case intro.intro
k : Type u
inst✝ : Field k
v : MonicIrreducible k →₀ MvPolynomial (MonicIrreducible k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (MonicIrreducible k) k) (MvPolynomial (MonicIrreducible k) k) Set.univ
hv : ∑ x in v.support, ↑(toSplittingField k v.support) (↑v x • evalXSelf k x) = 1
j : MonicIrreducible k
hj : j ∈ v.support
⊢ ↑(toSplittingField k v.support) (↑v j • evalXSelf k j) = 0
[PROOFSTEP]
rw [smul_eq_mul, AlgHom.map_mul, toSplittingField_evalXSelf (s := v.support) hj, mul_zero]
[GOAL]
k : Type u
inst✝ : Field k
z : AdjoinMonic k
⊢ IsIntegral k z
[PROOFSTEP]
let ⟨p, hp⟩ := Ideal.Quotient.mk_surjective z
[GOAL]
k : Type u
inst✝ : Field k
z : AdjoinMonic k
p : MvPolynomial (MonicIrreducible k) k
hp : ↑(Ideal.Quotient.mk (maxIdeal k)) p = z
⊢ IsIntegral k z
[PROOFSTEP]
rw [← hp]
[GOAL]
k : Type u
inst✝ : Field k
z : AdjoinMonic k
p : MvPolynomial (MonicIrreducible k) k
hp : ↑(Ideal.Quotient.mk (maxIdeal k)) p = z
⊢ IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) p)
[PROOFSTEP]
induction p using MvPolynomial.induction_on generalizing z with
| h_C => exact isIntegral_algebraMap
| h_add _ _ ha hb => exact isIntegral_add (ha _ rfl) (hb _ rfl)
| h_X p f ih =>
  · refine @isIntegral_mul k _ _ _ _ _ (Ideal.Quotient.mk (maxIdeal k) _) (ih _ rfl) ?_
    refine ⟨f, f.2.1, ?_⟩
    erw [AdjoinMonic.algebraMap, ← hom_eval₂, Ideal.Quotient.eq_zero_iff_mem]
    exact le_maxIdeal k (Ideal.subset_span ⟨f, rfl⟩)
[GOAL]
k : Type u
inst✝ : Field k
z : AdjoinMonic k
p : MvPolynomial (MonicIrreducible k) k
hp : ↑(Ideal.Quotient.mk (maxIdeal k)) p = z
⊢ IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) p)
[PROOFSTEP]
induction p using MvPolynomial.induction_on generalizing z with
| h_C => exact isIntegral_algebraMap
| h_add _ _ ha hb => exact isIntegral_add (ha _ rfl) (hb _ rfl)
| h_X p f ih =>
  · refine @isIntegral_mul k _ _ _ _ _ (Ideal.Quotient.mk (maxIdeal k) _) (ih _ rfl) ?_
    refine ⟨f, f.2.1, ?_⟩
    erw [AdjoinMonic.algebraMap, ← hom_eval₂, Ideal.Quotient.eq_zero_iff_mem]
    exact le_maxIdeal k (Ideal.subset_span ⟨f, rfl⟩)
[GOAL]
case h_C
k : Type u
inst✝ : Field k
a✝ : k
z : AdjoinMonic k
hp : ↑(Ideal.Quotient.mk (maxIdeal k)) (↑MvPolynomial.C a✝) = z
⊢ IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) (↑MvPolynomial.C a✝))
[PROOFSTEP]

| h_C => exact isIntegral_algebraMap
[GOAL]
case h_C
k : Type u
inst✝ : Field k
a✝ : k
z : AdjoinMonic k
hp : ↑(Ideal.Quotient.mk (maxIdeal k)) (↑MvPolynomial.C a✝) = z
⊢ IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) (↑MvPolynomial.C a✝))
[PROOFSTEP]
exact isIntegral_algebraMap
[GOAL]
case h_add
k : Type u
inst✝ : Field k
p✝ q✝ : MvPolynomial (MonicIrreducible k) k
ha :
  ∀ (z : AdjoinMonic k), ↑(Ideal.Quotient.mk (maxIdeal k)) p✝ = z → IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) p✝)
hb :
  ∀ (z : AdjoinMonic k), ↑(Ideal.Quotient.mk (maxIdeal k)) q✝ = z → IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) q✝)
z : AdjoinMonic k
hp : ↑(Ideal.Quotient.mk (maxIdeal k)) (p✝ + q✝) = z
⊢ IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) (p✝ + q✝))
[PROOFSTEP]

| h_add _ _ ha hb => exact isIntegral_add (ha _ rfl) (hb _ rfl)
[GOAL]
case h_add
k : Type u
inst✝ : Field k
p✝ q✝ : MvPolynomial (MonicIrreducible k) k
ha :
  ∀ (z : AdjoinMonic k), ↑(Ideal.Quotient.mk (maxIdeal k)) p✝ = z → IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) p✝)
hb :
  ∀ (z : AdjoinMonic k), ↑(Ideal.Quotient.mk (maxIdeal k)) q✝ = z → IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) q✝)
z : AdjoinMonic k
hp : ↑(Ideal.Quotient.mk (maxIdeal k)) (p✝ + q✝) = z
⊢ IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) (p✝ + q✝))
[PROOFSTEP]
exact isIntegral_add (ha _ rfl) (hb _ rfl)
[GOAL]
case h_X
k : Type u
inst✝ : Field k
p : MvPolynomial (MonicIrreducible k) k
f : MonicIrreducible k
ih : ∀ (z : AdjoinMonic k), ↑(Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) p)
z : AdjoinMonic k
hp : ↑(Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X f) = z
⊢ IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X f))
[PROOFSTEP]

| h_X p f ih =>
  · refine @isIntegral_mul k _ _ _ _ _ (Ideal.Quotient.mk (maxIdeal k) _) (ih _ rfl) ?_
    refine ⟨f, f.2.1, ?_⟩
    erw [AdjoinMonic.algebraMap, ← hom_eval₂, Ideal.Quotient.eq_zero_iff_mem]
    exact le_maxIdeal k (Ideal.subset_span ⟨f, rfl⟩)
[GOAL]
case h_X
k : Type u
inst✝ : Field k
p : MvPolynomial (MonicIrreducible k) k
f : MonicIrreducible k
ih : ∀ (z : AdjoinMonic k), ↑(Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) p)
z : AdjoinMonic k
hp : ↑(Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X f) = z
⊢ IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X f))
[PROOFSTEP]
refine @isIntegral_mul k _ _ _ _ _ (Ideal.Quotient.mk (maxIdeal k) _) (ih _ rfl) ?_
[GOAL]
case h_X
k : Type u
inst✝ : Field k
p : MvPolynomial (MonicIrreducible k) k
f : MonicIrreducible k
ih : ∀ (z : AdjoinMonic k), ↑(Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) p)
z : AdjoinMonic k
hp : ↑(Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X f) = z
⊢ IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X f))
[PROOFSTEP]
refine ⟨f, f.2.1, ?_⟩
[GOAL]
case h_X
k : Type u
inst✝ : Field k
p : MvPolynomial (MonicIrreducible k) k
f : MonicIrreducible k
ih : ∀ (z : AdjoinMonic k), ↑(Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) p)
z : AdjoinMonic k
hp : ↑(Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X f) = z
⊢ Polynomial.eval₂
      (_root_.algebraMap k ((fun x => MvPolynomial (MonicIrreducible k) k ⧸ maxIdeal k) (MvPolynomial.X f)))
      (↑(Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X f)) ↑f =
    0
[PROOFSTEP]
erw [AdjoinMonic.algebraMap, ← hom_eval₂, Ideal.Quotient.eq_zero_iff_mem]
[GOAL]
case h_X
k : Type u
inst✝ : Field k
p : MvPolynomial (MonicIrreducible k) k
f : MonicIrreducible k
ih : ∀ (z : AdjoinMonic k), ↑(Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k (↑(Ideal.Quotient.mk (maxIdeal k)) p)
z : AdjoinMonic k
hp : ↑(Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X f) = z
⊢ Polynomial.eval₂ MvPolynomial.C (MvPolynomial.X f) ↑f ∈ maxIdeal k
[PROOFSTEP]
exact le_maxIdeal k (Ideal.subset_span ⟨f, rfl⟩)
[GOAL]
k : Type u
inst✝ : Field k
f : k[X]
hfm : Monic f
hfi : Irreducible f
⊢ Polynomial.eval₂ (toAdjoinMonic k)
      (↑(Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X { val := f, property := (_ : Monic f ∧ Irreducible f) })) f =
    0
[PROOFSTEP]
rw [toAdjoinMonic, ← hom_eval₂, Ideal.Quotient.eq_zero_iff_mem]
[GOAL]
k : Type u
inst✝ : Field k
f : k[X]
hfm : Monic f
hfi : Irreducible f
⊢ Polynomial.eval₂ MvPolynomial.C (MvPolynomial.X { val := f, property := (_ : Monic f ∧ Irreducible f) }) f ∈
    maxIdeal k
[PROOFSTEP]
exact le_maxIdeal k (Ideal.subset_span <| ⟨_, rfl⟩)
[GOAL]
k : Type u
inst✝ : Field k
n : ℕ
f : (Step k n)[X]
hfm : Monic f
hfi : Irreducible f
⊢ ∃ x, Polynomial.eval₂ (toStepSucc k n) x f = 0
[PROOFSTEP]
obtain ⟨x, hx⟩ := @AdjoinMonic.exists_root _ (Step.field k n) _ hfm hfi
[GOAL]
case intro
k : Type u
inst✝ : Field k
n : ℕ
f : (Step k n)[X]
hfm : Monic f
hfi : Irreducible f
x : AdjoinMonic (Step k n)
hx : Polynomial.eval₂ (toAdjoinMonic (Step k n)) x f = 0
⊢ ∃ x, Polynomial.eval₂ (toStepSucc k n) x f = 0
[PROOFSTEP]
exact ⟨x, by apply hx⟩
[GOAL]
k : Type u
inst✝ : Field k
n : ℕ
f : (Step k n)[X]
hfm : Monic f
hfi : Irreducible f
x : AdjoinMonic (Step k n)
hx : Polynomial.eval₂ (toAdjoinMonic (Step k n)) x f = 0
⊢ Polynomial.eval₂ (toStepSucc k n) x f = 0
[PROOFSTEP]
apply hx
[GOAL]
k : Type u
inst✝ : Field k
m n : ℕ
h : m ≤ n
⊢ AlgebraicClosure.toStepOfLE' k m (Nat.succ n) (_ : m ≤ Nat.succ n) =
    ↑(toStepSucc k n) ∘ AlgebraicClosure.toStepOfLE' k m n h
[PROOFSTEP]
ext x
[GOAL]
case h
k : Type u
inst✝ : Field k
m n : ℕ
h : m ≤ n
x : Step k m
⊢ AlgebraicClosure.toStepOfLE' k m (Nat.succ n) (_ : m ≤ Nat.succ n) x =
    (↑(toStepSucc k n) ∘ AlgebraicClosure.toStepOfLE' k m n h) x
[PROOFSTEP]
convert Nat.leRecOn_succ h x
[GOAL]
case h.convert_1
k : Type u
inst✝ : Field k
m n : ℕ
h : m ≤ n
x : Step k m
⊢ m ≤ n + 1
[PROOFSTEP]
exact h.trans n.le_succ
[GOAL]
k : Type u
inst✝ : Field k
m n : ℕ
h : m ≤ n
⊢ AlgebraicClosure.toStepOfLE' k m n h 1 = 1
[PROOFSTEP]
induction' h with a h ih
[GOAL]
case refl
k : Type u
inst✝ : Field k
m n : ℕ
⊢ AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1
[PROOFSTEP]
exact Nat.leRecOn_self 1
[GOAL]
case step
k : Type u
inst✝ : Field k
m n a : ℕ
h : Nat.le m a
ih : AlgebraicClosure.toStepOfLE' k m a h 1 = 1
⊢ AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1
[PROOFSTEP]
rw [toStepOfLE'.succ k m a h]
[GOAL]
case step
k : Type u
inst✝ : Field k
m n a : ℕ
h : Nat.le m a
ih : AlgebraicClosure.toStepOfLE' k m a h 1 = 1
⊢ (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) 1 = 1
[PROOFSTEP]
simp [ih]
[GOAL]
k : Type u
inst✝ : Field k
m n : ℕ
h : m ≤ n
x y : Step k m
⊢ OneHom.toFun
      { toFun := AlgebraicClosure.toStepOfLE' k m n h, map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := AlgebraicClosure.toStepOfLE' k m n h, map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
        x *
      OneHom.toFun
        { toFun := AlgebraicClosure.toStepOfLE' k m n h, map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
        y
[PROOFSTEP]
induction' h with a h ih
[GOAL]
case refl
k : Type u
inst✝ : Field k
m n : ℕ
x y : Step k m
⊢ OneHom.toFun
      { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
        x *
      OneHom.toFun
        { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
        y
[PROOFSTEP]
dsimp [toStepOfLE']
[GOAL]
case refl
k : Type u
inst✝ : Field k
m n : ℕ
x y : Step k m
⊢ Nat.leRecOn (_ : Nat.le m m) (fun a => ↑(toStepSucc k a)) (x * y) =
    Nat.leRecOn (_ : Nat.le m m) (fun a => ↑(toStepSucc k a)) x *
      Nat.leRecOn (_ : Nat.le m m) (fun a => ↑(toStepSucc k a)) y
[PROOFSTEP]
simp_rw [Nat.leRecOn_self]
[GOAL]
case step
k : Type u
inst✝ : Field k
m n : ℕ
x y : Step k m
a : ℕ
h : Nat.le m a
ih :
  OneHom.toFun
      { toFun := AlgebraicClosure.toStepOfLE' k m a h, map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := AlgebraicClosure.toStepOfLE' k m a h, map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
        x *
      OneHom.toFun
        { toFun := AlgebraicClosure.toStepOfLE' k m a h, map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
        y
⊢ OneHom.toFun
      { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
        x *
      OneHom.toFun
        { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
        y
[PROOFSTEP]
simp_rw [toStepOfLE'.succ k m a h]
[GOAL]
case step
k : Type u
inst✝ : Field k
m n : ℕ
x y : Step k m
a : ℕ
h : Nat.le m a
ih :
  OneHom.toFun
      { toFun := AlgebraicClosure.toStepOfLE' k m a h, map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := AlgebraicClosure.toStepOfLE' k m a h, map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
        x *
      OneHom.toFun
        { toFun := AlgebraicClosure.toStepOfLE' k m a h, map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
        y
⊢ (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) (x * y) =
    (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) x *
      (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) y
[PROOFSTEP]
simp only at ih
[GOAL]
case step
k : Type u
inst✝ : Field k
m n : ℕ
x y : Step k m
a : ℕ
h : Nat.le m a
ih :
  AlgebraicClosure.toStepOfLE' k m a h (x * y) =
    AlgebraicClosure.toStepOfLE' k m a h x * AlgebraicClosure.toStepOfLE' k m a h y
⊢ (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) (x * y) =
    (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) x *
      (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) y
[PROOFSTEP]
simp [ih]
  -- Porting note: original proof was `induction' h with n h ih; · exact Nat.leRecOn_self 0`
  --                                   `rw [Nat.leRecOn_succ h, ih, RingHom.map_zero]`
[GOAL]
k : Type u
inst✝ : Field k
m n : ℕ
h : m ≤ n
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := AlgebraicClosure.toStepOfLE' k m n h,
              map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Step k m),
                OneHom.toFun
                    { toFun := AlgebraicClosure.toStepOfLE' k m n h,
                      map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m n h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m n h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
                      y) })
      0 =
    0
[PROOFSTEP]
induction' h with a h ih
[GOAL]
case refl
k : Type u
inst✝ : Field k
m n : ℕ
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
              map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Step k m),
                OneHom.toFun
                    { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
                      map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
                      y) })
      0 =
    0
[PROOFSTEP]
exact Nat.leRecOn_self 0
[GOAL]
case step
k : Type u
inst✝ : Field k
m n a : ℕ
h : Nat.le m a
ih :
  OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := AlgebraicClosure.toStepOfLE' k m a h,
              map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Step k m),
                OneHom.toFun
                    { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                      map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                      y) })
      0 =
    0
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
              map_one' := (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Step k m),
                OneHom.toFun
                    { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
                      map_one' :=
                        (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
                        map_one' :=
                          (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
                        map_one' :=
                          (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
                      y) })
      0 =
    0
[PROOFSTEP]
simp_rw [toStepOfLE'.succ k m a h]
[GOAL]
case step
k : Type u
inst✝ : Field k
m n a : ℕ
h : Nat.le m a
ih :
  OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := AlgebraicClosure.toStepOfLE' k m a h,
              map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Step k m),
                OneHom.toFun
                    { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                      map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                      y) })
      0 =
    0
⊢ (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) 0 = 0
[PROOFSTEP]
simp only at ih
[GOAL]
case step
k : Type u
inst✝ : Field k
m n a : ℕ
h : Nat.le m a
ih : AlgebraicClosure.toStepOfLE' k m a h 0 = 0
⊢ (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) 0 = 0
[PROOFSTEP]
simp [ih]
[GOAL]
k : Type u
inst✝ : Field k
m n : ℕ
h : m ≤ n
x y : Step k m
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := AlgebraicClosure.toStepOfLE' k m n h,
              map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Step k m),
                OneHom.toFun
                    { toFun := AlgebraicClosure.toStepOfLE' k m n h,
                      map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m n h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m n h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
                      y) })
      (x + y) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := AlgebraicClosure.toStepOfLE' k m n h,
                map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Step k m),
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m n h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m n h,
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m n h,
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
                        y) })
        x +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := AlgebraicClosure.toStepOfLE' k m n h,
                map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Step k m),
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m n h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m n h,
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m n h,
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m n h 1 = 1) }
                        y) })
        y
[PROOFSTEP]
induction' h with a h ih
[GOAL]
case refl
k : Type u
inst✝ : Field k
m n : ℕ
x y : Step k m
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
              map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Step k m),
                OneHom.toFun
                    { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
                      map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
                      y) })
      (x + y) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
                map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Step k m),
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
                        y) })
        x +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
                map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Step k m),
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m),
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m m (_ : Nat.le m m) 1 = 1) }
                        y) })
        y
[PROOFSTEP]
dsimp [toStepOfLE']
[GOAL]
case refl
k : Type u
inst✝ : Field k
m n : ℕ
x y : Step k m
⊢ Nat.leRecOn (_ : Nat.le m m) (fun a => ↑(toStepSucc k a)) (x + y) =
    Nat.leRecOn (_ : Nat.le m m) (fun a => ↑(toStepSucc k a)) x +
      Nat.leRecOn (_ : Nat.le m m) (fun a => ↑(toStepSucc k a)) y
[PROOFSTEP]
simp_rw [Nat.leRecOn_self]
[GOAL]
case step
k : Type u
inst✝ : Field k
m n : ℕ
x y : Step k m
a : ℕ
h : Nat.le m a
ih :
  OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := AlgebraicClosure.toStepOfLE' k m a h,
              map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Step k m),
                OneHom.toFun
                    { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                      map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                      y) })
      (x + y) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Step k m),
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                        y) })
        x +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Step k m),
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                        y) })
        y
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
              map_one' := (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Step k m),
                OneHom.toFun
                    { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
                      map_one' :=
                        (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
                        map_one' :=
                          (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
                        map_one' :=
                          (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
                      y) })
      (x + y) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
                map_one' := (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Step k m),
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
                        map_one' :=
                          (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
                          map_one' :=
                            (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
                          map_one' :=
                            (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
                        y) })
        x +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
                map_one' := (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Step k m),
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
                        map_one' :=
                          (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
                          map_one' :=
                            (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)),
                          map_one' :=
                            (_ : AlgebraicClosure.toStepOfLE' k m (Nat.succ a) (_ : Nat.le m (Nat.succ a)) 1 = 1) }
                        y) })
        y
[PROOFSTEP]
simp_rw [toStepOfLE'.succ k m a h]
[GOAL]
case step
k : Type u
inst✝ : Field k
m n : ℕ
x y : Step k m
a : ℕ
h : Nat.le m a
ih :
  OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := AlgebraicClosure.toStepOfLE' k m a h,
              map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Step k m),
                OneHom.toFun
                    { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                      map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                      y) })
      (x + y) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Step k m),
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                        y) })
        x +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Step k m),
                  OneHom.toFun
                      { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                        map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := AlgebraicClosure.toStepOfLE' k m a h,
                          map_one' := (_ : AlgebraicClosure.toStepOfLE' k m a h 1 = 1) }
                        y) })
        y
⊢ (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) (x + y) =
    (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) x +
      (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) y
[PROOFSTEP]
simp only at ih
[GOAL]
case step
k : Type u
inst✝ : Field k
m n : ℕ
x y : Step k m
a : ℕ
h : Nat.le m a
ih :
  AlgebraicClosure.toStepOfLE' k m a h (x + y) =
    AlgebraicClosure.toStepOfLE' k m a h x + AlgebraicClosure.toStepOfLE' k m a h y
⊢ (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) (x + y) =
    (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) x +
      (↑(toStepSucc k a) ∘ AlgebraicClosure.toStepOfLE' k m a h) y
[PROOFSTEP]
simp [ih]
[GOAL]
k : Type u
inst✝ : Field k
n : ℕ
h : 0 ≤ n
⊢ toStepOfLE k 0 (n + 1) (_ : 0 ≤ n + 1) = RingHom.comp (toStepSucc k n) (toStepOfLE k 0 n h)
[PROOFSTEP]
ext1 x
[GOAL]
case a
k : Type u
inst✝ : Field k
n : ℕ
h : 0 ≤ n
x : Step k 0
⊢ ↑(toStepOfLE k 0 (n + 1) (_ : 0 ≤ n + 1)) x = ↑(RingHom.comp (toStepSucc k n) (toStepOfLE k 0 n h)) x
[PROOFSTEP]
rw [RingHom.comp_apply]
[GOAL]
case a
k : Type u
inst✝ : Field k
n : ℕ
h : 0 ≤ n
x : Step k 0
⊢ ↑(toStepOfLE k 0 (n + 1) (_ : 0 ≤ n + 1)) x = ↑(toStepSucc k n) (↑(toStepOfLE k 0 n h) x)
[PROOFSTEP]
simp only [toStepOfLE, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
[GOAL]
case a
k : Type u
inst✝ : Field k
n : ℕ
h : 0 ≤ n
x : Step k 0
⊢ AlgebraicClosure.toStepOfLE' k 0 (n + 1) (_ : 0 ≤ n + 1) x =
    ↑(toStepSucc k n) (AlgebraicClosure.toStepOfLE' k 0 n h x)
[PROOFSTEP]
change _ = (_ ∘ _) x
[GOAL]
case a
k : Type u
inst✝ : Field k
n : ℕ
h : 0 ≤ n
x : Step k 0
⊢ AlgebraicClosure.toStepOfLE' k 0 (n + 1) (_ : 0 ≤ n + 1) x =
    (↑(toStepSucc k n) ∘ AlgebraicClosure.toStepOfLE' k 0 n h) x
[PROOFSTEP]
rw [toStepOfLE'.succ k 0 n h]
[GOAL]
k : Type u
inst✝ : Field k
n : ℕ
⊢ ∀ (z : Step k n), IsIntegral k z
[PROOFSTEP]
induction' n with a h
[GOAL]
case zero
k : Type u
inst✝ : Field k
⊢ ∀ (z : Step k Nat.zero), IsIntegral k z
[PROOFSTEP]
intro z
[GOAL]
case zero
k : Type u
inst✝ : Field k
z : Step k Nat.zero
⊢ IsIntegral k z
[PROOFSTEP]
exact isIntegral_algebraMap
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
⊢ ∀ (z : Step k (Nat.succ a)), IsIntegral k z
[PROOFSTEP]
intro z
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
z : Step k (Nat.succ a)
⊢ IsIntegral k z
[PROOFSTEP]
change RingHom.IsIntegralElem _ _
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
z : Step k (Nat.succ a)
⊢ RingHom.IsIntegralElem (algebraMap k (Step k (Nat.succ a))) z
[PROOFSTEP]
revert z
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
⊢ ∀ (z : Step k (Nat.succ a)), RingHom.IsIntegralElem (algebraMap k (Step k (Nat.succ a))) z
[PROOFSTEP]
change RingHom.IsIntegral _
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
⊢ RingHom.IsIntegral (algebraMap k (Step k (Nat.succ a)))
[PROOFSTEP]
unfold algebraMap
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
⊢ RingHom.IsIntegral Algebra.toRingHom
[PROOFSTEP]
unfold Algebra.toRingHom
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
⊢ RingHom.IsIntegral (algebra k (Nat.succ a)).2
[PROOFSTEP]
unfold algebra
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
⊢ RingHom.IsIntegral (RingHom.toAlgebra (toStepOfLE k 0 (Nat.succ a) (_ : 0 ≤ Nat.succ a))).2
[PROOFSTEP]
unfold RingHom.toAlgebra
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
⊢ RingHom.IsIntegral
    (RingHom.toAlgebra' (toStepOfLE k 0 (Nat.succ a) (_ : 0 ≤ Nat.succ a))
        (_ :
          ∀ (x : Step k 0) (b : (fun x => Step k (Nat.succ a)) x),
            ↑(toStepOfLE k 0 (Nat.succ a) (_ : 0 ≤ Nat.succ a)) x * b =
              b * ↑(toStepOfLE k 0 (Nat.succ a) (_ : 0 ≤ Nat.succ a)) x)).2
[PROOFSTEP]
unfold RingHom.toAlgebra'
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
⊢ RingHom.IsIntegral
    (Algebra.mk (toStepOfLE k 0 (Nat.succ a) (_ : 0 ≤ Nat.succ a))
        (_ :
          ∀ (x : Step k 0) (b : (fun x => Step k (Nat.succ a)) x),
            ↑(toStepOfLE k 0 (Nat.succ a) (_ : 0 ≤ Nat.succ a)) x * b =
              b * ↑(toStepOfLE k 0 (Nat.succ a) (_ : 0 ≤ Nat.succ a)) x)
        (_ : ∀ (x : Step k 0) (x_1 : Step k (Nat.succ a)), x • x_1 = x • x_1)).2
[PROOFSTEP]
simp only
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
⊢ RingHom.IsIntegral (toStepOfLE k 0 (Nat.succ a) (_ : 0 ≤ Nat.succ a))
[PROOFSTEP]
rw [toStepOfLE.succ k a a.zero_le]
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
⊢ RingHom.IsIntegral (RingHom.comp (toStepSucc k a) (toStepOfLE k 0 a (_ : 0 ≤ a)))
[PROOFSTEP]
apply
  @RingHom.isIntegral_trans (Step k 0) (Step k a) (Step k (a + 1)) _ _ _ (toStepOfLE k 0 a (a.zero_le : 0 ≤ a))
    (toStepSucc k a) _
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
⊢ RingHom.IsIntegral (toStepSucc k a)
[PROOFSTEP]
intro z
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
z : Step k (a + 1)
⊢ RingHom.IsIntegralElem (toStepSucc k a) z
[PROOFSTEP]
have := AdjoinMonic.isIntegral (Step k a) (z : Step k (a + 1))
[GOAL]
case succ
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
z : Step k (a + 1)
this : IsIntegral (Step k a) z
⊢ RingHom.IsIntegralElem (toStepSucc k a) z
[PROOFSTEP]
convert this
[GOAL]
k : Type u
inst✝ : Field k
a : ℕ
h : ∀ (z : Step k a), IsIntegral k z
⊢ RingHom.IsIntegral (toStepOfLE k 0 a (_ : 0 ≤ a))
[PROOFSTEP]
convert h
[GOAL]
k : Type u
inst✝ : Field k
n : ℕ
⊢ RingHom.comp (ofStep k (n + 1)) (toStepSucc k n) = ofStep k n
[PROOFSTEP]
ext x
[GOAL]
case a
k : Type u
inst✝ : Field k
n : ℕ
x : Step k n
⊢ ↑(RingHom.comp (ofStep k (n + 1)) (toStepSucc k n)) x = ↑(ofStep k n) x
[PROOFSTEP]
have hx : toStepOfLE' k n (n + 1) n.le_succ x = toStepSucc k n x := Nat.leRecOn_succ' x
[GOAL]
case a
k : Type u
inst✝ : Field k
n : ℕ
x : Step k n
hx : AlgebraicClosure.toStepOfLE' k n (n + 1) (_ : n ≤ Nat.succ n) x = ↑(toStepSucc k n) x
⊢ ↑(RingHom.comp (ofStep k (n + 1)) (toStepSucc k n)) x = ↑(ofStep k n) x
[PROOFSTEP]
unfold ofStep
[GOAL]
case a
k : Type u
inst✝ : Field k
n : ℕ
x : Step k n
hx : AlgebraicClosure.toStepOfLE' k n (n + 1) (_ : n ≤ Nat.succ n) x = ↑(toStepSucc k n) x
⊢ ↑(RingHom.comp (Ring.DirectLimit.of (Step k) (fun i j h => ↑(toStepOfLE k i j h)) (n + 1)) (toStepSucc k n)) x =
    ↑(Ring.DirectLimit.of (Step k) (fun i j h => ↑(toStepOfLE k i j h)) n) x
[PROOFSTEP]
rw [RingHom.comp_apply]
[GOAL]
case a
k : Type u
inst✝ : Field k
n : ℕ
x : Step k n
hx : AlgebraicClosure.toStepOfLE' k n (n + 1) (_ : n ≤ Nat.succ n) x = ↑(toStepSucc k n) x
⊢ ↑(Ring.DirectLimit.of (Step k) (fun i j h => ↑(toStepOfLE k i j h)) (n + 1)) (↑(toStepSucc k n) x) =
    ↑(Ring.DirectLimit.of (Step k) (fun i j h => ↑(toStepOfLE k i j h)) n) x
[PROOFSTEP]
dsimp [toStepOfLE]
[GOAL]
case a
k : Type u
inst✝ : Field k
n : ℕ
x : Step k n
hx : AlgebraicClosure.toStepOfLE' k n (n + 1) (_ : n ≤ Nat.succ n) x = ↑(toStepSucc k n) x
⊢ ↑(Ring.DirectLimit.of (Step k) (fun i j h => AlgebraicClosure.toStepOfLE' k i j h) (n + 1)) (↑(toStepSucc k n) x) =
    ↑(Ring.DirectLimit.of (Step k) (fun i j h => AlgebraicClosure.toStepOfLE' k i j h) n) x
[PROOFSTEP]
rw [← hx]
[GOAL]
case a
k : Type u
inst✝ : Field k
n : ℕ
x : Step k n
hx : AlgebraicClosure.toStepOfLE' k n (n + 1) (_ : n ≤ Nat.succ n) x = ↑(toStepSucc k n) x
⊢ ↑(Ring.DirectLimit.of (Step k) (fun i j h => AlgebraicClosure.toStepOfLE' k i j h) (n + 1))
      (AlgebraicClosure.toStepOfLE' k n (n + 1) (_ : n ≤ Nat.succ n) x) =
    ↑(Ring.DirectLimit.of (Step k) (fun i j h => AlgebraicClosure.toStepOfLE' k i j h) n) x
[PROOFSTEP]
change Ring.DirectLimit.of (Step k) (toStepOfLE' k) (n + 1) (_) = Ring.DirectLimit.of (Step k) (toStepOfLE' k) n x
[GOAL]
case a
k : Type u
inst✝ : Field k
n : ℕ
x : Step k n
hx : AlgebraicClosure.toStepOfLE' k n (n + 1) (_ : n ≤ Nat.succ n) x = ↑(toStepSucc k n) x
⊢ ↑(Ring.DirectLimit.of (Step k) (AlgebraicClosure.toStepOfLE' k) (n + 1))
      (AlgebraicClosure.toStepOfLE' k n (n + 1) (_ : n ≤ Nat.succ n) x) =
    ↑(Ring.DirectLimit.of (Step k) (AlgebraicClosure.toStepOfLE' k) n) x
[PROOFSTEP]
convert Ring.DirectLimit.of_f n.le_succ x
[GOAL]
k : Type u
inst✝ : Field k
f : (AlgebraicClosure k)[X]
hfm : Monic f
hfi : Irreducible f
⊢ ∃ x, eval x f = 0
[PROOFSTEP]
have : ∃ n p, Polynomial.map (ofStep k n) p = f := by convert Ring.DirectLimit.Polynomial.exists_of f
[GOAL]
k : Type u
inst✝ : Field k
f : (AlgebraicClosure k)[X]
hfm : Monic f
hfi : Irreducible f
⊢ ∃ n p, map (ofStep k n) p = f
[PROOFSTEP]
convert Ring.DirectLimit.Polynomial.exists_of f
[GOAL]
k : Type u
inst✝ : Field k
f : (AlgebraicClosure k)[X]
hfm : Monic f
hfi : Irreducible f
this : ∃ n p, map (ofStep k n) p = f
⊢ ∃ x, eval x f = 0
[PROOFSTEP]
obtain ⟨n, p, rfl⟩ := this
[GOAL]
case intro.intro
k : Type u
inst✝ : Field k
n : ℕ
p : (Step k n)[X]
hfm : Monic (map (ofStep k n) p)
hfi : Irreducible (map (ofStep k n) p)
⊢ ∃ x, eval x (map (ofStep k n) p) = 0
[PROOFSTEP]
rw [monic_map_iff] at hfm
[GOAL]
case intro.intro
k : Type u
inst✝ : Field k
n : ℕ
p : (Step k n)[X]
hfm : Monic p
hfi : Irreducible (map (ofStep k n) p)
⊢ ∃ x, eval x (map (ofStep k n) p) = 0
[PROOFSTEP]
have := hfm.irreducible_of_irreducible_map (ofStep k n) p hfi
[GOAL]
case intro.intro
k : Type u
inst✝ : Field k
n : ℕ
p : (Step k n)[X]
hfm : Monic p
hfi : Irreducible (map (ofStep k n) p)
this : Irreducible p
⊢ ∃ x, eval x (map (ofStep k n) p) = 0
[PROOFSTEP]
obtain ⟨x, hx⟩ := toStepSucc.exists_root k hfm this
[GOAL]
case intro.intro.intro
k : Type u
inst✝ : Field k
n : ℕ
p : (Step k n)[X]
hfm : Monic p
hfi : Irreducible (map (ofStep k n) p)
this : Irreducible p
x : Step k (n + 1)
hx : eval₂ (toStepSucc k n) x p = 0
⊢ ∃ x, eval x (map (ofStep k n) p) = 0
[PROOFSTEP]
refine' ⟨ofStep k (n + 1) x, _⟩
[GOAL]
case intro.intro.intro
k : Type u
inst✝ : Field k
n : ℕ
p : (Step k n)[X]
hfm : Monic p
hfi : Irreducible (map (ofStep k n) p)
this : Irreducible p
x : Step k (n + 1)
hx : eval₂ (toStepSucc k n) x p = 0
⊢ eval (↑(ofStep k (n + 1)) x) (map (ofStep k n) p) = 0
[PROOFSTEP]
rw [← ofStep_succ k n, eval_map, ← hom_eval₂, hx, RingHom.map_zero]
[GOAL]
k : Type u
inst✝⁶ : Field k
R : Type u_1
S : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : Algebra S k
inst✝¹ : Algebra R k
inst✝ : IsScalarTower R S k
⊢ IsScalarTower R S (AlgebraicClosure k)
[PROOFSTEP]
apply IsScalarTower.of_algebraMap_eq _
[GOAL]
k : Type u
inst✝⁶ : Field k
R : Type u_1
S : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : Algebra S k
inst✝¹ : Algebra R k
inst✝ : IsScalarTower R S k
⊢ ∀ (x : R), ↑(algebraMap R (AlgebraicClosure k)) x = ↑(algebraMap S (AlgebraicClosure k)) (↑(algebraMap R S) x)
[PROOFSTEP]
intro x
[GOAL]
k : Type u
inst✝⁶ : Field k
R : Type u_1
S : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : Algebra S k
inst✝¹ : Algebra R k
inst✝ : IsScalarTower R S k
x : R
⊢ ↑(algebraMap R (AlgebraicClosure k)) x = ↑(algebraMap S (AlgebraicClosure k)) (↑(algebraMap R S) x)
[PROOFSTEP]
simp only [algebraMap_def]
[GOAL]
k : Type u
inst✝⁶ : Field k
R : Type u_1
S : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : Algebra S k
inst✝¹ : Algebra R k
inst✝ : IsScalarTower R S k
x : R
⊢ ↑(RingHom.comp (ofStep k 0) (algebraMap R (Step k 0))) x =
    ↑(RingHom.comp (ofStep k 0) (algebraMap S (Step k 0))) (↑(algebraMap R S) x)
[PROOFSTEP]
rw [RingHom.comp_apply, RingHom.comp_apply]
[GOAL]
k : Type u
inst✝⁶ : Field k
R : Type u_1
S : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : Algebra S k
inst✝¹ : Algebra R k
inst✝ : IsScalarTower R S k
x : R
⊢ ↑(ofStep k 0) (↑(algebraMap R (Step k 0)) x) = ↑(ofStep k 0) (↑(algebraMap S (Step k 0)) (↑(algebraMap R S) x))
[PROOFSTEP]
exact
  RingHom.congr_arg _
    (IsScalarTower.algebraMap_apply R S k x : _)
      -- Porting Note: Original proof (without `by`) didn't work anymore, I think it couldn't figure
        -- out `algebraMap_def`. Orignally:
        -- IsScalarTower.of_algebraMap_eq fun x =>
        --   RingHom.congr_arg _ (IsScalarTower.algebraMap_apply R S k x : _)
[GOAL]
k : Type u
inst✝ : Field k
n : ℕ
src✝ : Step k n →+* AlgebraicClosure k := ofStep k n
⊢ ∀ (r : k),
    OneHom.toFun
        (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ :
                  ∀ (x y : Step k n),
                    OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
        (↑(algebraMap k (Step k n)) r) =
      ↑(algebraMap k (AlgebraicClosure k)) r
[PROOFSTEP]
intro x
[GOAL]
k : Type u
inst✝ : Field k
n : ℕ
src✝ : Step k n →+* AlgebraicClosure k := ofStep k n
x : k
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : Step k n),
                  OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap k (Step k n)) x) =
    ↑(algebraMap k (AlgebraicClosure k)) x
[PROOFSTEP]
simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, MonoidHom.coe_coe]
[GOAL]
k : Type u
inst✝ : Field k
n : ℕ
src✝ : Step k n →+* AlgebraicClosure k := ofStep k n
x : k
⊢ ↑(ofStep k n) (↑(algebraMap k (Step k n)) x) = ↑(algebraMap k (AlgebraicClosure k)) x
[PROOFSTEP]
convert @Ring.DirectLimit.of_f ℕ _ (Step k) _ (fun m n h => (toStepOfLE k m n h : _ → _)) 0 n n.zero_le x