awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
ι : Type u_2
ι' : Type u_3
K : Type u_1
inst : Field K
inst_1 : DecidableEq ι
inst_2 : DecidableEq ι'
inst_3 : Fintype ι
inst_4 : Fintype ι'
inst_5 : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b' : (a : ι') → K) i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K) i j)
rw :
  discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    discr (ι := ι') ℚ (B := K)
      (Matrix.vecMul (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)
        (Matrix.map ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)) (⇑(algebraMap ℚ K) : (a : ℚ) → K)))
rw₁ :
  discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
      discr.{0, u_1, u_3} (ι := ι') ℚ (B := K) (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)
rw₂ :
  1 * discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
      discr.{0, u_1, u_3} (ι := ι') ℚ (B := K) (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)
⊢ discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    discr.{0, u_1, u_3} (ι := ι') ℚ (B := K) (⇑b' : (a : ι') → K)
have rw₃ : 1 * discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
  HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
    discr.{0, u_1, u_3} (ι := ι') ℚ (B := K)
      (Function.comp.{u_3 + 1, u_2 + 1, u_1 + 1} (β := ι) (⇑b : (a : ι) → K) (⇑(b.indexEquiv b').symm : (a : ι') → ι))
Tactic: classical
  rw [← (b.reindex (b.indexEquiv b')).toMatrix_map_vecMul b', discr_of_matrix_vecMul,
    ← one_mul (discr ℚ b), Basis.coe_reindex, discr_reindex]
  congr
  have hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix b').det :=
    IsIntegral.det fun i j => h _ _
  obtain ⟨r, hr⟩ := IsIntegrallyClosed.isIntegral_iff.1 hint
  have hunit : IsUnit r := by
    have : IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b'))).det :=
      IsIntegral.det fun i j => h' _ _
    obtain ⟨r', hr'⟩ := IsIntegrallyClosed.isIntegral_iff.1 this
    refine isUnit_iff_exists_inv.2 ⟨r', ?_⟩
    suffices algebraMap ℤ ℚ (r * r') = 1 by
      rw [← map_one (algebraMap ℤ ℚ)] at this
      exact (IsFractionRing.injective ℤ ℚ) this
    rw [map_mul, hr, hr', ← Matrix.det_mul, Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one]
  rw [← map_one (algebraMap ℤ ℚ), ← hr]
  rcases Int.isUnit_iff.1 hunit with hp | hm
  · simp [hp]
  · simp [hm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
ι : Type u_2
ι' : Type u_3
K : Type u_1
inst : Field K
inst_1 : DecidableEq ι
inst_2 : DecidableEq ι'
inst_3 : Fintype ι
inst_4 : Fintype ι'
inst_5 : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b' : (a : ι') → K) i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K) i j)
rw :
  discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    discr (ι := ι') ℚ (B := K)
      (Matrix.vecMul (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)
        (Matrix.map ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)) (⇑(algebraMap ℚ K) : (a : ℚ) → K)))
rw₁ :
  discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
      discr.{0, u_1, u_3} (ι := ι') ℚ (B := K) (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)
rw₂ :
  1 * discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
      discr.{0, u_1, u_3} (ι := ι') ℚ (B := K) (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)
rw₃ :
  1 * discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
      discr.{0, u_1, u_3} (ι := ι') ℚ (B := K)
        (Function.comp.{u_3 + 1, u_2 + 1, u_1 + 1} (β := ι) (⇑b : (a : ι) → K) (⇑(b.indexEquiv b').symm : (a : ι') → ι))
⊢ discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    discr.{0, u_1, u_3} (ι := ι') ℚ (B := K) (⇑b' : (a : ι') → K)
have rw₄ : 1 * discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
  HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
    discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K)
Tactic: classical
  rw [← (b.reindex (b.indexEquiv b')).toMatrix_map_vecMul b', discr_of_matrix_vecMul,
    ← one_mul (discr ℚ b), Basis.coe_reindex, discr_reindex]
  congr
  have hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix b').det :=
    IsIntegral.det fun i j => h _ _
  obtain ⟨r, hr⟩ := IsIntegrallyClosed.isIntegral_iff.1 hint
  have hunit : IsUnit r := by
    have : IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b'))).det :=
      IsIntegral.det fun i j => h' _ _
    obtain ⟨r', hr'⟩ := IsIntegrallyClosed.isIntegral_iff.1 this
    refine isUnit_iff_exists_inv.2 ⟨r', ?_⟩
    suffices algebraMap ℤ ℚ (r * r') = 1 by
      rw [← map_one (algebraMap ℤ ℚ)] at this
      exact (IsFractionRing.injective ℤ ℚ) this
    rw [map_mul, hr, hr', ← Matrix.det_mul, Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one]
  rw [← map_one (algebraMap ℤ ℚ), ← hr]
  rcases Int.isUnit_iff.1 hunit with hp | hm
  · simp [hp]
  · simp [hm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
ι : Type u_2
ι' : Type u_3
K : Type u_1
inst : Field K
inst_1 : DecidableEq ι
inst_2 : DecidableEq ι'
inst_3 : Fintype ι
inst_4 : Fintype ι'
inst_5 : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b' : (a : ι') → K) i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K) i j)
rw :
  discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    discr (ι := ι') ℚ (B := K)
      (Matrix.vecMul (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)
        (Matrix.map ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)) (⇑(algebraMap ℚ K) : (a : ℚ) → K)))
rw₁ :
  discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
      discr.{0, u_1, u_3} (ι := ι') ℚ (B := K) (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)
rw₂ :
  1 * discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
      discr.{0, u_1, u_3} (ι := ι') ℚ (B := K) (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)
rw₃ :
  1 * discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
      discr.{0, u_1, u_3} (ι := ι') ℚ (B := K)
        (Function.comp.{u_3 + 1, u_2 + 1, u_1 + 1} (β := ι) (⇑b : (a : ι) → K) (⇑(b.indexEquiv b').symm : (a : ι') → ι))
rw₄ rw₅ rw₆ :
  1 * discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
      discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K)
⊢ discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    discr.{0, u_1, u_3} (ι := ι') ℚ (B := K) (⇑b' : (a : ι') → K)
have e_a : 1 = HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2
Tactic: classical
  rw [← (b.reindex (b.indexEquiv b')).toMatrix_map_vecMul b', discr_of_matrix_vecMul,
    ← one_mul (discr ℚ b), Basis.coe_reindex, discr_reindex]
  congr
  have hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix b').det :=
    IsIntegral.det fun i j => h _ _
  obtain ⟨r, hr⟩ := IsIntegrallyClosed.isIntegral_iff.1 hint
  have hunit : IsUnit r := by
    have : IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b'))).det :=
      IsIntegral.det fun i j => h' _ _
    obtain ⟨r', hr'⟩ := IsIntegrallyClosed.isIntegral_iff.1 this
    refine isUnit_iff_exists_inv.2 ⟨r', ?_⟩
    suffices algebraMap ℤ ℚ (r * r') = 1 by
      rw [← map_one (algebraMap ℤ ℚ)] at this
      exact (IsFractionRing.injective ℤ ℚ) this
    rw [map_mul, hr, hr', ← Matrix.det_mul, Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one]
  rw [← map_one (algebraMap ℤ ℚ), ← hr]
  rcases Int.isUnit_iff.1 hunit with hp | hm
  · simp [hp]
  · simp [hm]
-- 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 ℤ 𝒪
⊢ (Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪) = (discr K).natAbs
have refine : AddSubgroup.relIndex.{u_2} (G := 𝒪) (Submodule.toAddSubgroup (differentIdeal ℤ 𝒪)) ⊤ = (discr K).natAbs
Tactic: refine (differentIdeal ℤ 𝒪).toAddSubgroup.relIndex_top_right.symm.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 ℤ 𝒪
⊢ AddSubgroup.relIndex.{u_2} (G := 𝒪) (Submodule.toAddSubgroup (differentIdeal ℤ 𝒪)) ⊤ = (discr K).natAbs
have rw : AddSubgroup.relIndex.{u_2} (G := 𝒪)
    (Submodule.toAddSubgroup
      (Submodule.comap (Algebra.linearMap 𝒪 K) (Submodule.map (Algebra.linearMap 𝒪 K) (differentIdeal ℤ 𝒪))))
    ⊤ =
  (discr K).natAbs
Tactic: rw [← Submodule.comap_map_eq_of_injective (f := Algebra.linearMap 𝒪 K)
    (FaithfulSMul.algebraMap_injective 𝒪 K) (differentIdeal ℤ 𝒪)]
-- 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 ℤ 𝒪
⊢ AddSubgroup.relIndex.{u_2} (G := 𝒪)
      (Submodule.toAddSubgroup
        (Submodule.comap (Algebra.linearMap 𝒪 K) (Submodule.map (Algebra.linearMap 𝒪 K) (differentIdeal ℤ 𝒪))))
      ⊤ =
    (discr K).natAbs
have 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
Tactic: refine (AddSubgroup.relIndex_comap (IsLocalization.coeSubmodule K
    (differentIdeal ℤ 𝒪)).toAddSubgroup (algebraMap 𝒪 K).toAddMonoidHom ⊤).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 ℤ 𝒪
⊢ 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
have 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
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
-- 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 ℤ 𝒪
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
have 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)))
Tactic: have := Nat.card_congr this.toEquiv
-- 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)))
⊢ 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
have 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
Tactic: refine this.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)))
⊢ 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
have 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
Tactic: rw [FractionalIdeal.coe_one, coeIdeal_differentIdeal (K := ℚ), inv_inv]
-- 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
⊢ 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)
have 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
Tactic: ext
-- 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 ℤ 𝒪
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
⊢ 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 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)
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