awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
⊢ 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)
have 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)
Tactic: rw [mem_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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 : 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)
have 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)
Tactic: apply IsIntegrallyClosed.isIntegral_iff.mp
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
⊢ 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)
have hx : IsIntegral.{u_1, u} A (A := L) ((Algebra.linearMap B L : (a : B) → L) x : L)
Tactic: apply isIntegral_trace
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
⊢ IsIntegral.{u_1, u} A (A := L) ((Algebra.linearMap B L : (a : B) → L) x : L)
have hx : ∃ (y : B), Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) ((Algebra.linearMap B L : (a : B) → L) x : L)
Tactic: rw [IsIntegralClosure.isIntegral_iff (A := B)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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ᵛ
⊢ IsIntegral A (discr.{u_2, u, u_4} (ι := ι) K (B := L) (⇑b : (a : ι) → L) • a * x)
have hinv : 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
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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)))
⊢ IsIntegral A (discr.{u_2, u, u_4} (ι := ι) K (B := L) (⇑b : (a : ι) → L) • a * x)
have 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))
Tactic: have H := mulVec_cramer (traceMatrix K b) fun i => trace K L (x * a * b i)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)))
have rwa : IsUnit (M := Matrix ι ι K) (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L))
Tactic: rwa [mulVec_injective_iff_isUnit, isUnit_iff_isUnit_det]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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))
⊢ IsIntegral A (discr.{u_2, u, u_4} (ι := ι) K (B := L) (⇑b : (a : ι) → L) • a * x)
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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)))
⊢ IsIntegral A (discr.{u_2, u, u_4} (ι := ι) K (B := L) (⇑b : (a : ι) → L) • a * x)
have 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)
Tactic: rw [← traceMatrix_of_basis_mulVec, ← mulVec_smul, this.eq_iff,
    traceMatrix_of_basis_mulVec] at H
Cleared hypotheses: H, this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)))
⊢ IsIntegral A (discr.{u_2, u, u_4} (ι := ι) K (B := L) (⇑b : (a : ι) → L) • a * x)
have 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))
Tactic: rw [← b.equivFun.symm_apply_apply (_ * _), b.equivFun_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)))
⊢ 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))
have 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))
Tactic: apply IsIntegral.sum
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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))
have 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))
Tactic: rw [smul_mul_assoc, b.equivFun.map_smul, discr_def, mul_comm, ← H, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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))
have 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))
Tactic: refine RingHom.IsIntegralElem.mul _ ?_ (hb _)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
⊢ 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))
have 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)
Tactic: apply IsIntegral.algebraMap