awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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 ℤ 𝒪
refine : AddSubgroup.relIndex.{u_2} (G := 𝒪) (Submodule.toAddSubgroup (differentIdeal ℤ 𝒪)) ⊤ = (discr K).natAbs
⊢ (Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪) = (discr K).natAbs

Tactic:
refine (differentIdeal ℤ 𝒪).toAddSubgroup.relIndex_top_right.symm.trans ?_

Premises used: differentIdeal, Int, AddSubgroup.relIndex_top_right, Submodule.toAddSubgroup, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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 ℤ 𝒪
rw :
  AddSubgroup.relIndex.{u_2} (G := 𝒪)
      (Submodule.toAddSubgroup
        (Submodule.comap (Algebra.linearMap 𝒪 K) (Submodule.map (Algebra.linearMap 𝒪 K) (differentIdeal ℤ 𝒪))))
      ⊤ =
    (discr K).natAbs
⊢ AddSubgroup.relIndex.{u_2} (G := 𝒪) (Submodule.toAddSubgroup (differentIdeal ℤ 𝒪)) ⊤ = (discr K).natAbs

Tactic:
rw [← Submodule.comap_map_eq_of_injective (f := Algebra.linearMap 𝒪 K)
    (FaithfulSMul.algebraMap_injective 𝒪 K) (differentIdeal ℤ 𝒪)]

Premises used: Submodule.comap_map_eq_of_injective, differentIdeal, Int, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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 ℤ 𝒪
⊢ AddSubgroup.relIndex.{u_2} (G := 𝒪)
      (Submodule.toAddSubgroup
        (Submodule.comap (Algebra.linearMap 𝒪 K) (Submodule.map (Algebra.linearMap 𝒪 K) (differentIdeal ℤ 𝒪))))
      ⊤ =
    (discr K).natAbs

Tactic:
(AddSubgroup.relIndex_comap (IsLocalization.coeSubmodule K
    (differentIdeal ℤ 𝒪)).toAddSubgroup (algebraMap 𝒪 K).toAddMonoidHom ⊤).trans ?_

Premises used: AddSubgroup.comap, Algebra.algebraMap, differentIdeal, Int, RingHom.toAddMonoidHom, Submodule.toAddSubgroup, Top.top, AddSubgroup.relIndex_comap, IsLocalization.coeSubmodule, Eq.trans
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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 ℤ 𝒪
refine :
  AddSubgroup.relIndex.{u_1} (G := K)
      (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule)
        (IsLocalization.coeSubmodule K (differentIdeal ℤ 𝒪)))
      (AddSubgroup.map.{u_2, u_1} (G := 𝒪) (RingHom.toAddMonoidHom (algebraMap 𝒪 K)) ⊤) =
    (discr K).natAbs
⊢ AddSubgroup.relIndex.{u_2} (G := 𝒪)
      (Submodule.toAddSubgroup
        (Submodule.comap (Algebra.linearMap 𝒪 K) (Submodule.map (Algebra.linearMap 𝒪 K) (differentIdeal ℤ 𝒪))))
      ⊤ =
    (discr K).natAbs

Tactic:
refine (AddSubgroup.relIndex_comap (IsLocalization.coeSubmodule K
    (differentIdeal ℤ 𝒪)).toAddSubgroup (algebraMap 𝒪 K).toAddMonoidHom ⊤).trans ?_

Premises used: Algebra.algebraMap, differentIdeal, Int, RingHom.toAddMonoidHom, Submodule.toAddSubgroup, Top.top, AddSubgroup.relIndex_comap, IsLocalization.coeSubmodule, Eq.trans
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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 ℤ 𝒪
⊢ HMul.hMul (α := FractionalIdeal.{u_2, u_1} (R := 𝒪) 𝒪⁰ K) 1 1 =
    HMul.hMul (α := FractionalIdeal.{u_2, u_1} (R := 𝒪) 𝒪⁰ K) (↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)⁻¹
      (↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)

Tactic:
simp [differentIdeal_ne_bot]

Premises used: differentIdeal_ne_bot
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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 ℤ 𝒪
⊢ LT.lt.{u_1} (α := FractionalIdeal.{u_2, u_1} (R := 𝒪) 𝒪⁰ K) 0 (↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K)

Tactic:
simp [pos_iff_ne_zero, differentIdeal_ne_bot]

Premises used: differentIdeal_ne_bot, pos_iff_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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 ℤ 𝒪
⊢ LE.le.{u_1} (α := FractionalIdeal.{u_2, u_1} (R := 𝒪) 𝒪⁰ K) (↑(differentIdeal ℤ 𝒪) : FractionalIdeal 𝒪⁰ K) 1⁻¹

Tactic:
simpa using FractionalIdeal.coeIdeal_le_one

Premises used: FractionalIdeal.coeIdeal_le_one
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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 ℤ 𝒪
have :
  ∀
    (this :
      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))),
    AddSubgroup.relIndex.{u_1} (G := K)
        (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule)
          (IsLocalization.coeSubmodule K (differentIdeal ℤ 𝒪)))
        (AddSubgroup.map.{u_2, u_1} (G := 𝒪) (RingHom.toAddMonoidHom (algebraMap 𝒪 K)) ⊤) =
      (discr K).natAbs
⊢ AddSubgroup.relIndex.{u_1} (G := K)
      (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule)
        (IsLocalization.coeSubmodule K (differentIdeal ℤ 𝒪)))
      (AddSubgroup.map.{u_2, u_1} (G := 𝒪) (RingHom.toAddMonoidHom (algebraMap 𝒪 K)) ⊤) =
    (discr K).natAbs

Tactic:
have := FractionalIdeal.quotientEquiv (R := 𝒪) (K := K) 1 (differentIdeal ℤ 𝒪)
    (differentIdeal ℤ 𝒪)⁻¹ 1 (by simp [differentIdeal_ne_bot]) FractionalIdeal.coeIdeal_le_one
    (le_inv_of_le_inv₀ (by simp [pos_iff_ne_zero, differentIdeal_ne_bot])
      (by simpa using FractionalIdeal.coeIdeal_le_one)) one_ne_zero one_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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 :
  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))
⊢ 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)))

Tactic:
have := Nat.card_congr this.toEquiv
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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)))
⊢ AddSubgroup.relIndex.{u_1} (G := K)
      (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule)
        (IsLocalization.coeSubmodule K (differentIdeal ℤ 𝒪)))
      (AddSubgroup.map.{u_2, u_1} (G := 𝒪) (RingHom.toAddMonoidHom (algebraMap 𝒪 K)) ⊤) =
    (discr K).natAbs

Tactic:
this.trans ?_

Premises used: AddSubgroup.comap, AddSubgroup.index, Set.Mem, AddSubgroup.relIndex, FractionalIdeal.coeToSubmodule, Submodule.quotientRel, Submodule.map, AddSubgroup.addSubgroupOf, IsLocalization.coeSubmodule, Eq.trans, AddSubgroup.map
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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)))
refine :
  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))) =
    (discr K).natAbs
⊢ AddSubgroup.relIndex.{u_1} (G := K)
      (Submodule.toAddSubgroup.{u_2, u_1} (R := 𝒪) (module_M := Algebra.toModule)
        (IsLocalization.coeSubmodule K (differentIdeal ℤ 𝒪)))
      (AddSubgroup.map.{u_2, u_1} (G := 𝒪) (RingHom.toAddMonoidHom (algebraMap 𝒪 K)) ⊤) =
    (discr K).natAbs

Tactic:
refine this.trans ?_

Premises used: Eq.trans
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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)))
rw :
  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
⊢ 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))) =
    (discr K).natAbs

Tactic:
rw [FractionalIdeal.coe_one, coeIdeal_differentIdeal (K := ℚ), inv_inv]

Premises used: Rat, coeIdeal_differentIdeal, FractionalIdeal.coe_one, inv_inv
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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
h :
  ∀ (x : K),
    Membership.mem (γ := Submodule ℤ K)
        (Submodule.span ℤ
          (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
        x ↔
      Membership.mem (γ := Submodule ℤ K) (Submodule.restrictScalars.{0, u_2, u_1} ℤ (R := 𝒪) 1) x
⊢ 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)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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
x : K
e : AlgEquiv.{0, u_1, u_2} ℤ (𝓞 K) 𝒪 := IsIntegralClosure.equiv ℤ (𝓞 K) K 𝒪
⊢ Membership.mem (γ := Submodule ℤ K)
      (Submodule.span ℤ (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (⇑b : (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)))
      x ↔
    Membership.mem (γ := Submodule ℤ K) (Submodule.restrictScalars.{0, u_2, u_1} ℤ (R := 𝒪) 1) x

Tactic:
simpa [e.symm.exists_congr_left, e] using mem_span_integralBasis K

Premises used: Equiv.exists_congr_left, AlgEquiv.symm, NumberField.mem_span_integralBasis, AlgEquiv.toEquiv
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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
⊢ 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)

Tactic:
have hb : Submodule.span ℤ (Set.range b) = (1 : Submodule 𝒪 K).restrictScalars ℤ := by
    ext
    let e := IsIntegralClosure.equiv ℤ (RingOfIntegers K) K 𝒪
    simpa [e.symm.exists_congr_left, e] using mem_span_integralBasis K
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Different
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)
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) : ℚ)|
⊢ 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

Tactic:
qify