case inl
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hp : Irreducible p
h✝ : map (RingHom.id K) p = 0
⊢ degree p = 1

case inr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hp : Irreducible p
hp_splits : ∀ {g : K[X]}, Irreducible g → g ∣ map (RingHom.id K) p → degree g = 1
⊢ degree p = 1
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hp : Irreducible p
hp_splits : Splits (RingHom.id K) p
⊢ degree p = 1
rcases hp_splits with ⟨⟩ | hp_splits
case inl.h
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hp : Irreducible p
h✝ : map (RingHom.id K) p = 0
⊢ False
case inl
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hp : Irreducible p
h✝ : map (RingHom.id K) p = 0
⊢ degree p = 1
exfalso
no goals
case inl.h
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hp : Irreducible p
h✝ : map (RingHom.id K) p = 0
⊢ False
simp_all
case inr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hp : Irreducible p
hp_splits : ∀ {g : K[X]}, Irreducible g → g ∣ map (RingHom.id K) p → degree g = 1
⊢ p ∣ map (RingHom.id K) p
case inr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hp : Irreducible p
hp_splits : ∀ {g : K[X]}, Irreducible g → g ∣ map (RingHom.id K) p → degree g = 1
⊢ degree p = 1
apply hp_splits hp
no goals
case inr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hp : Irreducible p
hp_splits : ∀ {g : K[X]}, Irreducible g → g ∣ map (RingHom.id K) p → degree g = 1
⊢ p ∣ map (RingHom.id K) p
simp