awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (hypothesis)
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 : ℚ)
⊢ r * r' = 1
have this₁ : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (r * r') : ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 : ℚ)
Tactic: rw [← map_one (algebraMap ℤ ℚ)] at this
Cleared hypotheses: this
-- 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)
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))
⊢ r * r' = 1
have suffices : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (r * r') : ℚ) (1 : ℚ)
Tactic: suffices algebraMap ℤ ℚ (r * r') = 1 by
      rw [← map_one (algebraMap ℤ ℚ)] at this
      exact (IsFractionRing.injective ℤ ℚ) this
-- 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)
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))
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (r * r') : ℚ) (1 : ℚ)
have rw : HMul.hMul (α := ℚ) (β := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r : ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r' : ℚ) = 1
Tactic: rw [map_mul, hr, hr', ← Matrix.det_mul, Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one]
-- 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)
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
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (r * r') : ℚ) (1 : ℚ)
have rw₁ : HMul.hMul (β := ℚ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r' : ℚ) =
  1
Tactic: rw [map_mul, hr, hr', ← Matrix.det_mul, Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one]
-- 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)
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
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (r * r') : ℚ) (1 : ℚ)
have rw₂ : Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)) *
    Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)) =
  1
Tactic: rw [map_mul, hr, hr', ← Matrix.det_mul, Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one]
-- 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)
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
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (r * r') : ℚ) (1 : ℚ)
have rw₃ : (HMul.hMul (α := Matrix ι' ι' ℚ) ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))
      (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K))).det =
  1
Tactic: rw [map_mul, hr, hr', ← Matrix.det_mul, Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one]
-- 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)
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
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (r * r') : ℚ) (1 : ℚ)
have rw₄ : Eq (α := ℚ) (Matrix.det.{0, u_3} (n := ι') 1) 1
Tactic: rw [map_mul, hr, hr', ← Matrix.det_mul, Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one]
-- 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)
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
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (r * r') : ℚ) (1 : ℚ)
have rw₅ : Eq (α := ℚ) 1 1
Tactic: rw [map_mul, hr, hr', ← Matrix.det_mul, Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (hypothesis)
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))
⊢ 1 = HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2
have hunit : 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]
-- 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)
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
⊢ 1 = HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2
have e_a : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 = HPow.hPow (α := ℚ) (β := ℕ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r : ℚ) 2
Tactic: rw [← map_one (algebraMap ℤ ℚ), ← hr]
-- 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)
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
⊢ (algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 = HPow.hPow (α := ℚ) (β := ℕ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r : ℚ) 2
have e_a : ∀ (hp : r = 1), (algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 = HPow.hPow (α := ℚ) (β := ℕ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r : ℚ) 2
Tactic: rcases Int.isUnit_iff.1 hunit with hp | 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)
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
⊢ (algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 = HPow.hPow (α := ℚ) (β := ℕ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r : ℚ) 2
have e_a₁ : ∀ (hm : r = -1), (algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 = HPow.hPow (α := ℚ) (β := ℕ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) r : ℚ) 2
Tactic: rcases Int.isUnit_iff.1 hunit with hp | 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)
⊢ discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    discr.{0, u_1, u_3} (ι := ι') ℚ (B := K) (⇑b' : (a : ι') → K)
have 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)))
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)))
⊢ discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    discr.{0, u_1, u_3} (ι := ι') ℚ (B := K) (⇑b' : (a : ι') → K)
have 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)
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)
⊢ 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) (⇑(b.reindex (b.indexEquiv 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]