awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this_1 :
  HasQuotient.Quotient ↥(↑1 : Submodule 𝒪 K) (B := Submodule 𝒪 ↥(↑1 : Submodule 𝒪 K))
      (Submodule.comap (Submodule.subtype (↑1 : Submodule 𝒪 K))
        (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) : Submodule 𝒪 K)) ≃ₗ[𝒪]
    HasQuotient.Quotient ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K) (B :=
      Submodule 𝒪 ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
      (Submodule.comap (Submodule.subtype (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
        (↑1 : Submodule 𝒪 K))
this :
  Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑1 : Submodule 𝒪 K) (B := Submodule 𝒪 ↥(↑1 : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑1 : Submodule 𝒪 K))
          (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) : Submodule 𝒪 K))) =
    Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K) (B :=
        Submodule 𝒪 ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
          (↑1 : Submodule 𝒪 K)))
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K :=
  LinearMap.BilinForm.dualBasis.{u_1, 0, u_1} (V := K) (K := ℚ) (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
    (Algebra.traceForm ℚ K) ⋯ b
hb :
  Eq (α := Submodule ℤ K)
    (Submodule.span ℤ (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
    (Submodule.restrictScalars.{0, u_2, u_1} ℤ (R := 𝒪) 1)
⊢ Eq (α := AddSubgroup K)
    (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule)
      (↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K))
    (AddSubgroup.closure
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b' : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
have refine_3 : Eq (α := Submodule ℤ K)
  ((AddSubgroup.toIntSubmodule : (a : AddSubgroup K) → Submodule ℤ K)
      (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule)
        (↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K)) :
    Submodule ℤ K)
  ((AddSubgroup.toIntSubmodule : (a : AddSubgroup K) → Submodule ℤ K)
      (AddSubgroup.closure
        (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b' : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))) :
    Submodule ℤ K)
Tactic: apply AddSubgroup.toIntSubmodule.injective
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this_1 :
  HasQuotient.Quotient ↥(↑1 : Submodule 𝒪 K) (B := Submodule 𝒪 ↥(↑1 : Submodule 𝒪 K))
      (Submodule.comap (Submodule.subtype (↑1 : Submodule 𝒪 K))
        (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) : Submodule 𝒪 K)) ≃ₗ[𝒪]
    HasQuotient.Quotient ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K) (B :=
      Submodule 𝒪 ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
      (Submodule.comap (Submodule.subtype (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
        (↑1 : Submodule 𝒪 K))
this :
  Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑1 : Submodule 𝒪 K) (B := Submodule 𝒪 ↥(↑1 : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑1 : Submodule 𝒪 K))
          (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) : Submodule 𝒪 K))) =
    Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K) (B :=
        Submodule 𝒪 ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
          (↑1 : Submodule 𝒪 K)))
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K :=
  LinearMap.BilinForm.dualBasis.{u_1, 0, u_1} (V := K) (K := ℚ) (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
    (Algebra.traceForm ℚ K) ⋯ b
hb :
  Eq (α := Submodule ℤ K)
    (Submodule.span ℤ (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
    (Submodule.restrictScalars.{0, u_2, u_1} ℤ (R := 𝒪) 1)
⊢ Eq (α := Submodule ℤ K)
    ((AddSubgroup.toIntSubmodule : (a : AddSubgroup K) → Submodule ℤ K)
        (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule)
          (↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K)) :
      Submodule ℤ K)
    ((AddSubgroup.toIntSubmodule : (a : AddSubgroup K) → Submodule ℤ K)
        (AddSubgroup.closure
          (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b' : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))) :
      Submodule ℤ K)
have refine_3 : Eq.{u_1 + 1} (α := Submodule ℤ K)
  ((AddSubgroup.toIntSubmodule : (a : AddSubgroup K) → Submodule ℤ K)
      (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule)
        (↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K)) :
    Submodule ℤ K)
  (LinearMap.BilinForm.dualSubmodule (Algebra.traceForm ℚ K) (Submodule.restrictScalars.{0, u_2, u_1} ℤ (R := 𝒪) 1) :
    Submodule ℤ K)
Tactic: rw [AddSubgroup.toIntSubmodule_closure, ← LinearMap.BilinForm.dualSubmodule_span_of_basis, hb]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this_1 :
  HasQuotient.Quotient ↥(↑1 : Submodule 𝒪 K) (B := Submodule 𝒪 ↥(↑1 : Submodule 𝒪 K))
      (Submodule.comap (Submodule.subtype (↑1 : Submodule 𝒪 K))
        (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) : Submodule 𝒪 K)) ≃ₗ[𝒪]
    HasQuotient.Quotient ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K) (B :=
      Submodule 𝒪 ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
      (Submodule.comap (Submodule.subtype (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
        (↑1 : Submodule 𝒪 K))
this :
  Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑1 : Submodule 𝒪 K) (B := Submodule 𝒪 ↥(↑1 : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑1 : Submodule 𝒪 K))
          (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) : Submodule 𝒪 K))) =
    Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K) (B :=
        Submodule 𝒪 ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
          (↑1 : Submodule 𝒪 K)))
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K :=
  LinearMap.BilinForm.dualBasis.{u_1, 0, u_1} (V := K) (K := ℚ) (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
    (Algebra.traceForm ℚ K) ⋯ b
hb :
  Eq (α := Submodule ℤ K)
    (Submodule.span ℤ (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
    (Submodule.restrictScalars.{0, u_2, u_1} ℤ (R := 𝒪) 1)
⊢ |Matrix.det (b'.toMatrix (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))| =
    |(↑(Matrix.det (n := Free.ChooseBasisIndex ℤ (𝓞 K))
            (Algebra.traceMatrix ℤ (B := 𝓞 K)
              (⇑(RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
                (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K))) :
        ℚ)|
have refine_4 : |Matrix.det (b'.toMatrix (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))| =
  |Matrix.det.{0, u_1} (n := Free.ChooseBasisIndex ℤ (𝓞 K))
      ((RingHom.mapMatrix (algebraMap ℤ ℚ) :
          (a : Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ) →
            Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ)
        (Algebra.traceMatrix ℤ (B := 𝓞 K)
          (⇑(RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K)))|
Tactic: rw [← eq_intCast (algebraMap ℤ ℚ), RingHom.map_det]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this_1 :
  HasQuotient.Quotient ↥(↑1 : Submodule 𝒪 K) (B := Submodule 𝒪 ↥(↑1 : Submodule 𝒪 K))
      (Submodule.comap (Submodule.subtype (↑1 : Submodule 𝒪 K))
        (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) : Submodule 𝒪 K)) ≃ₗ[𝒪]
    HasQuotient.Quotient ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K) (B :=
      Submodule 𝒪 ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
      (Submodule.comap (Submodule.subtype (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
        (↑1 : Submodule 𝒪 K))
this :
  Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑1 : Submodule 𝒪 K) (B := Submodule 𝒪 ↥(↑1 : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑1 : Submodule 𝒪 K))
          (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) : Submodule 𝒪 K))) =
    Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K) (B :=
        Submodule 𝒪 ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
          (↑1 : Submodule 𝒪 K)))
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K :=
  LinearMap.BilinForm.dualBasis.{u_1, 0, u_1} (V := K) (K := ℚ) (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
    (Algebra.traceForm ℚ K) ⋯ b
hb :
  Eq (α := Submodule ℤ K)
    (Submodule.span ℤ (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
    (Submodule.restrictScalars.{0, u_2, u_1} ℤ (R := 𝒪) 1)
⊢ |Matrix.det (b'.toMatrix (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))| =
    |Matrix.det.{0, u_1} (n := Free.ChooseBasisIndex ℤ (𝓞 K))
        ((RingHom.mapMatrix (algebraMap ℤ ℚ) :
            (a : Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ) →
              Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ)
          (Algebra.traceMatrix ℤ (B := 𝓞 K)
            (⇑(RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K)))|
have refine_4 : Eq (α := Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ)
  (b'.toMatrix (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))
  ((RingHom.mapMatrix (algebraMap ℤ ℚ) :
      (a : Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ) →
        Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ)
    (Algebra.traceMatrix ℤ (B := 𝓞 K)
      (⇑(RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K)))
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this_1 :
  HasQuotient.Quotient ↥(↑1 : Submodule 𝒪 K) (B := Submodule 𝒪 ↥(↑1 : Submodule 𝒪 K))
      (Submodule.comap (Submodule.subtype (↑1 : Submodule 𝒪 K))
        (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) : Submodule 𝒪 K)) ≃ₗ[𝒪]
    HasQuotient.Quotient ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K) (B :=
      Submodule 𝒪 ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
      (Submodule.comap (Submodule.subtype (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
        (↑1 : Submodule 𝒪 K))
this :
  Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑1 : Submodule 𝒪 K) (B := Submodule 𝒪 ↥(↑1 : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑1 : Submodule 𝒪 K))
          (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) : Submodule 𝒪 K))) =
    Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K) (B :=
        Submodule 𝒪 ↥(↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑(↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹ : Submodule 𝒪 K))
          (↑1 : Submodule 𝒪 K)))
b : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K := integralBasis K
b' : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K :=
  LinearMap.BilinForm.dualBasis.{u_1, 0, u_1} (V := K) (K := ℚ) (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
    (Algebra.traceForm ℚ K) ⋯ b
hb :
  Eq (α := Submodule ℤ K)
    (Submodule.span ℤ (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
    (Submodule.restrictScalars.{0, u_2, u_1} ℤ (R := 𝒪) 1)
⊢ Eq (α := Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ)
    (b'.toMatrix (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K))
    ((RingHom.mapMatrix (algebraMap ℤ ℚ) :
        (a : Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ) →
          Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ)
      (Algebra.traceMatrix ℤ (B := 𝓞 K)
        (⇑(RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K)))
have refine_4 : ∀ (i j : Free.ChooseBasisIndex ℤ (𝓞 K)),
  b'.toMatrix (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K) i j =
    (RingHom.mapMatrix (algebraMap ℤ ℚ) :
        (a : Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ) →
          Matrix (Free.ChooseBasisIndex ℤ (𝓞 K)) (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ)
      (Algebra.traceMatrix ℤ (B := 𝓞 K)
        (⇑(RingOfIntegers.basis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℤ (𝓞 K)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → 𝓞 K))
      i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (hypothesis)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
⊢ Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
have this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : 𝒪)
Tactic: have := (differentIdeal ℤ 𝒪).absNorm_mem
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this :
  Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : 𝒪)
h : discr K = (↑(discr K).natAbs : ℤ)
⊢ Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
have inl : ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K).natAbs : 𝒪))
  (h : discr K = (↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
Tactic: rwa [absNorm_differentIdeal K, ← Int.cast_natCast, ← h] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this :
  Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : 𝒪)
h : discr K = (↑(discr K).natAbs : ℤ)
inl :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K).natAbs : 𝒪))
    (h : discr K = (↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
⊢ Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
have inl₁ : ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(↑(discr K).natAbs : ℤ) : 𝒪))
  (h : discr K = (↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
Tactic: rwa [absNorm_differentIdeal K, ← Int.cast_natCast, ← h] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this :
  Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : 𝒪)
h : discr K = (↑(discr K).natAbs : ℤ)
inl :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K).natAbs : 𝒪))
    (h : discr K = (↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
inl₁ :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(↑(discr K).natAbs : ℤ) : 𝒪))
    (h : discr K = (↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
⊢ Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
have inl₂ : ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)) (h : discr K = (↑(discr K).natAbs : ℤ)),
  Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
Tactic: rwa [absNorm_differentIdeal K, ← Int.cast_natCast, ← h] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this :
  Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : 𝒪)
h : discr K = -(↑(discr K).natAbs : ℤ)
⊢ Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
have inr : ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K).natAbs : 𝒪))
  (h : discr K = -(↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
Tactic: rwa [absNorm_differentIdeal K, ← Int.cast_natCast, Int.eq_neg_comm.mp h,
      Int.cast_neg, neg_mem_iff] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this :
  Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : 𝒪)
h : discr K = -(↑(discr K).natAbs : ℤ)
inr :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K).natAbs : 𝒪))
    (h : discr K = -(↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
⊢ Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
have inr₁ : ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(↑(discr K).natAbs : ℤ) : 𝒪))
  (h : discr K = -(↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
Tactic: rwa [absNorm_differentIdeal K, ← Int.cast_natCast, Int.eq_neg_comm.mp h,
      Int.cast_neg, neg_mem_iff] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this :
  Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : 𝒪)
h : discr K = -(↑(discr K).natAbs : ℤ)
inr :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K).natAbs : 𝒪))
    (h : discr K = -(↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
inr₁ :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(↑(discr K).natAbs : ℤ) : 𝒪))
    (h : discr K = -(↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
⊢ Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
have inr₂ : ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(-discr K) : 𝒪))
  (h : discr K = -(↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
Tactic: rwa [absNorm_differentIdeal K, ← Int.cast_natCast, Int.eq_neg_comm.mp h,
      Int.cast_neg, neg_mem_iff] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Different (goal)
Goal:
K : Type u_1
𝒪 : Type u_2
inst : Field K
inst_1 : NumberField K
inst_2 : CommRing 𝒪
inst_3 : Algebra 𝒪 K
inst_4 : IsFractionRing 𝒪 K
inst_5 : IsDedekindDomain 𝒪
inst_6 : CharZero 𝒪
inst_7 : Module.Finite ℤ 𝒪
this :
  Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑((Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪)) : 𝒪)
h : discr K = -(↑(discr K).natAbs : ℤ)
inr :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K).natAbs : 𝒪))
    (h : discr K = -(↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
inr₁ :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(↑(discr K).natAbs : ℤ) : 𝒪))
    (h : discr K = -(↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
inr₂ :
  ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(-discr K) : 𝒪))
    (h : discr K = -(↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
⊢ Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
have inr₃ : ∀ (this : Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (-(↑(discr K) : 𝒪)))
  (h : discr K = -(↑(discr K).natAbs : ℤ)), Membership.mem (γ := Ideal 𝒪) (differentIdeal ℤ 𝒪) (↑(discr K) : 𝒪)
Tactic: rwa [absNorm_differentIdeal K, ← Int.cast_natCast, Int.eq_neg_comm.mp h,
      Int.cast_neg, neg_mem_iff] at this
Cleared hypotheses: this, h