-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean
theorem splits_in_splittingField_of_comp (hq : q.natDegree ≠ 0) :
    p.Splits (algebraMap F (p.comp q).SplittingField)

Proof state:
case neg.intro
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
r : F[X]
hr : Irreducible r
hr' : ¬r.natDegree = 0
x : (r.comp q).SplittingField
hx : eval₂ (algebraMap F (r.comp q).SplittingField) x (r.comp q) = 0
⊢ P r

Tactic:
rw [← aeval_def, aeval_comp] at hx

Result:
case neg.intro
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
r : F[X]
hr : Irreducible r
hr' : ¬r.natDegree = 0
x : (r.comp q).SplittingField
hx : (aeval ((aeval x) q)) r = 0
⊢ P r

Proof state:
case pos
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : p₂.comp q = 0
⊢ P (p₁ * p₂)

Tactic:
rcases comp_eq_zero_iff.mp h₂ with h | h

Result:
case pos.inl
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : p₂.comp q = 0
h : p₂ = 0
⊢ P (p₁ * p₂)

case pos.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : p₂.comp q = 0
h : eval (q.coeff 0) p₂ = 0 ∧ q = C (q.coeff 0)
⊢ P (p₁ * p₂)

Proof state:
case pos.inl
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : p₁.comp q = 0
h : p₁ = 0
⊢ P 0

Tactic:
exact splits_zero _

Result:
no goals

Proof state:
case pos
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
r : F[X]
hr : Irreducible r
hr' : r.natDegree = 0
⊢ P r

Tactic:
exact splits_of_natDegree_le_one _ (le_trans (le_of_eq hr') zero_le_one)

Result:
no goals

Proof state:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
r : F[X]
hr : Irreducible r
hr' : ¬r.natDegree = 0
⊢ P r

Tactic:
obtain ⟨x, hx⟩ :=
  exists_root_of_splits _ (SplittingField.splits (r.comp q)) fun h =>
    hr'
      ((mul_eq_zero.mp
            (natDegree_comp.symm.trans (natDegree_eq_of_degree_eq_some h))).resolve_right
        hq)

Result:
case neg.intro
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
r : F[X]
hr : Irreducible r
hr' : ¬r.natDegree = 0
x : (r.comp q).SplittingField
hx : eval₂ (algebraMap F (r.comp q).SplittingField) x (r.comp q) = 0
⊢ P r

Proof state:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : ¬p₂.comp q = 0
⊢ P (p₁ * p₂)

Tactic:
have key := mul_splits_in_splittingField_of_mul h₁ h₂ hp₁ hp₂

Result:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : ¬p₂.comp q = 0
key : Splits (algebraMap F (p₁.comp q * p₂.comp q).SplittingField) (p₁ * p₂)
⊢ P (p₁ * p₂)

Proof state:
case neg.intro
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
r : F[X]
hr : Irreducible r
hr' : ¬r.natDegree = 0
x : (r.comp q).SplittingField
hx : (aeval ((aeval x) q)) r = 0
h_normal : Normal F (r.comp q).SplittingField
qx_int : IsIntegral F ((aeval x) q)
⊢ P r

Tactic:
exact
  splits_of_splits_of_dvd _ (minpoly.ne_zero qx_int) (Normal.splits h_normal _)
    ((minpoly.irreducible qx_int).dvd_symm hr (minpoly.dvd F _ hx))

Result:
no goals

Proof state:
case pos.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : p₁.comp q = 0
h : eval (q.coeff 0) p₁ = 0 ∧ q = C (q.coeff 0)
⊢ P (p₁ * p₂)

Tactic:
exact False.elim (hq (by rw [h.2, natDegree_C]))

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : p₁.comp q = 0
h : eval (q.coeff 0) p₁ = 0 ∧ q = C (q.coeff 0)
⊢ q.natDegree = 0

Tactic:
rw [h.2, natDegree_C]

Result:
no goals

Proof state:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : ¬p₂.comp q = 0
key : Splits (algebraMap F (p₁.comp q * p₂.comp q).SplittingField) (p₁ * p₂)
⊢ P (p₁ * p₂)

Tactic:
rwa [← mul_comp] at key

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
⊢ P (p₁ * p₂)

Tactic:
by_cases h₁ : p₁.comp q = 0

Result:
case pos
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : p₁.comp q = 0
⊢ P (p₁ * p₂)

case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
⊢ P (p₁ * p₂)

Proof state:
case pos.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : p₂.comp q = 0
h : eval (q.coeff 0) p₂ = 0 ∧ q = C (q.coeff 0)
⊢ P (p₁ * p₂)

Tactic:
exact False.elim (hq (by rw [h.2, natDegree_C]))

Result:
no goals

Proof state:
case pos.inl
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r => Splits (algebraMap F (r.comp q).SplittingField) r
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : p₂.comp q = 0
h : p₂ = 0
⊢ P 0

Tactic:
exact splits_zero _

Result:
no goals