-- 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))
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)))
refine_3 :
  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)))
⊢ 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_4 : Eq (α := ℚ)
  (|((Basis.det.{0, u_1, u_1} (R := ℚ) (M := K) (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) b' :
            K [⋀^Free.ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℚ] ℚ) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K) → K) → ℚ)
        (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)| :
    ℚ)
  (|(↑(discr K) : ℚ)| : ℚ)
Tactic: refine (AddSubgroup.relIndex_eq_abs_det (1 : Submodule 𝒪 K).toAddSubgroup (FractionalIdeal.dual
    ℤ ℚ 1 : FractionalIdeal 𝒪⁰ K).coeToSubmodule.toAddSubgroup ?_ b b' ?_ ?_).trans ?_