-- Mathlib/NumberTheory/NumberField/Norm.lean
theorem dvd_norm [IsGalois K L] (x : 𝓞 L) : x ∣ algebraMap (𝓞 K) (𝓞 L) (norm K x)

Proof state:
case 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
hint : IsIntegral ℤ (∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x)
⊢ ↑((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x)) = ↑(x * ⟨∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x, hint⟩)

Tactic:
rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms]

Result:
case 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
hint : IsIntegral ℤ (∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x)
⊢ ∏ σ : L ≃ₐ[K] L, σ ↑x = ↑(x * ⟨∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x, hint⟩)

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
⊢ x ∣ (algebraMap (𝓞 K) (𝓞 L)) ((norm K) x)

Tactic:
have hint :
  IsIntegral ℤ (∏ σ ∈ univ.erase (AlgEquiv.refl : L ≃ₐ[K] L), σ x) :=
  IsIntegral.prod _ (fun σ _ =>
    ((RingOfIntegers.isIntegral_coe x).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
hint : IsIntegral ℤ (∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x)
⊢ 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
⊢ x ∣ (algebraMap (𝓞 K) (𝓞 L)) ((norm K) x)

Tactic:
classical
have hint :
  IsIntegral ℤ (∏ σ ∈ univ.erase (AlgEquiv.refl : L ≃ₐ[K] L), σ x) :=
  IsIntegral.prod _ (fun σ _ =>
    ((RingOfIntegers.isIntegral_coe x).map σ))
refine ⟨⟨_, hint⟩, ?_⟩
ext
rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms]
simp [← Finset.mul_prod_erase _ _ (mem_univ AlgEquiv.refl)]

Result:
no goals

Proof state:
case 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
hint : IsIntegral ℤ (∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x)
⊢ ∏ σ : L ≃ₐ[K] L, σ ↑x = ↑(x * ⟨∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x, hint⟩)

Tactic:
simp [← Finset.mul_prod_erase _ _ (mem_univ AlgEquiv.refl)]

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
hint : IsIntegral ℤ (∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x)
⊢ (algebraMap (𝓞 K) (𝓞 L)) ((norm K) x) = x * ⟨∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x, hint⟩

Tactic:
ext

Result:
case 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
hint : IsIntegral ℤ (∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x)
⊢ ↑((algebraMap (𝓞 K) (𝓞 L)) ((norm K) x)) = ↑(x * ⟨∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x, hint⟩)

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
hint : IsIntegral ℤ (∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x)
⊢ x ∣ (algebraMap (𝓞 K) (𝓞 L)) ((norm K) x)

Tactic:
refine ⟨⟨_, hint⟩, ?_⟩

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
hint : IsIntegral ℤ (∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x)
⊢ (algebraMap (𝓞 K) (𝓞 L)) ((norm K) x) = x * ⟨∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x, hint⟩