awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
F : Type u_1
inst : Field F
K : Type u_2
inst_1 : Field K
inst_2 : CharZero K
inst_3 : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst_4 : ∀ (i : ι), IsTotallyReal.{u_2} ↥(k i)
i : ι
⊢ IsTotallyReal.{u_2} ↥(⨆ (i : ι), k i)
have inr : ∀ (i : ι), k i ≤ maximalRealSubfield K
Tactic: rw [isTotallyReal_iff_le_maximalRealSubfield, iSup_le_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (hypothesis)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
h : Eq (α := Subfield K) (maximalRealSubfield K) ⊤
⊢ IsTotallyReal K
have this : Algebra.IsIntegral (↥⊤) K
Tactic: have : Algebra.IsIntegral (⊤ : Subfield K) K := Algebra.IsIntegral.tower_top ℚ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
h : Eq (α := Subfield K) (maximalRealSubfield K) ⊤
this : Algebra.IsIntegral (↥⊤) K
⊢ IsTotallyReal K
have rw : IsTotallyReal.{u_2} ↥⊤
Tactic: rw [← isTotallyReal_top_iff, isTotallyReal_iff_le_maximalRealSubfield, h]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
h : Eq (α := Subfield K) (maximalRealSubfield K) ⊤
this : Algebra.IsIntegral (↥⊤) K
rw : IsTotallyReal.{u_2} ↥⊤
⊢ IsTotallyReal K
have rw₁ : LE.le (α := Subfield K) ⊤ (maximalRealSubfield K)
Tactic: rw [← isTotallyReal_top_iff, isTotallyReal_iff_le_maximalRealSubfield, h]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsAlgebraic ℚ K
h : Eq (α := Subfield K) (maximalRealSubfield K) ⊤
this : Algebra.IsIntegral (↥⊤) K
rw : IsTotallyReal.{u_2} ↥⊤
rw₁ : LE.le (α := Subfield K) ⊤ (maximalRealSubfield K)
⊢ IsTotallyReal K
have rw₂ : LE.le.{u_2} (α := Subfield K) ⊤ ⊤
Tactic: rw [← isTotallyReal_top_iff, isTotallyReal_iff_le_maximalRealSubfield, h]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : NumberField K
h : IsTotallyComplex K
⊢ finrank ℚ K = 2 * nrComplexPlaces K
have rw : nrRealPlaces K + 2 * nrComplexPlaces K = 2 * nrComplexPlaces K
Tactic: rw [← card_add_two_mul_card_eq_rank, nrRealPlaces_eq_zero_iff.mpr h, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : NumberField K
h : IsTotallyComplex K
rw : nrRealPlaces K + 2 * nrComplexPlaces K = 2 * nrComplexPlaces K
⊢ finrank ℚ K = 2 * nrComplexPlaces K
have rw₁ : 0 + 2 * nrComplexPlaces K = 2 * nrComplexPlaces K
Tactic: rw [← card_add_two_mul_card_eq_rank, nrRealPlaces_eq_zero_iff.mpr h, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : NumberField K
h : IsTotallyComplex K
rw : nrRealPlaces K + 2 * nrComplexPlaces K = 2 * nrComplexPlaces K
rw₁ : 0 + 2 * nrComplexPlaces K = 2 * nrComplexPlaces K
⊢ finrank ℚ K = 2 * nrComplexPlaces K
have rw₂ : 2 * nrComplexPlaces K = 2 * nrComplexPlaces K
Tactic: rw [← card_add_two_mul_card_eq_rank, nrRealPlaces_eq_zero_iff.mpr h, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
Goal:
L : Type u_1
K : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : 𝓞 K
⊢ (norm K : (a : 𝓞 L) → 𝓞 K) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x) = x ^ finrank K L
have rw : (↑((norm K : (a : 𝓞 L) → 𝓞 K) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x)) : K) = (↑(x ^ finrank K L) : K)
Tactic: rw [RingOfIntegers.ext_iff, RingOfIntegers.coe_eq_algebraMap,
    RingOfIntegers.algebraMap_norm_algebraMap, Algebra.norm_algebraMap,
    RingOfIntegers.coe_eq_algebraMap, map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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)
⊢ (norm K : (a : 𝓞 L) → 𝓞 K) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x) = x ^ finrank K L
have 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)
Tactic: rw [RingOfIntegers.ext_iff, RingOfIntegers.coe_eq_algebraMap,
    RingOfIntegers.algebraMap_norm_algebraMap, Algebra.norm_algebraMap,
    RingOfIntegers.coe_eq_algebraMap, map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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)
⊢ (norm K : (a : 𝓞 L) → 𝓞 K) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x) = x ^ finrank K L
have 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)
Tactic: rw [RingOfIntegers.ext_iff, RingOfIntegers.coe_eq_algebraMap,
    RingOfIntegers.algebraMap_norm_algebraMap, Algebra.norm_algebraMap,
    RingOfIntegers.coe_eq_algebraMap, map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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)
⊢ (norm K : (a : 𝓞 L) → 𝓞 K) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x) = x ^ finrank K L
have rw₃ : HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) x : K) (finrank K L) = (↑(x ^ finrank K L) : K)
Tactic: rw [RingOfIntegers.ext_iff, RingOfIntegers.coe_eq_algebraMap,
    RingOfIntegers.algebraMap_norm_algebraMap, Algebra.norm_algebraMap,
    RingOfIntegers.coe_eq_algebraMap, map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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)
⊢ (norm K : (a : 𝓞 L) → 𝓞 K) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x) = x ^ finrank K L
have 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)
Tactic: rw [RingOfIntegers.ext_iff, RingOfIntegers.coe_eq_algebraMap,
    RingOfIntegers.algebraMap_norm_algebraMap, Algebra.norm_algebraMap,
    RingOfIntegers.coe_eq_algebraMap, map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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)
⊢ (norm K : (a : 𝓞 L) → 𝓞 K) ((algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) x) = x ^ finrank K L
have 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)
Tactic: rw [RingOfIntegers.ext_iff, RingOfIntegers.coe_eq_algebraMap,
    RingOfIntegers.algebraMap_norm_algebraMap, Algebra.norm_algebraMap,
    RingOfIntegers.coe_eq_algebraMap, map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (hypothesis)
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
⊢ 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))
Tactic: have hint :
    IsIntegral ℤ (∏ σ ∈ univ.erase (AlgEquiv.refl : Gal(L/K)), σ x) :=
    IsIntegral.prod _ (fun σ _ =>
      ((RingOfIntegers.isIntegral_coe x).map σ))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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)
have 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
Tactic: refine ⟨⟨_, hint⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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))
⊢ (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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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))
⊢ (↑((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)
have 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)
Tactic: rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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
⊢ x ∣ (algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x)
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)
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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)
⊢ x ∣ (algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x)
have 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
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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
⊢ x ∣ (algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x)
have 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)
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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)
⊢ x ∣ (algebraMap (𝓞 K) (𝓞 L) : (a : 𝓞 K) → 𝓞 L) ((norm K : (a : 𝓞 L) → 𝓞 K) x)
have 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)
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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
⊢ Eq.{u_2 + 1} (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) ((norm F : (a : 𝓞 L) → 𝓞 F) x) : 𝓞 K)
    ((norm K : (a : 𝓞 L) → 𝓞 K) x : 𝓞 K)
have 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)
Tactic: rw [RingOfIntegers.ext_iff, coe_norm, coe_norm, coe_norm, Algebra.norm_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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)
⊢ Eq.{u_2 + 1} (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) ((norm F : (a : 𝓞 L) → 𝓞 F) x) : 𝓞 K)
    ((norm K : (a : 𝓞 L) → 𝓞 K) x : 𝓞 K)
have 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)
Tactic: rw [RingOfIntegers.ext_iff, coe_norm, coe_norm, coe_norm, Algebra.norm_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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)
⊢ Eq.{u_2 + 1} (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) ((norm F : (a : 𝓞 L) → 𝓞 F) x) : 𝓞 K)
    ((norm K : (a : 𝓞 L) → 𝓞 K) x : 𝓞 K)
have 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)
Tactic: rw [RingOfIntegers.ext_iff, coe_norm, coe_norm, coe_norm, Algebra.norm_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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)
⊢ Eq.{u_2 + 1} (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) ((norm F : (a : 𝓞 L) → 𝓞 F) x) : 𝓞 K)
    ((norm K : (a : 𝓞 L) → 𝓞 K) x : 𝓞 K)
have 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)
Tactic: rw [RingOfIntegers.ext_iff, coe_norm, coe_norm, coe_norm, Algebra.norm_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (goal)
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)
⊢ Eq.{u_2 + 1} (α := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) ((norm F : (a : 𝓞 L) → 𝓞 F) x) : 𝓞 K)
    ((norm K : (a : 𝓞 L) → 𝓞 K) x : 𝓞 K)
have rw₄ : Eq.{u_2 + 1} (α := K) ((Algebra.norm K : (a : L) → K) (↑x : L) : K) ((Algebra.norm K : (a : L) → K) (↑x : L) : K)
Tactic: rw [RingOfIntegers.ext_iff, coe_norm, coe_norm, coe_norm, Algebra.norm_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (hypothesis)
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)
⊢ IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) ↔ IsUnit x
have this₁ : FiniteDimensional F ↥L
Tactic: haveI : FiniteDimensional F L := FiniteDimensional.right K F L
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Norm (hypothesis)
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
⊢ IsUnit.{u_2} (M := 𝓞 K) ((norm K : (a : 𝓞 F) → 𝓞 K) x : 𝓞 K) ↔ IsUnit x
have this₁ : IsGalois F ↥L
Tactic: haveI : IsGalois F L := IsGalois.tower_top_of_isGalois K F L