-- 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
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
⊢ ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥

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

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)
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),
      Equiv.Perm.sign σ •
        ∏ i_1 : Fin B.dim, (traceMatrix K ⇑B.basis).updateCol i (fun i => (trace K L) (z * B.basis i)) (σ i_1) i_1 ∈
    ⊥

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
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
⊢ (traceMatrix K ⇑B.basis).updateCol i (fun i => (trace K L) (z * B.basis i)) (σ j) j ∈ ⊥

Tactic:
by_cases hji : j = i

Result:
case pos
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 ∈ ⊥

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 ∈ ⊥

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.equivFun z i
⊢ discr K ⇑B.basis • (B.basis.repr z) i • B.basis i ∈ adjoin R {B.gen}

Tactic:
rw [Basis.equivFun_apply] at hr

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
⊢ discr K ⇑B.basis • (B.basis.repr z) i • B.basis i ∈ adjoin R {B.gen}