-- Mathlib/NumberTheory/NumberField/Norm.lean
theorem isUnit_norm_of_isGalois [IsGalois K L] {x : 𝓞 L} : IsUnit (norm K x) ↔ IsUnit x

Proof state:
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 : 𝓞 L
hx : IsUnit ((norm K) x)
⊢ IsUnit x

Tactic:
replace hx : IsUnit (algebraMap (𝓞 K) (𝓞 L) <| norm K x) := hx.map (algebraMap (𝓞 K) <| 𝓞 L)

Result:
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 : 𝓞 L
hx : IsUnit ((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))
⊢ IsUnit x

Proof state:
case h.e'_3.h.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 : 𝓞 L
hx : IsUnit ((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))
⊢ (∏ σ ∈ univ \ {AlgEquiv.refl}, σ ↑x) * ∏ σ ∈ {AlgEquiv.refl}, σ ↑x = ↑((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))

Tactic:
rw [prod_sdiff <| subset_univ _, ← norm_eq_prod_automorphisms, coe_algebraMap_norm]

Result:
no goals

Proof state:
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 : 𝓞 L
hx : IsUnit ((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))
⊢ ⟨∏ σ ∈ univ \ {AlgEquiv.refl}, σ ↑x, ⋯⟩ * x = (algebraMap (𝓞 K) (𝓞 L)) ((norm K) x)

Tactic:
ext

Result:
case h.e'_3.h
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 : 𝓞 L
hx : IsUnit ((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))
⊢ ↑(⟨∏ σ ∈ univ \ {AlgEquiv.refl}, σ ↑x, ⋯⟩ * x) = ↑((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))

Proof state:
case h.e'_3.h
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 : 𝓞 L
hx : IsUnit ((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))
⊢ ↑(⟨∏ σ ∈ univ \ {AlgEquiv.refl}, σ ↑x, ⋯⟩ * x) = ↑((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))

Tactic:
convert_to ((univ \ {AlgEquiv.refl}).prod fun σ : L ≃ₐ[K] L => σ x) *
  ∏ σ ∈ {(AlgEquiv.refl : L ≃ₐ[K] L)}, σ x = _

Result:
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 : 𝓞 L
hx : IsUnit ((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))
⊢ ↑(⟨∏ σ ∈ univ \ {AlgEquiv.refl}, σ ↑x, ⋯⟩ * x) = (∏ σ ∈ univ \ {AlgEquiv.refl}, σ ↑x) * ∏ σ ∈ {AlgEquiv.refl}, σ ↑x

case h.e'_3.h.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 : 𝓞 L
hx : IsUnit ((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))
⊢ (∏ σ ∈ univ \ {AlgEquiv.refl}, σ ↑x) * ∏ σ ∈ {AlgEquiv.refl}, σ ↑x = ↑((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))

Proof state:
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 : 𝓞 L
hx : IsUnit ((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))
⊢ IsUnit x

Tactic:
refine @isUnit_of_mul_isUnit_right (𝓞 L) _
  ⟨(univ \ {AlgEquiv.refl}).prod fun σ : L ≃ₐ[K] L => σ x,
    prod_mem fun σ _ => x.2.map (σ : L →+* L).toIntAlgHom⟩ _ ?_

Result:
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 : 𝓞 L
hx : IsUnit ((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))
⊢ IsUnit (⟨∏ σ ∈ univ \ {AlgEquiv.refl}, σ ↑x, ⋯⟩ * x)

Proof state:
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 : 𝓞 L
hx : IsUnit ((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))
⊢ IsUnit (⟨∏ σ ∈ univ \ {AlgEquiv.refl}, σ ↑x, ⋯⟩ * x)

Tactic:
convert hx using 1

Result:
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 : 𝓞 L
hx : IsUnit ((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))
⊢ ⟨∏ σ ∈ univ \ {AlgEquiv.refl}, σ ↑x, ⋯⟩ * x = (algebraMap (𝓞 K) (𝓞 L)) ((norm K) x)

Proof state:
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 : 𝓞 L
hx : IsUnit ((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x))
⊢ ↑(⟨∏ σ ∈ univ \ {AlgEquiv.refl}, σ ↑x, ⋯⟩ * x) = (∏ σ ∈ univ \ {AlgEquiv.refl}, σ ↑x) * ∏ σ ∈ {AlgEquiv.refl}, σ ↑x

Tactic:
rw [prod_singleton, AlgEquiv.coe_refl, _root_.id, RingOfIntegers.coe_eq_algebraMap, map_mul,
  RingOfIntegers.map_mk]

Result:
no goals

Proof state:
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 : 𝓞 L
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Tactic:
refine ⟨fun hx => ?_, IsUnit.map _⟩

Result:
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 : 𝓞 L
hx : IsUnit ((norm K) x)
⊢ IsUnit x