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)
⊢ Nat.card.{u_1}
      (HasQuotient.Quotient ↥(↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K) (B :=
        Submodule 𝒪 ↥(↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K))
        (Submodule.comap (Submodule.subtype (↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K)) 1)) =
    (discr K).natAbs
have qify : Eq (α := ℚ)
  (↑(Nat.card.{u_1}
        (HasQuotient.Quotient ↥(↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K) (B :=
          Submodule 𝒪 ↥(↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K))
          (Submodule.comap (Submodule.subtype (↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K)) 1))) :
    ℚ)
  |(↑(discr K) : ℚ)|
Tactic: qify
-- 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 (α := ℚ)
    (↑(Nat.card.{u_1}
          (HasQuotient.Quotient ↥(↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K) (B :=
            Submodule 𝒪 ↥(↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K))
            (Submodule.comap (Submodule.subtype (↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K)) 1))) :
      ℚ)
    |(↑(discr K) : ℚ)|
have refine_1 : LE.le.{u_1} (α := AddSubgroup K) (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule) 1)
  (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule)
    (↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K))
Tactic: refine (AddSubgroup.relIndex_eq_abs_det (1 : Submodule 𝒪 K).toAddSubgroup (FractionalIdeal.dual
    ℤ ℚ 1 : FractionalIdeal 𝒪⁰ K).coeToSubmodule.toAddSubgroup ?_ b b' ?_ ?_).trans ?_
-- 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)
refine_1 :
  LE.le.{u_1} (α := AddSubgroup K) (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule) 1)
    (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule)
      (↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K))
⊢ Eq (α := ℚ)
    (↑(Nat.card.{u_1}
          (HasQuotient.Quotient ↥(↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K) (B :=
            Submodule 𝒪 ↥(↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K))
            (Submodule.comap (Submodule.subtype (↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K)) 1))) :
      ℚ)
    |(↑(discr K) : ℚ)|
have refine_2 : Eq (α := AddSubgroup K) (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule) 1)
  (AddSubgroup.closure (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
Tactic: refine (AddSubgroup.relIndex_eq_abs_det (1 : Submodule 𝒪 K).toAddSubgroup (FractionalIdeal.dual
    ℤ ℚ 1 : FractionalIdeal 𝒪⁰ K).coeToSubmodule.toAddSubgroup ?_ b b' ?_ ?_).trans ?_
-- 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)
⊢ LE.le.{u_1} (α := AddSubgroup K) (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule) 1)
    (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule)
      (↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K))
have refine_1 : LE.le.{u_1} (α := Submodule 𝒪 K) (↑1 : Submodule 𝒪 K) (↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K)
Tactic: rw [Submodule.toAddSubgroup_le, ← FractionalIdeal.coe_one]
-- 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)
refine_1 : LE.le.{u_1} (α := Submodule 𝒪 K) (↑1 : Submodule 𝒪 K) (↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K)
⊢ LE.le.{u_1} (α := AddSubgroup K) (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule) 1)
    (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule)
      (↑(FractionalIdeal.dual ℤ ℚ 1) : Submodule 𝒪 K))
have rw : Submonoid 𝒪
Tactic: rw [Submodule.toAddSubgroup_le, ← FractionalIdeal.coe_one]
-- 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) 1)
    (AddSubgroup.closure
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
have refine_2 : Eq (α := Submodule ℤ K)
  ((AddSubgroup.toIntSubmodule : (a : AddSubgroup K) → Submodule ℤ K)
      (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule) 1) :
    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) 1) :
      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_2 : Eq.{u_1 + 1} (α := Submodule ℤ K)
  ((AddSubgroup.toIntSubmodule : (a : AddSubgroup K) → Submodule ℤ K)
      (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule) 1) :
    Submodule ℤ K)
  (Submodule.span ℤ (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
    Submodule ℤ K)
Tactic: rw [AddSubgroup.toIntSubmodule_closure, hb, Submodule.toIntSubmodule_toAddSubgroup]
-- 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)
refine_2 :
  Eq.{u_1 + 1} (α := Submodule ℤ K)
    ((AddSubgroup.toIntSubmodule : (a : AddSubgroup K) → Submodule ℤ K)
        (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule) 1) :
      Submodule ℤ K)
    (Submodule.span ℤ (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)) :
      Submodule ℤ K)
⊢ Eq (α := Submodule ℤ K)
    ((AddSubgroup.toIntSubmodule : (a : AddSubgroup K) → Submodule ℤ K)
        (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule) 1) :
      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_2₁ : Eq.{u_1 + 1} (α := Submodule ℤ K)
  ((AddSubgroup.toIntSubmodule : (a : AddSubgroup K) → Submodule ℤ K)
      (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule) 1) :
    Submodule ℤ K)
  (Submodule.restrictScalars.{0, u_2, u_1} ℤ (R := 𝒪) 1 : Submodule ℤ K)
Tactic: rw [AddSubgroup.toIntSubmodule_closure, hb, Submodule.toIntSubmodule_toAddSubgroup]