-- 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:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
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:
wlog hn : n₁ ≤ n₂

Result:
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]),
    g₁.Separable →
      (expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), g₂.Separable → (expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂

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₂

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
hgf₁ : (expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hgf₂ : (expand F (p ^ k)) g₂ = g₁
⊢ n₁ = n₁ + 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
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₂

Proof state:
case intro.inr
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
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
hf0 : (expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂) ≠ 0
⊢ n₁ = n₁ ∧ g₂ = g₂

Tactic:
constructor <;> rfl

Result:
no goals

Proof state:
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₂

Tactic:
rcases isUnit_or_eq_zero_of_separable_expand p k hp hg₁ with (h | rfl)

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 : IsUnit g₂
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂

case intro.inr
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
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
hf0 : (expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂) ≠ 0
⊢ n₁ = n₁ + 0 ∧ (expand F (p ^ 0)) 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 : ∃ r, IsUnit r ∧ C r = g₂
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂

Tactic:
rcases h with ⟨r, hr, rfl⟩

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
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

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]),
    g₁.Separable →
      (expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), g₂.Separable → (expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂

Tactic:
intro g₁ hg₁ Hg₁ g₂ hg₂ Hg₂

Result:
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₂

Proof state:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
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₂

Tactic:
revert g₁ g₂

Result:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
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₂

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
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₂

Tactic:
rw [← hgf₁, pow_add, expand_mul, expand_inj (pow_pos hp n₁)] at hgf₂

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 ^ k)) g₂ = g₁
⊢ n₁ = n₁ + k ∧ g₁ = g₂

Proof state:
case intro.inr
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
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
hf0 : (expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂) ≠ 0
⊢ n₁ = n₁ + 0 ∧ (expand F (p ^ 0)) g₂ = g₂

Tactic:
rw [add_zero, pow_zero, expand_one]

Result:
case intro.inr
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
hg₁ : ((expand F (p ^ 0)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂))
hf0 : (expand F (p ^ n₁)) ((expand F (p ^ 0)) g₂) ≠ 0
⊢ n₁ = n₁ ∧ g₂ = g₂