awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  Eq (α := p.Gal × q.Gal) ((restrictProd p q : (a : (p * q).Gal) → p.Gal × q.Gal) f : p.Gal × q.Gal)
    ((restrictProd p q : (a : (p * q).Gal) → p.Gal × q.Gal) g : p.Gal × q.Gal)
⊢ f = g
have neg : ∀
  (hfg :
    Eq (α := p.Gal × q.Gal)
      ((MonoidHom.prod (if hq : p * q = 0 then 1 else restrict p (p * q).SplittingField)
              (if hq : p * q = 0 then 1 else restrict q (p * q).SplittingField) :
            (a : (p * q).Gal) → p.Gal × q.Gal)
          f :
        p.Gal × q.Gal)
      ((MonoidHom.prod (if hq : p * q = 0 then 1 else restrict p (p * q).SplittingField)
              (if hq : p * q = 0 then 1 else restrict q (p * q).SplittingField) :
            (a : (p * q).Gal) → p.Gal × q.Gal)
          g :
        p.Gal × q.Gal)),
  f = g
Tactic: classical
  simp only [restrictProd, restrictDvd_def] at hfg
  simp only [dif_neg hpq, MonoidHom.prod_apply, Prod.mk_inj] at hfg
  ext (x hx)
  rw [rootSet_def, aroots_mul hpq] at hx
  rcases Multiset.mem_add.mp (Multiset.mem_toFinset.mp hx) with h | h
  · haveI : Fact ((p.map (algebraMap F (p * q).SplittingField)).Splits) :=
      ⟨(SplittingField.splits (p * q)).of_dvd (map_ne_zero hpq)
        ((map_dvd_map' _).mpr (dvd_mul_right p q))⟩
    have key :
      x =
        algebraMap p.SplittingField (p * q).SplittingField
          ((rootsEquivRoots p _).invFun
            ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
      Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots p _) ⟨x, _⟩).symm
    rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
    exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.1 _)
  · haveI : Fact ((q.map (algebraMap F (p * q).SplittingField)).Splits) :=
      ⟨(SplittingField.splits (p * q)).of_dvd (map_ne_zero hpq)
        ((map_dvd_map' _).mpr (dvd_mul_left q p))⟩
    have key :
      x =
        algebraMap q.SplittingField (p * q).SplittingField
          ((rootsEquivRoots q _).invFun
            ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
      Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots q _) ⟨x, _⟩).symm
    rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
    exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.2 _)
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  Eq (α := p.Gal × q.Gal) ((restrictProd p q : (a : (p * q).Gal) → p.Gal × q.Gal) f : p.Gal × q.Gal)
    ((restrictProd p q : (a : (p * q).Gal) → p.Gal × q.Gal) g : p.Gal × q.Gal)
neg :
  ∀
    (hfg :
      Eq (α := p.Gal × q.Gal)
        ((MonoidHom.prod (if hq : p * q = 0 then 1 else restrict p (p * q).SplittingField)
                (if hq : p * q = 0 then 1 else restrict q (p * q).SplittingField) :
              (a : (p * q).Gal) → p.Gal × q.Gal)
            f :
          p.Gal × q.Gal)
        ((MonoidHom.prod (if hq : p * q = 0 then 1 else restrict p (p * q).SplittingField)
                (if hq : p * q = 0 then 1 else restrict q (p * q).SplittingField) :
              (a : (p * q).Gal) → p.Gal × q.Gal)
            g :
          p.Gal × q.Gal)),
    f = g
⊢ f = g
have neg₁ : ∀
  (hfg :
    Eq (α := p.Gal) ((restrict p (p * q).SplittingField : (a : (p * q).Gal) → p.Gal) f : p.Gal)
        ((restrict p (p * q).SplittingField : (a : (p * q).Gal) → p.Gal) g : p.Gal) ∧
      Eq (α := q.Gal) ((restrict q (p * q).SplittingField : (a : (p * q).Gal) → q.Gal) f : q.Gal)
        ((restrict q (p * q).SplittingField : (a : (p * q).Gal) → q.Gal) g : q.Gal)),
  f = g
Tactic: classical
  simp only [restrictProd, restrictDvd_def] at hfg
  simp only [dif_neg hpq, MonoidHom.prod_apply, Prod.mk_inj] at hfg
  ext (x hx)
  rw [rootSet_def, aroots_mul hpq] at hx
  rcases Multiset.mem_add.mp (Multiset.mem_toFinset.mp hx) with h | h
  · haveI : Fact ((p.map (algebraMap F (p * q).SplittingField)).Splits) :=
      ⟨(SplittingField.splits (p * q)).of_dvd (map_ne_zero hpq)
        ((map_dvd_map' _).mpr (dvd_mul_right p q))⟩
    have key :
      x =
        algebraMap p.SplittingField (p * q).SplittingField
          ((rootsEquivRoots p _).invFun
            ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
      Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots p _) ⟨x, _⟩).symm
    rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
    exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.1 _)
  · haveI : Fact ((q.map (algebraMap F (p * q).SplittingField)).Splits) :=
      ⟨(SplittingField.splits (p * q)).of_dvd (map_ne_zero hpq)
        ((map_dvd_map' _).mpr (dvd_mul_left q p))⟩
    have key :
      x =
        algebraMap q.SplittingField (p * q).SplittingField
          ((rootsEquivRoots q _).invFun
            ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
      Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots q _) ⟨x, _⟩).symm
    rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
    exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.2 _)
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (R := q₁.SplittingField) (map (algebraMap F q₁.SplittingField) p₁)
h₂ : Splits (R := q₂.SplittingField) (map (algebraMap F q₂.SplittingField) p₂)
⊢ Splits (R := (q₁ * q₂).SplittingField) (map (algebraMap F (q₁ * q₂).SplittingField) (p₁ * p₂))
have rw : (HMul.hMul (α := (q₁ * q₂).SplittingField[X]) (map (algebraMap F (q₁ * q₂).SplittingField) p₁)
    (map (algebraMap F (q₁ * q₂).SplittingField) p₂)).Splits
Tactic: rw [Polynomial.map_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (R := q₁.SplittingField) (map (algebraMap F q₁.SplittingField) p₁)
h₂ : Splits (R := q₂.SplittingField) (map (algebraMap F q₂.SplittingField) p₂)
⊢ (HMul.hMul (α := (q₁ * q₂).SplittingField[X]) (map (algebraMap F (q₁ * q₂).SplittingField) p₁)
      (map (algebraMap F (q₁ * q₂).SplittingField) p₂)).Splits
have hf : Splits (R := (q₁ * q₂).SplittingField) (map (algebraMap F (q₁ * q₂).SplittingField) p₁)
Tactic: apply Splits.mul
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (R := q₁.SplittingField) (map (algebraMap F q₁.SplittingField) p₁)
h₂ : Splits (R := q₂.SplittingField) (map (algebraMap F q₂.SplittingField) p₂)
hf : Splits (R := (q₁ * q₂).SplittingField) (map (algebraMap F (q₁ * q₂).SplittingField) p₁)
⊢ (HMul.hMul (α := (q₁ * q₂).SplittingField[X]) (map (algebraMap F (q₁ * q₂).SplittingField) p₁)
      (map (algebraMap F (q₁ * q₂).SplittingField) p₂)).Splits
have hg : Splits (R := (q₁ * q₂).SplittingField) (map (algebraMap F (q₁ * q₂).SplittingField) p₂)
Tactic: apply Splits.mul
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (R := q₁.SplittingField) (map (algebraMap F q₁.SplittingField) p₁)
h₂ : Splits (R := q₂.SplittingField) (map (algebraMap F q₂.SplittingField) p₂)
⊢ Splits (R := (q₁ * q₂).SplittingField) (map (algebraMap F (q₁ * q₂).SplittingField) p₁)
have hf : Splits
  (map (↑(SplittingField.lift q₁ sorry) : q₁.SplittingField →+* (q₁ * q₂).SplittingField)
    (map (algebraMap F q₁.SplittingField) p₁))
Tactic: rw [←
      (SplittingField.lift q₁
          ((SplittingField.splits _).of_dvd (map_ne_zero (mul_ne_zero hq₁ hq₂))
             ((map_dvd_map' _).mpr (dvd_mul_right q₁ q₂)))).comp_algebraMap, ← map_map]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (R := q₁.SplittingField) (map (algebraMap F q₁.SplittingField) p₁)
h₂ : Splits (R := q₂.SplittingField) (map (algebraMap F q₂.SplittingField) p₂)
⊢ Splits (R := (q₁ * q₂).SplittingField) (map (algebraMap F (q₁ * q₂).SplittingField) p₂)
have hg : Splits
  (map (↑(SplittingField.lift q₂ sorry) : q₂.SplittingField →+* (q₁ * q₂).SplittingField)
    (map (algebraMap F q₂.SplittingField) p₂))
Tactic: rw [←
      (SplittingField.lift q₂
          ((SplittingField.splits _).of_dvd (map_ne_zero (mul_ne_zero hq₁ hq₂))
             ((map_dvd_map' _).mpr (dvd_mul_left q₂ q₁)))).comp_algebraMap, ← map_map]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hq : q.natDegree ≠ 0
⊢ Function.Surjective (α := (p.comp q).Gal) (β := p.Gal) (⇑(restrictComp p q hq) : (a : (p.comp q).Gal) → p.Gal)
have this : Fact (Splits (R := (p.comp q).SplittingField) (map (algebraMap F (p.comp q).SplittingField) p))
Tactic: haveI : Fact (Splits (p.map (algebraMap F (SplittingField (comp p q))))) :=
    ⟨splits_in_splittingField_of_comp p q hq⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
⊢ p.natDegree ∣ Nat.card.{u_1} p.Gal
have rw : p.natDegree ∣ finrank F p.SplittingField
Tactic: rw [Gal.card_of_separable p_irr.separable]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
⊢ p.natDegree ∣ finrank F p.SplittingField
have hp : p.degree ≠ 0
Tactic: have hp : p.degree ≠ 0 := fun h =>
    Nat.Prime.ne_zero p_deg (natDegree_eq_zero_iff_degree_le_zero.mpr (le_of_eq h))
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (hypothesis)
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
⊢ p.natDegree ∣ finrank F p.SplittingField
have hα : IsIntegral F α
Tactic: have hα : IsIntegral F α := .of_finite F α
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
⊢ p.natDegree ∣ finrank F p.SplittingField
have h : finrank F p.SplittingField = p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
Tactic: use Module.finrank F⟮α⟯ p.SplittingField
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
this : natDegree (minpoly F α) = p.natDegree
x : AddCommGroup ↥F⟮α⟯ := Ring.toAddCommGroup
⊢ finrank F p.SplittingField = p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
have rw : finrank F ↥F⟮α⟯ * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField =
  p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
Tactic: rw [← Module.finrank_mul_finrank F F⟮α⟯ p.SplittingField,
      IntermediateField.adjoin.finrank hα, this]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
this : natDegree (minpoly F α) = p.natDegree
x : AddCommGroup ↥F⟮α⟯ := Ring.toAddCommGroup
rw :
  finrank F ↥F⟮α⟯ * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField =
    p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
⊢ finrank F p.SplittingField = p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
have rw₁ : natDegree (minpoly F α) * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField =
  p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
Tactic: rw [← Module.finrank_mul_finrank F F⟮α⟯ p.SplittingField,
      IntermediateField.adjoin.finrank hα, this]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
this : natDegree (minpoly F α) = p.natDegree
x : AddCommGroup ↥F⟮α⟯ := Ring.toAddCommGroup
rw :
  finrank F ↥F⟮α⟯ * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField =
    p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
rw₁ :
  natDegree (minpoly F α) * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField =
    p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
⊢ finrank F p.SplittingField = p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
have rw₂ : p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField = p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
Tactic: rw [← Module.finrank_mul_finrank F F⟮α⟯ p.SplittingField,
      IntermediateField.adjoin.finrank hα, this]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
⊢ finrank F p.SplittingField = p.natDegree * finrank.{u_1, u_1} (↥F⟮α⟯) p.SplittingField
have h : natDegree (minpoly F α) = p.natDegree
Tactic: suffices (minpoly F α).natDegree = p.natDegree by
    letI _ : AddCommGroup F⟮α⟯ := Ring.toAddCommGroup
    rw [← Module.finrank_mul_finrank F F⟮α⟯ p.SplittingField,
      IntermediateField.adjoin.finrank hα, this]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ natDegree (minpoly F α) = p.natDegree
have a : natDegree (minpoly F α) ≤ p.natDegree
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
a : natDegree (minpoly F α) ≤ p.natDegree
⊢ natDegree (minpoly F α) = p.natDegree
have a₁ : p.natDegree ≤ natDegree (minpoly F α)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
⊢ natDegree (minpoly F α) = p.natDegree
have h : minpoly F α ∣ p
Tactic: suffices minpoly F α ∣ p by
    have key := (minpoly.irreducible hα).dvd_symm p_irr this
    apply le_antisymm
    · exact natDegree_le_of_dvd this p_irr.ne_zero
    · exact natDegree_le_of_dvd key (minpoly.ne_zero hα)
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
⊢ minpoly F α ∣ p
have h : Eq (α := p.SplittingField) ((aeval α : (a : F[X]) → p.SplittingField) p) 0
Tactic: apply minpoly.dvd F α
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
⊢ Eq (α := p.SplittingField) ((aeval α : (a : F[X]) → p.SplittingField) p) 0
have h : eval α (map (algebraMap F p.SplittingField) p) = 0
Tactic: rw [← eval_map_algebraMap, eval_rootOfSplits]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
inst_1 : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
h : eval α (map (algebraMap F p.SplittingField) p) = 0
⊢ Eq (α := p.SplittingField) ((aeval α : (a : F[X]) → p.SplittingField) p) 0
have h₁ : Eq.{u_1 + 1} (α := p.SplittingField) 0 0
Tactic: rw [← eval_map_algebraMap, eval_rootOfSplits]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimeField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
⊢ Eq (α := Subfield K) ⊥ (RingHom.fieldRange (algebraMap ℚ K))
have rw : Eq (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) ⊥
Tactic: rw [eq_comm, eq_bot_iff, ← Subfield.map_bot (algebraMap ℚ K),
    subsingleton_iff_bot_eq_top.mpr inferInstance, ← RingHom.fieldRange_eq_map]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimeField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
rw : Eq (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) ⊥
⊢ Eq (α := Subfield K) ⊥ (RingHom.fieldRange (algebraMap ℚ K))
have rw₁ : LE.le (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) ⊥
Tactic: rw [eq_comm, eq_bot_iff, ← Subfield.map_bot (algebraMap ℚ K),
    subsingleton_iff_bot_eq_top.mpr inferInstance, ← RingHom.fieldRange_eq_map]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimeField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
rw : Eq (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) ⊥
rw₁ : LE.le (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) ⊥
⊢ Eq (α := Subfield K) ⊥ (RingHom.fieldRange (algebraMap ℚ K))
have rw₂ : LE.le (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) (map (algebraMap ℚ K) ⊥)
Tactic: rw [eq_comm, eq_bot_iff, ← Subfield.map_bot (algebraMap ℚ K),
    subsingleton_iff_bot_eq_top.mpr inferInstance, ← RingHom.fieldRange_eq_map]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimeField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
rw : Eq (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) ⊥
rw₁ : LE.le (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) ⊥
rw₂ : LE.le (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) (map (algebraMap ℚ K) ⊥)
⊢ Eq (α := Subfield K) ⊥ (RingHom.fieldRange (algebraMap ℚ K))
have rw₃ : LE.le (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) (map (algebraMap ℚ K) ⊤)
Tactic: rw [eq_comm, eq_bot_iff, ← Subfield.map_bot (algebraMap ℚ K),
    subsingleton_iff_bot_eq_top.mpr inferInstance, ← RingHom.fieldRange_eq_map]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimeField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
rw : Eq (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) ⊥
rw₁ : LE.le (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) ⊥
rw₂ : LE.le (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) (map (algebraMap ℚ K) ⊥)
rw₃ : LE.le (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) (map (algebraMap ℚ K) ⊤)
⊢ Eq (α := Subfield K) ⊥ (RingHom.fieldRange (algebraMap ℚ K))
have rw₄ : LE.le (α := Subfield K) (RingHom.fieldRange (algebraMap ℚ K)) (RingHom.fieldRange (algebraMap ℚ K))
Tactic: rw [eq_comm, eq_bot_iff, ← Subfield.map_bot (algebraMap ℚ K),
    subsingleton_iff_bot_eq_top.mpr inferInstance, ← RingHom.fieldRange_eq_map]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimeField (goal)
Goal:
K : Type u_1
p : ℕ
hp : Fact (Nat.Prime p)
inst : Field K
inst_1 : Algebra (ZMod p) K
⊢ Eq.{u_1 + 1} (α := Subfield K) ⊥ (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
have rw : Eq.{u_1 + 1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K)) ⊥
Tactic: rw [eq_comm, eq_bot_iff, ← Subfield.map_bot (algebraMap (ZMod p) K),
    subsingleton_iff_bot_eq_top.mpr inferInstance, ← RingHom.fieldRange_eq_map]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimeField (goal)
Goal:
K : Type u_1
p : ℕ
hp : Fact (Nat.Prime p)
inst : Field K
inst_1 : Algebra (ZMod p) K
rw : Eq.{u_1 + 1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K)) ⊥
⊢ Eq.{u_1 + 1} (α := Subfield K) ⊥ (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
have rw₁ : LE.le.{u_1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K)) ⊥
Tactic: rw [eq_comm, eq_bot_iff, ← Subfield.map_bot (algebraMap (ZMod p) K),
    subsingleton_iff_bot_eq_top.mpr inferInstance, ← RingHom.fieldRange_eq_map]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimeField (goal)
Goal:
K : Type u_1
p : ℕ
hp : Fact (Nat.Prime p)
inst : Field K
inst_1 : Algebra (ZMod p) K
rw : Eq.{u_1 + 1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K)) ⊥
rw₁ : LE.le.{u_1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K)) ⊥
⊢ Eq.{u_1 + 1} (α := Subfield K) ⊥ (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
have rw₂ : LE.le.{u_1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
  (map (K := ZMod p) (algebraMap (ZMod p) K) ⊥)
Tactic: rw [eq_comm, eq_bot_iff, ← Subfield.map_bot (algebraMap (ZMod p) K),
    subsingleton_iff_bot_eq_top.mpr inferInstance, ← RingHom.fieldRange_eq_map]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimeField (goal)
Goal:
K : Type u_1
p : ℕ
hp : Fact (Nat.Prime p)
inst : Field K
inst_1 : Algebra (ZMod p) K
rw : Eq.{u_1 + 1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K)) ⊥
rw₁ : LE.le.{u_1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K)) ⊥
rw₂ :
  LE.le.{u_1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
    (map (K := ZMod p) (algebraMap (ZMod p) K) ⊥)
⊢ Eq.{u_1 + 1} (α := Subfield K) ⊥ (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
have rw₃ : LE.le.{u_1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
  (map (K := ZMod p) (algebraMap (ZMod p) K) ⊤)
Tactic: rw [eq_comm, eq_bot_iff, ← Subfield.map_bot (algebraMap (ZMod p) K),
    subsingleton_iff_bot_eq_top.mpr inferInstance, ← RingHom.fieldRange_eq_map]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimeField (goal)
Goal:
K : Type u_1
p : ℕ
hp : Fact (Nat.Prime p)
inst : Field K
inst_1 : Algebra (ZMod p) K
rw : Eq.{u_1 + 1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K)) ⊥
rw₁ : LE.le.{u_1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K)) ⊥
rw₂ :
  LE.le.{u_1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
    (map (K := ZMod p) (algebraMap (ZMod p) K) ⊥)
rw₃ :
  LE.le.{u_1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
    (map (K := ZMod p) (algebraMap (ZMod p) K) ⊤)
⊢ Eq.{u_1 + 1} (α := Subfield K) ⊥ (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
have rw₄ : LE.le.{u_1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
  (RingHom.fieldRange (K := ZMod p) (algebraMap (ZMod p) K))
Tactic: rw [eq_comm, eq_bot_iff, ← Subfield.map_bot (algebraMap (ZMod p) K),
    subsingleton_iff_bot_eq_top.mpr inferInstance, ← RingHom.fieldRange_eq_map]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Ring K
inst_4 : Algebra F K
e : K ≃ₐ[F] E
inst_5 : IsPurelyInseparable F K
x : E
⊢ IsIntegral F x
have rw : IsIntegral.{u_1, u_3} F (A := K) ((e.symm : (a : E) → K) x : K)
Tactic: rw [← isIntegral_algEquiv e.symm]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Ring K
inst_4 : Algebra F K
e : K ≃ₐ[F] E
inst_5 : IsPurelyInseparable F K
⊢ IsPurelyInseparable F E
have refine : ∀ (x : E) (h : IsSeparable F x), Membership.mem (γ := Subring E) (RingHom.range.{u_1, u_2} (R := F) (algebraMap F E)) x
Tactic: refine ⟨⟨fun _ ↦ by rw [← isIntegral_algEquiv e.symm]; exact IsPurelyInseparable.isIntegral' F _⟩,
    fun x h ↦ ?_⟩