-- Mathlib/RingTheory/Norm/Basic.lean
theorem _root_.IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots (x : L)
    (hf : (minpoly K x).Splits (algebraMap K F)) :
    (algebraMap K F) (norm K (AdjoinSimple.gen K x)) =
      ((minpoly K x).aroots F).prod

Proof state:
case neg
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : Splits (algebraMap K F) (minpoly K x)
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : ¬IsIntegral K x
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod

Tactic:
simp [minpoly.eq_zero hx, IntermediateField.AdjoinSimple.norm_gen_eq_one hx, aroots_def]

Result:
no goals

Proof state:
case pos
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : Splits (algebraMap K F) (minpoly K x)
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod

Tactic:
rw [← adjoin.powerBasis_gen hx, PowerBasis.norm_gen_eq_prod_roots] <;>
  rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL] <;>
  simp only [AdjoinSimple.algebraMap_gen _ _, hf]

Result:
no goals

Proof state:
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : Splits (algebraMap K F) (minpoly K x)
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod

Tactic:
have injKxL := (algebraMap K⟮x⟯ L).injective

Result:
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : Splits (algebraMap K F) (minpoly K x)
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod

Proof state:
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : Splits (algebraMap K F) (minpoly K x)
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod

Tactic:
by_cases hx : IsIntegral K x

Result:
case pos
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : Splits (algebraMap K F) (minpoly K x)
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod

case neg
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : Splits (algebraMap K F) (minpoly K x)
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : ¬IsIntegral K x
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod

Proof state:
case pos
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : Splits (algebraMap K F) (minpoly K x)
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod

case neg
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : Splits (algebraMap K F) (minpoly K x)
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : ¬IsIntegral K x
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod

Tactic:
swap

Result:
case neg
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : Splits (algebraMap K F) (minpoly K x)
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : ¬IsIntegral K x
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod

case pos
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K L
inst✝ : Algebra K F
x : L
hf : Splits (algebraMap K F) (minpoly K x)
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod