awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
f : F[X]
hf : Irreducible f
h : Ne (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
g : F[X]
hg1 : Membership.mem (γ := Set F[X]) (nonunits F[X]) g
_hg2 : g ≠ 0
h_1 : g ∣ f
hg4 : g ∣ (derivative : (a : F[X]) → F[X]) f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : (↑u : F[X]) = p
rwa rwa₁ rwa₂ rwa₃ : g ∣ (derivative : (a : F[X]) → F[X]) f
⊢ g * (↑u : F[X]) ∣ (derivative : (a : F[X]) → F[X]) f

Tactic:
rwa [Units.mul_right_dvd]

Premises used: Units.mul_right_dvd
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
S : Type u_1
inst_1 : CommRing S
inst_2 : Nontrivial S
f : F →+* S
p : F[X]
⊢ (map f p).Separable ↔ p.Separable

Tactic:
⟨fun H ↦ ?_, fun H ↦ H.map⟩

Premises used: Polynomial.Separable.map, Iff.intro
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
S : Type u_1
inst_1 : CommRing S
inst_2 : Nontrivial S
f : F →+* S
p : F[X]
refine : ∀ (H : (map f p).Separable), p.Separable
⊢ (map f p).Separable ↔ p.Separable

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H.map⟩
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
S : Type u_1
inst_1 : CommRing S
inst_2 : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
obtain : ∀ (m : Ideal S) (hm : m.IsMaximal), p.Separable
⊢ p.Separable

Tactic:
obtain ⟨m, hm⟩ := Ideal.exists_maximal S

Premises used: Ideal.exists_maximal
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
S : Type u_1
inst_1 : CommRing S
inst_2 : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
⊢ (map (Ideal.Quotient.mk m) (map f p)).Separable

Tactic:
have := Separable.map H (f := Ideal.Quotient.mk m)
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
S : Type u_1
inst_1 : CommRing S
inst_2 : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : (map (Ideal.Quotient.mk m) (map f p)).Separable
rwa : ∀ (this : (map (RingHom.comp (Ideal.Quotient.mk m) f) p).Separable), p.Separable
rwa₁ :
  ∀
    (this :
      IsCoprime (map (RingHom.comp (Ideal.Quotient.mk m) f) p)
        ((derivative : (a : (S ⧸ m)[X]) → (S ⧸ m)[X]) (map (RingHom.comp (Ideal.Quotient.mk m) f) p))),
    p.Separable
rwa₂ :
  ∀
    (this :
      IsCoprime (map (RingHom.comp (Ideal.Quotient.mk m) f) p)
        (map (RingHom.comp (Ideal.Quotient.mk m) f) ((derivative : (a : F[X]) → F[X]) p))),
    p.Separable
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : IsCoprime p ((derivative : (a : F[X]) → F[X]) p)), p.Separable
⊢ p.Separable

Tactic:
rwa [map_map, separable_def, derivative_map, isCoprime_map] at this

Premises used: Polynomial.separable_def, Polynomial.isCoprime_map, Polynomial.derivative_map, Polynomial.map_map
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
ι : Type u_1
f : ι → F
s : Finset ι
H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
rw :
  Separable.{u} (R := F)
    (∏ x ∈ s.attach, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (f (↑x : ι)) : F[X]))
⊢ Separable.{u} (R := F) (∏ i ∈ s, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (f i) : F[X]))

Tactic:
rw [← prod_attach]

Premises used: Finset.prod_attach
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
ι : Type u_1
f : ι → F
s : Finset ι
H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
⊢ Separable.{u} (R := F)
    (∏ x ∈ s.attach, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (f (↑x : ι)) : F[X]))

Tactic:
separable_prod'
        (fun x _hx y _hy hxy =>
          @pairwise_coprime_X_sub_C _ _ { x // x ∈ s } (fun x => f x)
            (fun x y hxy => Subtype.ext <| H x.1 x.2 y.1 y.2 hxy) _ _ hxy)
        fun _ _ => separable_X_sub_C

Premises used: Polynomial.separable_prod', Polynomial.separable_X_sub_C, Subtype.val, Polynomial.pairwise_coprime_X_sub_C, Subtype.property, Subtype.ext
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
ι : Type u_1
f : ι → F
s : Finset ι
H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
⊢ Separable.{u} (R := F)
    (∏ x ∈ s.attach, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (f (↑x : ι)) : F[X]))

Tactic:
exact
      separable_prod'
        (fun x _hx y _hy hxy =>
          @pairwise_coprime_X_sub_C _ _ { x // x ∈ s } (fun x => f x)
            (fun x y hxy => Subtype.ext <| H x.1 x.2 y.1 y.2 hxy) _ _ hxy)
        fun _ _ => separable_X_sub_C

Premises used: Polynomial.separable_prod', Polynomial.separable_X_sub_C, Subtype.val, Polynomial.pairwise_coprime_X_sub_C, Subtype.property, Subtype.ext
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
ι : Type u_1
inst_1 : Fintype ι
f : ι → F
simp_rw : (∀ (x : ι), True → ∀ (y : ι), True → f x = f y → x = y) ↔ Function.Injective f
simp_rw₁ : (∀ (x y : ι), f x = f y → x = y) ↔ Function.Injective f
⊢ (∀ (x : ι),
      Membership.mem (γ := Finset ι) univ x → ∀ (y : ι), Membership.mem (γ := Finset ι) univ y → f x = f y → x = y) ↔
    Function.Injective f

Tactic:
simp_rw [mem_univ, true_imp_iff, Function.Injective]

Premises used: Finset.mem_univ, true_imp_iff, Function.Injective
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
inl :
  ∀ [HF : CharP F 0], f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F 0 : (a : F[X]) → F[X]) g = f
inr : ∀ (hp : p > 0), f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F p : (a : F[X]) → F[X]) g = f
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F p : (a : F[X]) → F[X]) g = f

Tactic:
rcases p.eq_zero_or_pos with (rfl | hp)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
HF : CharP F 0
⊢ CharZero F

Tactic:
haveI := CharP.charP_to_charZero F
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
HF : CharP F 0
this : CharZero F
⊢ f.natDegree = 0

Tactic:
have := natDegree_eq_zero_of_derivative_eq_zero H
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
HF : CharP F 0
this_1 : CharZero F
this : f.natDegree = 0
⊢ f.natDegree ≠ 0

Tactic:
have := (natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_irreducible hf).ne'
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
HF : CharP F 0
this_1 : CharZero F
this_2 : f.natDegree = 0
this : f.natDegree ≠ 0
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F 0 : (a : F[X]) → F[X]) g = f

Tactic:
contradiction
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
hp : p > 0
⊢ IsLocalHom (R := F[X]) (S := F[X]) (F := F[X] →ₐ[F] F[X]) (expand F p)

Tactic:
haveI := isLocalHom_expand F hp
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
hp : p > 0
this : IsLocalHom (R := F[X]) (S := F[X]) (F := F[X] →ₐ[F] F[X]) (expand F p)
rw : ¬Ne (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
rw₁ : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
rw₂ rw₃ : Eq.{u + 1} (α := F[X]) 0 0
⊢ ¬f.Separable

Tactic:
rw [separable_iff_derivative_ne_zero hf, Classical.not_not, H]

Premises used: Classical.not_not, Polynomial.separable_iff_derivative_ne_zero
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
hp : p > 0
this : IsLocalHom (R := F[X]) (S := F[X]) (F := F[X] →ₐ[F] F[X]) (expand F p)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hf : Irreducible (M := F[X]) ((expand F p : (a : F[X]) → F[X]) (contract p f) : F[X]))
    (H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])) (hp : p > 0)
    (this : IsLocalHom (R := F[X]) (S := F[X]) (F := F[X] →ₐ[F] F[X]) (expand F p)),
    Irreducible (M := F[X]) ((expand F p : (a : F[X]) → F[X]) (contract p f) : F[X])
⊢ Irreducible (M := F[X]) ((expand F p : (a : F[X]) → F[X]) (contract p f) : F[X])

Tactic:
rwa [← expand_contract p H hp.ne'] at hf

Premises used: Polynomial.expand_contract, LT.lt.ne'
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
hp : p > 0
this : IsLocalHom (R := F[X]) (S := F[X]) (F := F[X] →ₐ[F] F[X]) (expand F p)
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F p : (a : F[X]) → F[X]) g = f

Tactic:
exact
      Or.inr
        ⟨by rw [separable_iff_derivative_ne_zero hf, Classical.not_not, H], contract p f,
          Irreducible.of_map (by rwa [← expand_contract p H hp.ne'] at hf),
          expand_contract p H hp.ne'⟩

Premises used: Or.inr
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F p : (a : F[X]) → F[X]) g = f

Tactic:
exact if H : derivative f = 0 then by
    rcases p.eq_zero_or_pos with (rfl | hp)
    · haveI := CharP.charP_to_charZero F
      have := natDegree_eq_zero_of_derivative_eq_zero H
      have := (natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_irreducible hf).ne'
      contradiction
    haveI := isLocalHom_expand F hp
    exact
      Or.inr
        ⟨by rw [separable_iff_derivative_ne_zero hf, Classical.not_not, H], contract p f,
          Irreducible.of_map (by rwa [← expand_contract p H hp.ne'] at hf),
          expand_contract p H hp.ne'⟩
  else Or.inl <| (separable_iff_derivative_ne_zero hf).2 H

Premises used: Polynomial.derivative, Or.inl, DFunLike.coe
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F p : (a : F[X]) → F[X]) g = f

Tactic:
classical
  exact if H : derivative f = 0 then by
    rcases p.eq_zero_or_pos with (rfl | hp)
    · haveI := CharP.charP_to_charZero F
      have := natDegree_eq_zero_of_derivative_eq_zero H
      have := (natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_irreducible hf).ne'
      contradiction
    haveI := isLocalHom_expand F hp
    exact
      Or.inr
        ⟨by rw [separable_iff_derivative_ne_zero hf, Classical.not_not, H], contract p f,
          Irreducible.of_map (by rwa [← expand_contract p H hp.ne'] at hf),
          expand_contract p H hp.ne'⟩
  else Or.inl <| (separable_iff_derivative_ne_zero hf).2 H

Premises used: Polynomial.derivative, Or.inl, DFunLike.coe
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : p ≠ 0
⊢ Nat.Prime p

Tactic:
replace hp : p.Prime := (CharP.char_is_prime_or_zero F p).resolve_right hp
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : Nat.Prime p
h :
  ∀ (N : ℕ)
    (ih :
      ∀ m < N,
        ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
          ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f)
    {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = N),
    ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f

Tactic:
induction hn : f.natDegree using Nat.strong_induction_on generalizing f with | _ N ih

Premises used: Polynomial.natDegree
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih :
  ∀ m < N,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
h : ∀ (h : f.Separable), ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
h₁ :
  ∀ (h1 : ¬f.Separable) (g : F[X]) (hg : Irreducible g) (hgf : (expand F p : (a : F[X]) → F[X]) g = f),
    ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f

Tactic:
rcases separable_or p hf with (h | ⟨h1, g, hg, hgf⟩)

Premises used: Polynomial.separable_or
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih :
  ∀ m < N,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
h : f.Separable
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f

Tactic:
⟨0, f, h, ?_⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih :
  ∀ m < N,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
h : f.Separable
h₁ : (expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) f = f
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f

Tactic:
refine ⟨0, f, h, ?_⟩
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih :
  ∀ m < N,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
h : f.Separable
h₁ : (expand F 1 : (a : F[X]) → F[X]) f = f
h₂ h₃ : f = f
⊢ (expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) f = f

Tactic:
rw [pow_zero, expand_one]

Premises used: Polynomial.expand_one, pow_zero
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
N : ℕ
ih :
  ∀ m < N,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
f : F[X]
hf : Irreducible f
hn : f.natDegree = N
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
h :
  ∀
    (ih :
      ∀ m < 0,
        ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
          ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f)
    (hn : f.natDegree = 0), ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
h₁ :
  ∀ (N : ℕ)
    (ih :
      ∀ m < N + 1,
        ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
          ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f)
    (hn : f.natDegree = N + 1), ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f

Tactic:
rcases N with - | N
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
ih :
  ∀ m < 0,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = 0
⊢ f = (C : (a : F) → F[X]) (f.coeff 0)

Tactic:
rw [natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hn

Premises used: Polynomial.degree_le_zero_iff, Polynomial.natDegree_eq_zero_iff_degree_le_zero
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
ih :
  ∀ m < 0,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f = (C : (a : F) → F[X]) (f.coeff 0)
h :
  ∀ (h1 : f.coeff 0 = 0) (g : F[X]) (hg : Irreducible g) (hgf : (expand F p : (a : F[X]) → F[X]) g = f)
    (ih :
      ∀ m < 0,
        ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
          ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f)
    (hn : f = (C : (a : F) → F[X]) (f.coeff 0)),
    ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f

Tactic:
rw [hn, separable_C, isUnit_iff_ne_zero, Classical.not_not] at h1

Premises used: Classical.not_not, isUnit_iff_ne_zero, Polynomial.separable_C
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : f.coeff 0 = 0
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
ih :
  ∀ m < 0,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f = (C : (a : F) → F[X]) (f.coeff 0)
⊢ f ≠ 0

Tactic:
have hf0 : f ≠ 0 := hf.ne_zero
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : f.coeff 0 = 0
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
ih :
  ∀ m < 0,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f = (C : (a : F) → F[X]) (f.coeff 0)
hf0 : f ≠ 0
⊢ f = 0

Tactic:
rw [h1, C_0] at hn

Premises used: Polynomial.C_0
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : f.coeff 0 = 0
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
ih :
  ∀ m < 0,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f = (C : (a : F) → F[X]) (f.coeff 0)
hf0 : f ≠ 0
hn₁ : f = 0
⊢ f ≠ 0

Tactic:
rw [h1, C_0] at hn

Premises used: Polynomial.C_0
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : f.coeff 0 = 0
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
ih :
  ∀ m < 0,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f = 0
hf0 : f ≠ 0
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f

Tactic:
absurd hn hf0

Premises used: absurd
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : f.coeff 0 = 0
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
ih :
  ∀ m < 0,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f = 0
hf0 : f ≠ 0
⊢ ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f

Tactic:
exact absurd hn hf0

Premises used: absurd
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
N : ℕ
ih :
  ∀ m < N + 1,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = N + 1
rwa : natDegree.{u} (R := F) ((expand F p : (a : F[X]) → F[X]) g) = N.succ
rwa₁ rwa₂ rwa₃ rwa₄ : f.natDegree = N.succ
⊢ g.natDegree * p = N.succ

Tactic:
rwa [← natDegree_expand, hgf]

Premises used: Polynomial.natDegree_expand
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
N : ℕ
ih :
  ∀ m < N + 1,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = N + 1
⊢ g.natDegree * p = N.succ

Tactic:
have hg1 : g.natDegree * p = N.succ := by rwa [← natDegree_expand, hgf]
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
N : ℕ
ih :
  ∀ m < N + 1,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
this : g.natDegree = 0
⊢ 0 = N.succ

Tactic:
rw [this, zero_mul] at hg1

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
N : ℕ
ih :
  ∀ m < N + 1,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
this : g.natDegree = 0
hg1₁ : 0 = N.succ
⊢ g.natDegree = 0

Tactic:
rw [this, zero_mul] at hg1

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
N : ℕ
ih :
  ∀ m < N + 1,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = N + 1
hg1 : 0 = N.succ
this : g.natDegree = 0
⊢ False

Tactic:
cases hg1
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
N : ℕ
ih :
  ∀ m < N + 1,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
⊢ g.natDegree ≠ 0

Tactic:
have hg2 : g.natDegree ≠ 0 := by
      intro this
      rw [this, zero_mul] at hg1
      cases hg1
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p : (a : F[X]) → F[X]) g = f
N : ℕ
ih :
  ∀ m < N + 1,
    ∀ {f : F[X]} (hf : Irreducible f) (hn : f.natDegree = m),
      ∃ (n : ℕ) (g : F[X]), g.Separable ∧ (expand F (p ^ n) : (a : F[X]) → F[X]) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
hg2 : g.natDegree ≠ 0
rw : g.natDegree * 1 < g.natDegree * p
⊢ g.natDegree < N.succ

Tactic:
rw [← mul_one g.natDegree, ← hg1]

Premises used: mul_one, Polynomial.natDegree