awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Perfect
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
h :
  Function.Commute (α := S) (⇑(frobeniusEquiv S p) : (a : S) → S) (⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)
⊢ Function.Commute (α := S) (⇑(frobenius S p) : (a : S) → S) (⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)

Tactic:
rw [← coe_frobeniusEquiv]

Premises used: coe_frobeniusEquiv
-- Module: Mathlib.FieldTheory.Perfect
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) (⇑(frobeniusEquiv S p) : (a : S) → S) (⇑(RingEquiv.symm (frobeniusEquiv S p)) : (a : S) → S)

Tactic:
simp [Function.Commute, Function.Semiconj]

Premises used: Function.Commute, Function.Semiconj
-- Module: Mathlib.FieldTheory.Perfect
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
h :
  Function.Commute (α := R) (⇑(frobeniusEquiv R p) : (a : R) → R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)
⊢ Function.Commute (α := R) (⇑(frobenius R p) : (a : R) → R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)

Tactic:
rw [← coe_frobeniusEquiv]

Premises used: coe_frobeniusEquiv
-- Module: Mathlib.FieldTheory.Perfect
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) (⇑(frobeniusEquiv R p) : (a : R) → R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)

Tactic:
simp [Function.Commute, Function.Semiconj]

Premises used: Function.Commute, Function.Semiconj
-- Module: Mathlib.FieldTheory.Perfect
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
inj : Injective (α := S) (β := S) (⇑(frobeniusEquiv S p) : (a : S) → S)
⊢ Injective (α := S) (⇑(frobeniusEquiv S p) : (a : S) → S)^[n]

Tactic:
apply Function.Injective.iterate

Premises used: Function.Injective.iterate
-- Module: Mathlib.FieldTheory.Perfect
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) (β := S) (⇑(frobeniusEquiv S p) : (a : S) → S)

Tactic:
simp
-- Module: Mathlib.FieldTheory.Perfect
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)

Tactic:
MonoidHom.map_iterate_frobeniusEquiv_symm p (f.toMonoidHom) n x

Premises used: RingHom.toMonoidHom, MonoidHom.map_iterate_frobeniusEquiv_symm
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x y : R
h : x ^ p = y ^ p
⊢ x = y

Tactic:
(frobeniusEquiv R p).injective h

Premises used: frobeniusEquiv, RingEquiv.injective
-- Module: Mathlib.FieldTheory.Perfect
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])
rw₄ 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])
⊢ (expand R p : (a : R[X]) → R[X]) f =
    HPow.hPow (α := R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f) p

Tactic:
rw [← (f.map (S := R) (frobeniusEquiv R p).symm).map_frobenius_expand p, map_expand, map_map,
    frobenius_comp_frobeniusEquiv_symm, map_id]

Premises used: Polynomial.map_expand, Polynomial.map_id, frobenius_comp_frobeniusEquiv_symm, Polynomial.map, Polynomial.map_frobenius_expand, Polynomial.map_map
-- Module: Mathlib.FieldTheory.Perfect
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]
rw : ¬Irreducible (HPow.hPow (α := R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f) p)
⊢ ¬Irreducible (M := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])

Tactic:
rw [polynomial_expand_eq]

Premises used: polynomial_expand_eq
-- Module: Mathlib.FieldTheory.Perfect
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 (HPow.hPow (α := R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f) p)

Tactic:
not_irreducible_pow (Fact.out : p.Prime).ne_one

Premises used: not_irreducible_pow, Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.FieldTheory.Perfect
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 (HPow.hPow (α := R[X]) (map (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) f) p)

Tactic:
exact not_irreducible_pow (Fact.out : p.Prime).ne_one

Premises used: not_irreducible_pow, Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.FieldTheory.Perfect
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
prime : ∀ (hp : Nat.Prime p) [CharP K p], PerfectField K
⊢ PerfectField K

Tactic:
obtain hp | ⟨hp⟩ := ‹ExpChar K p›

Premises used: ExpChar
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : ExpChar K 1
inst_3 : PerfectRing K 1
⊢ PerfectField K

Tactic:
⟨Irreducible.separable⟩

Premises used: PerfectField.mk, Irreducible.separable
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : ExpChar K 1
inst_3 : PerfectRing K 1
⊢ PerfectField K

Tactic:
exact ⟨Irreducible.separable⟩
-- Module: Mathlib.FieldTheory.Perfect
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

Tactic:
PerfectField.mk fun hf ↦ ?_

Premises used: PerfectField.mk
-- Module: Mathlib.FieldTheory.Perfect
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
prime : ∀ {f : K[X]} (hf : Irreducible f), f.Separable
⊢ PerfectField K

Tactic:
refine PerfectField.mk fun hf ↦ ?_

Premises used: PerfectField.mk
-- Module: Mathlib.FieldTheory.Perfect
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
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)
⊢ f.Separable

Tactic:
rcases separable_or p hf with h | ⟨-, g, -, rfl⟩

Premises used: Polynomial.separable_or, rfl
-- Module: Mathlib.FieldTheory.Perfect
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
h : f.Separable
⊢ f.Separable

Tactic:
assumption
-- Module: Mathlib.FieldTheory.Perfect
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])
prime : False
⊢ Separable.{u_1} (R := K) ((expand K p : (a : K[X]) → K[X]) g)

Tactic:
exfalso
-- Module: Mathlib.FieldTheory.Perfect
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])
prime : ∀ (hf : Irreducible (M := K[X]) ((expand K p : (a : K[X]) → K[X]) g : K[X])), False
⊢ False

Tactic:
revert hf
-- Module: Mathlib.FieldTheory.Perfect
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]
⊢ Fact (Nat.Prime p)

Tactic:
haveI := Fact.mk hp
-- Module: Mathlib.FieldTheory.Perfect
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]
this : Fact (Nat.Prime p)
⊢ ∀ (hf : Irreducible (M := K[X]) ((expand K p : (a : K[X]) → K[X]) g : K[X])), False

Tactic:
simp
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
⊢ PerfectField K

Tactic:
⟨Irreducible.separable⟩

Premises used: PerfectField.mk, Irreducible.separable
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : Finite K
obtain : ∀ (p : ℕ) (_instP : CharP K p), PerfectField K
⊢ PerfectField K

Tactic:
obtain ⟨p, _instP⟩ := CharP.exists K

Premises used: CharP.exists
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : Finite K
p : ℕ
_instP : CharP K p
⊢ Fact (Nat.Prime p)

Tactic:
have : Fact p.Prime := ⟨CharP.char_is_prime K p⟩
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : Finite K
p : ℕ
_instP : CharP K p
this : Fact (Nat.Prime p)
⊢ PerfectField K

Tactic:
PerfectRing.toPerfectField K p

Premises used: PerfectRing.toPerfectField
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : Finite K
p : ℕ
_instP : CharP K p
this : Fact (Nat.Prime p)
⊢ PerfectField K

Tactic:
exact PerfectRing.toPerfectField K p

Premises used: PerfectRing.toPerfectField
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
p : ℕ
hp : ExpChar K p
⊢ PerfectRing K p

Tactic:
PerfectRing.ofSurjective _ _ fun y ↦ ?_

Premises used: PerfectRing.ofSurjective
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
p : ℕ
hp : ExpChar K p
refine : ∀ (y : K), ∃ (a : K), (frobenius K p : (a : K) → K) a = y
⊢ PerfectRing K p

Tactic:
refine PerfectRing.ofSurjective _ _ fun y ↦ ?_

Premises used: PerfectRing.ofSurjective
-- Module: Mathlib.FieldTheory.Perfect
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
prime : ∀ (hp : Nat.Prime p) [hchar : CharP K p], ∃ (a : K), (frobenius K p : (a : K) → K) a = y
⊢ ∃ (a : K), (frobenius K p : (a : K) → K) a = y

Tactic:
rcases hp with _ | hp
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
y : K
inst_2 : CharZero K
⊢ ∃ (a : K), (frobenius K 1 : (a : K) → K) a = y

Tactic:
simp [frobenius]

Premises used: frobenius
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
p : ℕ
y : K
hp : Nat.Prime p
hchar : CharP K p
prime : ¬∀ (x : K), ¬(frobenius K p : (a : K) → K) x = y
⊢ ∃ (a : K), (frobenius K p : (a : K) → K) a = y

Tactic:
rw [← not_forall_not]

Premises used: not_forall_not
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
p : ℕ
y : K
hp : Nat.Prime p
hchar : CharP K p
prime : ¬Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) y : K[X]))
⊢ ¬∀ (x : K), ¬(frobenius K p : (a : K) → K) x = y

Tactic:
apply mt (X_pow_sub_C_irreducible_of_prime hp)

Premises used: mt, X_pow_sub_C_irreducible_of_prime
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
p : ℕ
y : K
hp : Nat.Prime p
hchar : CharP K p
prime : ¬(HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) y : K[X])).Separable
⊢ ¬Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) y : K[X]))

Tactic:
apply mt separable_of_irreducible

Premises used: PerfectField.separable_of_irreducible, mt
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
p : ℕ
y : K
hp : Nat.Prime p
hchar : CharP K p
⊢ ¬(HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) y : K[X])).Separable

Tactic:
simp [separable_def, isCoprime_zero_right, isUnit_iff_degree_eq_zero,
    derivative_X_pow, degree_X_pow_sub_C hp.pos, hp.ne_zero]

Premises used: Nat.Prime.pos, Polynomial.degree_X_pow_sub_C, Polynomial.separable_def, Polynomial.derivative_X_pow, Nat.Prime.ne_zero, Polynomial.isUnit_iff_degree_eq_zero, isCoprime_zero_right
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
g : K[X]
⊢ g.Separable ↔ Squarefree g

Tactic:
⟨Separable.squarefree, fun sqf ↦ isCoprime_of_irreducible_dvd (sqf.ne_zero ·.1) ?_⟩

Premises used: isCoprime_of_irreducible_dvd, And.left, Squarefree.ne_zero, Iff.intro, Polynomial.Separable.squarefree
-- Module: Mathlib.FieldTheory.Perfect
Goal:
K : Type u_1
inst : Field K
inst_1 : PerfectField K
g : K[X]
refine : ∀ (sqf : Squarefree g) (z : K[X]), Irreducible z → z ∣ g → ¬z ∣ (derivative : (a : K[X]) → K[X]) g
⊢ g.Separable ↔ Squarefree g

Tactic:
refine ⟨Separable.squarefree, fun sqf ↦ isCoprime_of_irreducible_dvd (sqf.ne_zero ·.1) ?_⟩
-- Module: Mathlib.FieldTheory.Perfect
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 ∣ 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

Premises used: Polynomial.derivative_mul, dvd_add_left, dvd_mul_right
-- Module: Mathlib.FieldTheory.Perfect
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 ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) p : K[X]) q
⊢ p ∣ q

Tactic:
(separable_of_irreducible h).dvd_of_dvd_mul_left dvd

Premises used: PerfectField.separable_of_irreducible, IsCoprime.dvd_of_dvd_mul_left
-- Module: Mathlib.FieldTheory.Perfect
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 ∣ HMul.hMul (α := K[X]) ((derivative : (a : K[X]) → K[X]) p : K[X]) q
⊢ p ∣ q

Tactic:
exact (separable_of_irreducible h).dvd_of_dvd_mul_left dvd

Premises used: PerfectField.separable_of_irreducible, IsCoprime.dvd_of_dvd_mul_left
-- Module: Mathlib.FieldTheory.Perfect
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

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
-- Module: Mathlib.FieldTheory.Perfect
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 ∣ q
⊢ False

Tactic:
(h.1 : ¬ IsUnit p) (sqf _ <| mul_dvd_mul_left _ dvd)

Premises used: Irreducible.not_isUnit, mul_dvd_mul_left
-- Module: Mathlib.FieldTheory.Perfect
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 ∣ q
⊢ False

Tactic:
exact (h.1 : ¬ IsUnit p) (sqf _ <| mul_dvd_mul_left _ dvd)

Premises used: Irreducible.not_isUnit, mul_dvd_mul_left
-- Module: Mathlib.FieldTheory.Perfect
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
⊢ Algebra.IsSeparable K L

Tactic:
⟨fun x ↦ PerfectField.separable_of_irreducible <|
    minpoly.irreducible (Algebra.IsIntegral.isIntegral x)⟩

Premises used: Algebra.IsIntegral.isIntegral, PerfectField.separable_of_irreducible, minpoly.irreducible, Algebra.IsSeparable.mk
-- Module: Mathlib.FieldTheory.Perfect
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
obtain : ∀ (w : K[X]), w.Monic → ∀ (hi : Irreducible w) (h : f ∣ map (algebraMap K L) w), f.Separable
⊢ f.Separable

Tactic:
obtain ⟨_, _, hi, h⟩ := hf.exists_dvd_monic_irreducible_of_isIntegral (K := K)

Premises used: Irreducible.exists_dvd_monic_irreducible_of_isIntegral
-- Module: Mathlib.FieldTheory.Perfect
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
w : K[X]
left : w.Monic
hi : Irreducible w
h : f ∣ map (algebraMap K L) w
⊢ f.Separable

Tactic:
(PerfectField.separable_of_irreducible hi).map |>.of_dvd h

Premises used: PerfectField.separable_of_irreducible, Polynomial.Separable.map, Polynomial.Separable.of_dvd
-- Module: Mathlib.FieldTheory.Perfect
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
w : K[X]
left : w.Monic
hi : Irreducible w
h : f ∣ map (algebraMap K L) w
⊢ f.Separable

Tactic:
exact (PerfectField.separable_of_irreducible hi).map |>.of_dvd h

Premises used: PerfectField.separable_of_irreducible, Polynomial.Separable.map, Polynomial.Separable.of_dvd
-- Module: Mathlib.FieldTheory.Perfect
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

Tactic:
le_iff_count.2 fun r ↦ ?_

Premises used: Iff.mpr, Multiset.le_iff_count
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
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)
⊢ 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

Tactic:
refine le_iff_count.2 fun r ↦ ?_

Premises used: Iff.mpr, Multiset.le_iff_count
-- Module: Mathlib.FieldTheory.Perfect
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)
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)
⊢ 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
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
r : R
h : ∃ (s : R), r = s ^ p ^ n
pos :
  ∀ (s : R),
    count (s ^ p ^ n)
        (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
          (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
      count (s ^ p ^ n) (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)

Tactic:
obtain ⟨s, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
s : R
pos :
  card.{u_1} (α := R)
      (filter (fun (a : R) ↦ s ^ p ^ n = (iterateFrobenius R p n : (a : R) → R) a)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    card.{u_1} (α := R) (filter (fun (x : R) ↦ s = x) (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)))
⊢ count (s ^ p ^ n)
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    count (s ^ p ^ n) (p ^ n • f.roots)

Tactic:
simp_rw [count_nsmul, count_roots, ← rootMultiplicity_expand_pow, ← count_roots, count_map,
      count_eq_card_filter_eq]

Premises used: Polynomial.rootMultiplicity_expand_pow, Multiset.count_eq_card_filter_eq, Polynomial.count_roots, Multiset.count_nsmul, Multiset.count_map
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
s : R
⊢ card.{u_1} (α := R)
      (filter (fun (a : R) ↦ s ^ p ^ n = (iterateFrobenius R p n : (a : R) → R) a)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    card.{u_1} (α := R) (filter (fun (x : R) ↦ s = x) (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)))

Tactic:
card_le_card (monotone_filter_right _ fun _ h ↦ iterateFrobenius_inj R p n h)

Premises used: Multiset.card_le_card, Multiset.monotone_filter_right, iterateFrobenius_inj
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
s : R
⊢ card.{u_1} (α := R)
      (filter (fun (a : R) ↦ s ^ p ^ n = (iterateFrobenius R p n : (a : R) → R) a)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) ≤
    card.{u_1} (α := R) (filter (fun (x : R) ↦ s = x) (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)))

Tactic:
exact card_le_card (monotone_filter_right _ fun _ h ↦ iterateFrobenius_inj R p n h)

Premises used: Multiset.card_le_card, Multiset.monotone_filter_right, iterateFrobenius_inj
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
r : R
h : ¬∃ (s : R), r = s ^ p ^ n
⊢ 0 ≤ count r (p ^ n • f.roots)

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
r : R
h : ¬∃ (s : R), r = s ^ p ^ n
h₁ :
  count r
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) =
    0
⊢ 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:
convert! Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.FieldTheory.Perfect
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p n : ℕ
inst_2 : ExpChar R p
f : R[X]
r : R
h : ¬∃ (s : R), r = s ^ p ^ n
h₁ :
  Eq.{u_1 + 1} (α := Multiset R)
    (filter (fun (a : R) ↦ r = (iterateFrobenius R p n : (a : R) → R) a)
      (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f)))
    0
⊢ count r
      (Multiset.map (α := R) (⇑(iterateFrobenius R p n) : (a : R) → R)
        (roots ((expand R (p ^ n) : (a : R[X]) → R[X]) f))) =
    0

Tactic:
simp_rw [count_map, card_eq_zero]

Premises used: Multiset.card_eq_zero, Multiset.count_map