-- Mathlib/FieldTheory/Separable.lean
theorem unique_separable_of_irreducible {f : F[X]} (hf : Irreducible f) (hp : 0 < p) (n₁ : ℕ)
    (g₁ : F[X]) (hg₁ : g₁.Separable) (hgf₁ : expand F (p ^ n₁) g₁ = f) (n₂ : ℕ) (g₂ : F[X])
    (hg₂ : g₂.Separable) (hgf₂ : expand F (p ^ n₂) g₂ = f) : n₁ = n₂ ∧ g₁ = g₂

Proof state:
case inr
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
this :
  ∀ {F : Type u} [inst : Field F] (p : ℕ) [HF : CharP F p] {f : F[X]},
    Irreducible f →
      0 < p →
        ∀ (n₁ n₂ : ℕ),
          n₁ ≤ n₂ →
            ∀ (g₁ : F[X]),
              g₁.Separable →
                (expand F (p ^ n₁)) g₁ = f →
                  ∀ (g₂ : F[X]), g₂.Separable → (expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
hn : ¬n₁ ≤ n₂
g₁ : F[X]
hg₁ : g₁.Separable
Hg₁ : (expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
Hg₂ : (expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂

Tactic:
simpa only [eq_comm] using this p hf hp n₂ n₁ (le_of_not_le hn) g₂ hg₂ Hg₂ g₁ hg₁ Hg₁

Result:
no goals

Proof state:
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
hn : ∃ c, n₂ = n₁ + c
hf0 : f ≠ 0
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
hgf₂ : (expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂

Tactic:
rcases hn with ⟨k, rfl⟩

Result:
case intro
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
hf0 : f ≠ 0
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hgf₂ : (expand F (p ^ (n₁ + k))) g₂ = f
⊢ n₁ = n₁ + k ∧ g₁ = g₂

Proof state:
case intro.inl
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : ((expand F (p ^ k)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ k)) g₂))
hf0 : (expand F (p ^ n₁)) ((expand F (p ^ k)) g₂) ≠ 0
h : IsUnit g₂
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂

Tactic:
rw [isUnit_iff] at h

Result:
case intro.inl
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : ((expand F (p ^ k)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ k)) g₂))
hf0 : (expand F (p ^ n₁)) ((expand F (p ^ k)) g₂) ≠ 0
h : ∃ r, IsUnit r ∧ C r = g₂
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂

Proof state:
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
hn : n₁ ≤ n₂
hf0 : f ≠ 0
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
hgf₂ : (expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂

Tactic:
rw [le_iff_exists_add] at hn

Result:
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
hn : ∃ c, n₂ = n₁ + c
hf0 : f ≠ 0
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
hgf₂ : (expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂

Proof state:
case intro
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
hf0 : f ≠ 0
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : ((expand F (p ^ k)) g₂).Separable
hgf₁ : (expand F (p ^ n₁)) ((expand F (p ^ k)) g₂) = f
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂

Tactic:
subst hgf₁

Result:
case intro
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : ((expand F (p ^ k)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ k)) g₂))
hf0 : (expand F (p ^ n₁)) ((expand F (p ^ k)) g₂) ≠ 0
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂

Proof state:
case intro.inl.intro.intro
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ k : ℕ
r : F
hr : IsUnit r
hg₂ : (C r).Separable
hg₁ : ((expand F (p ^ k)) (C r)).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ k)) (C r)))
hf0 : (expand F (p ^ n₁)) ((expand F (p ^ k)) (C r)) ≠ 0
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) (C r) = C r

Tactic:
simp_rw [expand_C] at hf

Result:
case intro.inl.intro.intro
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ k : ℕ
r : F
hr : IsUnit r
hg₂ : (C r).Separable
hg₁ : ((expand F (p ^ k)) (C r)).Separable
hf0 : (expand F (p ^ n₁)) ((expand F (p ^ k)) (C r)) ≠ 0
hf : Irreducible (C r)
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) (C r) = C r

Proof state:
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
hn : n₁ ≤ n₂
hf0 : f ≠ 0
⊢ ∀ (g₁ : F[X]),
    g₁.Separable →
      (expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), g₂.Separable → (expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂

Tactic:
intros g₁ hg₁ hgf₁ g₂ hg₂ hgf₂

Result:
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
hn : n₁ ≤ n₂
hf0 : f ≠ 0
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
hgf₂ : (expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂

Proof state:
case intro.inl.intro.intro
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ k : ℕ
r : F
hr : IsUnit r
hg₂ : (C r).Separable
hg₁ : ((expand F (p ^ k)) (C r)).Separable
hf0 : (expand F (p ^ n₁)) ((expand F (p ^ k)) (C r)) ≠ 0
hf : Irreducible (C r)
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) (C r) = C r

Tactic:
exact absurd (isUnit_C.2 hr) hf.1

Result:
no goals

Proof state:
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
hn : n₁ ≤ n₂
⊢ ∀ (g₁ : F[X]),
    g₁.Separable →
      (expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), g₂.Separable → (expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂

Tactic:
have hf0 : f ≠ 0 := hf.ne_zero

Result:
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
hn : n₁ ≤ n₂
hf0 : f ≠ 0
⊢ ∀ (g₁ : F[X]),
    g₁.Separable →
      (expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), g₂.Separable → (expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂