awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
rw :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
          ((LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)
          ((LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
⊢ Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
have rw₁ : Eq (α := ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
        ((LinearEquiv.symm (AddEquiv.toIntLinearEquiv (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
            ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
          𝓞 ℚ)
        ((LinearEquiv.symm (AddEquiv.toIntLinearEquiv (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
            ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
          𝓞 ℚ)) :
    ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
Tactic: 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
rw :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
          ((LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)
          ((LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
rw₁ :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
          ((LinearEquiv.symm (AddEquiv.toIntLinearEquiv (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)
          ((LinearEquiv.symm (AddEquiv.toIntLinearEquiv (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
⊢ Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
have rw₂ : Eq (α := ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
        ((AddEquiv.toIntLinearEquiv (AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
            ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
          𝓞 ℚ)
        ((AddEquiv.toIntLinearEquiv (AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
            ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
          𝓞 ℚ)) :
    ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
Tactic: 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
rw :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
          ((LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)
          ((LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
rw₁ :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
          ((LinearEquiv.symm (AddEquiv.toIntLinearEquiv (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)
          ((LinearEquiv.symm (AddEquiv.toIntLinearEquiv (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
rw₂ :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
          ((AddEquiv.toIntLinearEquiv (AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)
          ((AddEquiv.toIntLinearEquiv (AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
⊢ Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
have rw₃ : Eq (α := ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
        ((AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ) : (a : ℤ) → 𝓞 ℚ)
            ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
          𝓞 ℚ)
        ((AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ) : (a : ℤ) → 𝓞 ℚ)
            ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
          𝓞 ℚ)) :
    ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
Tactic: 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
rw :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
          ((LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)
          ((LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
rw₁ :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
          ((LinearEquiv.symm (AddEquiv.toIntLinearEquiv (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)
          ((LinearEquiv.symm (AddEquiv.toIntLinearEquiv (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
rw₂ :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
          ((AddEquiv.toIntLinearEquiv (AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)
          ((AddEquiv.toIntLinearEquiv (AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ)) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
rw₃ :
  Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) (β := 𝓞 ℚ)
          ((AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)
          ((AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ) : (a : ℤ) → 𝓞 ℚ)
              ((Basis.singleton (Fin 1) ℤ : (a : Fin 1) → ℤ) default) :
            𝓞 ℚ)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
⊢ Eq (α := ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
        (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default)) :
      ℤ)
    ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
have rw₄ : Eq (α := ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ) : (a : ℤ) → 𝓞 ℚ) 1)
        ((AddEquiv.symm (↑ringOfIntegersEquiv : 𝓞 ℚ ≃+ ℤ) : (a : ℤ) → 𝓞 ℚ) 1)) :
    ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ)
Tactic: 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
⊢ Eq (α := ℤ) ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ) (1 : ℤ)
have rw : Eq (α := ℤ) (Matrix.trace (n := Fin 1) ((Algebra.leftMulMatrix b : (a : 𝓞 ℚ) → Matrix (Fin 1) (Fin 1) ℤ) 1)) 1
Tactic: rw [Algebra.trace_eq_matrix_trace b]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
  Basis.map (Basis.singleton (Fin 1) ℤ) (LinearEquiv.symm ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv)
⊢ discr ℚ = 1
have calc : discr ℚ = Algebra.discr (ι := Fin 1) ℤ (B := 𝓞 ℚ) (⇑b : (a : Fin 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
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) → 𝓞 ℚ)
⊢ discr ℚ = 1
have 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))
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
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))
⊢ discr ℚ = 1
have calc₂ : Eq (α := ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ)
      (HMul.hMul (α := 𝓞 ℚ) ((b : (a : Fin 1) → 𝓞 ℚ) default) ((b : (a : Fin 1) → 𝓞 ℚ) default)) :
    ℤ)
  ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
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 : ℤ)
⊢ discr ℚ = 1
have calc₃ : Eq (α := ℤ) ((Algebra.trace ℤ (𝓞 ℚ) : (a : 𝓞 ℚ) → ℤ) 1 : ℤ) (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
-- 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 : (a : ι) → K) i j)
i j : ι'
⊢ IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K) i j)
have 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 : ι)
Tactic: convert! h' i ((b.indexEquiv b').symm j)
-- 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 : (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 h'₁ : ∀ (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]
Cleared hypotheses: h'
-- 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 : 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: rw [← (b.reindex (b.indexEquiv b')).toMatrix_map_vecMul b', discr_of_matrix_vecMul,
    ← one_mul (discr ℚ b), Basis.coe_reindex, discr_reindex]
-- 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)
⊢ 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)
have e_a : 1 = HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2
Tactic: congr
-- 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)
⊢ 1 = HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2
have hint : 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 _ _
-- 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)))
⊢ 1 = HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2
have 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
Tactic: obtain ⟨r, hr⟩ := IsIntegrallyClosed.isIntegral_iff.1 hint
-- 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))
⊢ IsUnit r
have this : 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' _ _
-- 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)))
⊢ IsUnit r
have obtain : ∀ (r' : ℤ)
  (hr' : (algebraMap ℤ ℚ : (a : ℤ) → ℚ) r' = Matrix.det (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K))),
  IsUnit r
Tactic: obtain ⟨r', hr'⟩ := IsIntegrallyClosed.isIntegral_iff.1 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))
⊢ IsUnit r
have refine : r * r' = 1
Tactic: refine isUnit_iff_exists_inv.2 ⟨r', ?_⟩