awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ 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)
have 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)
Tactic: rw [← H, ← mulVec_smul] at cramer
Cleared hypotheses: cramer, i
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
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
⊢ 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)
have 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)
Tactic: replace cramer := congr_arg (mulVec (traceMatrix K B.basis)⁻¹) cramer
Cleared hypotheses: cramer
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
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)
⊢ 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)
have 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)
Tactic: rw [mulVec_mulVec, nonsing_inv_mul _ hinv, mulVec_mulVec, nonsing_inv_mul _ hinv, one_mulVec,
    one_mulVec] at cramer
Cleared hypotheses: cramer
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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) ⊥
    (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)
have 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))
Tactic: rw [← congr_fun cramer i, cramer_apply, det_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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))
have _ : ∀ (σ : 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)
Tactic: refine
    Subalgebra.sum_mem _ fun σ _ => Subalgebra.zsmul_mem _ (Subalgebra.prod_mem _ fun j _ => ?_) _
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ 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)
have 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)
Tactic: by_cases hji : j = i
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hji : j = i
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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 (γ := 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)
have 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)
Tactic: simp only [updateCol_apply, hji, PowerBasis.coe_basis]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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 (γ := 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)
have 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)
Tactic: simp only [updateCol_apply, hji, PowerBasis.coe_basis]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
⊢ discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b : (a : ι) → A) = discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)
have h : Eq (α := ι → A) (⇑b : (a : ι) → A)
  ((⇑b' : (a : ι) → A) ᵥ* Matrix.map (b'.toMatrix (⇑b : (a : ι) → A)) (⇑(algebraMap ℤ A) : (a : ℤ) → A))
Tactic: convert! Algebra.discr_of_matrix_vecMul b' (b'.toMatrix b)