-- 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
dvd : g ∣ (map i f).comp (map i p)
hd : (map i p).degree = 1
⊢ g.degree = 1

Tactic:
let _ := invertibleOfNonzero (leadingCoeff_ne_zero.mpr
    (ne_zero_of_degree_gt (n := ⊥) (by rw [hd]; decide)))

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
dvd : g ∣ (map i f).comp (map i p)
hd : (map i p).degree = 1
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
⊢ g.degree = 1

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

Tactic:
exact Or.inl hzero

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

Tactic:
intro g irr dvd

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]
irr : Irreducible g
dvd : g ∣ map i (f.comp p)
⊢ g.degree = 1

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 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 p)
⊢ g.degree = 1

Tactic:
rw [map_comp] at dvd hzero

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

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.natDegree = 1

Tactic:
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:
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)
hd : (map i p).degree = 1
⊢ ⊥ < degree ?m.46139

Tactic:
rw [hd]

Result:
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)
hd : (map i p).degree = 1
⊢ ⊥ < 1

Proof state:
case neg.inr.h.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 : ¬C (eval ((map i p).coeff 0) (map i f)) = 0
h : ∀ {g : L[X]}, Irreducible g → g ∣ map i f → g.degree = 1
g : L[X]
irr : Irreducible g
dvd : g ∣ C (eval ((map i p).coeff 0) (map i f))
hd : (map i p).degree < 1
⊢ IsUnit (C (eval ((map i p).coeff 0) (map i f)))

Tactic:
simpa using hzero

Result:
no goals

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
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)
hd : (map i p).degree = 1
⊢ ⊥ < 1

Tactic:
decide

Result:
no goals

Proof state:
case neg.inr.h.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 (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)
hd : (map i p).degree < 1
⊢ g.degree = 1

Tactic:
rw [eq_C_of_degree_le_zero (Nat.WithBot.lt_one_iff_le_zero.mp hd), comp_C] at dvd hzero

Result:
case neg.inr.h.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 : ¬C (eval ((map i p).coeff 0) (map i f)) = 0
h : ∀ {g : L[X]}, Irreducible g → g ∣ map i f → g.degree = 1
g : L[X]
irr : Irreducible g
dvd : g ∣ C (eval ((map i p).coeff 0) (map i f))
hd : (map i p).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
dvd : g ∣ (map i f).comp (map i p)
hd : (map i p).degree = 1
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
⊢ g.degree = 1

Tactic:
rw [eq_X_add_C_of_degree_eq_one hd, dvd_comp_C_mul_X_add_C_iff _ _] at 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
⊢ g.degree = 1

Proof state:
case neg.inr.h.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 : ¬C (eval ((map i p).coeff 0) (map i f)) = 0
h : ∀ {g : L[X]}, Irreducible g → g ∣ map i f → g.degree = 1
g : L[X]
irr : Irreducible g
dvd : g ∣ C (eval ((map i p).coeff 0) (map i f))
hd : (map i p).degree < 1
⊢ g.degree = 1

Tactic:
refine False.elim (irr.1 (isUnit_of_dvd_unit dvd ?_))

Result:
case neg.inr.h.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 : ¬C (eval ((map i p).coeff 0) (map i f)) = 0
h : ∀ {g : L[X]}, Irreducible g → g ∣ map i f → g.degree = 1
g : L[X]
irr : Irreducible g
dvd : g ∣ C (eval ((map i p).coeff 0) (map i f))
hd : (map i p).degree < 1
⊢ IsUnit (C (eval ((map i p).coeff 0) (map i f)))