awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst_16 : DecidableEq ι
inst_17 : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral.{u_1, u} A (A := L) ((b : (a : ι) → L) i : L)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
H :
  ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K) fun (i : ι) ↦
      (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      ((b.equivFun : (a : L) → ι → K) (x * a) : ι → K)
this : Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
h :
  IsIntegral A
    (HMul.hMul (α := L) (β := L)
      ((algebraMap K L : (a : K) → L)
          ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K)
              (fun (i : ι) ↦ (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L)))
              i :
            K) :
        L)
      ((b : (a : ι) → L) i : L))
⊢ IsIntegral A
    (HSMul.hSMul.{u_2, u, u} (α := K) (β := L)
      ((b.equivFun : (a : L) → ι → K) (discr.{u_2, u, u_4} (ι := ι) K (B := L) (⇑b : (a : ι) → L) • a * x) i : K)
      ((b : (a : ι) → L) i : L))

Tactic:
rw [smul_mul_assoc, b.equivFun.map_smul, discr_def, mul_comm, ← H, Algebra.smul_def]

Premises used: smul_mul_assoc, Algebra.discr_def, LinearEquiv.map_smul, mul_comm, Algebra.smul_def, Module.Basis.equivFun
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst_16 : DecidableEq ι
inst_17 : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral.{u_1, u} A (A := L) ((b : (a : ι) → L) i : L)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
H :
  ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K) fun (i : ι) ↦
      (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      ((b.equivFun : (a : L) → ι → K) (x * a) : ι → K)
this : Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ IsIntegral A
    (HMul.hMul (α := L) (β := L)
      ((algebraMap K L : (a : K) → L)
          ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K)
              (fun (i : ι) ↦ (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L)))
              i :
            K) :
        L)
      ((b : (a : ι) → L) i : L))

Tactic:
RingHom.IsIntegralElem.mul _ ?_ (hb _)

Premises used: IsIntegral, RingHom.IsIntegralElem.mul
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst_16 : DecidableEq ι
inst_17 : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral.{u_1, u} A (A := L) ((b : (a : ι) → L) i : L)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
H :
  ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K) fun (i : ι) ↦
      (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      ((b.equivFun : (a : L) → ι → K) (x * a) : ι → K)
this : Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
h :
  RingHom.IsIntegralElem (algebraMap A L)
    ((algebraMap K L : (a : K) → L)
      ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K)
          (fun (i : ι) ↦ (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) i :
        K))
⊢ IsIntegral A
    (HMul.hMul (α := L) (β := L)
      ((algebraMap K L : (a : K) → L)
          ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K)
              (fun (i : ι) ↦ (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L)))
              i :
            K) :
        L)
      ((b : (a : ι) → L) i : L))

Tactic:
refine RingHom.IsIntegralElem.mul _ ?_ (hb _)

Premises used: RingHom.IsIntegralElem.mul
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst_16 : DecidableEq ι
inst_17 : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral.{u_1, u} A (A := L) ((b : (a : ι) → L) i : L)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
H :
  ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K) fun (i : ι) ↦
      (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      ((b.equivFun : (a : L) → ι → K) (x * a) : ι → K)
this : Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
h :
  IsIntegral.{u_1, u_2} A (A := K)
    ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K)
        (fun (i : ι) ↦ (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) i :
      K)
⊢ RingHom.IsIntegralElem (algebraMap A L)
    ((algebraMap K L : (a : K) → L)
      ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K)
          (fun (i : ι) ↦ (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) i :
        K))

Tactic:
apply IsIntegral.algebraMap

Premises used: IsIntegral.algebraMap
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst_16 : DecidableEq ι
inst_17 : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral.{u_1, u} A (A := L) ((b : (a : ι) → L) i : L)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
H :
  ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K) fun (i : ι) ↦
      (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      ((b.equivFun : (a : L) → ι → K) (x * a) : ι → K)
this : Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
h :
  IsIntegral A
    (updateCol (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) i fun (i : ι) ↦
        (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))).det
⊢ IsIntegral.{u_1, u_2} A (A := K)
    ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K)
        (fun (i : ι) ↦ (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) i :
      K)

Tactic:
rw [cramer_apply]

Premises used: Matrix.cramer_apply
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst_16 : DecidableEq ι
inst_17 : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral.{u_1, u} A (A := L) ((b : (a : ι) → L) i : L)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
H :
  ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K) fun (i : ι) ↦
      (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      ((b.equivFun : (a : L) → ι → K) (x * a) : ι → K)
this : Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
h :
  ∀ (i_1 j : ι),
    IsIntegral A
      (updateCol (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) i
        (fun (i : ι) ↦ (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) i_1 j)
⊢ IsIntegral A
    (updateCol (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) i fun (i : ι) ↦
        (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))).det

Tactic:
apply IsIntegral.det

Premises used: IsIntegral.det
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst_16 : DecidableEq ι
inst_17 : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral.{u_1, u} A (A := L) ((b : (a : ι) → L) i : L)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
H :
  ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K) fun (i : ι) ↦
      (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      ((b.equivFun : (a : L) → ι → K) (x * a) : ι → K)
this : Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
j k : ι
h :
  IsIntegral.{u_1, u_2} A (A := K)
    (if k = i then (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) j : L))
      else traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L) j k :
      K)
⊢ IsIntegral A
    (updateCol (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) i
      (fun (i : ι) ↦ (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) j k)

Tactic:
rw [updateCol_apply]

Premises used: Matrix.updateCol_apply
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst_16 : DecidableEq ι
inst_17 : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral.{u_1, u} A (A := L) ((b : (a : ι) → L) i : L)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
H :
  ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K) fun (i : ι) ↦
      (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      ((b.equivFun : (a : L) → ι → K) (x * a) : ι → K)
this : Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
j k : ι
h :
  k = i →
    IsIntegral.{u_1, u_2} A (A := K)
      ((Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) j : L)) : K)
h₁ : ¬k = i → IsIntegral A (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L) j k)
⊢ IsIntegral.{u_1, u_2} A (A := K)
    (if k = i then (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) j : L))
      else traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L) j k :
      K)

Tactic:
split
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst_16 : DecidableEq ι
inst_17 : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral.{u_1, u} A (A := L) ((b : (a : ι) → L) i : L)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
H :
  ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K) fun (i : ι) ↦
      (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      ((b.equivFun : (a : L) → ι → K) (x * a) : ι → K)
this : Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
j k : ι
h_2 : k = i
h :
  IsIntegral.{u_1, u_2} A (A := K)
    ((Algebra.trace K L : (a : L) → K) (x * HMul.hMul (β := L) a ((b : (a : ι) → L) j : L)) : K)
⊢ IsIntegral.{u_1, u_2} A (A := K)
    ((Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) j : L)) : K)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst_16 : DecidableEq ι
inst_17 : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral.{u_1, u} A (A := L) ((b : (a : ι) → L) i : L)
a x : L
ha : a ∈ I
hx : x ∈ Iᵛ
hinv : IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
H :
  ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K) fun (i : ι) ↦
      (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      ((b.equivFun : (a : L) → ι → K) (x * a) : ι → K)
this : Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
j k : ι
h_2 : k = i
h :
  ∀
    (hx :
      ∀ a ∈ I,
        IsIntegral.{u_1, u_2} A (A := K) ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) a : K))
    (hinv : IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L))))
    (H :
      ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K) fun (i : ι) ↦
          (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) =
        HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
          ((b.equivFun : (a : L) → ι → K) (x * a) : ι → K))
    (this : Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))) (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      ∀ (j k : ι),
        k = i →
          IsIntegral.{u_1, u_2} A (A := K)
            ((Algebra.trace K L : (a : L) → K) (x * HMul.hMul (β := L) a ((b : (a : ι) → L) j : L)) : K)
⊢ IsIntegral.{u_1, u_2} A (A := K)
    ((Algebra.trace K L : (a : L) → K) (x * HMul.hMul (β := L) a ((b : (a : ι) → L) j : L)) : K)

Tactic:
rw [mem_traceDual_iff_isIntegral] at hx

Premises used: Submodule.mem_traceDual_iff_isIntegral
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst_16 : DecidableEq ι
inst_17 : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral.{u_1, u} A (A := L) ((b : (a : ι) → L) i : L)
a x : L
ha : a ∈ I
hx :
  ∀ a ∈ I,
    IsIntegral.{u_1, u_2} A (A := K) ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) a : K)
hinv : IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
H :
  ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K) fun (i : ι) ↦
      (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      ((b.equivFun : (a : L) → ι → K) (x * a) : ι → K)
this : Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
j k : ι
h_2 : k = i
h : HMul.hMul (β := L) a ((b : (a : ι) → L) j : L) ∈ I
⊢ IsIntegral.{u_1, u_2} A (A := K)
    ((Algebra.trace K L : (a : L) → K) (x * HMul.hMul (β := L) a ((b : (a : ι) → L) j : L)) : K)

Tactic:
apply hx
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_4
inst_16 : DecidableEq ι
inst_17 : Fintype ι
b : Basis ι K L
hb : ∀ (i : ι), IsIntegral.{u_1, u} A (A := L) ((b : (a : ι) → L) i : L)
a x : L
ha : a ∈ I
hx :
  ∀ a ∈ I,
    IsIntegral.{u_1, u_2} A (A := K) ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) a : K)
hinv : IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
H :
  ((cramer (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)) : (a : ι → K) → ι → K) fun (i : ι) ↦
      (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      ((b.equivFun : (a : L) → ι → K) (x * a) : ι → K)
this : Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
j k : ι
h_2 : k = i
h :
  ∀ (y : B) (hy : Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) ((b : (a : ι) → L) j : L)),
    HMul.hMul (β := L) a ((b : (a : ι) → L) j : L) ∈ I
⊢ HMul.hMul (β := L) a ((b : (a : ι) → L) j : L) ∈ I

Tactic:
have ⟨y, hy⟩ := (IsIntegralClosure.isIntegral_iff (A := B)).mp (hb j)