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

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 (RingHom.id L) ((map i f).comp (map i p))
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
⊢ map i f =
    (map i f).comp
      ((C (map i p).leadingCoeff * X + C ((map i p).coeff 0)).comp
        (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0))))

Tactic:
simp only [coeff_map, invOf_eq_inv, mul_sub, ← C_mul, add_comp, mul_comp, C_comp, X_comp,
  ← mul_assoc]

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
h : Splits (RingHom.id L) ((map i f).comp (map i p))
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
⊢ map i f =
    (map i f).comp
      (C ((map i p).leadingCoeff * (map i p).leadingCoeff⁻¹) * X -
          C ((map i p).leadingCoeff * (map i p).leadingCoeff⁻¹ * i (p.coeff 0)) +
        C (i (p.coeff 0)))

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 (RingHom.id L) ((map i f).comp (map i p))
⊢ ⊥ < 1

Tactic:
decide

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
h : Splits (RingHom.id L) ((map i f).comp (map i p))
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
⊢ map i f = ((map i f).comp (map i p)).comp (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0)))

Tactic:
rw [comp_assoc]

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
h : Splits (RingHom.id L) ((map i f).comp (map i p))
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
⊢ map i f = (map i f).comp ((map i p).comp (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0))))

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 (RingHom.id L) ((map i f).comp (map i p))
⊢ Splits (RingHom.id L) (map i f)

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

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
h : Splits (RingHom.id L) ((map i f).comp (map i p))
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
⊢ Splits (RingHom.id L) (map i f)

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 (RingHom.id L) ((map i f).comp (map i p))
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
this : map i f = ((map i f).comp (map i p)).comp (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0)))
⊢ (map (RingHom.id L) (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0)))).degree ≤ 1

Tactic:
simp [degree_C (inv_ne_zero (Invertible.ne_zero (a := (map i p).leadingCoeff)))]

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
h : Splits (RingHom.id L) ((map i f).comp (map i p))
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
this : map i f = ((map i f).comp (map i p)).comp (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0)))
⊢ Splits (RingHom.id L) (map i f)

Tactic:
refine this ▸ Splits.comp_of_map_degree_le_one ?_ h

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
h : Splits (RingHom.id L) ((map i f).comp (map i p))
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
this : map i f = ((map i f).comp (map i p)).comp (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0)))
⊢ (map (RingHom.id L) (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0)))).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 (RingHom.id L) ((map i f).comp (map i p))
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
⊢ Splits (RingHom.id L) (map i f)

Tactic:
have : (map i f) = ((map i f).comp (map i p)).comp ((C ⅟ (map i p).leadingCoeff *
    (X - C ((map i p).coeff 0)))) := by
  rw [comp_assoc]
  nth_rw 1 [eq_X_add_C_of_degree_eq_one hd]
  simp only [coeff_map, invOf_eq_inv, mul_sub, ← C_mul, add_comp, mul_comp, C_comp, X_comp,
    ← mul_assoc]
  simp

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
h : Splits (RingHom.id L) ((map i f).comp (map i p))
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
this : map i f = ((map i f).comp (map i p)).comp (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0)))
⊢ Splits (RingHom.id L) (map i f)

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
⊢ Splits i f ↔ Splits i (f.comp p)

Tactic:
rw [← splits_id_iff_splits, ← splits_id_iff_splits (f := f.comp p), map_comp]

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
⊢ Splits (RingHom.id L) (map i f) ↔ Splits (RingHom.id L) ((map i f).comp (map i p))

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 (RingHom.id L) ((map i f).comp (map i p))
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
⊢ map i f =
    (map i f).comp
      (C ((map i p).leadingCoeff * (map i p).leadingCoeff⁻¹) * X -
          C ((map i p).leadingCoeff * (map i p).leadingCoeff⁻¹ * i (p.coeff 0)) +
        C (i (p.coeff 0)))

Tactic:
simp

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
h : Splits (RingHom.id L) ((map i f).comp (map i p))
⊢ ⊥ < degree ?m.59706

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
h : Splits (RingHom.id L) ((map i f).comp (map i p))
⊢ ⊥ < 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 (RingHom.id L) ((map i f).comp (map i p))
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
⊢ map i f = (map i f).comp ((map i p).comp (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0))))

Tactic:
nth_rw 1 [eq_X_add_C_of_degree_eq_one 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
h : Splits (RingHom.id L) ((map i f).comp (map i p))
x✝ : Invertible (map i p).leadingCoeff := invertibleOfNonzero ⋯
⊢ map i f =
    (map i f).comp
      ((C (map i p).leadingCoeff * X + C ((map i p).coeff 0)).comp
        (C ⅟(map i p).leadingCoeff * (X - C ((map i p).coeff 0))))

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
⊢ Splits (RingHom.id L) (map i f) ↔ Splits (RingHom.id L) ((map i f).comp (map i p))

Tactic:
refine ⟨fun h => Splits.comp_of_map_degree_le_one
  (le_of_eq (map_id (R := L) ▸ hd)) h, fun h => ?_⟩

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
h : Splits (RingHom.id L) ((map i f).comp (map i p))
⊢ Splits (RingHom.id L) (map i f)