-- Mathlib/RingTheory/Norm/Basic.lean
theorem norm_eq_prod_automorphisms [FiniteDimensional K L] [IsGalois K L] (x : L) :
    algebraMap K L (norm K x) = ∏ σ : L ≃ₐ[K] L, σ x

Proof state:
case a.h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
σ : L →ₐ[K] AlgebraicClosure L
⊢ σ x = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) σ) x)

Tactic:
simp only [Normal.algHomEquivAut, AlgHom.restrictNormal', Equiv.coe_fn_mk,
  AlgEquiv.coe_ofBijective, AlgHom.restrictNormal_commutes, id.map_eq_id, RingHom.id_apply]

Result:
no goals

Proof state:
case a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) = ∏ x : L →ₐ[K] AlgebraicClosure L, ?a.f✝ x

Tactic:
rw [← norm_eq_prod_embeddings _ _ x, ← IsScalarTower.algebraMap_apply]

Result:
no goals

Proof state:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap K L) ((norm K) x) = ∏ σ : L ≃ₐ[K] L, σ x

Tactic:
apply FaithfulSMul.algebraMap_injective L (AlgebraicClosure L)

Result:
case a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) =
    (algebraMap L (AlgebraicClosure L)) (∏ σ : L ≃ₐ[K] L, σ x)

Proof state:
case a.h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ ∀ (x_1 : L →ₐ[K] AlgebraicClosure L),
    x_1 x = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) x_1) x)

Tactic:
intro σ

Result:
case a.h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
σ : L →ₐ[K] AlgebraicClosure L
⊢ σ x = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) σ) x)

Proof state:
case a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) =
    ∏ x_1 : L ≃ₐ[K] L, (algebraMap L (AlgebraicClosure L)) (x_1 x)

Tactic:
rw [← Fintype.prod_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)]

Result:
case a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) = ∏ x : L →ₐ[K] AlgebraicClosure L, ?a.f✝ x

case a.f
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (L →ₐ[K] AlgebraicClosure L) → AlgebraicClosure L

case a.h
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ ∀ (x_1 : L →ₐ[K] AlgebraicClosure L),
    ?a.f✝ x_1 = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) x_1) x)

Proof state:
case a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) =
    (algebraMap L (AlgebraicClosure L)) (∏ σ : L ≃ₐ[K] L, σ x)

Tactic:
rw [map_prod (algebraMap L (AlgebraicClosure L))]

Result:
case a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) =
    ∏ x_1 : L ≃ₐ[K] L, (algebraMap L (AlgebraicClosure L)) (x_1 x)