awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
s : Multiset K
h :
  map i f =
    HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
      (Multiset.prod
          (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
        K[X])
h₁ : s.Nodup
⊢ map i f =
    HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) ((i : (a : F) → K) f.leadingCoeff) : K[X])
      (∏ a ∈ s.toFinset, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) : K[X])

Tactic:
rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq, leadingCoeff_map]

Premises used: Finset.prod_eq_multiset_prod, Multiset.toFinset_eq, Polynomial.leadingCoeff_map
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
s : Multiset K
h :
  map i f =
    HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
      (Multiset.prod
          (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
        K[X])
h₁ :
  Separable (R := K)
    (Multiset.prod (Multiset.map (fun (a : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) s))
⊢ s.Nodup

Tactic:
apply nodup_of_separable_prod

Premises used: Polynomial.nodup_of_separable_prod
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
s : Multiset K
h :
  map i f =
    HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
      (Multiset.prod
          (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
        K[X])
h₁ :
  (HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
      (Multiset.prod
          (Multiset.map (fun (a : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) s) :
        K[X])).Separable
h₂ : K[X]
⊢ Separable (R := K)
    (Multiset.prod (Multiset.map (fun (a : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) s))

Tactic:
apply Separable.of_mul_right

Premises used: Polynomial.Separable.of_mul_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
s : Multiset K
h :
  map i f =
    HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
      (Multiset.prod
          (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
        K[X])
⊢ (map i f).Separable

Tactic:
sep.map

Premises used: Polynomial.Separable.map
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
s : Multiset K
h :
  map i f =
    HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
      (Multiset.prod
          (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
        K[X])
⊢ (map i f).Separable

Tactic:
exact sep.map

Premises used: Polynomial.Separable.map
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
inst_1 : CharZero F
f : F[X]
hf : Irreducible f
rw : ¬Eq (α := WithBot ℕ) (↑(f.natDegree - 1) : WithBot ℕ) ⊥
hp : 0 < f.natDegree
⊢ f.Separable

Tactic:
rw [separable_iff_derivative_ne_zero hf, Ne, ← degree_eq_bot, degree_derivative_eq]

Premises used: Polynomial.degree_derivative_eq, Ne, Polynomial.separable_iff_derivative_ne_zero, Polynomial.degree_eq_bot
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
inst_1 : CharZero F
f : F[X]
hf : Irreducible f
⊢ 0 < f.natDegree

Tactic:
Irreducible.natDegree_pos hf

Premises used: Irreducible.natDegree_pos
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
inst_1 : CharZero F
f : F[X]
hf : Irreducible f
⊢ 0 < f.natDegree

Tactic:
exact Irreducible.natDegree_pos hf

Premises used: Irreducible.natDegree_pos
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
inst_3 : Algebra.IsSeparable F K
⊢ ∀ (x : K), IsSeparable F x

Tactic:
Algebra.IsSeparable.isSeparable'

Premises used: Algebra.IsSeparable.isSeparable'
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
x : K
h : IsSeparable F x
inl : Subsingleton F → IsIntegral F x
inr : Nontrivial F → IsIntegral F x
⊢ IsIntegral F x

Tactic:
cases subsingleton_or_nontrivial F

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
x : K
h : IsSeparable F x
h_1 : Subsingleton F
⊢ Subsingleton K

Tactic:
haveI := Module.subsingleton F K
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
x : K
h : IsSeparable F x
h_1 : Subsingleton F
this : Subsingleton K
⊢ IsIntegral F x

Tactic:
⟨1, monic_one, Subsingleton.elim _ _⟩

Premises used: RingHom.IsIntegralElem, IsIntegral, And.intro, Exists.intro, Polynomial.monic_one, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
x : K
h : IsSeparable F x
h_1 : Subsingleton F
this : Subsingleton K
⊢ IsIntegral F x

Tactic:
exact ⟨1, monic_one, Subsingleton.elim _ _⟩
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
x : K
h : IsSeparable F x
h_1 : Nontrivial F
⊢ IsIntegral F x

Tactic:
of_not_not (h.ne_zero <| minpoly.eq_zero ·)

Premises used: Polynomial.Separable.ne_zero, minpoly.eq_zero, of_not_not
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
x : K
h : IsSeparable F x
h_1 : Nontrivial F
⊢ IsIntegral F x

Tactic:
exact of_not_not (h.ne_zero <| minpoly.eq_zero ·)

Premises used: Polynomial.Separable.ne_zero, minpoly.eq_zero, of_not_not
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
inst_3 : Algebra.IsSeparable F K
⊢ ∀ (x : K), IsIntegral F x

Tactic:
fun x ↦ _root_.IsSeparable.isIntegral (Algebra.IsSeparable.isSeparable F x)

Premises used: Algebra.IsSeparable.isSeparable, IsSeparable.isIntegral
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
L : Type u_2
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
inst_3 : Nontrivial F
inst_4 : Algebra.IsSeparable F K
⊢ Algebra.IsAlgebraic F K

Tactic:
⟨fun x ↦ (Algebra.IsSeparable.isIntegral F x).isAlgebraic⟩

Premises used: IsIntegral.isAlgebraic, Algebra.IsAlgebraic.mk, Algebra.IsSeparable.isIntegral
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
⊢ Algebra.IsSeparable F K ↔ ∀ (x : K), IsIntegral F x ∧ IsSeparable F x

Tactic:
⟨fun _ x => ⟨Algebra.IsSeparable.isIntegral F x, Algebra.IsSeparable.isSeparable F x⟩,
    fun h => ⟨fun x => (h x).2⟩⟩

Premises used: Algebra.IsSeparable.isSeparable, And.right, And.intro, Iff.intro, Algebra.IsSeparable.isIntegral, Algebra.IsSeparable.mk
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
L : Type u_2
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
inst_3 : Ring L
inst_4 : Algebra F L
x : K
f : K →ₐ[F] L
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := K) (β := L) (⇑f : (a : K) → L)
H : IsSeparable F x
⊢ IsSeparable.{u_1, u_2} F (K := L) ((f : (a : K) → L) x : L)

Tactic:
(isSeparable_map_iff f hf).mpr H

Premises used: Iff.mpr, isSeparable_map_iff
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
L : Type u_2
inst : CommRing F
inst_1 : Ring L
inst_2 : Algebra F L
S : Subalgebra F L
simp_rw : (∀ (x : ↥S), IsSeparable F x) ↔ ∀ x ∈ S, IsSeparable F x
simp_rw₁ : (∀ (a : L) (b : a ∈ S), IsSeparable F (Subtype.mk (p := fun (a : L) ↦ a ∈ S) a b)) ↔ ∀ x ∈ S, IsSeparable F x
simp_rw₂ :
  (∀ (a : L) (b : a ∈ S),
      IsSeparable F (K := L) ((S.val : (a : ↥S) → L) (Subtype.mk (p := fun (a : L) ↦ a ∈ S) a b) : L)) ↔
    ∀ x ∈ S, IsSeparable F x
⊢ Algebra.IsSeparable.{u_1, u_2} F ↥S ↔ ∀ x ∈ S, IsSeparable F x

Tactic:
simp_rw [Algebra.isSeparable_def, Subtype.forall,
    ← isSeparable_map_iff S.val Subtype.val_injective, coe_val]

Premises used: isSeparable_map_iff, Subtype.val_injective, Subalgebra.val, Subtype.forall, Algebra.isSeparable_def, Subalgebra.coe_val
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
E : Type u_4
inst_3 : Ring E
inst_4 : Algebra F E
e : K ≃ₐ[F] E
x : K
⊢ IsSeparable.{u_1, u_4} F (K := E) ((e : (a : K) → E) x : E) ↔ IsSeparable F x

Tactic:
simp only [IsSeparable, minpoly.algEquiv_eq e x]

Premises used: minpoly.algEquiv_eq, IsSeparable
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
E : Type u_4
inst_3 : Ring E
inst_4 : Algebra F E
e : K ≃ₐ[F] E
inst_5 : Algebra.IsSeparable F K
⊢ Algebra.IsSeparable F E

Tactic:
⟨fun _ ↦ e.symm.isSeparable_iff.mp (Algebra.IsSeparable.isSeparable _ _)⟩

Premises used: Algebra.IsSeparable.isSeparable, AlgEquiv.isSeparable_iff, AlgEquiv.symm, Iff.mp, DFunLike.coe, Algebra.IsSeparable.mk
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
E : Type u_4
inst_3 : Ring E
inst_4 : Algebra F E
e : K ≃ₐ[F] E
⊢ Algebra.IsSeparable F K ↔ Algebra.IsSeparable F E

Tactic:
⟨fun _ ↦ AlgEquiv.Algebra.isSeparable e, fun _ ↦ AlgEquiv.Algebra.isSeparable e.symm⟩

Premises used: AlgEquiv.symm, Iff.intro, AlgEquiv.Algebra.isSeparable
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
L : Type u_2
inst : CommRing F
E : Type u_4
inst_1 : Field L
inst_2 : Ring E
inst_3 : Algebra F L
inst_4 : Algebra F E
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
x : E
h : IsSeparable F x
⊢ IsSeparable L x

Tactic:
.of_dvd (.map h) (minpoly.dvd_map_of_isScalarTower ..)

Premises used: minpoly.dvd_map_of_isScalarTower, Polynomial.Separable.map, IsSeparable, Polynomial.Separable.of_dvd
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
L : Type u_2
inst : CommRing F
E : Type u_4
inst_1 : Field L
inst_2 : Ring E
inst_3 : Algebra F L
inst_4 : Algebra F E
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
inst_7 : Algebra.IsSeparable F E
⊢ Algebra.IsSeparable L E

Tactic:
⟨fun x ↦ IsSeparable.tower_top _ (Algebra.IsSeparable.isSeparable F x)⟩

Premises used: Algebra.IsSeparable.isSeparable, IsSeparable.tower_top, Algebra.IsSeparable.mk
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Ring K
inst_2 : Algebra F K
x : F
⊢ Eq.{u_2 + 1} (α := K)
    (((aeval ((algebraMap F K : (a : F) → K) x) : F[X] →ₐ[F] K) : (a : F[X]) → K)
        (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])) :
      K)
    (0 : K)

Tactic:
simp
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
inst : Field F
K : Type u_2
E : Type u_3
E' : Type u_4
inst_1 : Ring K
inst_2 : Algebra F K
⊢ Algebra.IsSeparable F F

Tactic:
⟨isSeparable_algebraMap⟩

Premises used: isSeparable_algebraMap, Algebra.IsSeparable.mk
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Ring K
inst_2 : Algebra F K
inst_3 : IsDomain K
inst_4 : Algebra.IsIntegral F K
inst_5 : CharZero F
x : K
⊢ IsSeparable F x

Tactic:
(minpoly.irreducible <| Algebra.IsIntegral.isIntegral x).separable

Premises used: Algebra.IsIntegral.isIntegral, Irreducible.separable, IsSeparable, minpoly.irreducible
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
inst : Field F
K : Type u_2
E : Type u_3
E' : Type u_4
inst_1 : Ring K
inst_2 : Algebra F K
inst_3 : IsDomain K
inst_4 : Algebra.IsIntegral F K
inst_5 : CharZero F
⊢ Algebra.IsSeparable F K

Tactic:
⟨_root_.IsSeparable.of_integral _⟩

Premises used: IsSeparable.of_integral, Algebra.IsSeparable.mk
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
inst : Field F
K : Type u_2
E : Type u_3
inst_1 : Field K
inst_2 : Ring E
inst_3 : Algebra F K
inst_4 : Algebra F E
inst_5 : Algebra K E
inst_6 : Nontrivial E
inst_7 : IsScalarTower F K E
x : K
h : IsSeparable.{u_1, u_3} F (K := E) ((algebraMap K E : (a : K) → E) x : E)
⊢ IsSeparable F x

Tactic:
have ⟨_q, hq⟩ :=
      minpoly.dvd F x
        ((aeval_algebraMap_eq_zero_iff _ _ _).mp (minpoly.aeval F ((algebraMap K E) x)))
    (Eq.mp (congrArg Separable hq) h).of_mul_left

Premises used: _private.0.IsSeparable.tower_bot.match_1, Polynomial.aeval_algebraMap_eq_zero_iff, Algebra.algebraMap, congrArg, Eq.mp, Polynomial.Separable.of_mul_left, minpoly.aeval, minpoly, Iff.mp, minpoly.dvd, IsSeparable, Polynomial.Separable, DFunLike.coe
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
inst : Field F
K : Type u_2
E : Type u_3
inst_1 : Field K
inst_2 : Ring E
inst_3 : Algebra F K
inst_4 : Algebra F E
inst_5 : Algebra K E
inst_6 : Nontrivial E
inst_7 : IsScalarTower F K E
h : Algebra.IsSeparable F E
⊢ Algebra.IsSeparable F K

Tactic:
⟨fun _ ↦ IsSeparable.tower_bot (h.isSeparable _ _)⟩

Premises used: Algebra.IsSeparable.isSeparable, Algebra.algebraMap, IsSeparable.tower_bot, DFunLike.coe, Algebra.IsSeparable.mk
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
inst : Field F
E : Type u_3
E' : Type u_4
inst_1 : Field E
inst_2 : Field E'
inst_3 : Algebra F E
inst_4 : Algebra F E'
f : E →ₐ[F] E'
x : E
h : IsSeparable.{u_1, u_4} F (K := E') ((f : (a : E) → E') x : E')
x_1 : Algebra E E' := f.toAlgebra
⊢ IsScalarTower F E E'

Tactic:
haveI : IsScalarTower F E E' := IsScalarTower.of_algebraMap_eq fun x => (f.commutes x).symm
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
inst : Field F
E : Type u_3
E' : Type u_4
inst_1 : Field E
inst_2 : Field E'
inst_3 : Algebra F E
inst_4 : Algebra F E'
f : E →ₐ[F] E'
x : E
h : IsSeparable.{u_1, u_4} F (K := E') ((f : (a : E) → E') x : E')
x_1 : Algebra E E' := f.toAlgebra
this : IsScalarTower F E E'
⊢ IsSeparable F x

Tactic:
h.tower_bot

Premises used: IsSeparable.tower_bot
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
inst : Field F
E : Type u_3
E' : Type u_4
inst_1 : Field E
inst_2 : Field E'
inst_3 : Algebra F E
inst_4 : Algebra F E'
f : E →ₐ[F] E'
x : E
h : IsSeparable.{u_1, u_4} F (K := E') ((f : (a : E) → E') x : E')
x_1 : Algebra E E' := f.toAlgebra
this : IsScalarTower F E E'
⊢ IsSeparable F x

Tactic:
exact h.tower_bot

Premises used: IsSeparable.tower_bot
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
inst : Field F
E : Type u_3
E' : Type u_4
inst_1 : Field E
inst_2 : Field E'
inst_3 : Algebra F E
inst_4 : Algebra F E'
f : E →ₐ[F] E'
inst_5 : Algebra.IsSeparable F E'
⊢ Algebra.IsSeparable F E

Tactic:
⟨fun x => (Algebra.IsSeparable.isSeparable F (f x)).of_algHom⟩

Premises used: Algebra.IsSeparable.isSeparable, IsSeparable.of_algHom, DFunLike.coe, Algebra.IsSeparable.mk
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
inst : Field F
K : Type u_2
E : Type u_3
E' : Type u_4
inst_1 : Field K
inst_2 : Algebra F K
M : IntermediateField F K
inst_3 : Algebra.IsSeparable F K
⊢ Algebra.IsSeparable.{u_1, u_2} F ↥M

Tactic:
Algebra.isSeparable_tower_bot_of_isSeparable F M K

Premises used: Membership.mem, Subtype, Algebra.isSeparable_tower_bot_of_isSeparable
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
inst : Field F
K : Type u_2
E : Type u_3
E' : Type u_4
inst_1 : Field K
inst_2 : Algebra F K
M : IntermediateField F K
inst_3 : Algebra.IsSeparable F K
⊢ Algebra.IsSeparable (↥M) K

Tactic:
Algebra.isSeparable_tower_top_of_isSeparable F M K

Premises used: Membership.mem, Subtype, Algebra.isSeparable_tower_top_of_isSeparable
-- Module: Mathlib.FieldTheory.Separable
Goal:
A₁ : Type u_1
B₁ : Type u_2
A₂ : Type u_3
B₂ : Type u_4
inst : Field A₁
inst_1 : Ring B₁
inst_2 : Field A₂
inst_3 : Ring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
x_1 : B₁
h : IsSeparable A₁ x_1
this_1 : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this_2 : Algebra A₂ B₁ :=
  let __src : A₂ →+* B₁ := RingHom.comp (algebraMap A₁ B₁) e₁.symm.toRingHom;
  { smul := fun (a : A₂) (b : B₁) ↦ ((algebraMap A₁ B₁).comp e₁.symm.toRingHom : (a : A₂) → B₁) a * b,
    algebraMap := RingHom.comp (algebraMap A₁ B₁) e₁.symm.toRingHom, commutes' := ⋯, smul_def' := ⋯ }
this : IsScalarTower A₁ A₂ B₁
x : A₂
⊢ e₂.toFun ((algebraMap A₂ B₁ : (a : A₂) → B₁) x) = (algebraMap A₂ B₂ : (a : A₂) → B₂) x

Tactic:
simpa [RingHom.algebraMap_toAlgebra] using DFunLike.congr_fun he.symm (e₁.symm x)

Premises used: DFunLike.congr_fun, RingHom.algebraMap_toAlgebra, Eq.symm, DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.FieldTheory.Separable
Goal:
A₁ : Type u_1
B₁ : Type u_2
A₂ : Type u_3
B₂ : Type u_4
inst : Field A₁
inst_1 : Ring B₁
inst_2 : Field A₂
inst_3 : Ring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
inst_6 : Algebra.IsSeparable A₁ B₁
⊢ Algebra.IsSeparable A₂ B₂

Tactic:
⟨fun x ↦ (e₂.apply_symm_apply x) ▸ _root_.IsSeparable.of_equiv_equiv e₁ e₂ he
    (Algebra.IsSeparable.isSeparable _ _)⟩

Premises used: RingEquiv.apply_symm_apply, Algebra.IsSeparable.isSeparable, Eq.rec, DFunLike.coe, IsSeparable.of_equiv_equiv, Algebra.IsSeparable.mk, RingEquiv.symm
-- Module: Mathlib.FieldTheory.Separable
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw : (aroots (minpoly K pb.gen) L).Nodup
⊢ Nat.card (S →ₐ[K] L) = pb.dim

Tactic:
rw [Nat.card_congr pb.liftEquiv', Nat.subtype_card _ (fun x => Multiset.mem_toFinset),
    ← pb.natDegree_minpoly, ← natDegree_map (algebraMap K L), h_splits.natDegree_eq_card_roots,
    Multiset.toFinset_card_of_nodup]

Premises used: PowerBasis.liftEquiv', Algebra.algebraMap, Polynomial.natDegree_map, Nat.subtype_card, Nat.card_congr, Polynomial.Splits.natDegree_eq_card_roots, Multiset.toFinset_card_of_nodup, PowerBasis.natDegree_minpoly, Multiset.mem_toFinset
-- Module: Mathlib.FieldTheory.Separable
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
⊢ (aroots (minpoly K pb.gen) L).Nodup

Tactic:
nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)

Premises used: Iff.mpr, Algebra.algebraMap, Polynomial.nodup_roots, Polynomial.separable_map
-- Module: Mathlib.FieldTheory.Separable
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
⊢ (aroots (minpoly K pb.gen) L).Nodup

Tactic:
exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)

Premises used: Iff.mpr, Algebra.algebraMap, Polynomial.nodup_roots, Polynomial.separable_map
-- Module: Mathlib.FieldTheory.Separable
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw : Nat.card.{u_5} { y : L // y ∈ aroots (minpoly K pb.gen) L } = pb.dim
rw₁ : #(aroots (minpoly K pb.gen) L).toFinset = pb.dim
rw₂ : #(aroots (minpoly K pb.gen) L).toFinset = natDegree (minpoly K pb.gen)
rw₃ : #(aroots (minpoly K pb.gen) L).toFinset = natDegree (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw₄ : #(aroots (minpoly K pb.gen) L).toFinset = (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen))).card
rw₅ : (aroots (minpoly K pb.gen) L).card = (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen))).card
rw₆ : (aroots (minpoly K pb.gen) L).Nodup
rw₇ : (aroots (minpoly K pb.gen) L).card = (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen))).card
rw₈ rw₉ : (aroots (minpoly K pb.gen) L).Nodup
⊢ Nat.card (S →ₐ[K] L) = pb.dim

Tactic:
classical
  rw [Nat.card_congr pb.liftEquiv', Nat.subtype_card _ (fun x => Multiset.mem_toFinset),
    ← pb.natDegree_minpoly, ← natDegree_map (algebraMap K L), h_splits.natDegree_eq_card_roots,
    Multiset.toFinset_card_of_nodup]
  exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)

Premises used: Iff.mpr, PowerBasis.liftEquiv', Algebra.algebraMap, Polynomial.natDegree_map, Nat.subtype_card, Nat.card_congr, Polynomial.Splits.natDegree_eq_card_roots, Multiset.toFinset_card_of_nodup, PowerBasis.natDegree_minpoly, Multiset.mem_toFinset, Polynomial.nodup_roots, Polynomial.separable_map
-- Module: Mathlib.FieldTheory.Separable
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw : Nat.card (S →ₐ[K] L) = pb.dim
rw₁ rw₂ : pb.dim = pb.dim
⊢ Fintype.card (S →ₐ[K] L) = pb.dim

Tactic:
rw [Fintype.card_eq_nat_card, AlgHom.natCard_of_powerBasis pb h_sep h_splits]

Premises used: AlgHom.natCard_of_powerBasis, Fintype.card_eq_nat_card
-- Module: Mathlib.FieldTheory.Separable
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw : Nat.card (S →ₐ[K] L) = pb.dim
rw₁ rw₂ : pb.dim = pb.dim
⊢ Fintype.card (S →ₐ[K] L) = pb.dim

Tactic:
classical
  rw [Fintype.card_eq_nat_card, AlgHom.natCard_of_powerBasis pb h_sep h_splits]

Premises used: AlgHom.natCard_of_powerBasis, Fintype.card_eq_nat_card
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
⊢ Membership.mem (γ := IntermediateField F E) (separableClosure F E) x ↔ IsSeparable F x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, IsSeparable, Polynomial.Separable, IsCoprime
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
x : E
simp_rw : IsSeparable.{u, w} F (K := K) ((i : (a : E) → K) x : K) ↔ IsSeparable F x
simp_rw₁ : Separable (minpoly.{u, w} F (B := K) ((i : (a : E) → K) x : K)) ↔ Separable (minpoly F x)
⊢ Membership.mem (α := K) (γ := IntermediateField F K) (separableClosure F K) ((i : (a : E) → K) x : K) ↔
    Membership.mem (γ := IntermediateField F E) (separableClosure F E) x

Tactic:
simp_rw [mem_separableClosure_iff, IsSeparable, minpoly.algHom_eq i i.injective]

Premises used: minpoly.algHom_eq, RingHom.injective, AlgHom.toRingHom, mem_separableClosure_iff, IsSeparable
-- Module: Mathlib.FieldTheory.SeparableClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
h : ∀ (x : E), x ∈ comap i (separableClosure F K) ↔ Membership.mem (γ := IntermediateField F E) (separableClosure F E) x
⊢ comap i (separableClosure F K) = separableClosure F E

Tactic:
ext x