-- Mathlib/Algebra/Polynomial/Splits.lean
theorem Splits.comp_of_map_degree_le_one {f : K[X]} {p : K[X]} (hd : (p.map i).degree ≤ 1)
    (h : f.Splits i) : (f.comp p).Splits i

Proof state:
case neg.inr.h.inr
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f p : K[X]
hd✝ : (map i p).degree ≤ 1
hzero : ¬(map i f).comp (map i p) = 0
h : ∀ {g : L[X]}, Irreducible g → g ∣ map i f → g.degree = 1
g : L[X]
irr : Irreducible g
hd : (map i p).degree = 1
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
dvd : g.comp (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0))) ∣ map i f
⊢ g.degree = 1

Tactic:
have := h (irr.map (algEquivCMulXAddC _ _).symm) dvd

Result:
case neg.inr.h.inr
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f p : K[X]
hd✝ : (map i p).degree ≤ 1
hzero : ¬(map i f).comp (map i p) = 0
h : ∀ {g : L[X]}, Irreducible g → g ∣ map i f → g.degree = 1
g : L[X]
irr : Irreducible g
hd : (map i p).degree = 1
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
dvd : g.comp (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0))) ∣ map i f
this : ((algEquivCMulXAddC (map i p).leadingCoeff ((map i p).coeff 0)).symm g).degree = 1
⊢ g.degree = 1

Proof state:
case neg.inr.h.inr
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f p : K[X]
hd✝ : (map i p).degree ≤ 1
hzero : ¬(map i f).comp (map i p) = 0
h : ∀ {g : L[X]}, Irreducible g → g ∣ map i f → g.degree = 1
g : L[X]
irr : Irreducible g
hd : (map i p).degree = 1
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
dvd : g.comp (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0))) ∣ map i f
this : ((algEquivCMulXAddC (map i p).leadingCoeff ((map i p).coeff 0)).symm g).degree = 1
⊢ g.degree = 1

Tactic:
rw [degree_eq_natDegree irr.ne_zero]

Result:
case neg.inr.h.inr
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f p : K[X]
hd✝ : (map i p).degree ≤ 1
hzero : ¬(map i f).comp (map i p) = 0
h : ∀ {g : L[X]}, Irreducible g → g ∣ map i f → g.degree = 1
g : L[X]
irr : Irreducible g
hd : (map i p).degree = 1
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
dvd : g.comp (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0))) ∣ map i f
this : ((algEquivCMulXAddC (map i p).leadingCoeff ((map i p).coeff 0)).symm g).degree = 1
⊢ ↑g.natDegree = 1

Proof state:
case neg.inl
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f p : K[X]
hd : (map i p).degree ≤ 1
hzero : ¬map i (f.comp p) = 0
h0 : map i f = 0
⊢ Splits i (f.comp p)

Tactic:
exact Or.inl <| map_comp i _ _ ▸ h0.symm ▸ zero_comp

Result:
no goals

Proof state:
case neg.inr.h
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f p : K[X]
hd : (map i p).degree ≤ 1
hzero : ¬(map i f).comp (map i p) = 0
h : ∀ {g : L[X]}, Irreducible g → g ∣ map i f → g.degree = 1
g : L[X]
irr : Irreducible g
dvd : g ∣ (map i f).comp (map i p)
⊢ g.degree = 1

Tactic:
cases lt_or_eq_of_le hd with
| inl hd =>
  rw [eq_C_of_degree_le_zero (Nat.WithBot.lt_one_iff_le_zero.mp hd), comp_C] at dvd hzero
  refine False.elim (irr.1 (isUnit_of_dvd_unit dvd ?_))
  simpa using hzero
| inr hd =>
  let _ := invertibleOfNonzero (leadingCoeff_ne_zero.mpr
      (ne_zero_of_degree_gt (n := ⊥) (by rw [hd]; decide)))
  rw [eq_X_add_C_of_degree_eq_one hd, dvd_comp_C_mul_X_add_C_iff _ _] at dvd
  have := h (irr.map (algEquivCMulXAddC _ _).symm) dvd
  rw [degree_eq_natDegree irr.ne_zero]
  rwa [algEquivCMulXAddC_symm_apply, ← comp_eq_aeval,
    degree_eq_natDegree (fun h => WithBot.bot_ne_one (h ▸ this)),
    natDegree_comp, natDegree_C_mul (invertibleInvOf.ne_zero),
    natDegree_X_sub_C, mul_one] at this

Result:
no goals

Proof state:
case neg.inr
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f p : K[X]
hd : (map i p).degree ≤ 1
hzero : ¬map i (f.comp p) = 0
h : ∀ {g : L[X]}, Irreducible g → g ∣ map i f → g.degree = 1
⊢ Splits i (f.comp p)

Tactic:
right

Result:
case neg.inr.h
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f p : K[X]
hd : (map i p).degree ≤ 1
hzero : ¬map i (f.comp p) = 0
h : ∀ {g : L[X]}, Irreducible g → g ∣ map i f → g.degree = 1
⊢ ∀ {g : L[X]}, Irreducible g → g ∣ map i (f.comp p) → g.degree = 1

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f p : K[X]
hd : (map i p).degree ≤ 1
h : Splits i f
⊢ Splits i (f.comp p)

Tactic:
by_cases hzero : map i (f.comp p) = 0

Result:
case pos
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f p : K[X]
hd : (map i p).degree ≤ 1
h : Splits i f
hzero : map i (f.comp p) = 0
⊢ Splits i (f.comp p)

case neg
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f p : K[X]
hd : (map i p).degree ≤ 1
h : Splits i f
hzero : ¬map i (f.comp p) = 0
⊢ Splits i (f.comp p)

Proof state:
case neg
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f p : K[X]
hd : (map i p).degree ≤ 1
h : Splits i f
hzero : ¬map i (f.comp p) = 0
⊢ Splits i (f.comp p)

Tactic:
cases h with
| inl h0 =>
  exact Or.inl <| map_comp i _ _ ▸ h0.symm ▸ zero_comp
| inr h =>
  right
  intro g irr dvd
  rw [map_comp] at dvd hzero
  cases lt_or_eq_of_le hd with
  | inl hd =>
    rw [eq_C_of_degree_le_zero (Nat.WithBot.lt_one_iff_le_zero.mp hd), comp_C] at dvd hzero
    refine False.elim (irr.1 (isUnit_of_dvd_unit dvd ?_))
    simpa using hzero
  | inr hd =>
    let _ := invertibleOfNonzero (leadingCoeff_ne_zero.mpr
        (ne_zero_of_degree_gt (n := ⊥) (by rw [hd]; decide)))
    rw [eq_X_add_C_of_degree_eq_one hd, dvd_comp_C_mul_X_add_C_iff _ _] at dvd
    have := h (irr.map (algEquivCMulXAddC _ _).symm) dvd
    rw [degree_eq_natDegree irr.ne_zero]
    rwa [algEquivCMulXAddC_symm_apply, ← comp_eq_aeval,
      degree_eq_natDegree (fun h => WithBot.bot_ne_one (h ▸ this)),
      natDegree_comp, natDegree_C_mul (invertibleInvOf.ne_zero),
      natDegree_X_sub_C, mul_one] at this

Result:
no goals