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

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
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
h₂ : ¬p₂.comp q = 0
⊢ P (p₁ * p₂)

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
⊢ Splits (algebraMap F (p.comp q).SplittingField) p

Tactic:
let P : F[X] → Prop := fun r => r.Splits (algebraMap F (r.comp q).SplittingField)

Result:
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
⊢ Splits (algebraMap F (p.comp q).SplittingField) 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₂.comp q = 0
h : p₂ = 0
⊢ P (p₁ * p₂)

Tactic:
rw [h, mul_zero]

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 0

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
⊢ P r

Tactic:
have qx_int := Normal.isIntegral h_normal (aeval x q)

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
h_normal : Normal F (r.comp q).SplittingField
qx_int : IsIntegral F ((aeval x) q)
⊢ P r

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
⊢ ∀ {r : F[X]}, Irreducible r → P r

Tactic:
intro r hr

Result:
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
⊢ P r

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 (p₁ * p₂)

Tactic:
rw [h, zero_mul]

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₁ = 0
⊢ P 0

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
⊢ P r

Tactic:
have h_normal : Normal F (r.comp q).SplittingField := SplittingField.instNormal (r.comp q)

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
h_normal : Normal F (r.comp q).SplittingField
⊢ P r

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]}, P p₁ → P p₂ → P (p₁ * p₂)

Tactic:
intro p₁ p₂ hp₁ hp₂

Result:
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₂)

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
⊢ 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₁ = 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 : eval (q.coeff 0) p₁ = 0 ∧ q = C (q.coeff 0)
⊢ P (p₁ * p₂)

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
key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂)
⊢ Splits (algebraMap F (p.comp q).SplittingField) p

Tactic:
exact
  WfDvdMonoid.induction_on_irreducible p (splits_zero _) (fun _ => splits_of_isUnit _)
    fun _ _ _ h => key2 (key1 h)

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₂ : 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:
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
⊢ P r

Tactic:
by_cases hr' : natDegree r = 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
r : F[X]
hr : Irreducible r
hr' : r.natDegree = 0
⊢ P r

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