awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
calc : discr ℚ = Algebra.discr (ι := Fin 1) ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ)
calc₁ :
  Algebra.discr (ι := Fin 1) ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 1) → 𝓞 ℚ) =
    (Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default))
calc₂ :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
calc₃ : Eq (α := ℤ) ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ) (1 : ℤ)
⊢ discr ℚ = 1

Tactic:
calc NumberField.discr ℚ
    _ = Algebra.discr ℤ b := by convert! (discr_eq_discr ℚ b).symm
    _ = Algebra.trace ℤ (𝓞 ℚ) (b default * b default) := by
      rw [Algebra.discr_def, Matrix.det_unique, Algebra.traceMatrix_apply, Algebra.traceForm_apply]
    _ = Algebra.trace ℤ (𝓞 ℚ) 1 := by
      rw [Basis.map_apply, RingEquiv.toAddEquiv_eq_coe, ← AddEquiv.toIntLinearEquiv_symm,
        AddEquiv.coe_toIntLinearEquiv, Basis.singleton_apply,
        show (AddEquiv.symm ↑ringOfIntegersEquiv) (1 : ℤ) = ringOfIntegersEquiv.symm 1 by rfl,
        map_one, mul_one]
    _ = 1 := by rw [Algebra.trace_eq_matrix_trace b]; simp

Premises used: Inhabited.default, HMul.hMul, Rat, Int, NumberField.discr, Algebra.trace, OfNat.ofNat, NumberField.RingOfIntegers, DFunLike.coe, Algebra.discr
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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 : (a : ι) → K) i j)
i j : ι'
⊢ IsIntegral ℤ
    (Basis.toMatrix.{u_3, u_2, 0, u_1} (ι' := ι) b' ((⇑b : (a : ι) → K) : (a : ι) → K) i
      (((b.indexEquiv b').symm : (a : ι') → ι) j : ι))

Tactic:
h' i ((b.indexEquiv b').symm j)

Premises used: Equiv.symm, Module.Basis.indexEquiv, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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 : (a : ι) → K) i j)
i j : ι'
h₁ :
  b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K) i j =
    Basis.toMatrix.{u_3, u_2, 0, u_1} (ι' := ι) b' ((⇑b : (a : ι) → K) : (a : ι) → K) i
      (((b.indexEquiv b').symm : (a : ι') → ι) j : ι)
⊢ IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K) i j)

Tactic:
convert! h' i ((b.indexEquiv b').symm j)

Premises used: Equiv.symm, Module.Basis.indexEquiv, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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 : (a : ι) → K) i j)
i j : ι'
⊢ b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K) i j =
    Basis.toMatrix.{u_3, u_2, 0, u_1} (ι' := ι) b' ((⇑b : (a : ι) → K) : (a : ι) → K) i
      (((b.indexEquiv b').symm : (a : ι') → ι) j : ι)

Tactic:
simp [Basis.toMatrix_apply]

Premises used: Module.Basis.toMatrix_apply
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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 : (a : ι) → K) i j)
⊢ ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K) i j)

Tactic:
replace h' : ∀ i j, IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b')) i j) := by
    intro i j
    convert! h' i ((b.indexEquiv b').symm j)
    simp [Basis.toMatrix_apply]
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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 :
  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)

Tactic:
rw [← (b.reindex (b.indexEquiv b')).toMatrix_map_vecMul b', discr_of_matrix_vecMul,
    ← one_mul (discr ℚ b), Basis.coe_reindex, discr_reindex]

Premises used: Rat, Module.Basis.coe_reindex, Algebra.discr_of_matrix_vecMul, Module.Basis.reindex, Module.Basis.indexEquiv, DFunLike.coe, Module.Basis.toMatrix_map_vecMul, Algebra.discr, one_mul, Algebra.discr_reindex
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
e_a : 1 = HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2
⊢ 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:
congr
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
⊢ IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))

Tactic:
have hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix b').det :=
    IsIntegral.det fun i j => h _ _
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
e_a :
  ∀ (r : ℤ)
    (hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))),
    1 = HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2
⊢ 1 = HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2

Tactic:
obtain ⟨r, hr⟩ := IsIntegrallyClosed.isIntegral_iff.1 hint

Premises used: IsIntegrallyClosed.isIntegral_iff, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
r : ℤ
hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
⊢ IsIntegral ℤ (Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)))

Tactic:
have : IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b'))).det :=
      IsIntegral.det fun i j => h' _ _
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
r : ℤ
hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
this : IsIntegral ℤ (Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)))
obtain :
  ∀ (r' : ℤ)
    (hr' :
      (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r' = Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K))),
    IsUnit r
⊢ IsUnit r

Tactic:
obtain ⟨r', hr'⟩ := IsIntegrallyClosed.isIntegral_iff.1 this

Premises used: IsIntegrallyClosed.isIntegral_iff, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
r : ℤ
hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
this : IsIntegral ℤ (Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)))
r' : ℤ
hr' : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r' = Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K))
⊢ IsUnit r

Tactic:
isUnit_iff_exists_inv.2 ⟨r', ?_⟩

Premises used: Iff.mpr, isUnit_iff_exists_inv, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
r : ℤ
hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
this : IsIntegral ℤ (Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)))
r' : ℤ
hr' : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r' = Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K))
refine : r * r' = 1
⊢ IsUnit r

Tactic:
refine isUnit_iff_exists_inv.2 ⟨r', ?_⟩

Premises used: Iff.mpr, isUnit_iff_exists_inv, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
r : ℤ
hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
this_1 : IsIntegral ℤ (Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)))
r' : ℤ
hr' : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r' = Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K))
this : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (r * r') : ℚ) (1 : ℚ)
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (r * r') : ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 : ℚ)

Tactic:
rw [← map_one (algebraMap ℤ ℚ)] at this

Premises used: Algebra.algebraMap, Rat, Int, map_one
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
r : ℤ
hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
this_1 : IsIntegral ℤ (Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)))
r' : ℤ
hr' : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r' = Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K))
this : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (r * r') : ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 : ℚ)
⊢ r * r' = 1

Tactic:
(IsFractionRing.injective ℤ ℚ) this

Premises used: IsFractionRing.injective, Rat, Int
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
r : ℤ
hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
this_1 : IsIntegral ℤ (Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)))
r' : ℤ
hr' : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r' = Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K))
this : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (r * r') : ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 : ℚ)
⊢ r * r' = 1

Tactic:
exact (IsFractionRing.injective ℤ ℚ) this

Premises used: IsFractionRing.injective, Rat, Int
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
r : ℤ
hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
this : IsIntegral ℤ (Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)))
r' : ℤ
hr' : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r' = Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K))
suffices : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (r * r') : ℚ) (1 : ℚ)
⊢ r * r' = 1

Tactic:
suffices algebraMap ℤ ℚ (r * r') = 1 by
      rw [← map_one (algebraMap ℤ ℚ)] at this
      exact (IsFractionRing.injective ℤ ℚ) this
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
r : ℤ
hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
this : IsIntegral ℤ (Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)))
r' : ℤ
hr' : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r' = Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K))
rw : HMul.hMul (α := ℚ) (β := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r : ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r' : ℚ) = 1
rw₁ :
  HMul.hMul (β := ℚ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
      ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r' : ℚ) =
    1
rw₂ :
  Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)) *
      Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)) =
    1
rw₃ :
  (HMul.hMul (α := Matrix ι' ι' ℚ) ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
        (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K))).det =
    1
rw₄ : Eq (α := ℚ) (Matrix.det.{0, u_3} (n := ι') 1) 1
rw₅ rw₆ : Eq (α := ℚ) 1 1
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (r * r') : ℚ) (1 : ℚ)

Tactic:
rw [map_mul, hr, hr', ← Matrix.det_mul, Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one]

Premises used: Matrix.det_mul, map_mul, Module.Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
r : ℤ
hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
⊢ IsUnit r

Tactic:
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]
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
r : ℤ
hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
hunit : IsUnit r
e_a : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 = HPow.hPow (α := ℚ) (β := ℕ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r : ℚ) 2
⊢ 1 = HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2

Tactic:
rw [← map_one (algebraMap ℤ ℚ), ← hr]

Premises used: Algebra.algebraMap, Rat, Int, map_one
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
r : ℤ
hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
hunit : IsUnit r
e_a :
  ∀ (hp : r = 1),
    (algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 = HPow.hPow (α := ℚ) (β := ℕ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r : ℚ) 2
e_a₁ :
  ∀ (hm : r = -1),
    (algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 = HPow.hPow (α := ℚ) (β := ℕ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r : ℚ) 2
⊢ (algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 = HPow.hPow (α := ℚ) (β := ℕ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r : ℚ) 2

Tactic:
rcases Int.isUnit_iff.1 hunit with hp | hm

Premises used: Iff.mp, Int.isUnit_iff
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
r : ℤ
hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
hunit : IsUnit r
hp : r = 1
⊢ (algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 = HPow.hPow (α := ℚ) (β := ℕ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r : ℚ) 2

Tactic:
simp [hp]
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs
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)
hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
r : ℤ
hr : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r = Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
hunit : IsUnit r
hm : r = -1
⊢ (algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 = HPow.hPow (α := ℚ) (β := ℕ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r : ℚ) 2

Tactic:
simp [hm]
-- 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 ℤ 𝒪
⊢ (Ideal.absNorm : (a : Ideal 𝒪) → ℕ) (differentIdeal ℤ 𝒪) = (discr K).natAbs

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

Premises used: AddSubgroup.index, differentIdeal, Nat.card, Int, Submodule.cardQuot, AddSubgroup.relIndex_top_right, Submodule.toAddSubgroup, ENat.toNat, WithTop.untopD, Eq.symm, WithTop.recTopCoe, Eq.trans