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
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.{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)
have 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
Tactic: rw [cramer_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)))
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ 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
have 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)
Tactic: apply IsIntegral.det
-- 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
j 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)
have 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)
Tactic: rw [updateCol_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)))
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
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)
have 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)
Tactic: split
-- 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_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)
⊢ 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)
have h₁ : ¬k = i → IsIntegral A (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L) j k)
Tactic: split
-- 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
j k : ι
h_1 : 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)
have 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)
Tactic: rw [mul_assoc]
-- 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
j k : ι
h_1 : 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)
have 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)
Tactic: rw [mem_traceDual_iff_isIntegral] at hx
Cleared hypotheses: hx, hinv, H, this, i, h, j, k, h_1
-- 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 :
  ∀ 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 : Membership.mem (γ := Finset ι) Finset.univ i
j k : ι
h_1 : 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)
have h : HMul.hMul (β := L) a ((b : (a : ι) → L) j : L) ∈ I
Tactic: apply hx
-- 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 :
  ∀ 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 : Membership.mem (γ := Finset ι) Finset.univ i
j k : ι
h_1 : k = i
⊢ HMul.hMul (β := L) a ((b : (a : ι) → L) j : L) ∈ I
have 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
Tactic: have ⟨y, hy⟩ := (IsIntegralClosure.isIntegral_iff (A := B)).mp (hb j)
-- 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 :
  ∀ 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 : Membership.mem (γ := Finset ι) Finset.univ i
j k : ι
h_1 : k = i
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
have h : y • a ∈ I
Tactic: rw [mul_comm, ← hy, ← 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.194059
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
inst_16 : IsDomain A
inst_17 : IsFractionRing B L
inst_18 : Nontrivial B
inst_19 : NoZeroDivisors B
I : FractionalIdeal (R := B) B⁰ L
hI : ¬I = 0
⊢ IsFractional B⁰ (↑I : Submodule B L)ᵛ
have have : ∀ (s : Finset L) (b : Basis (↥s) K L) (hb : ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)),
  IsFractional B⁰ (↑I : Submodule B L)ᵛ
Tactic: have ⟨s, b, hb⟩ := FiniteDimensional.exists_is_basis_integral A K L
-- 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.194059
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
inst_16 : IsDomain A
inst_17 : IsFractionRing B L
inst_18 : Nontrivial B
inst_19 : NoZeroDivisors B
I : FractionalIdeal (R := B) B⁰ L
hI : ¬I = 0
s : Finset L
b : Basis (↥s) K L
hb : ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)
⊢ IsFractional B⁰ (↑I : Submodule B L)ᵛ
have obtain : ∀ (x : B) (hx : x ≠ 0) (hx' : Membership.mem (α := L) I ((algebraMap B L : (a : B) → L) x : L)),
  IsFractional B⁰ (↑I : Submodule B L)ᵛ
Tactic: obtain ⟨x, hx, hx'⟩ := exists_ne_zero_mem_isInteger hI
-- 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.194059
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
inst_16 : IsDomain A
inst_17 : IsFractionRing B L
inst_18 : Nontrivial B
inst_19 : NoZeroDivisors B
I : FractionalIdeal (R := B) B⁰ L
hI : ¬I = 0
s : Finset L
b : Basis (↥s) K L
hb : ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)
x : B
hx : x ≠ 0
hx' : Membership.mem (α := L) I ((algebraMap B L : (a : B) → L) x : L)
⊢ IsFractional B⁰ (↑I : Submodule B L)ᵛ
have have : ∀ (y : B)
  (hy :
    Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L)
      ((algebraMap K L : (a : K) → L) (discr.{u_2, u, u} (ι := ↥s) K (B := L) (⇑b : (a : ↥s) → L)) : L)),
  IsFractional B⁰ (↑I : Submodule B L)ᵛ
Tactic: have ⟨y, hy⟩ := (IsIntegralClosure.isIntegral_iff (A := B)).mp
      (IsIntegral.algebraMap (B := L) (discr_isIntegral K 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.194059
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
inst_16 : IsDomain A
inst_17 : IsFractionRing B L
inst_18 : Nontrivial B
inst_19 : NoZeroDivisors B
I : FractionalIdeal (R := B) B⁰ L
hI : ¬I = 0
s : Finset L
b : Basis (↥s) K L
hb : ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)
x : B
hx : x ≠ 0
hx' : Membership.mem (α := L) I ((algebraMap B L : (a : B) → L) x : L)
y : B
hy :
  Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L)
    ((algebraMap K L : (a : K) → L) (discr.{u_2, u, u} (ι := ↥s) K (B := L) (⇑b : (a : ↥s) → L)) : L)
⊢ IsFractional B⁰ (↑I : Submodule B L)ᵛ
have refine_1 : y ≠ 0
Tactic: refine ⟨y * x, mem_nonZeroDivisors_iff_ne_zero.mpr (mul_ne_zero ?_ hx), fun z hz ↦ ?_⟩
-- 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.194059
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
inst_16 : IsDomain A
inst_17 : IsFractionRing B L
inst_18 : Nontrivial B
inst_19 : NoZeroDivisors B
I : FractionalIdeal (R := B) B⁰ L
hI : ¬I = 0
s : Finset L
b : Basis (↥s) K L
hb : ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)
x : B
hx : x ≠ 0
hx' : Membership.mem (α := L) I ((algebraMap B L : (a : B) → L) x : L)
y : B
hy :
  Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L)
    ((algebraMap K L : (a : K) → L) (discr.{u_2, u, u} (ι := ↥s) K (B := L) (⇑b : (a : ↥s) → L)) : L)
refine_1 : y ≠ 0
⊢ IsFractional B⁰ (↑I : Submodule B L)ᵛ
have refine_2 : ∀ (z : L) (hz : z ∈ (↑I : Submodule B L)ᵛ), IsInteger B ((y * x) • z)
Tactic: refine ⟨y * x, mem_nonZeroDivisors_iff_ne_zero.mpr (mul_ne_zero ?_ hx), fun z hz ↦ ?_⟩