awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
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₀)
⊢ 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:
apply Set.mem_union_left

Premises used: Set.mem_union_left
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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 : ℤ)}
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)

Tactic:
⟨⟨w₀, hw₀⟩, hK₁⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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 : ℤ)}
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)

Tactic:
exact ⟨⟨w₀, hw₀⟩, hK₁⟩
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
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₀)
⊢ 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:
apply Set.mem_union_right

Premises used: Set.mem_union_right
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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.IsComplex} ∧
        |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)

Tactic:
⟨⟨w₀, not_isReal_iff_isComplex.mp hw₀⟩, hK₁⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Iff.mp, NumberField.InfinitePlace.not_isReal_iff_isComplex
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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.IsComplex} ∧
        |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)

Tactic:
exact ⟨⟨w₀, not_isReal_iff_isComplex.mp hw₀⟩, hK₁⟩
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ (↑(discr K) : ℚ) =
    Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
      (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)

Tactic:
(Algebra.discr_localizationLocalization ℤ _ K (RingOfIntegers.basis K)).symm

Premises used: Int, NumberField.RingOfIntegers.basis, Algebra.discr_localizationLocalization, Eq.symm, Rat.ofInt
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
      (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) ≠
    (↑0 : ℚ)
⊢ discr K ≠ 0

Tactic:
rw [← (Int.cast_injective (α := ℚ)).ne_iff, coe_discr]

Premises used: Function.Injective.ne_iff, NumberField.coe_discr, Int.cast_injective
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
      (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) ≠
    (↑0 : ℚ)

Tactic:
Algebra.discr_not_zero_of_basis ℚ (integralBasis K)

Premises used: NumberField.integralBasis, Rat, Algebra.discr_not_zero_of_basis, Rat.ofInt
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ (B := K)
      (⇑(integralBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) ≠
    (↑0 : ℚ)

Tactic:
exact Algebra.discr_not_zero_of_basis ℚ (integralBasis K)

Premises used: NumberField.integralBasis, Rat, Algebra.discr_not_zero_of_basis
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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
rw₂ rw₃ :
  Algebra.discr (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (B := 𝓞 K)
      (⇑(RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K) =
    discr K
⊢ 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]

Premises used: Algebra.discr_eq_discr, Module.Basis.coe_reindex, NumberField.RingOfIntegers, Algebra.discr_reindex
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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))
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)) :
      ℚ)
⊢ discr K = discr 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₀)]

Premises used: NumberField.integralBasis, Module.Basis.map, Algebra.discr_eq_discr_of_algEquiv, NumberField.discr_eq_discr, Rat.intCast_inj, NumberField.RingOfIntegers.basis, NumberField.coe_discr, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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))
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)
⊢ 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))

Tactic:
rw [← Algebra.discr_localizationLocalization ℤ (nonZeroDivisors ℤ) L]

Premises used: nonZeroDivisors, Int, Algebra.discr_localizationLocalization
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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))
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)
⊢ 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:
congr 1
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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))
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)
⊢ 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:
ext
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
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)
⊢ 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:
simp only [Function.comp_apply, integralBasis_apply, Basis.localizationLocalization_apply,
    Basis.map_apply]

Premises used: NumberField.integralBasis_apply, Module.Basis.localizationLocalization_apply, Module.Basis.map_apply, Function.comp_apply
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
    ((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:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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
x : ℚ
⊢ Eq.{u_2 + 1} (α := L) ((f : (a : K) → L) ((algebraMap ℚ K : (a : ℚ) → K) x : K) : L)
    ((algebraMap ℚ L : (a : ℚ) → L) x : L)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
⊢ discr ℚ = Algebra.discr (ι := Fin 1) ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ)

Tactic:
(discr_eq_discr ℚ b).symm

Premises used: Rat, NumberField.discr_eq_discr, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
⊢ discr ℚ = Algebra.discr (ι := Fin 1) ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ)

Tactic:
convert! (discr_eq_discr ℚ b).symm

Premises used: Rat, NumberField.discr_eq_discr, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)) :
      ℤ)
rw₃ 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)) :
      ℤ)
⊢ Algebra.discr (ι := Fin 1) ℤ (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]

Premises used: Algebra.traceMatrix_apply, Algebra.traceForm_apply, Algebra.discr_def, Matrix.det_unique
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
⊢ Eq (α := 𝓞 ℚ) ((AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ) : (a : ℤ) → 𝓞 ℚ) 1)
    ((ringOfIntegersEquiv.symm : (a : ℤ) → 𝓞 ℚ) 1)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
rw : Eq (α := ℤ) (Matrix.trace (n := Fin 1) ((Algebra.leftMulMatrix b : (a : 𝓞 ℚ) → Matrix (Fin 1) (Fin 1) ℤ) 1)) 1
⊢ Eq (α := ℤ) ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ) (1 : ℤ)

Tactic:
rw [Algebra.trace_eq_matrix_trace b]

Premises used: Algebra.trace_eq_matrix_trace
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
⊢ Eq (α := ℤ) (Matrix.trace (n := Fin 1) ((Algebra.leftMulMatrix b : (a : 𝓞 ℚ) → Matrix (Fin 1) (Fin 1) ℤ) 1)) 1

Tactic:
simp