awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
x : R
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) x : R) : S)
    ((RingEquiv.symm (frobeniusEquiv S p) : (a : S) → S) ((f : (a : R) → S) x : S) : S)
have apply_fun : Eq (α := S)
  ((frobeniusEquiv S p : (a : S) → S)
      ((f : (a : R) → S) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) x : R) : S) :
    S)
  ((frobeniusEquiv S p : (a : S) → S)
      ((RingEquiv.symm (frobeniusEquiv S p) : (a : S) → S) ((f : (a : R) → S) x : S) : S) :
    S)
Tactic: apply_fun (frobeniusEquiv S p)
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →+* S
x : R
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) x : R) : S)
    ((RingEquiv.symm (frobeniusEquiv S p) : (a : S) → S) ((f : (a : R) → S) x : S) : S)
have apply_fun : Eq (α := S)
  ((frobeniusEquiv S p : (a : S) → S)
      ((f : (a : R) → S) ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R) x : R) : S) :
    S)
  ((frobeniusEquiv S p : (a : S) → S)
      ((RingEquiv.symm (frobeniusEquiv S p) : (a : S) → S) ((f : (a : R) → S) x : S) : S) :
    S)
Tactic: apply_fun (frobeniusEquiv S p)
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
n : ℕ
x : R
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x) : S)
    ((⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)^[n] ((f : (a : R) → S) x) : S)
have apply_fun : Eq (α := S)
  ((⇑(frobeniusEquiv S p) : (a : S) → S)^[n]
      ((f : (a : R) → S) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x)) :
    S)
  ((⇑(frobeniusEquiv S p) : (a : S) → S)^[n]
      ((⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)^[n] ((f : (a : R) → S) x)) :
    S)
Tactic: apply_fun (frobeniusEquiv S p)^[n]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
n : ℕ
x : R
apply_fun :
  Eq (α := S)
    ((⇑(frobeniusEquiv S p) : (a : S) → S)^[n]
        ((f : (a : R) → S) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x)) :
      S)
    ((⇑(frobeniusEquiv S p) : (a : S) → S)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)^[n] ((f : (a : R) → S) x)) :
      S)
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x) : S)
    ((⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)^[n] ((f : (a : R) → S) x) : S)
have inj : Injective (α := S) (⇑(frobeniusEquiv S p) : (a : S) → S)^[n]
Tactic: apply_fun (frobeniusEquiv S p)^[n]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
n : ℕ
x : R
⊢ Eq (α := S)
    ((⇑(frobeniusEquiv S p) : (a : S) → S)^[n]
        ((f : (a : R) → S) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x)) :
      S)
    ((⇑(frobeniusEquiv S p) : (a : S) → S)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)^[n] ((f : (a : R) → S) x)) :
      S)
have simp : Eq.{u_3 + 1} (α := S)
  ((f : (a : R) → S)
      ((⇑(frobenius R p) : (a : R) → R)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x)) :
    S)
  ((⇑(frobenius S p) : (a : S) → S)^[n]
      ((⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)^[n] ((f : (a : R) → S) x)) :
    S)
Tactic: simp only [coe_frobeniusEquiv, ← map_iterate_frobenius]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
n : ℕ
x : R
⊢ Eq.{u_3 + 1} (α := S)
    ((f : (a : R) → S)
        ((⇑(frobenius R p) : (a : R) → R)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x)) :
      S)
    ((⇑(frobenius S p) : (a : S) → S)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)^[n] ((f : (a : R) → S) x)) :
      S)
have rw : Eq.{u_3 + 1} (α := S)
  ((f : (a : R) → S)
      ((Function.comp (β := R) (⇑(frobenius R p) : (a : R) → R)
            (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R))^[n]
        x) :
    S)
  ((Function.comp (β := S) (⇑(frobenius S p) : (a : S) → S) (⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S))^[n]
      ((f : (a : R) → S) x) :
    S)
Tactic: rw [← Function.comp_apply (f := (⇑(frobenius R p))^[n]),
          ← Function.comp_apply (f := (⇑(frobenius S p))^[n]),
          ← Function.Commute.comp_iterate, ← Function.Commute.comp_iterate]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
n : ℕ
x : R
rw :
  Eq.{u_3 + 1} (α := S)
    ((f : (a : R) → S)
        ((Function.comp (β := R) (⇑(frobenius R p) : (a : R) → R)
              (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R))^[n]
          x) :
      S)
    ((Function.comp (β := S) (⇑(frobenius S p) : (a : S) → S)
            (⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S))^[n]
        ((f : (a : R) → S) x) :
      S)
⊢ Eq.{u_3 + 1} (α := S)
    ((f : (a : R) → S)
        ((⇑(frobenius R p) : (a : R) → R)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x)) :
      S)
    ((⇑(frobenius S p) : (a : S) → S)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)^[n] ((f : (a : R) → S) x)) :
      S)
have h : Function.Commute (α := S) (⇑(frobenius S p) : (a : S) → S) (⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)
Tactic: rw [← Function.comp_apply (f := (⇑(frobenius R p))^[n]),
          ← Function.comp_apply (f := (⇑(frobenius S p))^[n]),
          ← Function.Commute.comp_iterate, ← Function.Commute.comp_iterate]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
n : ℕ
x : R
rw :
  Eq.{u_3 + 1} (α := S)
    ((f : (a : R) → S)
        ((Function.comp (β := R) (⇑(frobenius R p) : (a : R) → R)
              (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R))^[n]
          x) :
      S)
    ((Function.comp (β := S) (⇑(frobenius S p) : (a : S) → S)
            (⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S))^[n]
        ((f : (a : R) → S) x) :
      S)
h : Function.Commute (α := S) (⇑(frobenius S p) : (a : S) → S) (⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)
⊢ Eq.{u_3 + 1} (α := S)
    ((f : (a : R) → S)
        ((⇑(frobenius R p) : (a : R) → R)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x)) :
      S)
    ((⇑(frobenius S p) : (a : S) → S)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)^[n] ((f : (a : R) → S) x)) :
      S)
have h₁ : Function.Commute (α := R) (⇑(frobenius R p) : (a : R) → R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)
Tactic: rw [← Function.comp_apply (f := (⇑(frobenius R p))^[n]),
          ← Function.comp_apply (f := (⇑(frobenius S p))^[n]),
          ← Function.Commute.comp_iterate, ← Function.Commute.comp_iterate]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
n : ℕ
x : R
⊢ Function.Commute (α := S) (⇑(frobenius S p) : (a : S) → S) (⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)
have h : Function.Commute (α := S) (⇑(frobeniusEquiv S p) : (a : S) → S) (⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)
Tactic: rw [← coe_frobeniusEquiv]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
n : ℕ
x : R
⊢ Function.Commute (α := R) (⇑(frobenius R p) : (a : R) → R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)
have h : Function.Commute (α := R) (⇑(frobeniusEquiv R p) : (a : R) → R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)
Tactic: rw [← coe_frobeniusEquiv]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
p : ℕ
inst_2 : ExpChar R p
inst_3 : PerfectRing R p
inst_4 : ExpChar S p
inst_5 : PerfectRing S p
f : R →* S
n : ℕ
x : R
⊢ Injective (α := S) (⇑(frobeniusEquiv S p) : (a : S) → S)^[n]
have inj : Injective (α := S) (β := S) (⇑(frobeniusEquiv S p) : (a : S) → S)
Tactic: apply Function.Injective.iterate
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
f : R[X]
⊢ (expand R p : (a : R[X]) → R[X]) f =
    HPow.hPow (α := R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f) p
have rw : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
  (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f)) :
    R[X])
Tactic: rw [← (f.map (S := R) (frobeniusEquiv R p).symm).map_frobenius_expand p, map_expand, map_map,
    frobenius_comp_frobeniusEquiv_symm, map_id]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
f : R[X]
rw :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f)) :
      R[X])
⊢ (expand R p : (a : R[X]) → R[X]) f =
    HPow.hPow (α := R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f) p
have rw₁ : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
  ((expand R p : (a : R[X]) → R[X]) (map (frobenius R p) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f)) :
    R[X])
Tactic: rw [← (f.map (S := R) (frobeniusEquiv R p).symm).map_frobenius_expand p, map_expand, map_map,
    frobenius_comp_frobeniusEquiv_symm, map_id]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
f : R[X]
rw :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f)) :
      R[X])
rw₁ :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X]) (map (frobenius R p) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f)) :
      R[X])
⊢ (expand R p : (a : R[X]) → R[X]) f =
    HPow.hPow (α := R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f) p
have rw₂ : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
  ((expand R p : (a : R[X]) → R[X])
      (map (RingHom.comp (frobenius R p) (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R)) f) :
    R[X])
Tactic: rw [← (f.map (S := R) (frobeniusEquiv R p).symm).map_frobenius_expand p, map_expand, map_map,
    frobenius_comp_frobeniusEquiv_symm, map_id]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
f : R[X]
rw :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f)) :
      R[X])
rw₁ :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X]) (map (frobenius R p) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f)) :
      R[X])
rw₂ :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X])
        (map (RingHom.comp (frobenius R p) (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R)) f) :
      R[X])
⊢ (expand R p : (a : R[X]) → R[X]) f =
    HPow.hPow (α := R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f) p
have rw₃ : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
  ((expand R p : (a : R[X]) → R[X]) (map (RingHom.id R) f) : R[X])
Tactic: rw [← (f.map (S := R) (frobeniusEquiv R p).symm).map_frobenius_expand p, map_expand, map_map,
    frobenius_comp_frobeniusEquiv_symm, map_id]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
f : R[X]
rw :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f)) :
      R[X])
rw₁ :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X]) (map (frobenius R p) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f)) :
      R[X])
rw₂ :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X])
        (map (RingHom.comp (frobenius R p) (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R)) f) :
      R[X])
rw₃ :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X]) (map (RingHom.id R) f) : R[X])
⊢ (expand R p : (a : R[X]) → R[X]) f =
    HPow.hPow (α := R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f) p
have rw₄ : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
Tactic: rw [← (f.map (S := R) (frobeniusEquiv R p).symm).map_frobenius_expand p, map_expand, map_map,
    frobenius_comp_frobeniusEquiv_symm, map_id]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_2
p : ℕ
inst : CommSemiring R
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP R p
inst_3 : PerfectRing R p
f : R[X]
⊢ ¬Irreducible (M := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
have rw : ¬Irreducible (HPow.hPow (α := R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f) p)
Tactic: rw [polynomial_expand_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
p : ℕ
inst : Field K
inst_1 : ExpChar K p
inst_2 : PerfectRing K p
⊢ PerfectField K
have zero : ∀ [CharZero K] [ExpChar K 1] [PerfectRing K 1], PerfectField K
Tactic: obtain hp | ⟨hp⟩ := ‹ExpChar K p›
Cleared hypotheses: p, inst_1, inst_2
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
p : ℕ
inst : Field K
inst_1 : ExpChar K p
inst_2 : PerfectRing K p
zero : ∀ [CharZero K] [ExpChar K 1] [PerfectRing K 1], PerfectField K
⊢ PerfectField K
have prime : ∀ (hp : Nat.Prime p) [CharP K p], PerfectField K
Tactic: obtain hp | ⟨hp⟩ := ‹ExpChar K p›
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
p : ℕ
inst : Field K
inst_1 : ExpChar K p
inst_2 : PerfectRing K p
hp : Nat.Prime p
hchar : CharP K p
⊢ PerfectField K
have prime : ∀ {f : K[X]} (hf : Irreducible f), f.Separable
Tactic: refine PerfectField.mk fun hf ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
p : ℕ
inst : Field K
inst_1 : ExpChar K p
inst_2 : PerfectRing K p
hp : Nat.Prime p
hchar : CharP K p
f : K[X]
hf : Irreducible f
⊢ f.Separable
have prime : ∀ (h : f.Separable), f.Separable
Tactic: rcases separable_or p hf with h | ⟨-, g, -, rfl⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
p : ℕ
inst : Field K
inst_1 : ExpChar K p
inst_2 : PerfectRing K p
hp : Nat.Prime p
hchar : CharP K p
f : K[X]
hf : Irreducible f
prime : ∀ (h : f.Separable), f.Separable
⊢ f.Separable
have prime₁ : ∀ (g : K[X]) (hf : Irreducible (M := K[X]) ((expand K p : (a : K[X]) → K[X]) g : K[X])),
  Separable.{u_1} (R := K) ((expand K p : (a : K[X]) → K[X]) g)
Tactic: rcases separable_or p hf with h | ⟨-, g, -, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
p : ℕ
inst : Field K
inst_1 : ExpChar K p
inst_2 : PerfectRing K p
hp : Nat.Prime p
hchar : CharP K p
g : K[X]
hf : Irreducible (M := K[X]) ((expand K p : (a : K[X]) → K[X]) g : K[X])
⊢ Separable.{u_1} (R := K) ((expand K p : (a : K[X]) → K[X]) g)
have prime : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
p : ℕ
inst : Field K
inst_1 : ExpChar K p
inst_2 : PerfectRing K p
hp : Nat.Prime p
hchar : CharP K p
g : K[X]
hf : Irreducible (M := K[X]) ((expand K p : (a : K[X]) → K[X]) g : K[X])
⊢ False
have prime : ∀ (hf : Irreducible (M := K[X]) ((expand K p : (a : K[X]) → K[X]) g : K[X])), False
Tactic: revert hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (hypothesis)
Goal:
K : Type u_1
p : ℕ
inst : Field K
inst_1 : ExpChar K p
inst_2 : PerfectRing K p
hp : Nat.Prime p
hchar : CharP K p
g : K[X]
⊢ ∀ (hf : Irreducible (M := K[X]) ((expand K p : (a : K[X]) → K[X]) g : K[X])), False
have this : Fact (Nat.Prime p)
Tactic: haveI := Fact.mk hp
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Finite K
⊢ PerfectField K
have obtain : ∀ (p : ℕ) (_instP : CharP K p), PerfectField K
Tactic: obtain ⟨p, _instP⟩ := CharP.exists K
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Finite K
p : ℕ
_instP : CharP K p
⊢ PerfectField K
have this : Fact (Nat.Prime p)
Tactic: have : Fact p.Prime := ⟨CharP.char_is_prime K p⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
p : ℕ
hp : ExpChar K p
⊢ PerfectRing K p
have refine : ∀ (y : K), ∃ (a : K), (frobenius K p : (a : K) → K) a = y
Tactic: refine PerfectRing.ofSurjective _ _ fun y ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
p : ℕ
hp : ExpChar K p
y : K
⊢ ∃ (a : K), (frobenius K p : (a : K) → K) a = y
have zero : ∀ [inst_2 : CharZero K], ∃ (a : K), (frobenius K 1 : (a : K) → K) a = y
Tactic: rcases hp with _ | hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
p : ℕ
hp : ExpChar K p
y : K
zero : ∀ [inst_2 : CharZero K], ∃ (a : K), (frobenius K 1 : (a : K) → K) a = y
⊢ ∃ (a : K), (frobenius K p : (a : K) → K) a = y
have prime : ∀ (hp : Nat.Prime p) [hchar : CharP K p], ∃ (a : K), (frobenius K p : (a : K) → K) a = y
Tactic: rcases hp with _ | hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
p : ℕ
y : K
hp : Nat.Prime p
hchar : CharP K p
⊢ ∃ (a : K), (frobenius K p : (a : K) → K) a = y
have prime : ¬∀ (x : K), ¬(frobenius K p : (a : K) → K) x = y
Tactic: rw [← not_forall_not]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
p : ℕ
y : K
hp : Nat.Prime p
hchar : CharP K p
⊢ ¬∀ (x : K), ¬(frobenius K p : (a : K) → K) x = y
have prime : ¬Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) y : K[X]))
Tactic: apply mt (X_pow_sub_C_irreducible_of_prime hp)
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
p : ℕ
y : K
hp : Nat.Prime p
hchar : CharP K p
⊢ ¬Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) y : K[X]))
have prime : ¬(HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) y : K[X])).Separable
Tactic: apply mt separable_of_irreducible
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
g : K[X]
⊢ g.Separable ↔ Squarefree g
have refine : ∀ (sqf : Squarefree g) (z : K[X]), Irreducible z → z ∣ g → ¬z ∣ (derivative : (a : K[X]) → K[X]) g
Tactic: refine ⟨Separable.squarefree, fun sqf ↦ isCoprime_of_irreducible_dvd (sqf.ne_zero ·.1) ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
p : K[X]
h : Irreducible p
q : K[X]
sqf : Squarefree (p * q)
dvd : p ∣ (derivative : (a : K[X]) → K[X]) (p * q)
⊢ p ∣ q
have dvd₁ : p ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) p : K[X]) q
Tactic: rw [derivative_mul, dvd_add_left (dvd_mul_right p _)] at dvd
Cleared hypotheses: dvd
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
p : K[X]
h : Irreducible p
q : K[X]
sqf : Squarefree (p * q)
dvd : p ∣ (derivative : (a : K[X]) → K[X]) (p * q)
⊢ False
have dvd₁ : p ∣ q
Tactic: replace dvd : p ∣ q := by
    rw [derivative_mul, dvd_add_left (dvd_mul_right p _)] at dvd
    exact (separable_of_irreducible h).dvd_of_dvd_mul_left dvd
Cleared hypotheses: dvd
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
inst_4 : PerfectField K
f : L[X]
hf : Irreducible f
⊢ f.Separable
have obtain : ∀ (w : K[X]), w.Monic → ∀ (hi : Irreducible w) (h : f ∣ map (algebraMap K L) w), f.Separable
Tactic: obtain ⟨_, _, hi, h⟩ := hf.exists_dvd_monic_irreducible_of_isIntegral (K := K)
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
⊢ Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R) (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)) ≤
    p ^ n • f.roots
have refine : ∀ (r : R),
  count r
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    count r (p ^ n • f.roots)
Tactic: refine le_iff_count.2 fun r ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
r : R
⊢ count r
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    count r (p ^ n • f.roots)
have pos : ∀ (h : ∃ (s : R), r = s ^ p ^ n),
  count r
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    count r (p ^ n • f.roots)
Tactic: by_cases h : ∃ s, r = s ^ p ^ n
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
r : R
pos :
  ∀ (h : ∃ (s : R), r = s ^ p ^ n),
    count r
        (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
          (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
      count r (p ^ n • f.roots)
⊢ count r
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    count r (p ^ n • f.roots)
have neg : ∀ (h : ¬∃ (s : R), r = s ^ p ^ n),
  count r
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    count r (p ^ n • f.roots)
Tactic: by_cases h : ∃ s, r = s ^ p ^ n