awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
rw : Algebra.IsIntegral (↥⊤) K
⊢ Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K

Tactic:
rw [← isAlgebraic_adjoin_iff_top, hs, Algebra.isAlgebraic_iff_isIntegral]

Premises used: IntermediateField.isAlgebraic_adjoin_iff_top, Algebra.isAlgebraic_iff_isIntegral
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
⊢ Algebra.IsIntegral (↥⊤) K

Tactic:
Algebra.isIntegral_of_surjective topEquiv.surjective

Premises used: Algebra.isIntegral_of_surjective, AlgEquiv.surjective, IntermediateField.topEquiv
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
⊢ Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K

Tactic:
have : Algebra.IsAlgebraic (Algebra.adjoin k (s : Set K)) K := by
      rw [← isAlgebraic_adjoin_iff_top, hs, Algebra.isAlgebraic_iff_isIntegral]
      exact Algebra.isIntegral_of_surjective topEquiv.surjective
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
inl :
  ∀ (t : Set K) (hts : t ⊆ (↑s : Set K))
    (ht : IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t))),
    ∃ (s : Finset K),
      IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
        Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K
⊢ ∃ (s : Finset K),
    IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
      Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K

Tactic:
obtain ⟨t, hts, ht⟩ := exists_isTranscendenceBasis_subset (R := k) (s : Set K)

Premises used: SetLike.coe, exists_isTranscendenceBasis_subset
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Set K
hts : t ⊆ (↑s : Set K)
ht : IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t))
⊢ t.Finite

Tactic:
s.finite_toSet.subset hts

Premises used: Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Set K
hts : t ⊆ (↑s : Set K)
ht : IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t))
inl :
  ∀ (t : Finset K) (hts : (↑t : Set K) ⊆ (↑s : Set K))
    (ht :
      IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑t : Set K) }) k
        (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))),
    ∃ (s : Finset K),
      IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
        Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K
⊢ ∃ (s : Finset K),
    IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
      Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K

Tactic:
lift t to Finset K using s.finite_toSet.subset hts

Premises used: Finset, Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Finset K
hts : (↑t : Set K) ⊆ (↑s : Set K)
ht :
  IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑t : Set K) }) k
    (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
⊢ Algebra.IsAlgebraic
    (↥(adjoin k (Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))))) K

Tactic:
ht.isAlgebraic_field

Premises used: IsTranscendenceBasis.isAlgebraic_field
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h_1 : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Finset K
hts : (↑t : Set K) ⊆ (↑s : Set K)
ht :
  IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑t : Set K) }) k
    (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
h :
  ∀ (x : K),
    (↑t : Set K) = Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
h₁ :
  ↥(adjoin k (↑t : Set K)) =
      ↥(adjoin k (Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K))))) →
    (↑t : Set K) = Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
h₂ :
  ↥(adjoin k (↑t : Set K)) =
      ↥(adjoin k (Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K))))) →
    HEq.{u_2 + 1} (α := CommRing ↥(adjoin k (↑t : Set K))) Field.toCommRing (β :=
        CommRing
          ↥(adjoin k
              (Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K))))))
        Field.toCommRing →
      (↑t : Set K) = Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
⊢ Algebra.IsAlgebraic (↥(adjoin k (↑t : Set K))) K

Tactic:
convert! ht.isAlgebraic_field

Premises used: IsTranscendenceBasis.isAlgebraic_field
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Finset K
hts : (↑t : Set K) ⊆ (↑s : Set K)
ht :
  IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑t : Set K) }) k
    (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
x : K
⊢ (↑t : Set K) = Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))

Tactic:
simp
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Finset K
hts : (↑t : Set K) ⊆ (↑s : Set K)
ht :
  IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑t : Set K) }) k
    (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
e_1 :
  ↥(adjoin k (↑t : Set K)) =
    ↥(adjoin k (Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))))
⊢ (↑t : Set K) = Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))

Tactic:
simp
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Finset K
hts : (↑t : Set K) ⊆ (↑s : Set K)
ht :
  IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑t : Set K) }) k
    (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
e_1 :
  ↥(adjoin k (↑t : Set K)) =
    ↥(adjoin k (Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))))
e_3 :
  HEq.{u_2 + 1} (α := CommRing ↥(adjoin k (↑t : Set K))) Field.toCommRing (β :=
    CommRing
      ↥(adjoin k (Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K))))))
    Field.toCommRing
⊢ (↑t : Set K) = Set.range (ι := { x : K // x ∈ (↑t : Set K) }) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))

Tactic:
simp
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Finset K
hts : (↑t : Set K) ⊆ (↑s : Set K)
ht :
  IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑t : Set K) }) k
    (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
⊢ Algebra.IsAlgebraic (↥(adjoin k (↑t : Set K))) K

Tactic:
have : Algebra.IsAlgebraic (IntermediateField.adjoin k (t : Set K)) K := by
      convert! ht.isAlgebraic_field <;> simp
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this_1 : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Finset K
hts : (↑t : Set K) ⊆ (↑s : Set K)
ht :
  IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑t : Set K) }) k
    (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
this : Algebra.IsAlgebraic (↥(adjoin k (↑t : Set K))) K
⊢ ∃ (s : Finset K),
    IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
      Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K

Tactic:
⟨t, ht, inferInstance⟩

Premises used: inferInstance, And.intro, Exists.intro
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this_1 : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Finset K
hts : (↑t : Set K) ⊆ (↑s : Set K)
ht :
  IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑t : Set K) }) k
    (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : Set K)))
this : Algebra.IsAlgebraic (↥(adjoin k (↑t : Set K))) K
⊢ ∃ (s : Finset K),
    IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
      Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K

Tactic:
exact ⟨t, ht, inferInstance⟩
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
⊢ ExpChar k p

Tactic:
have : ExpChar k p := .prime hp.out
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this : ExpChar k p
⊢ CharP K p

Tactic:
have : CharP K p := .of_ringHom_of_ne_zero (algebraMap k K) p hp.out.ne_zero
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this_1 : ExpChar k p
this : CharP K p
⊢ ∃ (s : Finset K),
    IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
      Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K

Tactic:
exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType
    p hp.out fun s hs ↦ ?_

Premises used: exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType, Fact.out
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this_1 : ExpChar k p
this : CharP K p
inr :
  ∀ (s : Finset K) (hs : LinearIndepOn k id (↑s : Set K)), LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
⊢ ∃ (s : Finset K),
    IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
      Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K

Tactic:
refine exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType
    p hp.out fun s hs ↦ ?_

Premises used: exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType, Fact.out
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this_1 : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id (↑s : Set K)
inr : ∀ (r : k), Eq (α := k) ((RingEquiv.symm (frobeniusEquiv k p) : (a : k) → k) r : k) (0 : k) → r = 0
inr₁ : ∀ (m : K), Eq (α := K) (((RingHom.toAddMonoidHom (frobenius K p) : K →+ K) : (a : K) → K) m : K) (0 : K) → m = 0
inr₂ :
  ∀ (r : k) (m : K),
    ((RingHom.toAddMonoidHom (frobenius K p) : K →+ K) : (a : K) → K)
        (HSMul.hSMul (α := k) ((RingEquiv.symm (frobeniusEquiv k p) : (a : k) → k) r : k) m) =
      HSMul.hSMul (β := K) r (((RingHom.toAddMonoidHom (frobenius K p) : K →+ K) : (a : K) → K) m : K)
⊢ LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)

Tactic:
apply hs.map_of_injective_injective (frobeniusEquiv k p).symm (frobenius K p).toAddMonoidHom

Premises used: frobeniusEquiv, RingHom.toAddMonoidHom, frobenius, DFunLike.coe, RingEquiv.symm, LinearIndependent.map_of_injective_injective
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this_1 : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id (↑s : Set K)
⊢ ∀ (r : k), Eq (α := k) ((RingEquiv.symm (frobeniusEquiv k p) : (a : k) → k) r : k) (0 : k) → r = 0

Tactic:
simp [frobenius, Algebra.smul_def, mul_pow, ← map_pow, frobeniusEquiv_symm_pow]

Premises used: map_pow, frobeniusEquiv_symm_pow, frobenius, Algebra.smul_def, mul_pow
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this_1 : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id (↑s : Set K)
⊢ ∀ (m : K), Eq (α := K) (((RingHom.toAddMonoidHom (frobenius K p) : K →+ K) : (a : K) → K) m : K) (0 : K) → m = 0

Tactic:
simp [frobenius, Algebra.smul_def, mul_pow, ← map_pow, frobeniusEquiv_symm_pow]

Premises used: map_pow, frobeniusEquiv_symm_pow, frobenius, Algebra.smul_def, mul_pow
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this_1 : ExpChar k p
this : CharP K p
s : Finset K
hs : LinearIndepOn k id (↑s : Set K)
⊢ ∀ (r : k) (m : K),
    ((RingHom.toAddMonoidHom (frobenius K p) : K →+ K) : (a : K) → K)
        (HSMul.hSMul (α := k) ((RingEquiv.symm (frobeniusEquiv k p) : (a : k) → k) r : k) m) =
      HSMul.hSMul (β := K) r (((RingHom.toAddMonoidHom (frobenius K p) : K →+ K) : (a : K) → K) m : K)

Tactic:
simp [frobenius, Algebra.smul_def, mul_pow, ← map_pow, frobeniusEquiv_symm_pow]

Premises used: map_pow, frobeniusEquiv_symm_pow, frobenius, Algebra.smul_def, mul_pow
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
pos :
  ∀ (H : ∃ (g : K[X]), Irreducible g ∧ g ∣ f),
    Irreducible (Classical.choose (p := fun (x : K[X]) ↦ Irreducible x ∧ x ∣ f) H)
neg : ∀ (H : ¬∃ (g : K[X]), Irreducible g ∧ g ∣ f), Irreducible.{v} (M := K[X]) X
⊢ Irreducible.{v} (M := K[X])
    (if H : ∃ (g : K[X]), Irreducible g ∧ g ∣ f then Classical.choose (p := fun (x : K[X]) ↦ Irreducible x ∧ x ∣ f) H
    else X)

Tactic:
split_ifs with H
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
H : ∃ (g : K[X]), Irreducible g ∧ g ∣ f
⊢ Irreducible (Classical.choose (p := fun (x : K[X]) ↦ Irreducible x ∧ x ∣ f) H)

Tactic:
(Classical.choose_spec H).1

Premises used: Classical.choose_spec, And.left
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
H : ∃ (g : K[X]), Irreducible g ∧ g ∣ f
⊢ Irreducible (Classical.choose (p := fun (x : K[X]) ↦ Irreducible x ∧ x ∣ f) H)

Tactic:
exact (Classical.choose_spec H).1

Premises used: Classical.choose_spec, And.left
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
H : ¬∃ (g : K[X]), Irreducible g ∧ g ∣ f
⊢ Irreducible.{v} (M := K[X]) X

Tactic:
irreducible_X

Premises used: Polynomial.irreducible_X
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
H : ¬∃ (g : K[X]), Irreducible g ∧ g ∣ f
⊢ Irreducible.{v} (M := K[X]) X

Tactic:
exact irreducible_X

Premises used: Polynomial.irreducible_X
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
⊢ Fact (Irreducible f.factor)

Tactic:
⟨irreducible_factor f⟩

Premises used: Fact.mk, Polynomial.irreducible_factor
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
hf1 : ¬IsUnit f
pos : ∀ (hf2 : f = 0), f.factor ∣ f
neg : ∀ (hf2 : ¬f = 0), f.factor ∣ f
⊢ f.factor ∣ f

Tactic:
by_cases hf2 : f = 0
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
pos : Dvd.dvd.{v} (α := K[X]) (factor 0) 0
⊢ f.factor ∣ f

Tactic:
rw [hf2]
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ Dvd.dvd.{v} (α := K[X]) (factor 0) 0

Tactic:
dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ Dvd.dvd.{v} (α := K[X]) (factor 0) 0

Tactic:
exact dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
neg : Classical.choose (p := fun (x : K[X]) ↦ Irreducible x ∧ x ∣ f) ⋯ ∣ f
⊢ f.factor ∣ f

Tactic:
rw [factor, dif_pos (WfDvdMonoid.exists_irreducible_factor hf1 hf2)]

Premises used: Polynomial.factor, dif_pos, WfDvdMonoid.exists_irreducible_factor
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ Classical.choose (p := fun (x : K[X]) ↦ Irreducible x ∧ x ∣ f) ⋯ ∣ f

Tactic:
(Classical.choose_spec <| WfDvdMonoid.exists_irreducible_factor hf1 hf2).2

Premises used: WfDvdMonoid.exists_irreducible_factor, Classical.choose_spec, And.right
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ Classical.choose (p := fun (x : K[X]) ↦ Irreducible x ∧ x ∣ f) ⋯ ∣ f

Tactic:
exact (Classical.choose_spec <| WfDvdMonoid.exists_irreducible_factor hf1 hf2).2

Premises used: WfDvdMonoid.exists_irreducible_factor, Classical.choose_spec, And.right
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
hf : f.degree ≠ 0
⊢ f.factor ∣ f

Tactic:
factor_dvd_of_not_isUnit (mt degree_eq_zero_of_isUnit hf)

Premises used: mt, Polynomial.factor_dvd_of_not_isUnit, Polynomial.degree_eq_zero_of_isUnit
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f : K[X]
hf : f.natDegree ≠ 0
⊢ f.factor ∣ f

Tactic:
factor_dvd_of_degree_ne_zero (mt natDegree_eq_of_degree_eq_some hf)

Premises used: mt, Polynomial.factor_dvd_of_degree_ne_zero, Polynomial.natDegree_eq_of_degree_eq_some
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f g : K[X]
⊢ IsCoprime f g ↔
    ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
      Ne (α := A) ((aeval a : (a : K[X]) → A) f : A) (0 : A) ∨ Ne (α := A) ((aeval a : (a : K[X]) → A) g : A) (0 : A)

Tactic:
⟨fun h => aeval_ne_zero_of_isCoprime h, fun h => isCoprime_of_dvd _ _ ?_ fun x hx _ => ?_⟩

Premises used: isCoprime_of_dvd, Polynomial.aeval_ne_zero_of_isCoprime, Iff.intro
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f g : K[X]
refine_1 :
  ∀
    (h :
      ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
        Ne (α := A) ((aeval a : (a : K[X]) → A) f : A) (0 : A) ∨
          Ne (α := A) ((aeval a : (a : K[X]) → A) g : A) (0 : A)),
    ¬(f = 0 ∧ g = 0)
refine_2 :
  ∀
    (h :
      ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
        Ne (α := A) ((aeval a : (a : K[X]) → A) f : A) (0 : A) ∨ Ne (α := A) ((aeval a : (a : K[X]) → A) g : A) (0 : A))
    (x : K[X]) (hx : Membership.mem (γ := Set K[X]) (nonunits K[X]) x), x ≠ 0 → x ∣ f → ¬x ∣ g
⊢ IsCoprime f g ↔
    ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
      Ne (α := A) ((aeval a : (a : K[X]) → A) f : A) (0 : A) ∨ Ne (α := A) ((aeval a : (a : K[X]) → A) g : A) (0 : A)

Tactic:
refine ⟨fun h => aeval_ne_zero_of_isCoprime h, fun h => isCoprime_of_dvd _ _ ?_ fun x hx _ => ?_⟩
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f g : K[X]
h :
  ∀ {A : Type v} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra K A] (a : A),
    Ne (α := A) ((aeval a : (a : K[X]) → A) f : A) (0 : A) ∨ Ne (α := A) ((aeval a : (a : K[X]) → A) g : A) (0 : A)
⊢ Ne (α := K) ((aeval 0 : (a : K[X]) → K) f : K) (0 : K) ∨ Ne (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)

Tactic:
replace h := @h K _ _ _ 0
-- Module: Mathlib.FieldTheory.SplittingField.Construction
Goal:
K : Type v
inst : Field K
f g : K[X]
h : Ne (α := K) ((aeval 0 : (a : K[X]) → K) f : K) (0 : K) ∨ Ne (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)
refine_1 :
  ∀ (h : f = 0 ∧ g = 0),
    Eq (α := K) ((aeval 0 : (a : K[X]) → K) f : K) (0 : K) ∧ Eq (α := K) ((aeval 0 : (a : K[X]) → K) g : K) (0 : K)
⊢ ¬(f = 0 ∧ g = 0)

Tactic:
contrapose! h