awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FGBaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
refine_1 : Subalgebra.FG (Algebra.adjoin R (↑(Finset.image (fun (j : A × B) ↦ j.2) S) : Set B))
⊢ ∃ (C : Subalgebra R B), C.FG ∧ Membership.mem (γ := Subalgebra A (A ⊗[R] B)) (Subalgebra.baseChange A C) x
have refine_2 : Membership.mem (γ := Subalgebra A (A ⊗[R] B))
  (Subalgebra.baseChange A (Algebra.adjoin R (↑(Finset.image (fun (j : A × B) ↦ j.2) S) : Set B))) x
Tactic: refine ⟨Algebra.adjoin R (S.image fun j ↦ j.2), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FGBaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ ∃ (C : Subalgebra R B), C.FG ∧ Membership.mem (γ := Subalgebra A (A ⊗[R] B)) (Subalgebra.baseChange A C) x
have refine_1 : Subalgebra.FG (Algebra.adjoin R (↑(Finset.image (fun (j : A × B) ↦ j.2) S) : Set B))
Tactic: classical
  refine ⟨Algebra.adjoin R (S.image fun j ↦ j.2), ?_, ?_⟩
  · exact Subalgebra.fg_adjoin_finset _
  · exact hS ▸ Subalgebra.sum_mem _ fun s hs ↦ (Subalgebra.tmul_mem_baseChange
      (Algebra.subset_adjoin (Finset.mem_image_of_mem _ hs)) s.1)
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FGBaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
refine_1 : Subalgebra.FG (Algebra.adjoin R (↑(Finset.image (fun (j : A × B) ↦ j.2) S) : Set B))
⊢ ∃ (C : Subalgebra R B), C.FG ∧ Membership.mem (γ := Subalgebra A (A ⊗[R] B)) (Subalgebra.baseChange A C) x
have refine_2 : Membership.mem (γ := Subalgebra A (A ⊗[R] B))
  (Subalgebra.baseChange A (Algebra.adjoin R (↑(Finset.image (fun (j : A × B) ↦ j.2) S) : Set B))) x
Tactic: classical
  refine ⟨Algebra.adjoin R (S.image fun j ↦ j.2), ?_, ?_⟩
  · exact Subalgebra.fg_adjoin_finset _
  · exact hS ▸ Subalgebra.sum_mem _ fun s hs ↦ (Subalgebra.tmul_mem_baseChange
      (Algebra.subset_adjoin (Finset.mem_image_of_mem _ hs)) s.1)
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_1
inst : Field F
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra F R
x : R
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly F x)) (β := ↥F[x])
    (⇑(Minpoly.toAdjoin F x) : (a : AdjoinRoot (minpoly F x)) → ↥F[x])
have refine : ∀ (P₁ : AdjoinRoot (minpoly F x))
  (hP₁ :
    Eq.{u_2 + 1} (α := ↥F[x])
      (((Minpoly.toAdjoin F x : AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F x)) ↥F[x]) :
            (a : AdjoinRoot (minpoly F x)) → ↥F[x])
          P₁ :
        ↥F[x])
      (0 : ↥F[x])),
  P₁ = 0
Tactic: refine ⟨(injective_iff_map_eq_zero _).2 fun P₁ hP₁ ↦ ?_, Minpoly.toAdjoin.surjective F x⟩
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_1
inst : Field F
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra F R
x : R
P₁ : AdjoinRoot (minpoly F x)
hP₁ :
  Eq.{u_2 + 1} (α := ↥F[x])
    (((Minpoly.toAdjoin F x : AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F x)) ↥F[x]) :
          (a : AdjoinRoot (minpoly F x)) → ↥F[x])
        P₁ :
      ↥F[x])
    (0 : ↥F[x])
⊢ P₁ = 0
have obtain : ∀ (P : F[X])
  (hP₁ :
    Eq.{u_2 + 1} (α := ↥F[x])
      (((Minpoly.toAdjoin F x : AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F x)) ↥F[x]) :
            (a : AdjoinRoot (minpoly F x)) → ↥F[x])
          ((AdjoinRoot.mk (minpoly F x) : (a : F[X]) → AdjoinRoot (minpoly F x)) P) :
        ↥F[x])
      (0 : ↥F[x])),
  Eq (α := AdjoinRoot (minpoly F x))
    ((AdjoinRoot.mk (minpoly F x) : (a : F[X]) → AdjoinRoot (minpoly F x)) P : AdjoinRoot (minpoly F x))
    (0 : AdjoinRoot (minpoly F x))
Tactic: obtain ⟨P, rfl⟩ := mk_surjective P₁
Cleared hypotheses: P₁, hP₁
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_1
inst : Field F
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra F R
x : R
P : F[X]
hP₁ :
  Eq.{u_2 + 1} (α := ↥F[x])
    (((Minpoly.toAdjoin F x : AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F x)) ↥F[x]) :
          (a : AdjoinRoot (minpoly F x)) → ↥F[x])
        ((AdjoinRoot.mk (minpoly F x) : (a : F[X]) → AdjoinRoot (minpoly F x)) P) :
      ↥F[x])
    (0 : ↥F[x])
⊢ Eq (α := AdjoinRoot (minpoly F x))
    ((AdjoinRoot.mk (minpoly F x) : (a : F[X]) → AdjoinRoot (minpoly F x)) P : AdjoinRoot (minpoly F x))
    (0 : AdjoinRoot (minpoly F x))
have refine : Eq.{u_2 + 1} (α := R) ((aeval x : (a : F[X]) → R) P : R) (0 : R)
Tactic: refine AdjoinRoot.mk_eq_zero.mpr (minpoly.dvd F x ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s : Finset K
⊢ (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
have refine_1 : (∀ (x : K), Membership.mem (γ := Finset K) ∅ x → IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
  Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑∅ : Set K))) L)
Tactic: refine Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s : Finset K
refine_1 :
  (∀ (x : K), Membership.mem (γ := Finset K) ∅ x → IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑∅ : Set K))) L)
⊢ (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
have refine_2 : ∀ (a : K) (s : Finset K),
  a ∉ s →
    ∀
      (ih :
        (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
          Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L))
      (H : ∀ x ∈ insert a s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))),
      Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
Tactic: refine Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s : Finset K
h : ∀ (x : K), Membership.mem (γ := Finset K) ∅ x → IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑∅ : Set K))) L)
have refine_1 : Nonempty (AlgHom.{u_2, u_3, u_4} F (↥⊥) L)
Tactic: rw [coe_empty, Algebra.adjoin_empty]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (hypothesis)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H : ∀ x ∈ insert a s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
have H₁ : (IsIntegral F a ∧ Splits (map (algebraMap F L) (minpoly F a))) ∧
  ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
Tactic: rw [forall_mem_insert] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (hypothesis)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H :
  (IsIntegral F a ∧ Splits (map (algebraMap F L) (minpoly F a))) ∧
    ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
have H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
Tactic: rcases H with ⟨⟨H1, H2⟩, H3⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (hypothesis)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H :
  (IsIntegral F a ∧ Splits (map (algebraMap F L) (minpoly F a))) ∧
    ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
have H1 : IsIntegral F a
Tactic: rcases H with ⟨⟨H1, H2⟩, H3⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (hypothesis)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H :
  (IsIntegral F a ∧ Splits (map (algebraMap F L) (minpoly F a))) ∧
    ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
H1 : IsIntegral F a
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
have H2 : Splits (map (algebraMap F L) (minpoly F a))
Tactic: rcases H with ⟨⟨H1, H2⟩, H3⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
have refine_2 : ∀ (f : AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L),
  Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
Tactic: obtain ⟨f⟩ := ih H3
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (hypothesis)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
f : AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
have H3₁ : ∀ x ∈ s, IsIntegral F x
Tactic: choose H3 _ using H3
Cleared hypotheses: H3
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (hypothesis)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H3 : ∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
f : AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L
H3₁ : ∀ x ∈ s, IsIntegral F x
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
have a₁ : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Tactic: choose H3 _ using H3
Cleared hypotheses: H3
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
f : AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑(insert a s) : Set K))) L)
have refine_2 : Nonempty
  (AlgHom.{u_2, u_3, u_4} F
    (↥(Subalgebra.restrictScalars F (S := ↥(Algebra.adjoin F (↑s : Set K))) (↥(Algebra.adjoin F (↑s : Set K)))[a])) L)
Tactic: rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
f : AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
⊢ Nonempty
    (AlgHom.{u_2, u_3, u_4} F
      (↥(Subalgebra.restrictScalars F (S := ↥(Algebra.adjoin F (↑s : Set K))) (↥(Algebra.adjoin F (↑s : Set K)))[a])) L)
have refine_2 : let Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K);
∀
  (ih :
    (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
      Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L))
  (f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L),
  Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)
Tactic: set Ks := Algebra.adjoin F (s : Set K)
Cleared hypotheses: ih, f
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (hypothesis)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)
have this : FiniteDimensional.{u_2, u_3} F ↥Ks
Tactic: haveI : FiniteDimensional F Ks := ((Submodule.fg_iff_finiteDimensional _).1
      (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (hypothesis)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)
have H5 : IsIntegral (↥Ks) a
Tactic: have H5 : IsIntegral Ks a := H1.tower_top
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
⊢ Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))
have refine : Dvd.dvd (α := L[X]) (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a)) (map (algebraMap F L) (minpoly F a))
Tactic: refine Splits.of_dvd H2 (map_ne_zero (minpoly.ne_zero H1)) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
⊢ Dvd.dvd (α := L[X]) (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a)) (map (algebraMap F L) (minpoly F a))
have rw : Dvd.dvd (α := (↥Ks)[X]) (minpoly (↥Ks) a) (map (algebraMap F ↥Ks) (minpoly F a))
Tactic: rw [IsScalarTower.algebraMap_eq F Ks L, ← map_map, map_dvd_map']
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (hypothesis)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)
have H6 : Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))
Tactic: have H6 : ((minpoly Ks a).map (algebraMap Ks L)).Splits := by
      refine Splits.of_dvd H2 (map_ne_zero (minpoly.ne_zero H1)) ?_
      rw [IsScalarTower.algebraMap_eq F Ks L, ← map_map, map_dvd_map']
      exact minpoly.dvd_map_of_isScalarTower F Ks a
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
H6 : Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)
have refine_2 : ∀ (y : L) (hy : eval y (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a)) = 0),
  Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)
Tactic: obtain ⟨y, hy⟩ := H6.exists_eval_eq_zero (by simp [(minpoly.degree_pos H5).ne'])
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (hypothesis)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s_1 : Finset K
a : K
s : Finset K
h : a ∉ s
H1 : IsIntegral F a
H2 : Splits (map (algebraMap F L) (minpoly F a))
H3 : ∀ x ∈ s, IsIntegral F x
h_1 : ∀ x ∈ s, Splits (map (algebraMap F L) (minpoly F x))
Ks : Subalgebra F K := Algebra.adjoin F (↑s : Set K)
ih :
  (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) → Nonempty (AlgHom.{u_2, u_3, u_4} F (↥Ks) L)
f : AlgHom.{u_2, u_3, u_4} F (↥Ks) L
this_1 : FiniteDimensional.{u_2, u_3} F ↥Ks
this_2 : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra.{u_3, u_4} (↥Ks) L := RingHom.toAlgebra (↑f : ↥Ks →+* L)
H5 : IsIntegral (↥Ks) a
H6 : Splits (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a))
y : L
hy : eval y (map (R := ↥Ks) (algebraMap (↥Ks) L) (minpoly (↥Ks) a)) = 0
⊢ Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Subalgebra.restrictScalars F (S := ↥Ks) (↥Ks)[a])) L)
have hy₁ : eval₂ (R := ↥Ks) (algebraMap (↥Ks) L) y (minpoly (↥Ks) a) = 0
Tactic: rw [eval_map] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Field (goal)
Goal:
F : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra F K
inst_4 : Algebra F L
s : Finset K
⊢ (∀ x ∈ s, IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
    Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑s : Set K))) L)
have refine_1 : (∀ (x : K), Membership.mem (γ := Finset K) ∅ x → IsIntegral F x ∧ Splits (map (algebraMap F L) (minpoly F x))) →
  Nonempty (AlgHom.{u_2, u_3, u_4} F (↥(Algebra.adjoin F (↑∅ : Set K))) L)
Tactic: classical
    refine Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_
    · rw [coe_empty, Algebra.adjoin_empty]
      exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
    rw [forall_mem_insert] at H
    rcases H with ⟨⟨H1, H2⟩, H3⟩
    obtain ⟨f⟩ := ih H3
    choose H3 _ using H3
    rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
    set Ks := Algebra.adjoin F (s : Set K)
    haveI : FiniteDimensional F Ks := ((Submodule.fg_iff_finiteDimensional _).1
      (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
    letI := fieldOfFiniteDimensional F Ks
    letI := (f : Ks →+* L).toAlgebra
    have H5 : IsIntegral Ks a := H1.tower_top
    have H6 : ((minpoly Ks a).map (algebraMap Ks L)).Splits := by
      refine Splits.of_dvd H2 (map_ne_zero (minpoly.ne_zero H1)) ?_
      rw [IsScalarTower.algebraMap_eq F Ks L, ← map_map, map_dvd_map']
      exact minpoly.dvd_map_of_isScalarTower F Ks a
    obtain ⟨y, hy⟩ := H6.exists_eval_eq_zero (by simp [(minpoly.degree_pos H5).ne'])
    rw [eval_map] at hy
    exact ⟨Subalgebra.ofRestrictScalars F _ <| Algebra.adjoin.liftSingleton Ks a y hy⟩