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))
cramer :
  (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
      (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))) 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
h : Membership.mem (γ := Finset (Fin B.dim)) univ i
r : R
hr :
  (algebraMap R K : (a : R) → K) r =
    HSMul.hSMul (β := K) (discr.{u, v, 0} (ι := Fin B.dim) K (B := L) (⇑B.basis : (a : Fin B.dim) → L))
      ((((B.basis.repr : (a : L) → Fin B.dim →₀ K) z : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i : K)
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] (B.gen ^ (↑i : ℕ))

Tactic:
Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _

Premises used: Set.mem_singleton, Set.Mem, Algebra.subset_adjoin, Subalgebra.pow_mem
-- 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))
cramer :
  (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
      (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))) 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
h : Membership.mem (γ := Finset (Fin B.dim)) univ i
r : R
hr :
  (algebraMap R K : (a : R) → K) r =
    HSMul.hSMul (β := K) (discr.{u, v, 0} (ι := Fin B.dim) K (B := L) (⇑B.basis : (a : Fin B.dim) → L))
      ((((B.basis.repr : (a : L) → Fin B.dim →₀ K) z : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i : K)
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] (B.gen ^ (↑i : ℕ))

Tactic:
exact Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _

Premises used: Set.mem_singleton, Algebra.subset_adjoin, Subalgebra.pow_mem
-- 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))
cramer :
  (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
      (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))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
suffices :
  ∀ (i : Fin B.dim),
    Membership.mem (γ := Subalgebra R K) ⊥
      (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) i)
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen]
    (discr.{u, v, 0} (ι := Fin B.dim) K (B := L) (⇑B.basis : (a : Fin B.dim) → L) • z)

Tactic:
suffices ∀ i, ((traceMatrix K B.basis).det • B.basis.equivFun z) i ∈ (⊥ : Subalgebra R K) by
    rw [← B.basis.sum_repr z, Finset.smul_sum]
    refine Subalgebra.sum_mem _ fun i _ => ?_
    replace this := this i
    rw [← discr_def, Pi.smul_apply, mem_bot] at this
    obtain ⟨r, hr⟩ := this
    rw [Basis.equivFun_apply] at hr
    rw [← smul_assoc, ← hr, algebraMap_smul]
    refine Subalgebra.smul_mem _ ?_ _
    rw [B.basis_eq_pow i]
    exact Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _
-- 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))
cramer :
  (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
      (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))) 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
rw :
  ∀
    (cramer :
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
          (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))) =
        traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → 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))
    (i : Fin B.dim),
    Membership.mem (γ := Subalgebra R K) ⊥
      (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) i)
⊢ Membership.mem (γ := Subalgebra R K) ⊥
    (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) i)

Tactic:
rw [← H, ← mulVec_smul] at cramer

Premises used: Matrix.mulVec_smul
-- 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))
cramer :
  (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
      (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))) =
    traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → 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)
i : 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) *ᵥ
        (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))) =
    (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) *ᵥ
        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)

Tactic:
replace cramer := congr_arg (mulVec (traceMatrix K B.basis)⁻¹) cramer
-- 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 :
  ((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) *ᵥ
        (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))) =
    (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) *ᵥ
        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)
⊢ ((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)

Tactic:
rw [mulVec_mulVec, nonsing_inv_mul _ hinv, mulVec_mulVec, nonsing_inv_mul _ hinv, one_mulVec,
    one_mulVec] at cramer

Premises used: Matrix.nonsing_inv_mul, Matrix.one_mulVec, Matrix.mulVec_mulVec
-- 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)
rw :
  Membership.mem (γ := Subalgebra R K) ⊥
    (∑ σ : Equiv.Perm (Fin B.dim),
      HSMul.hSMul (α := ℤˣ) (β := K) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin B.dim)) → ℤˣ) σ : ℤˣ)
        (∏ i_1 : Fin B.dim,
          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) i_1) i_1))
⊢ Membership.mem (γ := Subalgebra R K) ⊥
    (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) i)

Tactic:
rw [← congr_fun cramer i, cramer_apply, det_apply]

Premises used: Matrix.det_apply, Matrix.cramer_apply, congr_fun
-- 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)
⊢ Membership.mem (γ := Subalgebra R K) ⊥
    (∑ σ : Equiv.Perm (Fin B.dim),
      HSMul.hSMul (α := ℤˣ) (β := K) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin B.dim)) → ℤˣ) σ : ℤˣ)
        (∏ i_1 : Fin B.dim,
          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) i_1) i_1))

Tactic:
Subalgebra.sum_mem _ fun σ _ => Subalgebra.zsmul_mem _ (Subalgebra.prod_mem _ fun j _ => ?_) _

Premises used: Units.val, Set.Mem, Equiv.Perm.sign, Subalgebra.sum_mem, Bot.bot, Subalgebra.zsmul_mem, DFunLike.coe
-- 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)),
    Membership.mem (γ := Finset (Equiv.Perm (Fin B.dim))) univ σ →
      ∀ (j : Fin B.dim),
        Membership.mem (γ := Finset (Fin B.dim)) univ 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)
⊢ Membership.mem (γ := Subalgebra R K) ⊥
    (∑ σ : Equiv.Perm (Fin B.dim),
      HSMul.hSMul (α := ℤˣ) (β := K) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin B.dim)) → ℤˣ) σ : ℤˣ)
        (∏ i_1 : Fin B.dim,
          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) i_1) i_1))

Tactic:
refine
    Subalgebra.sum_mem _ fun σ _ => Subalgebra.zsmul_mem _ (Subalgebra.prod_mem _ fun j _ => ?_) _

Premises used: Subalgebra.sum_mem, Subalgebra.zsmul_mem