Theorem: prod_galRestrictHom_eq_norm (FltRegular/NumberTheory/GaloisPrime.lean)

State before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : S
⊢ ∏ σ : L ≃ₐ[K] L, ((galRestrictHom R K L S) ↑σ) x =
    (algebraMap R S) (IsIntegralClosure.mk' R ((Algebra.norm K) ((algebraMap S L) x)) ⋯)
Tactic:
apply IsIntegralClosure.algebraMap_injective S R L
State after:
case a
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : S
⊢ (algebraMap S L) (∏ σ : L ≃ₐ[K] L, ((galRestrictHom R K L S) ↑σ) x) =
    (algebraMap S L) ((algebraMap R S) (IsIntegralClosure.mk' R ((Algebra.norm K) ((algebraMap S L) x)) ⋯))

State before:
case a
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : S
⊢ (algebraMap S L) (∏ σ : L ≃ₐ[K] L, ((galRestrictHom R K L S) ↑σ) x) =
    (algebraMap S L) ((algebraMap R S) (IsIntegralClosure.mk' R ((Algebra.norm K) ((algebraMap S L) x)) ⋯))
Tactic:
rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_eq R K L]
State after:
case a
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : S
⊢ (algebraMap S L) (∏ σ : L ≃ₐ[K] L, ((galRestrictHom R K L S) ↑σ) x) =
    ((algebraMap K L).comp (algebraMap R K)) (IsIntegralClosure.mk' R ((Algebra.norm K) ((algebraMap S L) x)) ⋯)

State before:
case a
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : IsIntegralClosure S R L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : S
⊢ (algebraMap S L) (∏ σ : L ≃ₐ[K] L, ((galRestrictHom R K L S) ↑σ) x) =
    ((algebraMap K L).comp (algebraMap R K)) (IsIntegralClosure.mk' R ((Algebra.norm K) ((algebraMap S L) x)) ⋯)
Tactic:
simp only [map_prod, algebraMap_galRestrictHom_apply, IsIntegralClosure.algebraMap_mk',
  Algebra.norm_eq_prod_automorphisms, AlgHom.coe_coe, RingHom.coe_comp, Function.comp_apply]
State after:
no goals