-- Mathlib/RingTheory/Discriminant.lean
theorem discr_mul_isIntegral_mem_adjoin [Algebra.IsSeparable K L] [IsIntegrallyClosed R]
    [IsFractionRing R K] {B : PowerBasis K L} (hint : IsIntegral R B.gen) {z : L}
    (hz : IsIntegral R z) : discr K B.basis • z ∈ adjoin R ({B.gen} : Set L)

Proof state:
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
⊢ discr K ⇑B.basis • z ∈ adjoin R {B.gen}

Tactic:
have H :
  (traceMatrix K B.basis).det • (traceMatrix K B.basis) *ᵥ (B.basis.equivFun z) =
    (traceMatrix K B.basis).det • fun i => trace K L (z * B.basis i) := by
  congr; exact traceMatrix_of_basis_mulVec _ _

Result:
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)
⊢ discr K ⇑B.basis • z ∈ adjoin R {B.gen}

Proof state:
case intro
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i => (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : (algebraMap R K) r = discr K ⇑B.basis • (B.basis.repr z) i
⊢ r • B.basis i ∈ adjoin R {B.gen}

Tactic:
refine Subalgebra.smul_mem _ ?_ _

Result:
case intro
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i => (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : (algebraMap R K) r = discr K ⇑B.basis • (B.basis.repr z) i
⊢ B.basis i ∈ adjoin R {B.gen}

Proof state:
case intro
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i => (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : (algebraMap R K) r = discr K ⇑B.basis • (B.basis.repr z) i
⊢ B.basis i ∈ adjoin R {B.gen}

Tactic:
rw [B.basis_eq_pow i]

Result:
case intro
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i => (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : (algebraMap R K) r = discr K ⇑B.basis • (B.basis.repr z) i
⊢ B.gen ^ ↑i ∈ adjoin R {B.gen}

Proof state:
case neg
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i => (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
σ : Equiv.Perm (Fin B.dim)
x✝¹ : σ ∈ univ
j : Fin B.dim
x✝ : j ∈ univ
hji : ¬j = i
⊢ (traceMatrix K ⇑B.basis).updateCol i (fun i => (trace K L) (z * B.basis i)) (σ j) j ∈ ⊥

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

Result:
case neg
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i => (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
σ : Equiv.Perm (Fin B.dim)
x✝¹ : σ ∈ univ
j : Fin B.dim
x✝ : j ∈ univ
hji : ¬j = i
⊢ (if False then (trace K L) (z * B.gen ^ ↑(σ j)) else traceMatrix K (fun i => B.gen ^ ↑i) (σ j) j) ∈ ⊥