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
x : B
rw :
  ∃ (y : A),
    Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y : K)
      (((↑A :
                {S : Type u_2} →
                  {M : Type u} →
                    {M₂ : Type u_2} →
                      [inst : Semiring A] →
                        [inst_15 : Semiring S] →
                          [inst_16 : AddCommMonoid M] →
                            [inst_17 : AddCommMonoid M₂] →
                              [inst_18 : Module A M] →
                                [inst_19 : Module A M₂] →
                                  [inst_20 : Module S M] →
                                    [inst_21 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
              (Algebra.trace K L) :
            (a : L) → K)
          ((Algebra.linearMap B L : (a : B) → L) x : L) :
        K)
⊢ Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1
    (((↑A :
              {S : Type u_2} →
                {M : Type u} →
                  {M₂ : Type u_2} →
                    [inst : Semiring A] →
                      [inst_15 : Semiring S] →
                        [inst_16 : AddCommMonoid M] →
                          [inst_17 : AddCommMonoid M₂] →
                            [inst_18 : Module A M] →
                              [inst_19 : Module A M₂] →
                                [inst_20 : Module S M] →
                                  [inst_21 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
            (Algebra.trace K L) :
          (a : L) → K)
        ((Algebra.linearMap B L : (a : B) → L) x : L) :
      K)

Tactic:
rw [mem_one]

Premises used: Submodule.mem_one
-- 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
x : B
apply :
  IsIntegral.{u_1, u_2} A (A := K)
    (((↑A :
              {S : Type u_2} →
                {M : Type u} →
                  {M₂ : Type u_2} →
                    [inst : Semiring A] →
                      [inst_15 : Semiring S] →
                        [inst_16 : AddCommMonoid M] →
                          [inst_17 : AddCommMonoid M₂] →
                            [inst_18 : Module A M] →
                              [inst_19 : Module A M₂] →
                                [inst_20 : Module S M] →
                                  [inst_21 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
            (Algebra.trace K L) :
          (a : L) → K)
        ((Algebra.linearMap B L : (a : B) → L) x : L) :
      K)
⊢ ∃ (y : A),
    Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y : K)
      (((↑A :
                {S : Type u_2} →
                  {M : Type u} →
                    {M₂ : Type u_2} →
                      [inst : Semiring A] →
                        [inst_15 : Semiring S] →
                          [inst_16 : AddCommMonoid M] →
                            [inst_17 : AddCommMonoid M₂] →
                              [inst_18 : Module A M] →
                                [inst_19 : Module A M₂] →
                                  [inst_20 : Module S M] →
                                    [inst_21 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
              (Algebra.trace K L) :
            (a : L) → K)
          ((Algebra.linearMap B L : (a : B) → L) x : L) :
        K)

Tactic:
apply IsIntegrallyClosed.isIntegral_iff.mp

Premises used: IsIntegrallyClosed.isIntegral_iff, Iff.mp
-- 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
x : B
hx : IsIntegral.{u_1, u} A (A := L) ((Algebra.linearMap B L : (a : B) → L) x : L)
⊢ IsIntegral.{u_1, u_2} A (A := K)
    (((↑A :
              {S : Type u_2} →
                {M : Type u} →
                  {M₂ : Type u_2} →
                    [inst : Semiring A] →
                      [inst_15 : Semiring S] →
                        [inst_16 : AddCommMonoid M] →
                          [inst_17 : AddCommMonoid M₂] →
                            [inst_18 : Module A M] →
                              [inst_19 : Module A M₂] →
                                [inst_20 : Module S M] →
                                  [inst_21 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
            (Algebra.trace K L) :
          (a : L) → K)
        ((Algebra.linearMap B L : (a : B) → L) x : L) :
      K)

Tactic:
apply isIntegral_trace

Premises used: Algebra.isIntegral_trace
-- 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
x : B
hx : ∃ (y : B), Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) ((Algebra.linearMap B L : (a : B) → L) x : L)
⊢ IsIntegral.{u_1, u} A (A := L) ((Algebra.linearMap B L : (a : B) → L) x : L)

Tactic:
rw [IsIntegralClosure.isIntegral_iff (A := B)]

Premises used: IsIntegralClosure.isIntegral_iff
-- 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
x : B
⊢ ∃ (y : B), Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) ((Algebra.linearMap B L : (a : B) → L) x : L)

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- 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
x : B
⊢ ∃ (y : B), Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) ((Algebra.linearMap B L : (a : B) → L) x : L)

Tactic:
exact ⟨_, rfl⟩
-- 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ᵛ
⊢ IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))

Tactic:
simpa [← discr_def] using discr_isUnit_of_basis _ b

Premises used: Algebra.discr_def, Algebra.discr_isUnit_of_basis
-- 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ᵛ
⊢ IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))

Tactic:
have hinv : IsUnit (traceMatrix K b).det := by
    simpa [← discr_def] using discr_isUnit_of_basis _ b
-- 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)))
⊢ (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → 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))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      fun (i : ι) ↦ (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))

Tactic:
have H := mulVec_cramer (traceMatrix K b) fun i => trace K L (x * a * b i)
-- 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 :
  (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → 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))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      fun (i : ι) ↦ (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))
rwa : IsUnit (M := Matrix ι ι K) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L))
rwa₁ rwa₂ rwa₃ rwa₄ : IsUnit (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
⊢ Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))

Tactic:
rwa [mulVec_injective_iff_isUnit, isUnit_iff_isUnit_det]

Premises used: Matrix.isUnit_iff_isUnit_det, Matrix.mulVec_injective_iff_isUnit
-- 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 :
  (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → 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))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      fun (i : ι) ↦ (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))
⊢ Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))

Tactic:
have : Function.Injective (traceMatrix K b).mulVec := by
    rwa [mulVec_injective_iff_isUnit, isUnit_iff_isUnit_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 :
  (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → 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))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      fun (i : ι) ↦ (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))
this : Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → 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))) =
    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)

Tactic:
rw [← traceMatrix_of_basis_mulVec, ← mulVec_smul, this.eq_iff,
    traceMatrix_of_basis_mulVec] at H

Premises used: Function.Injective.eq_iff, Matrix.mulVec_smul, Algebra.traceMatrix_of_basis_mulVec
-- 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 :
  (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → 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))) =
    HSMul.hSMul (β := ι → K) (det.{u_2, u_4} (n := ι) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))
      fun (i : ι) ↦ (Algebra.trace K L : (a : L) → K) (HMul.hMul (β := L) (x * a) ((b : (a : ι) → L) i : L))
this : Function.Injective (α := ι → K) (mulVec (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)
⊢ Function.Injective (α := ι → K) (mulVec (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L)))

Tactic:
rw [← traceMatrix_of_basis_mulVec, ← mulVec_smul, this.eq_iff,
    traceMatrix_of_basis_mulVec] at H

Premises used: Function.Injective.eq_iff, Matrix.mulVec_smul, Algebra.traceMatrix_of_basis_mulVec
-- 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)))
rw :
  IsIntegral.{u_1, u} A (A := L)
    (∑ i : ι,
      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))
⊢ IsIntegral A (discr.{u_2, u, u_4} (ι := ι) K (B := L) (⇑b : (a : ι) → L) • a * x)

Tactic:
rw [← b.equivFun.symm_apply_apply (_ * _), b.equivFun_symm_apply]

Premises used: Module.Basis.equivFun_symm_apply, HMul.hMul, LinearEquiv.symm_apply_apply, 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)))
h :
  ∀ (x_1 : ι),
    Membership.mem (γ := Finset ι) Finset.univ x_1 →
      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) x_1 : K)
          ((b : (a : ι) → L) x_1 : L))
⊢ IsIntegral.{u_1, u} A (A := L)
    (∑ i : ι,
      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:
apply IsIntegral.sum

Premises used: IsIntegral.sum
-- 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
      (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))
⊢ Membership.mem (γ := Finset ι) Finset.univ i →
    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:
_