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))
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))

Tactic:
Subalgebra.sum_mem _ fun i _ => ?_

Premises used: Set.Mem, Subalgebra.sum_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))
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)
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))
⊢ 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))

Tactic:
refine Subalgebra.sum_mem _ fun i _ => ?_

Premises used: Subalgebra.sum_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))
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 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
-- 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
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 (γ := 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

Premises used: Algebra.mem_bot, Algebra.discr_def, Pi.smul_apply
-- 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
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))
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))
⊢ 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
-- 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.equivFun : (a : L) → Fin B.dim → K) z i : K)
⊢ (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

Premises used: Module.Basis.equivFun_apply
-- 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)
rw : Membership.mem (γ := Subalgebra R L) R[B.gen] (HSMul.hSMul (β := L) r ((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) •
      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:
rw [← smul_assoc, ← hr, algebraMap_smul]

Premises used: smul_assoc, algebraMap_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))) =
    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))

Tactic:
Subalgebra.smul_mem _ ?_ _

Premises used: Set.Mem, Subalgebra.smul_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)
refine : Membership.mem (α := L) (γ := Subalgebra R L) R[B.gen] ((B.basis : (a : Fin B.dim) → L) i : L)
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] (HSMul.hSMul (β := L) r ((B.basis : (a : Fin B.dim) → L) i : L))

Tactic:
refine Subalgebra.smul_mem _ ?_ _

Premises used: Subalgebra.smul_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)
rw : Membership.mem (γ := Subalgebra R L) R[B.gen] (B.gen ^ (↑i : ℕ))
⊢ Membership.mem (α := L) (γ := Subalgebra R L) R[B.gen] ((B.basis : (a : Fin B.dim) → L) i : L)

Tactic:
rw [B.basis_eq_pow i]

Premises used: PowerBasis.basis_eq_pow