awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K_1 : Type u
inst_1 : Field K_1
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K_1 L
inst_4 : Field M
inst_5 : Algebra K_1 M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K_1 L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
K : Type u_1
inst_17 : Field K
inst_18 : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := HPow.hPow (α := K[X]) X (n + 1) - 1
hfsep : f.Separable
hroot : n.succ = Fintype.card.{u_1} (↑(f.rootSet K) : Type u_1)
⊢ Fintype.card.{u_1} (↑(f.rootSet K) : Type u_1) ≤ Fintype.card K

Tactic:
exact Fintype.card_le_of_injective _ Subtype.coe_injective

Premises used: Fintype.card_le_of_injective, Subtype.coe_injective
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
K : Type u_1
J : Type u_2
L : Type v
inst : Field K
inst_1 : Field J
inst_2 : Field L
inst_3 : Algebra K J
inst_4 : Algebra J L
inst_5 : IsAlgClosure J L
inst_6 : Algebra K L
inst_7 : IsScalarTower K J L
inst_8 : Algebra.IsAlgebraic K J
⊢ IsAlgClosure K L

Tactic:
⟨IsAlgClosure.isAlgClosed J, .trans K J L⟩

Premises used: IsAlgClosure.mk, Algebra.IsAlgebraic.trans, IsAlgClosure.isAlgClosed
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : Algebra R S
inst_16 : Algebra R L
inst_17 : IsScalarTower R S L
inst_18 : Algebra K J
inst_19 : Algebra J L
inst_20 : IsAlgClosure J L
inst_21 : Algebra K L
inst_22 : IsScalarTower K J L
inst_23 : IsDomain R
inst_24 : IsDomain S
inst_25 : IsTorsionFree R S
inst_26 : Algebra.IsAlgebraic R L
⊢ IsTorsionFree R L

Tactic:
have : IsTorsionFree R L := .trans_faithfulSMul R S L
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : Algebra R S
inst_16 : Algebra R L
inst_17 : IsScalarTower R S L
inst_18 : Algebra K J
inst_19 : Algebra J L
inst_20 : IsAlgClosure J L
inst_21 : Algebra K L
inst_22 : IsScalarTower K J L
inst_23 : IsDomain R
inst_24 : IsDomain S
inst_25 : IsTorsionFree R S
inst_26 : Algebra.IsAlgebraic R L
this : IsTorsionFree R L
⊢ IsAlgClosure R L

Tactic:
have : IsAlgClosure R L :=
    { isAlgClosed := IsAlgClosure.isAlgClosed S
      isAlgebraic := ‹_› }
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : Algebra R S
inst_16 : Algebra R L
inst_17 : IsScalarTower R S L
inst_18 : Algebra K J
inst_19 : Algebra J L
inst_20 : IsAlgClosure J L
inst_21 : Algebra K L
inst_22 : IsScalarTower K J L
inst_23 : IsDomain R
inst_24 : IsDomain S
inst_25 : IsTorsionFree R S
inst_26 : Algebra.IsAlgebraic R L
this_1 : IsTorsionFree R L
this : IsAlgClosure R L
⊢ L ≃ₐ[R] M

Tactic:
exact IsAlgClosure.equiv _ _ _

Premises used: IsAlgClosure.equiv
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : IsDomain R
inst_16 : IsDomain S
hSR : S ≃+* R
this_1 : Algebra R S := hSR.symm.toRingHom.toAlgebra
this_2 : Algebra S R := hSR.toRingHom.toAlgebra
this : Algebra R L :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
⊢ IsScalarTower R S L

Tactic:
haveI : IsScalarTower R S L := .of_algebraMap_eq fun _ => rfl
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : IsDomain R
inst_16 : IsDomain S
hSR : S ≃+* R
this_1 : Algebra R S := hSR.symm.toRingHom.toAlgebra
this_2 : Algebra S R := hSR.toRingHom.toAlgebra
this_3 : Algebra R L :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
this : IsScalarTower R S L
⊢ ∀ (x : S),
    Eq.{v + 1} (α := L) ((algebraMap S L : (a : S) → L) x : L)
      ((algebraMap R L : (a : R) → L) ((algebraMap S R : (a : S) → R) x : R) : L)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : IsDomain R
inst_16 : IsDomain S
hSR : S ≃+* R
this_1 : Algebra R S := hSR.symm.toRingHom.toAlgebra
this_2 : Algebra S R := hSR.toRingHom.toAlgebra
this_3 : Algebra R L :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
this : IsScalarTower R S L
⊢ IsScalarTower S R L

Tactic:
haveI : IsScalarTower S R L := .of_algebraMap_eq (by simp [RingHom.algebraMap_toAlgebra])
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : IsDomain R
inst_16 : IsDomain S
hSR : S ≃+* R
this_1 : Algebra R S := hSR.symm.toRingHom.toAlgebra
this_2 : Algebra S R := hSR.toRingHom.toAlgebra
this_3 : Algebra R L :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
this_4 : IsScalarTower R S L
this : IsScalarTower S R L
⊢ FaithfulSMul R S

Tactic:
have : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr hSR.symm.injective
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : IsDomain R
inst_16 : IsDomain S
hSR : S ≃+* R
this_1 : Algebra R S := hSR.symm.toRingHom.toAlgebra
this_2 : Algebra S R := hSR.toRingHom.toAlgebra
this_3 : Algebra R L :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
this_4 : IsScalarTower R S L
this_5 : IsScalarTower S R L
this : FaithfulSMul R S
⊢ Algebra.IsAlgebraic R L

Tactic:
have : Algebra.IsAlgebraic R L := (IsAlgClosure.isAlgebraic.extendScalars
    (show Function.Injective (algebraMap S R) from hSR.injective))
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : IsDomain R
inst_16 : IsDomain S
hSR : S ≃+* R
this_1 : Algebra R S := hSR.symm.toRingHom.toAlgebra
this_2 : Algebra S R := hSR.toRingHom.toAlgebra
this_3 : Algebra R L :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
this_4 : IsScalarTower R S L
this_5 : IsScalarTower S R L
this_6 : FaithfulSMul R S
this : Algebra.IsAlgebraic R L
refine :
  Eq (α := S →+* M)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (equivOfAlgebraic' R S L M))) (algebraMap S L))
    (RingHom.comp (algebraMap R M) hSR.toRingHom)
⊢ { e : L ≃+* M // e.toRingHom.comp (algebraMap S L) = RingHom.comp (algebraMap R M) hSR.toRingHom }

Tactic:
refine ⟨equivOfAlgebraic' R S L M, ?_⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : IsDomain R
inst_16 : IsDomain S
hSR : S ≃+* R
this_1 : Algebra R S := hSR.symm.toRingHom.toAlgebra
this_2 : Algebra S R := hSR.toRingHom.toAlgebra
this_3 : Algebra R L :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
this_4 : IsScalarTower R S L
this_5 : IsScalarTower S R L
this_6 : FaithfulSMul R S
this : Algebra.IsAlgebraic R L
a :
  ∀ (x : S),
    Eq.{w + 1} (α := M)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (equivOfAlgebraic' R S L M))) (algebraMap S L) :
            (a : S) → M)
          x :
        M)
      ((RingHom.comp (algebraMap R M) hSR.toRingHom : (a : S) → M) x : M)
⊢ Eq (α := S →+* M)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (equivOfAlgebraic' R S L M))) (algebraMap S L))
    (RingHom.comp (algebraMap R M) hSR.toRingHom)

Tactic:
ext x
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : IsDomain R
inst_16 : IsDomain S
hSR : S ≃+* R
this_1 : Algebra R S := hSR.symm.toRingHom.toAlgebra
this_2 : Algebra S R := hSR.toRingHom.toAlgebra
this_3 : Algebra R L :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
this_4 : IsScalarTower R S L
this_5 : IsScalarTower S R L
this_6 : FaithfulSMul R S
this : Algebra.IsAlgebraic R L
x : S
a :
  Eq.{w + 1} (α := M) ((equivOfAlgebraic' R S L M : (a : L) → M) ((algebraMap S L : (a : S) → L) x : L) : M)
    ((algebraMap R M : (a : R) → M) ((hSR : (a : S) → R) x : R) : M)
⊢ Eq.{w + 1} (α := M)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (equivOfAlgebraic' R S L M))) (algebraMap S L) :
          (a : S) → M)
        x :
      M)
    ((RingHom.comp (algebraMap R M) hSR.toRingHom : (a : S) → M) x : M)

Tactic:
simp only [RingEquiv.toRingHom_eq_coe, Function.comp_apply, RingHom.coe_comp,
    AlgEquiv.coe_ringEquiv, RingEquiv.coe_toRingHom]

Premises used: AlgEquiv.coe_ringEquiv, RingHom.coe_comp, RingEquiv.toRingHom_eq_coe, Function.comp_apply, RingEquiv.coe_toRingHom
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : IsDomain R
inst_16 : IsDomain S
hSR : S ≃+* R
this_1 : Algebra R S := hSR.symm.toRingHom.toAlgebra
this_2 : Algebra S R := hSR.toRingHom.toAlgebra
this_3 : Algebra R L :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
this_4 : IsScalarTower R S L
this_5 : IsScalarTower S R L
this_6 : FaithfulSMul R S
this : Algebra.IsAlgebraic R L
x : S
rw :
  ((equivOfAlgebraic' R S L M : (a : L) → M)
      ((algebraMap S L : (a : S) → L) ((hSR.symm : (a : R) → S) ((hSR : (a : S) → R) x : R) : S) : L) :
    M)
| ((equivOfAlgebraic' R S L M : (a : L) → M) ((algebraMap S L : (a : S) → L) x : L) : M)

Tactic:
rw [← hSR.symm_apply_apply x]

Premises used: RingEquiv.symm_apply_apply
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : IsDomain R
inst_16 : IsDomain S
hSR : S ≃+* R
this_1 : Algebra R S := hSR.symm.toRingHom.toAlgebra
this_2 : Algebra S R := hSR.toRingHom.toAlgebra
this_3 : Algebra R L :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
this_4 : IsScalarTower R S L
this_5 : IsScalarTower S R L
this_6 : FaithfulSMul R S
this : Algebra.IsAlgebraic R L
x : S
a :
  Eq.{w + 1} (α := M)
    ((equivOfAlgebraic' R S L M : (a : L) → M)
        ((algebraMap S L : (a : S) → L) ((hSR.symm : (a : R) → S) ((hSR : (a : S) → R) x : R) : S) : L) :
      M)
    ((algebraMap R M : (a : R) → M) ((hSR : (a : S) → R) x : R) : M)
⊢ Eq.{w + 1} (α := M) ((equivOfAlgebraic' R S L M : (a : L) → M) ((algebraMap S L : (a : S) → L) x : L) : M)
    ((algebraMap R M : (a : R) → M) ((hSR : (a : S) → R) x : R) : M)

Tactic:
conv_lhs => rw [← hSR.symm_apply_apply x]

Premises used: RingEquiv.symm_apply_apply
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : IsDomain R
inst_16 : IsDomain S
hSR : S ≃+* R
this_1 : Algebra R S := hSR.symm.toRingHom.toAlgebra
this_2 : Algebra S R := hSR.toRingHom.toAlgebra
this_3 : Algebra R L :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
this_4 : IsScalarTower R S L
this_5 : IsScalarTower S R L
this_6 : FaithfulSMul R S
this : Algebra.IsAlgebraic R L
x : S
a :
  Eq.{w + 1} (α := M)
    ((equivOfAlgebraic' R S L M : (a : L) → M) ((algebraMap R L : (a : R) → L) ((hSR : (a : S) → R) x : R) : L) : M)
    ((algebraMap R M : (a : R) → M) ((hSR : (a : S) → R) x : R) : M)
⊢ Eq.{w + 1} (α := M)
    ((equivOfAlgebraic' R S L M : (a : L) → M)
        ((algebraMap S L : (a : S) → L) ((hSR.symm : (a : R) → S) ((hSR : (a : S) → R) x : R) : S) : L) :
      M)
    ((algebraMap R M : (a : R) → M) ((hSR : (a : S) → R) x : R) : M)

Tactic:
change equivOfAlgebraic' R S L M (algebraMap R L (hSR x)) = _

Premises used: Algebra.algebraMap, IsAlgClosure.equivOfAlgebraic', DFunLike.coe
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst_1 : Field K
inst_2 : Field J
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Field L
inst_6 : Field M
inst_7 : Algebra R M
inst_8 : IsTorsionFree R M
inst_9 : IsAlgClosure R M
inst_10 : Algebra K M
inst_11 : IsAlgClosure K M
inst_12 : Algebra S L
inst_13 : IsTorsionFree S L
inst_14 : IsAlgClosure S L
inst_15 : IsDomain R
inst_16 : IsDomain S
hSR : S ≃+* R
this_1 : Algebra R S := hSR.symm.toRingHom.toAlgebra
this_2 : Algebra S R := hSR.toRingHom.toAlgebra
this_3 : Algebra R L :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S))
this_4 : IsScalarTower R S L
this_5 : IsScalarTower S R L
this_6 : FaithfulSMul R S
this : Algebra.IsAlgebraic R L
x : S
a a₁ :
  Eq.{w + 1} (α := M) ((algebraMap R M : (a : R) → M) ((hSR : (a : S) → R) x : R) : M)
    ((algebraMap R M : (a : R) → M) ((hSR : (a : S) → R) x : R) : M)
⊢ Eq.{w + 1} (α := M)
    ((equivOfAlgebraic' R S L M : (a : L) → M) ((algebraMap R L : (a : R) → L) ((hSR : (a : S) → R) x : R) : L) : M)
    ((algebraMap R M : (a : R) → M) ((hSR : (a : S) → R) x : R) : M)

Tactic:
rw [AlgEquiv.commutes]

Premises used: AlgEquiv.commutes
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
R : Type u
S : Type u_3
L : Type v
M : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field L
inst_3 : Field M
inst_4 : Algebra R M
inst_5 : IsTorsionFree R M
inst_6 : IsAlgClosure R M
inst_7 : Algebra S L
inst_8 : IsTorsionFree S L
inst_9 : IsAlgClosure S L
inst_10 : IsDomain R
inst_11 : IsDomain S
hSR : S ≃+* R
⊢ Eq (α := S →+* M)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(equivOfEquiv L M hSR) : L →+* M) (algebraMap S L))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R M) (↑hSR : S →+* R))

Tactic:
(equivOfEquivAux L M hSR).2

Premises used: MonoidHomClass.toMonoidHom, IsAlgClosure.equivOfEquivAux, MulEquiv.toMonoidHom, RingHomClass.toRingHom, RingEquiv.toRingHom, Subtype.property
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
R : Type u
S : Type u_3
L : Type v
M : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field L
inst_3 : Field M
inst_4 : Algebra R M
inst_5 : IsTorsionFree R M
inst_6 : IsAlgClosure R M
inst_7 : Algebra S L
inst_8 : IsTorsionFree S L
inst_9 : IsAlgClosure S L
inst_10 : IsDomain R
inst_11 : IsDomain S
hSR : S ≃+* R
s : S
⊢ Eq.{w + 1} (α := M) ((equivOfEquiv L M hSR : (a : L) → M) ((algebraMap S L : (a : S) → L) s : L) : M)
    ((algebraMap R M : (a : R) → M) ((hSR : (a : S) → R) s : R) : M)

Tactic:
RingHom.ext_iff.1 (equivOfEquiv_comp_algebraMap L M hSR) s

Premises used: RingHom.ext_iff, IsAlgClosure.equivOfEquiv_comp_algebraMap, Iff.mp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
R : Type u
S : Type u_3
L : Type v
M : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field L
inst_3 : Field M
inst_4 : Algebra R M
inst_5 : IsTorsionFree R M
inst_6 : IsAlgClosure R M
inst_7 : Algebra S L
inst_8 : IsTorsionFree S L
inst_9 : IsAlgClosure S L
inst_10 : IsDomain R
inst_11 : IsDomain S
hSR : S ≃+* R
r : R
⊢ Eq.{w + 1} (α := M)
    ((equivOfEquiv L M hSR : (a : L) → M)
        ((RingEquiv.symm (equivOfEquiv L M hSR) : (a : M) → L) ((algebraMap R M : (a : R) → M) r : M) : L) :
      M)
    ((equivOfEquiv L M hSR : (a : L) → M) ((algebraMap S L : (a : S) → L) ((hSR.symm : (a : R) → S) r : S) : L) : M)

Tactic:
simp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
R : Type u
S : Type u_3
L : Type v
M : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field L
inst_3 : Field M
inst_4 : Algebra R M
inst_5 : IsTorsionFree R M
inst_6 : IsAlgClosure R M
inst_7 : Algebra S L
inst_8 : IsTorsionFree S L
inst_9 : IsAlgClosure S L
inst_10 : IsDomain R
inst_11 : IsDomain S
hSR : S ≃+* R
⊢ Eq (α := R →+* L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(RingEquiv.symm (equivOfEquiv L M hSR)) : M →+* L)
      (algebraMap R M))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (↑hSR.symm : R →+* S))

Tactic:
RingHom.ext_iff.2 (equivOfEquiv_symm_algebraMap L M hSR)

Premises used: Iff.mpr, RingHom.ext_iff, IsAlgClosure.equivOfEquiv_symm_algebraMap
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
F : Type u_1
K : Type u_2
A : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field A
inst_3 : Algebra F K
inst_4 : Algebra F A
inst_5 : Algebra.IsAlgebraic F K
inst_6 : IsAlgClosed A
x : K
⊢ (Set.range fun (ψ : K →ₐ[F] A) ↦ (ψ : (a : K) → A) x) = rootSet (minpoly F x) A

Tactic:
range_eval_eq_rootSet_minpoly_of_splits A (fun _ ↦ IsAlgClosed.splits _) x

Premises used: Algebra.algebraMap, minpoly, IsAlgClosed.splits, Polynomial.map, Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst_1 : Field F
inst_2 : Field K
inst_3 : Field A
inst_4 : Algebra F K
inst_5 : Algebra F A
inst_6 : Algebra.IsAlgebraic F K
L : IntermediateField F A
hL : ∀ (x : K), Splits.{u_3} (R := ↥L) (Polynomial.map (algebraMap F ↥L) (minpoly F x))
f : K →ₐ[F] A
x : K
rw : Splits.{u_3} (R := ↥L) (Polynomial.map (algebraMap F ↥L) (minpoly F x))
⊢ Splits.{u_3} (R := ↥L) (Polynomial.map (algebraMap F ↥L) (minpoly.{u_1, u_3} F (B := A) ((f : (a : K) → A) x : A)))

Tactic:
rw [minpoly.algHom_eq f f.injective]

Premises used: minpoly.algHom_eq, RingHom.injective, AlgHom.toRingHom
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst_1 : Field F
inst_2 : Field K
inst_3 : Field A
inst_4 : Algebra F K
inst_5 : Algebra F A
inst_6 : Algebra.IsAlgebraic F K
L : IntermediateField F A
hL : ∀ (x : K), Splits.{u_3} (R := ↥L) (Polynomial.map (algebraMap F ↥L) (minpoly F x))
f : K →ₐ[F] A
x : K
⊢ Splits.{u_3} (R := ↥L) (Polynomial.map (algebraMap F ↥L) (minpoly F x))

Tactic:
hL x
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
F : Type u_1
K : Type u_2
A : Type u_3
inst_1 : Field F
inst_2 : Field K
inst_3 : Field A
inst_4 : Algebra F K
inst_5 : Algebra F A
inst_6 : Algebra.IsAlgebraic F K
L : IntermediateField F A
hL : ∀ (x : K), Splits.{u_3} (R := ↥L) (Polynomial.map (algebraMap F ↥L) (minpoly F x))
f : K →ₐ[F] A
x : K
⊢ Splits.{u_3} (R := ↥L) (Polynomial.map (algebraMap F ↥L) (minpoly F x))

Tactic:
exact hL x
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
F : Type u_1
K : Type u_2
A : Type u_3
inst : Field F
inst_1 : Field K
inst_2 : Field A
inst_3 : Algebra F K
inst_4 : Algebra F A
inst_5 : Algebra.IsAlgebraic F K
L : IntermediateField F A
hL : ∀ (x : K), Splits.{u_3} (R := ↥L) (Polynomial.map (algebraMap F ↥L) (minpoly F x))
f : AlgHom.{u_1, u_2, u_3} F K ↥L
x : K
⊢ Eq.{u_3 + 1} (α := A)
    ((((algHomEquivAlgHomOfSplits A L hL : (a : K →ₐ[F] ↥L) → K →ₐ[F] A) f : K →ₐ[F] A) : (a : K) → A) x : A)
    ((algebraMap (↥L) A : (a : ↥L) → A) ((f : (a : K) → ↥L) x : ↥L) : A)

Tactic:
rfl

Premises used: rfl