awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
H :
  HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
        (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
    HSMul.hSMul (β := (i : Fin B.dim) → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
i : Fin B.dim
cramer :
  ((Matrix.cramer (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) :
        (a : Fin B.dim → K) → Fin B.dim → K)
      fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))) =
    HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      ((B.basis.equivFun : (a : L) → Fin B.dim → K) z : Fin B.dim → K)
σ : Equiv.Perm (Fin B.dim)
h : Membership.mem (γ := Finset (Equiv.Perm (Fin B.dim))) univ σ
j : Fin B.dim
h_1 : Membership.mem (γ := Finset (Fin B.dim)) univ j
pos :
  ∀ (hji : j = i),
    Membership.mem (γ := Subalgebra R K) ⊥
      (updateCol (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) i
        (fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L)))
        ((σ : (a : Fin B.dim) → Fin B.dim) j) j)
neg :
  ∀ (hji : ¬j = i),
    Membership.mem (γ := Subalgebra R K) ⊥
      (updateCol (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) i
        (fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L)))
        ((σ : (a : Fin B.dim) → Fin B.dim) j) j)
⊢ Membership.mem (γ := Subalgebra R K) ⊥
    (updateCol (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) i
      (fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L)))
      ((σ : (a : Fin B.dim) → Fin B.dim) j) j)

Tactic:
by_cases hji : j = i
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
H :
  HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
        (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
    HSMul.hSMul (β := (i : Fin B.dim) → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
i : Fin B.dim
cramer :
  ((Matrix.cramer (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) :
        (a : Fin B.dim → K) → Fin B.dim → K)
      fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))) =
    HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      ((B.basis.equivFun : (a : L) → Fin B.dim → K) z : Fin B.dim → K)
σ : Equiv.Perm (Fin B.dim)
h : Membership.mem (γ := Finset (Equiv.Perm (Fin B.dim))) univ σ
j : Fin B.dim
h_1 : Membership.mem (γ := Finset (Fin B.dim)) univ j
hji : j = i
pos :
  Membership.mem.{u, u} (α := K) (γ := Subalgebra R K) ⊥
    (if True then (trace K L : (a : L) → K) (z * B.gen ^ (↑((σ : (a : Fin B.dim) → Fin B.dim) i) : ℕ))
      else
        traceMatrix.{u, v, 0} K (B := L) (fun (i : Fin B.dim) ↦ B.gen ^ (↑i : ℕ)) ((σ : (a : Fin B.dim) → Fin B.dim) i)
          i :
      K)
⊢ Membership.mem (γ := Subalgebra R K) ⊥
    (updateCol (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) i
      (fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L)))
      ((σ : (a : Fin B.dim) → Fin B.dim) j) j)

Tactic:
simp only [updateCol_apply, hji, PowerBasis.coe_basis]

Premises used: Matrix.updateCol_apply, PowerBasis.coe_basis
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
H :
  HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
        (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
    HSMul.hSMul (β := (i : Fin B.dim) → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
i : Fin B.dim
cramer :
  ((Matrix.cramer (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) :
        (a : Fin B.dim → K) → Fin B.dim → K)
      fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))) =
    HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      ((B.basis.equivFun : (a : L) → Fin B.dim → K) z : Fin B.dim → K)
σ : Equiv.Perm (Fin B.dim)
h : Membership.mem (γ := Finset (Equiv.Perm (Fin B.dim))) univ σ
j : Fin B.dim
h_1 : Membership.mem (γ := Finset (Fin B.dim)) univ j
hji : j = i
⊢ Membership.mem.{u, u} (α := K) (γ := Subalgebra R K) ⊥
    (if True then (trace K L : (a : L) → K) (z * B.gen ^ (↑((σ : (a : Fin B.dim) → Fin B.dim) i) : ℕ))
      else
        traceMatrix.{u, v, 0} K (B := L) (fun (i : Fin B.dim) ↦ B.gen ^ (↑i : ℕ)) ((σ : (a : Fin B.dim) → Fin B.dim) i)
          i :
      K)

Tactic:
mem_bot.2 (IsIntegrallyClosed.isIntegral_iff.1 <| isIntegral_trace (hz.mul <| hint.pow _))

Premises used: Iff.mpr, IsIntegrallyClosed.isIntegral_iff, IsIntegral.mul, Algebra.isIntegral_trace, Set.Mem, Algebra.mem_bot, IsIntegral.pow, Iff.mp
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
H :
  HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
        (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
    HSMul.hSMul (β := (i : Fin B.dim) → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
i : Fin B.dim
cramer :
  ((Matrix.cramer (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) :
        (a : Fin B.dim → K) → Fin B.dim → K)
      fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))) =
    HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      ((B.basis.equivFun : (a : L) → Fin B.dim → K) z : Fin B.dim → K)
σ : Equiv.Perm (Fin B.dim)
h : Membership.mem (γ := Finset (Equiv.Perm (Fin B.dim))) univ σ
j : Fin B.dim
h_1 : Membership.mem (γ := Finset (Fin B.dim)) univ j
hji : j = i
⊢ Membership.mem.{u, u} (α := K) (γ := Subalgebra R K) ⊥
    (if True then (trace K L : (a : L) → K) (z * B.gen ^ (↑((σ : (a : Fin B.dim) → Fin B.dim) i) : ℕ))
      else
        traceMatrix.{u, v, 0} K (B := L) (fun (i : Fin B.dim) ↦ B.gen ^ (↑i : ℕ)) ((σ : (a : Fin B.dim) → Fin B.dim) i)
          i :
      K)

Tactic:
exact mem_bot.2 (IsIntegrallyClosed.isIntegral_iff.1 <| isIntegral_trace (hz.mul <| hint.pow _))

Premises used: Iff.mpr, IsIntegrallyClosed.isIntegral_iff, IsIntegral.mul, Algebra.isIntegral_trace, Algebra.mem_bot, IsIntegral.pow, Iff.mp
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
H :
  HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
        (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
    HSMul.hSMul (β := (i : Fin B.dim) → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
i : Fin B.dim
cramer :
  ((Matrix.cramer (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) :
        (a : Fin B.dim → K) → Fin B.dim → K)
      fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))) =
    HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      ((B.basis.equivFun : (a : L) → Fin B.dim → K) z : Fin B.dim → K)
σ : Equiv.Perm (Fin B.dim)
h : Membership.mem (γ := Finset (Equiv.Perm (Fin B.dim))) univ σ
j : Fin B.dim
h_1 : Membership.mem (γ := Finset (Fin B.dim)) univ j
hji : ¬j = i
neg :
  Membership.mem.{u, u} (α := K) (γ := Subalgebra R K) ⊥
    (if False then (trace K L : (a : L) → K) (z * B.gen ^ (↑((σ : (a : Fin B.dim) → Fin B.dim) j) : ℕ))
      else
        traceMatrix.{u, v, 0} K (B := L) (fun (i : Fin B.dim) ↦ B.gen ^ (↑i : ℕ)) ((σ : (a : Fin B.dim) → Fin B.dim) j)
          j :
      K)
⊢ Membership.mem (γ := Subalgebra R K) ⊥
    (updateCol (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) i
      (fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L)))
      ((σ : (a : Fin B.dim) → Fin B.dim) j) j)

Tactic:
simp only [updateCol_apply, hji, PowerBasis.coe_basis]

Premises used: Matrix.updateCol_apply, PowerBasis.coe_basis
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
H :
  HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
        (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
    HSMul.hSMul (β := (i : Fin B.dim) → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
i : Fin B.dim
cramer :
  ((Matrix.cramer (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) :
        (a : Fin B.dim → K) → Fin B.dim → K)
      fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))) =
    HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      ((B.basis.equivFun : (a : L) → Fin B.dim → K) z : Fin B.dim → K)
σ : Equiv.Perm (Fin B.dim)
h : Membership.mem (γ := Finset (Equiv.Perm (Fin B.dim))) univ σ
j : Fin B.dim
h_1 : Membership.mem (γ := Finset (Fin B.dim)) univ j
hji : ¬j = i
⊢ Membership.mem.{u, u} (α := K) (γ := Subalgebra R K) ⊥
    (if False then (trace K L : (a : L) → K) (z * B.gen ^ (↑((σ : (a : Fin B.dim) → Fin B.dim) j) : ℕ))
      else
        traceMatrix.{u, v, 0} K (B := L) (fun (i : Fin B.dim) ↦ B.gen ^ (↑i : ℕ)) ((σ : (a : Fin B.dim) → Fin B.dim) j)
          j :
      K)

Tactic:
mem_bot.2
      (IsIntegrallyClosed.isIntegral_iff.1 <| isIntegral_trace <| (hint.pow _).mul (hint.pow _))

Premises used: Iff.mpr, IsIntegrallyClosed.isIntegral_iff, IsIntegral.mul, Algebra.isIntegral_trace, Set.Mem, Algebra.mem_bot, IsIntegral.pow, Iff.mp
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
H :
  HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
        (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
    HSMul.hSMul (β := (i : Fin B.dim) → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
i : Fin B.dim
cramer :
  ((Matrix.cramer (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) :
        (a : Fin B.dim → K) → Fin B.dim → K)
      fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))) =
    HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      ((B.basis.equivFun : (a : L) → Fin B.dim → K) z : Fin B.dim → K)
σ : Equiv.Perm (Fin B.dim)
h : Membership.mem (γ := Finset (Equiv.Perm (Fin B.dim))) univ σ
j : Fin B.dim
h_1 : Membership.mem (γ := Finset (Fin B.dim)) univ j
hji : ¬j = i
⊢ Membership.mem.{u, u} (α := K) (γ := Subalgebra R K) ⊥
    (if False then (trace K L : (a : L) → K) (z * B.gen ^ (↑((σ : (a : Fin B.dim) → Fin B.dim) j) : ℕ))
      else
        traceMatrix.{u, v, 0} K (B := L) (fun (i : Fin B.dim) ↦ B.gen ^ (↑i : ℕ)) ((σ : (a : Fin B.dim) → Fin B.dim) j)
          j :
      K)

Tactic:
exact mem_bot.2
      (IsIntegrallyClosed.isIntegral_iff.1 <| isIntegral_trace <| (hint.pow _).mul (hint.pow _))

Premises used: Iff.mpr, IsIntegrallyClosed.isIntegral_iff, IsIntegral.mul, Algebra.isIntegral_trace, Algebra.mem_bot, IsIntegral.pow, Iff.mp
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
⊢ discr (ι := ι) ℤ (B := A)
      ((⇑b' : (a : ι) → A) ᵥ* Matrix.map (b'.toMatrix (⇑b : (a : ι) → A)) (⇑(algebraMap ℤ A) : (a : ℤ) → A)) =
    HPow.hPow (β := ℕ) (det (b'.toMatrix (⇑b : (a : ι) → A))) 2 *
      discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)

Tactic:
Algebra.discr_of_matrix_vecMul b' (b'.toMatrix b)

Premises used: Module.Basis.toMatrix, Algebra.discr_of_matrix_vecMul, DFunLike.coe
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
h :
  Eq (α := ι → A) (⇑b : (a : ι) → A)
    ((⇑b' : (a : ι) → A) ᵥ* Matrix.map (b'.toMatrix (⇑b : (a : ι) → A)) (⇑(algebraMap ℤ A) : (a : ℤ) → A))
h₁ :
  discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A) =
    HPow.hPow (β := ℕ) (det (b'.toMatrix (⇑b : (a : ι) → A))) 2 *
      discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)
⊢ discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b : (a : ι) → A) = discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)

Tactic:
convert! Algebra.discr_of_matrix_vecMul b' (b'.toMatrix b)

Premises used: Module.Basis.toMatrix, Algebra.discr_of_matrix_vecMul, DFunLike.coe
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
h h₁ : Eq (α := ι → A) (⇑b : (a : ι) → A) (⇑b : (a : ι) → A)
⊢ Eq (α := ι → A) (⇑b : (a : ι) → A)
    ((⇑b' : (a : ι) → A) ᵥ* Matrix.map (b'.toMatrix (⇑b : (a : ι) → A)) (⇑(algebraMap ℤ A) : (a : ℤ) → A))

Tactic:
rw [Basis.toMatrix_map_vecMul]

Premises used: Module.Basis.toMatrix_map_vecMul
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
this : IsUnit (det (b'.toMatrix (⇑b : (a : ι) → A)))
⊢ HPow.hPow (β := ℕ) (det (b'.toMatrix (⇑b : (a : ι) → A))) 2 = 1

Tactic:
rw [Int.isUnit_iff, ← sq_eq_one_iff] at this

Premises used: sq_eq_one_iff, Int.isUnit_iff
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
this : HPow.hPow (β := ℕ) (det (b'.toMatrix (⇑b : (a : ι) → A))) 2 = 1
rw :
  discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A) = 1 * discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)
rw₁ rw₂ :
  discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A) = discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)
⊢ discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A) =
    HPow.hPow (β := ℕ) (det (b'.toMatrix (⇑b : (a : ι) → A))) 2 *
      discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)

Tactic:
rw [this, one_mul]

Premises used: one_mul
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
h : IsUnit (det (b'.toMatrix (⇑b : (a : ι) → A)))
⊢ discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A) =
    HPow.hPow (β := ℕ) (det (b'.toMatrix (⇑b : (a : ι) → A))) 2 *
      discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)

Tactic:
suffices IsUnit (b'.toMatrix b).det by
      rw [Int.isUnit_iff, ← sq_eq_one_iff] at this
      rw [this, one_mul]
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
h : IsUnit (M := ℤ) (det.{0, w} (n := ι) ((LinearMap.toMatrix b b' : (a : A →ₗ[ℤ] A) → Matrix ι ι ℤ) LinearMap.id))
⊢ IsUnit (det (b'.toMatrix (⇑b : (a : ι) → A)))

Tactic:
rw [← LinearMap.toMatrix_id_eq_basis_toMatrix b b']

Premises used: LinearMap.toMatrix_id_eq_basis_toMatrix
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
⊢ IsUnit (M := ℤ) (det.{0, w} (n := ι) ((LinearMap.toMatrix b b' : (a : A →ₗ[ℤ] A) → Matrix ι ι ℤ) LinearMap.id))

Tactic:
LinearEquiv.isUnit_det (LinearEquiv.refl ℤ A) b b'

Premises used: Int, LinearEquiv.isUnit_det, LinearEquiv.refl
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
⊢ IsUnit (M := ℤ) (det.{0, w} (n := ι) ((LinearMap.toMatrix b b' : (a : A →ₗ[ℤ] A) → Matrix ι ι ℤ) LinearMap.id))

Tactic:
exact LinearEquiv.isUnit_det (LinearEquiv.refl ℤ A) b b'

Premises used: Int, LinearEquiv.isUnit_det, LinearEquiv.refl
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Function.Surjective (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (β :=
    RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    (⇑(mkAlgHom R (Rel R M)) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))

Tactic:
RingQuot.mkAlgHom_surjective _ _

Premises used: RingQuot.mkAlgHom_surjective
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
rw :
  Eq (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((algebraMap R (MvPolynomial.{u_2, u_1} (ℕ × M) R) : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) a : DividedPowerAlgebra R M)
rw₁ rw₂ :
  Eq (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((algebraMap R (RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) : (a : R) → RingQuot (Rel R M)) a :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) a : DividedPowerAlgebra R M)
⊢ Eq (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) a : DividedPowerAlgebra R M)

Tactic:
rw [← MvPolynomial.algebraMap_eq, AlgHom.commutes]

Premises used: MvPolynomial.algebraMap_eq, AlgHom.commutes