F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
⊢ ∀ (g₁ : F[X]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
g₁ : F[X]
hg₁ : Separable g₁
hgf₁ : ↑(expand F (p ^ n₁)) g₁ = f
n₂ : ℕ
g₂ : F[X]
hg₂ : Separable g₂
hgf₂ : ↑(expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂
revert g₁ g₂
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]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
⊢ ∀ (g₁ : F[X]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
clear! K
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]),
              Separable g₁ →
                ↑(expand F (p ^ n₁)) g₁ = f →
                  ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
hn : ¬n₁ ≤ n₂
⊢ ∀ (g₁ : F[X]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(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]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
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]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
wlog hn : n₁ ≤ n₂
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]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(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]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
have hf0 : f ≠ 0 := hf.ne_zero
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₁ : Separable g₁
hgf₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
hgf₂ : ↑(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₂
hf0 : f ≠ 0
⊢ ∀ (g₁ : F[X]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
intros g₁ hg₁ hgf₁ g₂ hg₂ hgf₂
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₁ : Separable g₁
hgf₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
hgf₂ : ↑(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₂
hf0 : f ≠ 0
g₁ : F[X]
hg₁ : Separable g₁
hgf₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
hgf₂ : ↑(expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂
rw [le_iff_exists_add] at hn
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₁ : Separable g₁
hgf₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
k : ℕ
hgf₂ : ↑(expand F (p ^ (n₁ + k))) g₂ = f
⊢ n₁ = n₁ + k ∧ 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 : ∃ c, n₂ = n₁ + c
hf0 : f ≠ 0
g₁ : F[X]
hg₁ : Separable g₁
hgf₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
hgf₂ : ↑(expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂
rcases hn with ⟨k, rfl⟩
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₁ : Separable g₁
hgf₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
k : ℕ
hgf₂ : ↑(expand F (p ^ k)) g₂ = g₁
⊢ n₁ = n₁ + k ∧ g₁ = g₂
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₁ : Separable g₁
hgf₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
k : ℕ
hgf₂ : ↑(expand F (p ^ (n₁ + k))) g₂ = f
⊢ n₁ = n₁ + k ∧ g₁ = g₂
rw [← hgf₁, pow_add, expand_mul, expand_inj (pow_pos hp n₁)] at hgf₂
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₂ : Separable g₂
k : ℕ
hg₁ : Separable (↑(expand F (p ^ k)) g₂)
hgf₁ : ↑(expand F (p ^ n₁)) (↑(expand F (p ^ k)) g₂) = f
⊢ n₁ = n₁ + k ∧ ↑(expand F (p ^ k)) g₂ = g₂
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₁ : Separable g₁
hgf₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
k : ℕ
hgf₂ : ↑(expand F (p ^ k)) g₂ = g₁
⊢ n₁ = n₁ + k ∧ g₁ = g₂
subst hgf₂
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₂ : Separable g₂
k : ℕ
hg₁ : Separable (↑(expand F (p ^ k)) g₂)
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₂
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₂ : Separable g₂
k : ℕ
hg₁ : Separable (↑(expand F (p ^ k)) g₂)
hgf₁ : ↑(expand F (p ^ n₁)) (↑(expand F (p ^ k)) g₂) = f
⊢ n₁ = n₁ + k ∧ ↑(expand F (p ^ k)) g₂ = g₂
subst hgf₁
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₂ : Separable g₂
k : ℕ
hg₁ : Separable (↑(expand F (p ^ k)) g₂)
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₂ : Separable g₂
hg₁ : Separable (↑(expand F (p ^ 0)) g₂)
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₂
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₂ : Separable g₂
k : ℕ
hg₁ : Separable (↑(expand F (p ^ k)) g₂)
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₂
rcases isUnit_or_eq_zero_of_separable_expand p k hp hg₁ with (h | rfl)
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]),
              Separable g₁ →
                ↑(expand F (p ^ n₁)) g₁ = f →
                  ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
hn : ¬n₁ ≤ n₂
g₁ : F[X]
hg₁ : Separable g₁
Hg₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
Hg₂ : ↑(expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂
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]),
              Separable g₁ →
                ↑(expand F (p ^ n₁)) g₁ = f →
                  ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
hn : ¬n₁ ≤ n₂
⊢ ∀ (g₁ : F[X]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
intro g₁ hg₁ Hg₁ g₂ hg₂ Hg₂
no goals
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]),
              Separable g₁ →
                ↑(expand F (p ^ n₁)) g₁ = f →
                  ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
hn : ¬n₁ ≤ n₂
g₁ : F[X]
hg₁ : Separable g₁
Hg₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
Hg₂ : ↑(expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂
simpa only [eq_comm] using this p hf hp n₂ n₁ (le_of_not_le hn) g₂ hg₂ Hg₂ g₁ hg₁ Hg₁
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₂ : Separable g₂
k : ℕ
hg₁ : Separable (↑(expand F (p ^ k)) g₂)
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₂
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₂ : Separable g₂
k : ℕ
hg₁ : Separable (↑(expand F (p ^ k)) g₂)
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₂
rw [isUnit_iff] at h
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₂ : Separable (↑C r)
hg₁ : Separable (↑(expand F (p ^ k)) (↑C r))
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
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₂ : Separable g₂
k : ℕ
hg₁ : Separable (↑(expand F (p ^ k)) g₂)
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₂
rcases h with ⟨r, hr, rfl⟩
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₂ : Separable (↑C r)
hg₁ : Separable (↑(expand F (p ^ k)) (↑C r))
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
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₂ : Separable (↑C r)
hg₁ : Separable (↑(expand F (p ^ k)) (↑C r))
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
simp_rw [expand_C] at hf
no goals
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₂ : Separable (↑C r)
hg₁ : Separable (↑(expand F (p ^ k)) (↑C r))
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
exact absurd (isUnit_C.2 hr) hf.1
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₂ : Separable g₂
hg₁ : Separable (↑(expand F (p ^ 0)) g₂)
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₂
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₂ : Separable g₂
hg₁ : Separable (↑(expand F (p ^ 0)) g₂)
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₂
rw [add_zero, pow_zero, expand_one]
no goals
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₂ : Separable g₂
hg₁ : Separable (↑(expand F (p ^ 0)) g₂)
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₂
constructor <;> rfl