awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional.{0, u_2} ℚ ↥K
hK₁ :
  Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
      |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
this_1 : CharZero.{u_2} ↥K
this : NumberField.{u_2} ↥K
w₀ : InfinitePlace ↥K
pos :
  ∀ (hw₀ : w₀.IsReal),
    Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
      ({K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
          Set.Nonempty.{u_2} (α := InfinitePlace ↥(↑K : IntermediateField ℚ A))
              {w : InfinitePlace ↥(↑K : IntermediateField ℚ A) | w.IsReal} ∧
            |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)} ∪
        {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
          Set.Nonempty.{u_2} (α := InfinitePlace ↥(↑K : IntermediateField ℚ A))
              {w : InfinitePlace ↥(↑K : IntermediateField ℚ A) | w.IsComplex} ∧
            |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)})
      (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
⊢ Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    ({K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
        Set.Nonempty.{u_2} (α := InfinitePlace ↥(↑K : IntermediateField ℚ A))
            {w : InfinitePlace ↥(↑K : IntermediateField ℚ A) | w.IsReal} ∧
          |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)} ∪
      {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
        Set.Nonempty.{u_2} (α := InfinitePlace ↥(↑K : IntermediateField ℚ A))
            {w : InfinitePlace ↥(↑K : IntermediateField ℚ A) | w.IsComplex} ∧
          |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)})
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
have neg : ∀ (hw₀ : ¬w₀.IsReal),
  Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    ({K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
        Set.Nonempty.{u_2} (α := InfinitePlace ↥(↑K : IntermediateField ℚ A))
            {w : InfinitePlace ↥(↑K : IntermediateField ℚ A) | w.IsReal} ∧
          |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)} ∪
      {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
        Set.Nonempty.{u_2} (α := InfinitePlace ↥(↑K : IntermediateField ℚ A))
            {w : InfinitePlace ↥(↑K : IntermediateField ℚ A) | w.IsComplex} ∧
          |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)})
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
Tactic: by_cases hw₀ : IsReal w₀
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional.{0, u_2} ℚ ↥K
hK₁ :
  Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
      |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
this_1 : CharZero.{u_2} ↥K
this : NumberField.{u_2} ↥K
w₀ : InfinitePlace ↥K
hw₀ : w₀.IsReal
⊢ Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    ({K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
        Set.Nonempty.{u_2} (α := InfinitePlace ↥(↑K : IntermediateField ℚ A))
            {w : InfinitePlace ↥(↑K : IntermediateField ℚ A) | w.IsReal} ∧
          |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)} ∪
      {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
        Set.Nonempty.{u_2} (α := InfinitePlace ↥(↑K : IntermediateField ℚ A))
            {w : InfinitePlace ↥(↑K : IntermediateField ℚ A) | w.IsComplex} ∧
          |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)})
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
have pos : Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
  {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
    Set.Nonempty.{u_2} (α := InfinitePlace ↥(↑K : IntermediateField ℚ A))
        {w : InfinitePlace ↥(↑K : IntermediateField ℚ A) | w.IsReal} ∧
      |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}
  (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
Tactic: apply Set.mem_union_left
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional.{0, u_2} ℚ ↥K
hK₁ :
  Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
      |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
this_1 : CharZero.{u_2} ↥K
this : NumberField.{u_2} ↥K
w₀ : InfinitePlace ↥K
hw₀ : ¬w₀.IsReal
⊢ Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    ({K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
        Set.Nonempty.{u_2} (α := InfinitePlace ↥(↑K : IntermediateField ℚ A))
            {w : InfinitePlace ↥(↑K : IntermediateField ℚ A) | w.IsReal} ∧
          |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)} ∪
      {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
        Set.Nonempty.{u_2} (α := InfinitePlace ↥(↑K : IntermediateField ℚ A))
            {w : InfinitePlace ↥(↑K : IntermediateField ℚ A) | w.IsComplex} ∧
          |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)})
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
have neg : Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
  {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
    Set.Nonempty.{u_2} (α := InfinitePlace ↥(↑K : IntermediateField ℚ A))
        {w : InfinitePlace ↥(↑K : IntermediateField ℚ A) | w.IsComplex} ∧
      |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}
  (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
Tactic: apply Set.mem_union_right
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ discr K ≠ 0
have rw : Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
    (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) ≠
  (↑0 : ℚ)
Tactic: rw [← (Int.cast_injective (α := ℚ)).ne_iff, coe_discr]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
b : Basis.{u_2, 0, u_1} ι ℤ (𝓞 K)
b₀ : Basis.{u_2, 0, u_1} ι ℤ (𝓞 K) :=
  Basis.reindex (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
    (RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K))
    (Basis.indexEquiv (RingOfIntegers.basis K) b : Equiv.{u_1 + 1, u_2 + 1} (Free.ChooseBasisIndex ℤ (𝓞 K)) ι)
⊢ Algebra.discr.{0, u_1, u_2} (ι := ι) ℤ (B := 𝓞 K) (⇑b : (a : ι) → 𝓞 K) = discr K
have rw : Algebra.discr.{0, u_1, u_2} (ι := ι) ℤ (B := 𝓞 K) (⇑b₀ : (a : ι) → 𝓞 K) = discr K
Tactic: rw [Algebra.discr_eq_discr (𝓞 K) b b₀, Basis.coe_reindex, Algebra.discr_reindex]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
b : Basis.{u_2, 0, u_1} ι ℤ (𝓞 K)
b₀ : Basis.{u_2, 0, u_1} ι ℤ (𝓞 K) :=
  Basis.reindex (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
    (RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K))
    (Basis.indexEquiv (RingOfIntegers.basis K) b : Equiv.{u_1 + 1, u_2 + 1} (Free.ChooseBasisIndex ℤ (𝓞 K)) ι)
rw : Algebra.discr.{0, u_1, u_2} (ι := ι) ℤ (B := 𝓞 K) (⇑b₀ : (a : ι) → 𝓞 K) = discr K
⊢ Algebra.discr.{0, u_1, u_2} (ι := ι) ℤ (B := 𝓞 K) (⇑b : (a : ι) → 𝓞 K) = discr K
have rw₁ : Algebra.discr.{0, u_1, u_2} (ι := ι) ℤ (B := 𝓞 K)
    (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
      (⇑(RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K)
      (⇑(Equiv.symm (Basis.indexEquiv (RingOfIntegers.basis K) b) :
            Equiv.{u_2 + 1, u_1 + 1} ι (Free.ChooseBasisIndex ℤ (𝓞 K))) :
        (a : ι) → Free.ChooseBasisIndex ℤ (𝓞 K))) =
  discr K
Tactic: rw [Algebra.discr_eq_discr (𝓞 K) b b₀, Basis.coe_reindex, Algebra.discr_reindex]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
b : Basis.{u_2, 0, u_1} ι ℤ (𝓞 K)
b₀ : Basis.{u_2, 0, u_1} ι ℤ (𝓞 K) :=
  Basis.reindex (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
    (RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K))
    (Basis.indexEquiv (RingOfIntegers.basis K) b : Equiv.{u_1 + 1, u_2 + 1} (Free.ChooseBasisIndex ℤ (𝓞 K)) ι)
rw : Algebra.discr.{0, u_1, u_2} (ι := ι) ℤ (B := 𝓞 K) (⇑b₀ : (a : ι) → 𝓞 K) = discr K
rw₁ :
  Algebra.discr.{0, u_1, u_2} (ι := ι) ℤ (B := 𝓞 K)
      (Function.comp (β := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K)
        (⇑(Equiv.symm (Basis.indexEquiv (RingOfIntegers.basis K) b) :
              Equiv.{u_2 + 1, u_1 + 1} ι (Free.ChooseBasisIndex ℤ (𝓞 K))) :
          (a : ι) → Free.ChooseBasisIndex ℤ (𝓞 K))) =
    discr K
⊢ Algebra.discr.{0, u_1, u_2} (ι := ι) ℤ (B := 𝓞 K) (⇑b : (a : ι) → 𝓞 K) = discr K
have rw₂ : Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (B := 𝓞 K)
    (⇑(RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
      (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K) =
  discr K
Tactic: rw [Algebra.discr_eq_discr (𝓞 K) b b₀, Basis.coe_reindex, Algebra.discr_reindex]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
L : Type u_2
inst_2 : Field L
inst_3 : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ) (𝓞 K) (𝓞 L) :=
  (↑(AlgEquiv.mapIntegralClosure (AlgEquiv.restrictScalars ℤ f)) : ↥(integralClosure ℤ K) ≃ₗ[ℤ] ↥(integralClosure ℤ L))
⊢ discr K = discr L
have rw : Algebra.discr.{0, u_2, u_1} (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := L)
    (Function.comp (β := K) (⇑f : (a : K) → L)
      (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) =
  (↑(Algebra.discr.{0, u_2, u_1} (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (B := 𝓞 L)
        (⇑(Basis.map (RingOfIntegers.basis K) f₀ : Basis.{u_1, 0, u_2} (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 L)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 L)) :
    ℚ)
Tactic: rw [← Rat.intCast_inj, coe_discr, Algebra.discr_eq_discr_of_algEquiv (integralBasis K) f,
    ← discr_eq_discr L ((RingOfIntegers.basis K).map f₀)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
L : Type u_2
inst_2 : Field L
inst_3 : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ) (𝓞 K) (𝓞 L) :=
  (↑(AlgEquiv.mapIntegralClosure (AlgEquiv.restrictScalars ℤ f)) : ↥(integralClosure ℤ K) ≃ₗ[ℤ] ↥(integralClosure ℤ L))
⊢ Algebra.discr.{0, u_2, u_1} (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := L)
      (Function.comp (β := K) (⇑f : (a : K) → L)
        (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) =
    (algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (Algebra.discr.{0, u_2, u_1} (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (B := 𝓞 L)
        (⇑(Basis.map (RingOfIntegers.basis K) f₀ : Basis.{u_1, 0, u_2} (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 L)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 L))
have rw : Algebra.discr.{0, u_2, u_1} (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := L)
    (Function.comp (β := K) (⇑f : (a : K) → L)
      (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) =
  Algebra.discr.{0, u_2, u_1} (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := L)
    (⇑(Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L (Basis.map (RingOfIntegers.basis K) f₀) :
          Basis.{u_1, 0, u_2} (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ L) :
      (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → L)
Tactic: rw [← Algebra.discr_localizationLocalization ℤ (nonZeroDivisors ℤ) L]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
L : Type u_2
inst_2 : Field L
inst_3 : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ) (𝓞 K) (𝓞 L) :=
  (↑(AlgEquiv.mapIntegralClosure (AlgEquiv.restrictScalars ℤ f)) : ↥(integralClosure ℤ K) ≃ₗ[ℤ] ↥(integralClosure ℤ L))
⊢ Algebra.discr.{0, u_2, u_1} (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := L)
      (Function.comp (β := K) (⇑f : (a : K) → L)
        (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) =
    Algebra.discr.{0, u_2, u_1} (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := L)
      (⇑(Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L (Basis.map (RingOfIntegers.basis K) f₀) :
            Basis.{u_1, 0, u_2} (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ L) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → L)
have e_b : Eq (α := Free.ChooseBasisIndex ℤ (𝓞 K) → L)
  (Function.comp (β := K) (⇑f : (a : K) → L)
    (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))
  (⇑(Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L (Basis.map (RingOfIntegers.basis K) f₀) :
        Basis.{u_1, 0, u_2} (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ L) :
    (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → L)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
L : Type u_2
inst_2 : Field L
inst_3 : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ) (𝓞 K) (𝓞 L) :=
  (↑(AlgEquiv.mapIntegralClosure (AlgEquiv.restrictScalars ℤ f)) : ↥(integralClosure ℤ K) ≃ₗ[ℤ] ↥(integralClosure ℤ L))
⊢ Eq (α := Free.ChooseBasisIndex ℤ (𝓞 K) → L)
    (Function.comp (β := K) (⇑f : (a : K) → L)
      (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))
    (⇑(Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L (Basis.map (RingOfIntegers.basis K) f₀) :
          Basis.{u_1, 0, u_2} (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ L) :
      (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → L)
have e_b : ∀ (x : Free.ChooseBasisIndex ℤ (𝓞 K)),
  Eq.{u_2 + 1} (α := L)
    (Function.comp (β := K) (⇑f : (a : K) → L)
        (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) x :
      L)
    (((Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L (Basis.map (RingOfIntegers.basis K) f₀) :
            Basis.{u_1, 0, u_2} (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ L) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → L)
        x :
      L)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
L : Type u_2
inst_2 : Field L
inst_3 : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : LinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℤ) (𝓞 K) (𝓞 L) :=
  (↑(AlgEquiv.mapIntegralClosure (AlgEquiv.restrictScalars ℤ f)) : ↥(integralClosure ℤ K) ≃ₗ[ℤ] ↥(integralClosure ℤ L))
x : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ Eq.{u_2 + 1} (α := L)
    (Function.comp (β := K) (⇑f : (a : K) → L)
        (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) x :
      L)
    (((Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L (Basis.map (RingOfIntegers.basis K) f₀) :
            Basis.{u_1, 0, u_2} (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ L) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → L)
        x :
      L)
have e_b : Eq.{u_2 + 1} (α := L)
  ((f : (a : K) → L)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (((RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
                (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K)
              x :
            𝓞 K) :
        K) :
    L)
  ((algebraMap (𝓞 L) L : (a : 𝓞 L) → L)
      ((f₀ : (a : 𝓞 K) → 𝓞 L)
          (((RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K)
            x) :
        𝓞 L) :
    L)
Tactic: simp only [Function.comp_apply, integralBasis_apply, Basis.localizationLocalization_apply,
    Basis.map_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
⊢ Algebra.discr (ι := Fin 1) ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ) =
    (Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default))
have rw : Matrix.det (n := Fin 1) (Algebra.traceMatrix ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ)) =
  (Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
    (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default))
Tactic: rw [Algebra.discr_def, Matrix.det_unique, Algebra.traceMatrix_apply, Algebra.traceForm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
rw :
  Matrix.det (n := Fin 1) (Algebra.traceMatrix ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ)) =
    (Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default))
⊢ Algebra.discr (ι := Fin 1) ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ) =
    (Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default))
have rw₁ : Algebra.traceMatrix (κ := Fin 1) ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ) default default =
  (Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
    (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default))
Tactic: rw [Algebra.discr_def, Matrix.det_unique, Algebra.traceMatrix_apply, Algebra.traceForm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
rw :
  Matrix.det (n := Fin 1) (Algebra.traceMatrix ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ)) =
    (Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default))
rw₁ :
  Algebra.traceMatrix (κ := Fin 1) ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ) default default =
    (Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default))
⊢ Algebra.discr (ι := Fin 1) ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ) =
    (Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default))
have rw₂ : Eq (α := ℤ)
  (((Algebra.traceForm ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → 𝓞 ℚ →ₗ[ℤ] ℤ) ((b : (a : Fin 1) → 𝓞 ℚ) default) : (a : 𝓞 ℚ) → ℤ)
      ((b : (a : Fin 1) → 𝓞 ℚ) default) :
    ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default)) :
    ℤ)
Tactic: rw [Algebra.discr_def, Matrix.det_unique, Algebra.traceMatrix_apply, Algebra.traceForm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
rw :
  Matrix.det (n := Fin 1) (Algebra.traceMatrix ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ)) =
    (Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default))
rw₁ :
  Algebra.traceMatrix (κ := Fin 1) ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ) default default =
    (Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default))
rw₂ :
  Eq (α := ℤ)
    (((Algebra.traceForm ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → 𝓞 ℚ →ₗ[ℤ] ℤ) ((b : (a : Fin 1) → 𝓞 ℚ) default) : (a : 𝓞 ℚ) → ℤ)
        ((b : (a : Fin 1) → 𝓞 ℚ) default) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default)) :
      ℤ)
⊢ Algebra.discr (ι := Fin 1) ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ) =
    (Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default))
have rw₃ : Eq (α := ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default)) :
    ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default)) :
    ℤ)
Tactic: rw [Algebra.discr_def, Matrix.det_unique, Algebra.traceMatrix_apply, Algebra.traceForm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
⊢ Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
have rw : Eq (α := ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
        ((LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv : (a : ℤ) → 𝓞 ℚ)
            ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
          𝓞 ℚ)
        ((LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv : (a : ℤ) → 𝓞 ℚ)
            ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
          𝓞 ℚ)) :
    ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
Tactic: rw [Basis.map_apply, RingEquiv.toAddEquiv_eq_coe, ← AddEquiv.toIntLinearEquiv_symm,
        AddEquiv.coe_toIntLinearEquiv, Basis.singleton_apply,
        show (AddEquiv.symm ↑ringOfIntegersEquiv) (1 : ℤ) = ringOfIntegersEquiv.symm 1 by rfl,
        map_one, mul_one]