-- Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
lemma Algebra.algebraMap_intNorm_of_isGalois
    [IsDomain A] [IsIntegrallyClosed A] [IsDomain B] [IsIntegrallyClosed B]
    [Module.Finite A B] [NoZeroSMulDivisors A B] [IsGalois (FractionRing A) (FractionRing B)]
    {x : B} :
    algebraMap A B (Algebra.intNorm A B x) = ∏ σ : B ≃ₐ[A] B, σ x

Proof state:
A : Type u_1
B : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : IsGalois (FractionRing A) (FractionRing B)
x : B
⊢ (algebraMap A B) ((intNorm A B) x) = ∏ σ : B ≃ₐ[A] B, σ x

Tactic:
haveI : IsIntegralClosure B A (FractionRing B) :=
  IsIntegralClosure.of_isIntegrallyClosed _ _ _

Result:
A : Type u_1
B : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : IsGalois (FractionRing A) (FractionRing B)
x : B
this : IsIntegralClosure B A (FractionRing B)
⊢ (algebraMap A B) ((intNorm A B) x) = ∏ σ : B ≃ₐ[A] B, σ x

Proof state:
A : Type u_1
B : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : IsGalois (FractionRing A) (FractionRing B)
x : B
this✝¹ : IsIntegralClosure B A (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ (algebraMap A B) ((intNorm A B) x) =
    ∏ i : FractionRing B ≃ₐ[FractionRing A] FractionRing B,
      ((galRestrict A (FractionRing A) (FractionRing B) B).toEquiv i) x

Tactic:
simp only [MulEquiv.toEquiv_eq_coe, EquivLike.coe_coe]

Result:
A : Type u_1
B : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : IsGalois (FractionRing A) (FractionRing B)
x : B
this✝¹ : IsIntegralClosure B A (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ (algebraMap A B) ((intNorm A B) x) =
    ∏ x_1 : FractionRing B ≃ₐ[FractionRing A] FractionRing B,
      ((galRestrict A (FractionRing A) (FractionRing B) B) x_1) x

Proof state:
A : Type u_1
B : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : IsGalois (FractionRing A) (FractionRing B)
x : B
this : IsIntegralClosure B A (FractionRing B)
⊢ (algebraMap A B) ((intNorm A B) x) = ∏ σ : B ≃ₐ[A] B, σ x

Tactic:
haveI : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) (FractionRing B) :=
  IsIntegralClosure.isLocalization _ (FractionRing A) _ _

Result:
A : Type u_1
B : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : IsGalois (FractionRing A) (FractionRing B)
x : B
this✝ : IsIntegralClosure B A (FractionRing B)
this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
⊢ (algebraMap A B) ((intNorm A B) x) = ∏ σ : B ≃ₐ[A] B, σ x

Proof state:
A : Type u_1
B : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : IsGalois (FractionRing A) (FractionRing B)
x : B
this✝¹ : IsIntegralClosure B A (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ (algebraMap A B) ((intNorm A B) x) =
    ∏ x_1 : FractionRing B ≃ₐ[FractionRing A] FractionRing B,
      ((galRestrict A (FractionRing A) (FractionRing B) B) x_1) x

Tactic:
convert (prod_galRestrict_eq_norm A (FractionRing A) (FractionRing B) B x).symm

Result:
no goals

Proof state:
A : Type u_1
B : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : IsGalois (FractionRing A) (FractionRing B)
x : B
this✝ : IsIntegralClosure B A (FractionRing B)
this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
⊢ (algebraMap A B) ((intNorm A B) x) = ∏ σ : B ≃ₐ[A] B, σ x

Tactic:
haveI : FiniteDimensional (FractionRing A) (FractionRing B) :=
  Module.Finite_of_isLocalization A B _ _ A⁰

Result:
A : Type u_1
B : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : IsGalois (FractionRing A) (FractionRing B)
x : B
this✝¹ : IsIntegralClosure B A (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ (algebraMap A B) ((intNorm A B) x) = ∏ σ : B ≃ₐ[A] B, σ x

Proof state:
A : Type u_1
B : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : IsGalois (FractionRing A) (FractionRing B)
x : B
this✝¹ : IsIntegralClosure B A (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ (algebraMap A B) ((intNorm A B) x) = ∏ σ : B ≃ₐ[A] B, σ x

Tactic:
rw [← (galRestrict A (FractionRing A) (FractionRing B) B).toEquiv.prod_comp]

Result:
A : Type u_1
B : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : IsGalois (FractionRing A) (FractionRing B)
x : B
this✝¹ : IsIntegralClosure B A (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ (algebraMap A B) ((intNorm A B) x) =
    ∏ i : FractionRing B ≃ₐ[FractionRing A] FractionRing B,
      ((galRestrict A (FractionRing A) (FractionRing B) B).toEquiv i) x