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))
this :
  ∀ (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]
    (∑ x : Fin B.dim,
      discr.{u, v, 0} (ι := Fin B.dim) K (B := L) (⇑B.basis : (a : Fin B.dim) → L) •
        HSMul.hSMul.{u, v, v} (α := K) (β := L)
          ((((B.basis.repr : (a : L) → Fin B.dim →₀ K) z : Fin B.dim →₀ K) : (a : Fin B.dim) → K) x : K)
          ((B.basis : (a : Fin B.dim) → L) x : L))
have refine : ∀ (i : Fin B.dim),
  Membership.mem (γ := Finset (Fin B.dim)) univ 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) •
        HSMul.hSMul.{u, v, v} (α := K) (β := L)
          ((((B.basis.repr : (a : L) → Fin B.dim →₀ K) z : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i : K)
          ((B.basis : (a : Fin B.dim) → L) i : L))
Tactic: refine Subalgebra.sum_mem _ fun 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))) =
    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))
this :
  ∀ (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)
i : Fin B.dim
h : Membership.mem (γ := Finset (Fin B.dim)) univ 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) •
      HSMul.hSMul.{u, v, v} (α := K) (β := L)
        ((((B.basis.repr : (a : L) → Fin B.dim →₀ K) z : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i : K)
        ((B.basis : (a : Fin B.dim) → L) i : L))
have this₁ : 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: replace this := this i
Cleared hypotheses: this
-- 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))) =
    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
this :
  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) •
      HSMul.hSMul.{u, v, v} (α := K) (β := L)
        ((((B.basis.repr : (a : L) → Fin B.dim →₀ K) z : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i : K)
        ((B.basis : (a : Fin B.dim) → L) i : L))
have this₁ : Membership.mem (γ := Set K) (Set.range.{u, z + 1} (ι := R) (⇑(algebraMap R K) : (a : R) → K))
  (HSMul.hSMul (β := K) (discr.{u, v, 0} (ι := Fin B.dim) K (B := L) (⇑B.basis : (a : Fin B.dim) → L))
    ((B.basis.equivFun : (a : L) → Fin B.dim → K) z i : K))
Tactic: rw [← discr_def, Pi.smul_apply, mem_bot] at this
Cleared hypotheses: this
-- 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
h : Membership.mem (γ := Finset (Fin B.dim)) univ i
this :
  Membership.mem (γ := Set K) (Set.range.{u, z + 1} (ι := R) (⇑(algebraMap R K) : (a : R) → K))
    (HSMul.hSMul (β := K) (discr.{u, v, 0} (ι := Fin B.dim) K (B := L) (⇑B.basis : (a : Fin B.dim) → L))
      ((B.basis.equivFun : (a : L) → Fin B.dim → K) z i : K))
⊢ 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) •
      HSMul.hSMul.{u, v, v} (α := K) (β := L)
        ((((B.basis.repr : (a : L) → Fin B.dim →₀ K) z : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i : K)
        ((B.basis : (a : Fin B.dim) → L) i : L))
have obtain : ∀ (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.equivFun : (a : L) → Fin B.dim → K) z i : K)),
  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) •
      HSMul.hSMul.{u, v, v} (α := K) (β := L)
        ((((B.basis.repr : (a : L) → Fin B.dim →₀ K) z : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i : K)
        ((B.basis : (a : Fin B.dim) → L) i : L))
Tactic: obtain ⟨r, hr⟩ := this
Cleared hypotheses: this
-- 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))) =
    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.equivFun : (a : L) → Fin B.dim → K) z i : K)
⊢ 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) •
      HSMul.hSMul.{u, v, v} (α := K) (β := L)
        ((((B.basis.repr : (a : L) → Fin B.dim →₀ K) z : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i : K)
        ((B.basis : (a : Fin B.dim) → L) i : L))
have 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)
Tactic: rw [Basis.equivFun_apply] at hr
Cleared hypotheses: hr
-- 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
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]
    (discr.{u, v, 0} (ι := Fin B.dim) K (B := L) (⇑B.basis : (a : Fin B.dim) → L) •
      HSMul.hSMul.{u, v, v} (α := K) (β := L)
        ((((B.basis.repr : (a : L) → Fin B.dim →₀ K) z : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i : K)
        ((B.basis : (a : Fin B.dim) → L) i : L))
have rw : Membership.mem (γ := Subalgebra R L) R[B.gen] (HSMul.hSMul (β := L) r ((B.basis : (a : Fin B.dim) → L) i : L))
Tactic: rw [← smul_assoc, ← hr, algebraMap_smul]
-- 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
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] (HSMul.hSMul (β := L) r ((B.basis : (a : Fin B.dim) → L) i : L))
have refine : Membership.mem (α := L) (γ := Subalgebra R L) R[B.gen] ((B.basis : (a : Fin B.dim) → L) i : L)
Tactic: refine Subalgebra.smul_mem _ ?_ _
-- 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
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 (α := L) (γ := Subalgebra R L) R[B.gen] ((B.basis : (a : Fin B.dim) → L) i : L)
have rw : Membership.mem (γ := Subalgebra R L) R[B.gen] (B.gen ^ (↑i : ℕ))
Tactic: rw [B.basis_eq_pow 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))
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))
⊢ 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)
have 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)
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 _)) _