[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
x : { x // x ∈ 𝓞 K }
⊢ ↑(norm K) (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) x) = x ^ finrank K L
[PROOFSTEP]
rw [← Subtype.coe_inj, RingOfIntegers.coe_norm_algebraMap, Algebra.norm_algebraMap, SubsemiringClass.coe_pow]
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
classical
refine' ⟨fun hx => _, IsUnit.map _⟩
replace hx : IsUnit (algebraMap (𝓞 K) (𝓞 L) <| norm K x) := hx.map (algebraMap (𝓞 K) <| 𝓞 L)
refine'
  @isUnit_of_mul_isUnit_right (𝓞 L) _
    ⟨(univ \ { AlgEquiv.refl }).prod fun σ : L ≃ₐ[K] L => σ x,
      prod_mem fun σ _ => map_isIntegral (σ : L →+* L).toIntAlgHom x.2⟩
    _ _
convert hx using 1
ext
push_cast
convert_to
  ((univ \ { AlgEquiv.refl }).prod fun σ : L ≃ₐ[K] L => σ x) * ∏ σ : L ≃ₐ[K] L in { AlgEquiv.refl }, σ (x : L) = _
· rw [prod_singleton, AlgEquiv.coe_refl, _root_.id]
· rw [prod_sdiff <| subset_univ _, ← norm_eq_prod_automorphisms, coe_algebraMap_norm]
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
refine' ⟨fun hx => _, IsUnit.map _⟩
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(norm K) x)
⊢ IsUnit x
[PROOFSTEP]
replace hx : IsUnit (algebraMap (𝓞 K) (𝓞 L) <| norm K x) := hx.map (algebraMap (𝓞 K) <| 𝓞 L)
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
⊢ IsUnit x
[PROOFSTEP]
refine'
  @isUnit_of_mul_isUnit_right (𝓞 L) _
    ⟨(univ \ { AlgEquiv.refl }).prod fun σ : L ≃ₐ[K] L => σ x,
      prod_mem fun σ _ => map_isIntegral (σ : L →+* L).toIntAlgHom x.2⟩
    _ _
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
⊢ IsUnit
    ({ val := ∏ σ in univ \ {AlgEquiv.refl}, ↑σ ↑x, property := (_ : ∏ c in univ \ {AlgEquiv.refl}, ↑c ↑x ∈ 𝓞 L) } * x)
[PROOFSTEP]
convert hx using 1
[GOAL]
case h.e'_3
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
⊢ { val := ∏ σ in univ \ {AlgEquiv.refl}, ↑σ ↑x, property := (_ : ∏ c in univ \ {AlgEquiv.refl}, ↑c ↑x ∈ 𝓞 L) } * x =
    ↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x)
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.a
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
⊢ ↑({ val := ∏ σ in univ \ {AlgEquiv.refl}, ↑σ ↑x, property := (_ : ∏ c in univ \ {AlgEquiv.refl}, ↑c ↑x ∈ 𝓞 L) } * x) =
    ↑(↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_3.a
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
⊢ (∏ x_1 in univ \ {AlgEquiv.refl}, ↑x_1 ↑x) * ↑x = ↑(↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
[PROOFSTEP]
convert_to
  ((univ \ { AlgEquiv.refl }).prod fun σ : L ≃ₐ[K] L => σ x) * ∏ σ : L ≃ₐ[K] L in { AlgEquiv.refl }, σ (x : L) = _
[GOAL]
case h.e'_2
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
⊢ (∏ x_1 in univ \ {AlgEquiv.refl}, ↑x_1 ↑x) * ↑x =
    (∏ σ in univ \ {AlgEquiv.refl}, ↑σ ↑x) * ∏ σ in {AlgEquiv.refl}, ↑σ ↑x
[PROOFSTEP]
rw [prod_singleton, AlgEquiv.coe_refl, _root_.id]
[GOAL]
case h.e'_3.a.convert_2
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
⊢ (∏ σ in univ \ {AlgEquiv.refl}, ↑σ ↑x) * ∏ σ in {AlgEquiv.refl}, ↑σ ↑x =
    ↑(↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
[PROOFSTEP]
rw [prod_sdiff <| subset_univ _, ← norm_eq_prod_automorphisms, coe_algebraMap_norm]
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
⊢ x ∣ ↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x)
[PROOFSTEP]
classical
have hint : ∏ σ : L ≃ₐ[K] L in univ.erase AlgEquiv.refl, σ x ∈ 𝓞 L :=
  Subalgebra.prod_mem _ fun σ _ => (mem_ringOfIntegers _ _).2 (map_isIntegral σ (RingOfIntegers.isIntegral_coe x))
refine' ⟨⟨_, hint⟩, Subtype.ext _⟩
rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms]
simp [← Finset.mul_prod_erase _ _ (mem_univ AlgEquiv.refl)]
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
⊢ x ∣ ↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x)
[PROOFSTEP]
have hint : ∏ σ : L ≃ₐ[K] L in univ.erase AlgEquiv.refl, σ x ∈ 𝓞 L :=
  Subalgebra.prod_mem _ fun σ _ => (mem_ringOfIntegers _ _).2 (map_isIntegral σ (RingOfIntegers.isIntegral_coe x))
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hint : ∏ σ in erase univ AlgEquiv.refl, ↑σ ↑x ∈ 𝓞 L
⊢ x ∣ ↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x)
[PROOFSTEP]
refine' ⟨⟨_, hint⟩, Subtype.ext _⟩
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hint : ∏ σ in erase univ AlgEquiv.refl, ↑σ ↑x ∈ 𝓞 L
⊢ ↑(↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x)) =
    ↑(x * { val := ∏ σ in erase univ AlgEquiv.refl, ↑σ ↑x, property := hint })
[PROOFSTEP]
rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms]
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hint : ∏ σ in erase univ AlgEquiv.refl, ↑σ ↑x ∈ 𝓞 L
⊢ ∏ σ : L ≃ₐ[K] L, ↑σ ↑x = ↑(x * { val := ∏ σ in erase univ AlgEquiv.refl, ↑σ ↑x, property := hint })
[PROOFSTEP]
simp [← Finset.mul_prod_erase _ _ (mem_univ AlgEquiv.refl)]
[GOAL]
L : Type u_1
K : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
F : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Algebra K F
inst✝⁶ : IsSeparable K F
inst✝⁵ : FiniteDimensional K F
inst✝⁴ : IsSeparable K L
inst✝³ : Algebra F L
inst✝² : IsSeparable F L
inst✝¹ : FiniteDimensional F L
inst✝ : IsScalarTower K F L
x : { x // x ∈ 𝓞 L }
⊢ ↑(norm K) (↑(norm F) x) = ↑(norm K) x
[PROOFSTEP]
rw [← Subtype.coe_inj, norm_apply_coe, norm_apply_coe, norm_apply_coe, Algebra.norm_norm]
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : { x // x ∈ 𝓞 F }
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
letI : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : { x // x ∈ 𝓞 F }
this : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
let L := normalClosure K F (AlgebraicClosure F)
[GOAL]
L✝ : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L✝
inst✝⁶ : Algebra K L✝
inst✝⁵ : FiniteDimensional K L✝
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : { x // x ∈ 𝓞 F }
this : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField F (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
haveI : FiniteDimensional F L := FiniteDimensional.right K F L
[GOAL]
L✝ : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L✝
inst✝⁶ : Algebra K L✝
inst✝⁵ : FiniteDimensional K L✝
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : { x // x ∈ 𝓞 F }
this✝ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField F (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this : FiniteDimensional F { x // x ∈ L }
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
haveI : IsAlgClosure K (AlgebraicClosure F) :=
  IsAlgClosure.ofAlgebraic K F (AlgebraicClosure F) (Algebra.isAlgebraic_of_finite K F)
[GOAL]
L✝ : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L✝
inst✝⁶ : Algebra K L✝
inst✝⁵ : FiniteDimensional K L✝
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : { x // x ∈ 𝓞 F }
this✝¹ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField F (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝ : FiniteDimensional F { x // x ∈ L }
this : IsAlgClosure K (AlgebraicClosure F)
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
haveI : IsGalois F L := IsGalois.tower_top_of_isGalois K F L
[GOAL]
L✝ : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L✝
inst✝⁶ : Algebra K L✝
inst✝⁵ : FiniteDimensional K L✝
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : { x // x ∈ 𝓞 F }
this✝² : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField F (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝¹ : FiniteDimensional F { x // x ∈ L }
this✝ : IsAlgClosure K (AlgebraicClosure F)
this : IsGalois F { x // x ∈ L }
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
calc
  IsUnit (norm K x) ↔ IsUnit ((norm K) x ^ finrank F L) := (isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)).symm
  _ ↔ IsUnit (norm K (algebraMap (𝓞 F) (𝓞 L) x)) := by
    rw [← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x), norm_algebraMap F _, map_pow]
  _ ↔ IsUnit (algebraMap (𝓞 F) (𝓞 L) x) := (isUnit_norm_of_isGalois K)
  _ ↔ IsUnit (norm F (algebraMap (𝓞 F) (𝓞 L) x)) := (isUnit_norm_of_isGalois F).symm
  _ ↔ IsUnit (x ^ finrank F L) := (congr_arg IsUnit (norm_algebraMap F _)).to_iff
  _ ↔ IsUnit x := isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)
[GOAL]
L✝ : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L✝
inst✝⁶ : Algebra K L✝
inst✝⁵ : FiniteDimensional K L✝
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : { x // x ∈ 𝓞 F }
this✝² : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField F (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝¹ : FiniteDimensional F { x // x ∈ L }
this✝ : IsAlgClosure K (AlgebraicClosure F)
this : IsGalois F { x // x ∈ L }
⊢ IsUnit (↑(norm K) x ^ finrank F { x // x ∈ L }) ↔
    IsUnit (↑(norm K) (↑(algebraMap { x // x ∈ 𝓞 F } { x // x ∈ 𝓞 { x // x ∈ L } }) x))
[PROOFSTEP]
rw [← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x), norm_algebraMap F _, map_pow]
