awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
L : Type u_1
K : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : 𝓞 L
⊢ Eq.{u_1 + 1} (α := L) ((↑((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x)) : L) : L)
    ((algebraMap K L : (a : K) → L) ((Algebra.norm K : (a : L) → K) (↑x : L) : K) : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
L : Type u_1
K : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : 𝓞 K
⊢ Eq (α := K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
        ((norm K : (a : 𝓞 L) → 𝓞 K) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x) : 𝓞 K) :
      K)
    ((Algebra.norm K : (a : L) → K) ((algebraMap K L : (a : K) → L) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) : L) :
      K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
L : Type u_1
K : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : 𝓞 K
rw : (↑((norm K : (a : 𝓞 L) → 𝓞 K) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x)) : K) = (↑(x ^ finrank K L) : K)
rw₁ :
  (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((norm K : (a : 𝓞 L) → 𝓞 K) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x) : 𝓞 K) =
    (↑(x ^ finrank K L) : K)
rw₂ :
  (Algebra.norm K : (a : L) → K) ((algebraMap K L : (a : K) → L) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) : L) =
    (↑(x ^ finrank K L) : K)
rw₃ : HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (finrank K L) = (↑(x ^ finrank K L) : K)
rw₄ :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (finrank K L) =
    (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (x ^ finrank K L)
rw₅ rw₆ :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (finrank K L) =
    HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (finrank K L)
⊢ (norm K : (a : 𝓞 L) → 𝓞 K) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x) = x ^ finrank K L

Tactic:
rw [RingOfIntegers.ext_iff, RingOfIntegers.coe_eq_algebraMap,
    RingOfIntegers.algebraMap_norm_algebraMap, Algebra.norm_algebraMap,
    RingOfIntegers.coe_eq_algebraMap, map_pow]

Premises used: map_pow, NumberField.RingOfIntegers.coe_eq_algebraMap, NumberField.RingOfIntegers.ext_iff, RingOfIntegers.algebraMap_norm_algebraMap, Algebra.norm_algebraMap
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
L : Type u_1
K : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : 𝓞 L
⊢ IsIntegral.{0, u_1} ℤ (A := L) (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L))

Tactic:
have hint :
    IsIntegral ℤ (∏ σ ∈ univ.erase (AlgEquiv.refl : Gal(L/K)), σ x) :=
    IsIntegral.prod _ (fun σ _ =>
      ((RingOfIntegers.isIntegral_coe x).map σ))
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
L : Type u_1
K : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : 𝓞 L
hint : IsIntegral.{0, u_1} ℤ (A := L) (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L))
⊢ x ∣ (algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x)

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

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
L : Type u_1
K : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : 𝓞 L
hint : IsIntegral.{0, u_1} ℤ (A := L) (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L))
refine :
  (algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x) =
    x *
      Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
        (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L)) hint
⊢ x ∣ (algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x)

Tactic:
refine ⟨⟨_, hint⟩, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
L : Type u_1
K : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : 𝓞 L
hint : IsIntegral.{0, u_1} ℤ (A := L) (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L))
h :
  (↑((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x)) : L) =
    (↑(x *
          Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
            (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L)) hint) :
      L)
⊢ (algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x) =
    x *
      Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
        (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L)) hint

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
L : Type u_1
K : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : 𝓞 L
hint : IsIntegral.{0, u_1} ℤ (A := L) (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L))
h :
  ∏ σ : Gal(L/K), (σ : (a : L) → L) (↑x : L) =
    (↑(x *
          Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
            (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L)) hint) :
      L)
⊢ (↑((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x)) : L) =
    (↑(x *
          Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
            (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L)) hint) :
      L)

Tactic:
rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms]

Premises used: Algebra.norm_eq_prod_automorphisms, RingOfIntegers.coe_algebraMap_norm
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
L : Type u_1
K : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : 𝓞 L
hint : IsIntegral.{0, u_1} ℤ (A := L) (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L))
⊢ ∏ σ : Gal(L/K), (σ : (a : L) → L) (↑x : L) =
    (↑(x *
          Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
            (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L)) hint) :
      L)

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

Premises used: Finset.mem_univ, Finset.mul_prod_erase, AlgEquiv.refl
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
L : Type u_1
K : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : 𝓞 L
have have₁ have₂ :
  ∀ (hint : IsIntegral.{0, u_1} ℤ (A := L) (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L))),
    x ∣ (algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x)
have₃ :
  ∀ (hint : IsIntegral.{0, u_1} ℤ (A := L) (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L))),
    (algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x) =
      x *
        Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
          (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L)) hint
h :
  ∀ (hint : IsIntegral.{0, u_1} ℤ (A := L) (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L))),
    (↑((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x)) : L) =
      (↑(x *
            Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
              (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L)) hint) :
        L)
h₁ :
  ∀ (hint : IsIntegral.{0, u_1} ℤ (A := L) (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L))),
    ∏ σ : Gal(L/K), (σ : (a : L) → L) (↑x : L) =
      (↑(x *
            Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := Subalgebra ℤ L) (integralClosure ℤ L) x)
              (∏ σ ∈ erase univ AlgEquiv.refl, (σ : (a : L) → L) (↑x : L)) hint) :
        L)
⊢ x ∣ (algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x)

Tactic:
classical
  have hint :
    IsIntegral ℤ (∏ σ ∈ univ.erase (AlgEquiv.refl : Gal(L/K)), σ 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)]

Premises used: Finset.mem_univ, Finset.mul_prod_erase, Algebra.norm_eq_prod_automorphisms, AlgEquiv.refl, RingOfIntegers.coe_algebraMap_norm
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
L : Type u_1
K : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : 𝓞 L
⊢ IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 L) → 𝓞 K) x : 𝓞 K) ↔ IsUnit x

Tactic:
⟨fun hx ↦ isUnit_of_dvd_unit (dvd_norm K x) (hx.map _), IsUnit.map _⟩

Premises used: Algebra.algebraMap, isUnit_of_dvd_unit, Iff.intro, IsUnit.map, NumberField.RingOfIntegers, RingOfIntegers.dvd_norm
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
L : Type u_1
K : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_3
inst_3 : Field F
inst_4 : Algebra K F
inst_5 : FiniteDimensional K F
inst_6 : Algebra F L
inst_7 : FiniteDimensional F L
inst_8 : IsScalarTower K F L
x : 𝓞 L
rw :
  Eq.{u_2 + 1} (α := K) (↑((norm K : (a : 𝓞 F) → 𝓞 K) ((norm F : (a : 𝓞 L) → 𝓞 F) x)) : K)
    (↑((norm K : (a : 𝓞 L) → 𝓞 K) x) : K)
rw₁ :
  Eq.{u_2 + 1} (α := K) ((Algebra.norm K : (a : F) → K) (↑((norm F : (a : 𝓞 L) → 𝓞 F) x) : F) : K)
    ((↑((norm K : (a : 𝓞 L) → 𝓞 K) x) : K) : K)
rw₂ :
  Eq.{u_2 + 1} (α := K) ((Algebra.norm K : (a : F) → K) ((Algebra.norm F : (a : L) → F) (↑x : L) : F) : K)
    ((↑((norm K : (a : 𝓞 L) → 𝓞 K) x) : K) : K)
rw₃ :
  Eq.{u_2 + 1} (α := K) ((Algebra.norm K : (a : F) → K) ((Algebra.norm F : (a : L) → F) (↑x : L) : F) : K)
    ((Algebra.norm K : (a : L) → K) (↑x : L) : K)
rw₄ rw₅ :
  Eq.{u_2 + 1} (α := K) ((Algebra.norm K : (a : L) → K) (↑x : L) : K) ((Algebra.norm K : (a : L) → K) (↑x : L) : K)
⊢ Eq.{u_2 + 1} (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) ((norm F : (a : 𝓞 L) → 𝓞 F) x) : 𝓞 K)
    ((norm K : (a : 𝓞 L) → 𝓞 K) x : 𝓞 K)

Tactic:
rw [RingOfIntegers.ext_iff, coe_norm, coe_norm, coe_norm, Algebra.norm_norm]

Premises used: RingOfIntegers.coe_norm, NumberField.RingOfIntegers.ext_iff, Algebra.norm_norm
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
K : Type u_2
inst : Field K
F : Type u_3
inst_1 : Field F
inst_2 : Algebra K F
inst_3 : FiniteDimensional K F
inst_4 : CharZero K
x : 𝓞 F
this : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
⊢ FiniteDimensional F ↥L

Tactic:
haveI : FiniteDimensional F L := FiniteDimensional.right K F L
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
K : Type u_2
inst : Field K
F : Type u_3
inst_1 : Field F
inst_2 : Algebra K F
inst_3 : FiniteDimensional K F
inst_4 : CharZero K
x : 𝓞 F
this_1 : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this : FiniteDimensional F ↥L
⊢ IsGalois F ↥L

Tactic:
haveI : IsGalois F L := IsGalois.tower_top_of_isGalois K F L
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
K : Type u_2
inst : Field K
F : Type u_3
inst_1 : Field F
inst_2 : Algebra K F
inst_3 : FiniteDimensional K F
inst_4 : CharZero K
x : 𝓞 F
this_1 : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this_2 : FiniteDimensional F ↥L
this : IsGalois F ↥L
⊢ IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) ↔
    IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L))

Tactic:
(isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)).symm

Premises used: isUnit_pow_iff, Iff.mp, pos_iff_ne_zero, Iff.symm, Module.finrank_pos
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
K : Type u_2
inst : Field K
F : Type u_3
inst_1 : Field F
inst_2 : Algebra K F
inst_3 : FiniteDimensional K F
inst_4 : CharZero K
x : 𝓞 F
this_1 : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this_2 : FiniteDimensional F ↥L
this : IsGalois F ↥L
rw :
  IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
    IsUnit.{u_2} (M := 𝓞 K)
      ((norm K : (a : 𝓞 F) → 𝓞 K) ((norm F : (a : 𝓞 ↥L) → 𝓞 F) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x)) : 𝓞 K)
rw₁ :
  IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
    IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) (x ^ finrank F ↥L) : 𝓞 K)
rw₂ rw₃ :
  IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
    IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L))
⊢ IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
    IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 ↥L) → 𝓞 K) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x) : 𝓞 K)

Tactic:
rw [← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x), norm_algebraMap F _, map_pow]

Premises used: Algebra.algebraMap, Membership.mem, RingOfIntegers.norm_algebraMap, Subtype, map_pow, RingOfIntegers.norm_norm, NumberField.RingOfIntegers, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
K : Type u_2
inst : Field K
F : Type u_3
inst_1 : Field F
inst_2 : Algebra K F
inst_3 : FiniteDimensional K F
inst_4 : CharZero K
x : 𝓞 F
this_1 : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this_2 : FiniteDimensional F ↥L
this : IsGalois F ↥L
⊢ IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 ↥L) → 𝓞 K) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x) : 𝓞 K) ↔
    IsUnit (M := 𝓞 ↥L) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x : 𝓞 ↥L)

Tactic:
isUnit_norm_of_isGalois K

Premises used: RingOfIntegers.isUnit_norm_of_isGalois
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
K : Type u_2
inst : Field K
F : Type u_3
inst_1 : Field F
inst_2 : Algebra K F
inst_3 : FiniteDimensional K F
inst_4 : CharZero K
x : 𝓞 F
this_1 : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this_2 : FiniteDimensional F ↥L
this : IsGalois F ↥L
⊢ IsUnit (M := 𝓞 ↥L) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x : 𝓞 ↥L) ↔
    IsUnit (M := 𝓞 F) ((norm F : (a : 𝓞 ↥L) → 𝓞 F) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x) : 𝓞 F)

Tactic:
(isUnit_norm_of_isGalois F).symm

Premises used: RingOfIntegers.isUnit_norm_of_isGalois, Iff.symm
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
K : Type u_2
inst : Field K
F : Type u_3
inst_1 : Field F
inst_2 : Algebra K F
inst_3 : FiniteDimensional K F
inst_4 : CharZero K
x : 𝓞 F
this_1 : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this_2 : FiniteDimensional F ↥L
this : IsGalois F ↥L
⊢ IsUnit (M := 𝓞 F) ((norm F : (a : 𝓞 ↥L) → 𝓞 F) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x) : 𝓞 F) ↔
    IsUnit (x ^ finrank F ↥L)

Tactic:
(congr_arg IsUnit (norm_algebraMap F _)).to_iff

Premises used: IsUnit, Eq.to_iff, RingOfIntegers.norm_algebraMap, congr_arg
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
K : Type u_2
inst : Field K
F : Type u_3
inst_1 : Field F
inst_2 : Algebra K F
inst_3 : FiniteDimensional K F
inst_4 : CharZero K
x : 𝓞 F
this_1 : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this_2 : FiniteDimensional F ↥L
this : IsGalois F ↥L
⊢ IsUnit (x ^ finrank F ↥L) ↔ IsUnit x

Tactic:
isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)

Premises used: isUnit_pow_iff, Iff.mp, pos_iff_ne_zero, Module.finrank_pos
-- Module: Mathlib.NumberTheory.NumberField.Norm
Goal:
K : Type u_2
inst : Field K
F : Type u_3
inst_1 : Field F
inst_2 : Algebra K F
inst_3 : FiniteDimensional K F
inst_4 : CharZero K
x : 𝓞 F
this_1 : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this_2 : FiniteDimensional F ↥L
this : IsGalois F ↥L
IsUnit :
  _root_.IsUnit (HPow.hPow (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) (finrank F ↥L)) ↔
    _root_.IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 ↥L) → 𝓞 K) ((algebraMap (𝓞 F) (𝓞 ↥L) : (a : 𝓞 F) → 𝓞 ↥L) x) : 𝓞 K)
⊢ _root_.IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) ↔ _root_.IsUnit x

Tactic:
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)

Premises used: Algebra.algebraMap, RingOfIntegers.isUnit_norm_of_isGalois, isUnit_pow_iff, IsUnit, Eq.to_iff, Membership.mem, RingOfIntegers.norm_algebraMap, Subtype, congr_arg, HPow.hPow, Iff.mp, NumberField.RingOfIntegers, RingOfIntegers.norm, pos_iff_ne_zero, DFunLike.coe, Iff.symm, Module.finrank_pos, Module.finrank
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
simp :
  Eq (α := ℝ)
    (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
      Norm.norm (E := adicCompletion K i) ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
    |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x) : ℝ)|⁻¹
⊢ Eq (α := ℝ) (∏ᶠ (w : FinitePlace K), (w : (a : K) → ℝ) (↑x : K)) |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x) : ℝ)|⁻¹

Tactic:
simp only [← finprod_comp_equiv equivHeightOneSpectrum.symm, equivHeightOneSpectrum_symm_apply]

Premises used: NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply, NumberField.FinitePlace.equivHeightOneSpectrum, finprod_comp_equiv, Equiv.symm
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
⊢ Eq (α := ℝ)
    (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
      Norm.norm (E := adicCompletion K i) ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
    |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x) : ℝ)|⁻¹

Tactic:
(inv_eq_of_mul_eq_one_left ?_).symm

Premises used: Eq.symm, inv_eq_of_mul_eq_one_left
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
refine :
  HMul.hMul (α := ℝ)
      (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
        Norm.norm (E := adicCompletion K i)
          ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
      |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x) : ℝ)| =
    1
⊢ Eq (α := ℝ)
    (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
      Norm.norm (E := adicCompletion K i) ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
    |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x) : ℝ)|⁻¹

Tactic:
refine (inv_eq_of_mul_eq_one_left ?_).symm

Premises used: Eq.symm, inv_eq_of_mul_eq_one_left
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
norm_cast :
  HMul.hMul (α := ℝ)
      (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
        Norm.norm (E := adicCompletion K i)
          ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
      (↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x| : ℝ) =
    1
⊢ HMul.hMul (α := ℝ)
      (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
        Norm.norm (E := adicCompletion K i)
          ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
      |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x) : ℝ)| =
    1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
⊢ Ne (α := Ideal (𝓞 K)) (span {x}) 0

Tactic:
simp [h_x_nezero]
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
⊢ Ne (α := Ideal (𝓞 K)) (span {x}) 0

Tactic:
have h_span_nezero : span {x} ≠ 0 := by simp [h_x_nezero]
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
rw :
  HMul.hMul (α := ℝ)
      (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
        Norm.norm (E := adicCompletion K i)
          ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) : ℝ) =
    1
⊢ HMul.hMul (α := ℝ)
      (∏ᶠ (i : HeightOneSpectrum (𝓞 K)),
        Norm.norm (E := adicCompletion K i)
          ((embedding i : (a : K) → adicCompletion K i) (↑x : K) : adicCompletion K i))
      (↑|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x| : ℝ) =
    1

Tactic:
rw [Int.abs_eq_natAbs, ← absNorm_span_singleton,
    ← finprod_heightOneSpectrum_factorization h_span_nezero, Int.cast_natCast]

Premises used: Int.cast_natCast, Ideal.absNorm_span_singleton, Ideal.finprod_heightOneSpectrum_factorization, Int.abs_eq_natAbs
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
⊢ t₀.Finite

Tactic:
simp only [← dvd_span_singleton, finite_factors h_span_nezero, t₀]

Premises used: Ideal.finite_factors, Ideal.dvd_span_singleton
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
⊢ t₀.Finite

Tactic:
have h_fin₀ : t₀.Finite := by simp only [← dvd_span_singleton, finite_factors h_span_nezero, t₀]
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
⊢ t₁ ⊆ t₀

Tactic:
simp [norm_eq_one_iff_notMem, t₁, t₀]

Premises used: NumberField.FinitePlace.norm_eq_one_iff_notMem
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : Ne (α := Ideal (𝓞 K)) (span {x}) 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    Norm.norm (E := adicCompletion K v) ((embedding v : (a : K) → adicCompletion K v) (↑x : K) : adicCompletion K v)
t₂ : Set (HeightOneSpectrum (𝓞 K)) :=
  mulSupport (M := ℝ) fun (v : HeightOneSpectrum (𝓞 K)) ↦
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (v.maxPowDividing (span {x}))) : ℝ)
⊢ t₁.Finite

Tactic:
have h_fin₁ : t₁.Finite := h_fin₀.subset <| by simp [norm_eq_one_iff_notMem, t₁, t₀]