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 :
  ∀ 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
y : B
hy : Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) ((b : (a : ι) → L) j : L)
h : y • a ∈ I
⊢ HMul.hMul (β := L) a ((b : (a : ι) → L) j : L) ∈ I

Tactic:
rw [mul_comm, ← hy, ← Algebra.smul_def]

Premises used: mul_comm, Algebra.smul_def
-- 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 : 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)
⊢ y • a ∈ I

Tactic:
I.smul_mem _ (ha)

Premises used: Set.Mem, Submodule.smul_mem
-- 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 : 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)
⊢ y • a ∈ I

Tactic:
exact I.smul_mem _ (ha)

Premises used: Submodule.smul_mem
-- 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
j k : ι
h_1 : ¬k = i
⊢ IsIntegral A (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L) j k)

Tactic:
isIntegral_trace (RingHom.IsIntegralElem.mul _ (hb j) (hb k))

Premises used: Algebra.isIntegral_trace, RingHom.IsIntegralElem.mul, Algebra.traceMatrix
-- 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
j k : ι
h_1 : ¬k = i
⊢ IsIntegral A (traceMatrix.{u_2, u, u_4} K (B := L) (⇑b : (a : ι) → L) j k)

Tactic:
exact isIntegral_trace (RingHom.IsIntegralElem.mul _ (hb j) (hb k))

Premises used: Algebra.isIntegral_trace, RingHom.IsIntegralElem.mul
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
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)ᵛ
⊢ IsFractional B⁰ (↑I : Submodule B L)ᵛ

Tactic:
have ⟨s, b, hb⟩ := FiniteDimensional.exists_is_basis_integral A K L
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)
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)ᵛ
⊢ IsFractional B⁰ (↑I : Submodule B L)ᵛ

Tactic:
obtain ⟨x, hx, hx'⟩ := exists_ne_zero_mem_isInteger hI

Premises used: FractionalIdeal.exists_ne_zero_mem_isInteger
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)
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)ᵛ
⊢ IsFractional B⁰ (↑I : Submodule B L)ᵛ

Tactic:
have ⟨y, hy⟩ := (IsIntegralClosure.isIntegral_iff (A := B)).mp
      (IsIntegral.algebraMap (B := L) (discr_isIntegral K hb))
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)ᵛ

Tactic:
⟨y * x, mem_nonZeroDivisors_iff_ne_zero.mpr (mul_ne_zero ?_ hx), fun z hz ↦ ?_⟩

Premises used: Iff.mpr, HMul.hMul, IsFractional, And.intro, Exists.intro, mem_nonZeroDivisors_iff_ne_zero, mul_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
refine_2 : ∀ (z : L) (hz : z ∈ (↑I : Submodule B L)ᵛ), IsInteger B ((y * x) • z)
⊢ IsFractional B⁰ (↑I : Submodule B L)ᵛ

Tactic:
refine ⟨y * x, mem_nonZeroDivisors_iff_ne_zero.mpr (mul_ne_zero ?_ hx), fun z hz ↦ ?_⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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 : discr.{u_2, u, u} (ι := ↥s) K (B := L) (⇑b : (a : ↥s) → L) ≠ 0
⊢ y ≠ 0

Tactic:
rw [← (IsIntegralClosure.algebraMap_injective B A L).ne_iff, hy, map_zero,
        ← (algebraMap K L).map_zero, (algebraMap K L).injective.ne_iff]

Premises used: Algebra.algebraMap, IsIntegralClosure.algebraMap_injective, map_zero, Function.Injective.ne_iff, RingHom.injective, RingHom.map_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)
⊢ discr.{u_2, u, u} (ι := ↥s) K (B := L) (⇑b : (a : ↥s) → L) ≠ 0

Tactic:
discr_not_zero_of_basis K b

Premises used: Algebra.discr_not_zero_of_basis
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)
⊢ discr.{u_2, u, u} (ι := ↥s) K (B := L) (⇑b : (a : ↥s) → L) ≠ 0

Tactic:
exact discr_not_zero_of_basis K b

Premises used: Algebra.discr_not_zero_of_basis
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)
z : L
hz : z ∈ (↑I : Submodule B L)ᵛ
⊢ IsIntegral A
    (HSMul.hSMul (β := L) (discr.{u_2, u, u} (ι := ↥s) K (B := L) (⇑b : (a : ↥s) → L))
        ((algebraMap B L : (a : B) → L) x : L) *
      z)

Tactic:
isIntegral_discr_mul_of_mem_traceDual I hb hx' hz

Premises used: isIntegral_discr_mul_of_mem_traceDual
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)
z : L
hz : z ∈ (↑I : Submodule B L)ᵛ
h : Eq.{u + 1} (α := (a : L) → Prop) (IsInteger B) (IsIntegral A)
h₁ :
  (y * x) • z =
    HSMul.hSMul (β := L) (discr.{u_2, u, u} (ι := ↥s) K (B := L) (⇑b : (a : ↥s) → L))
        ((algebraMap B L : (a : B) → L) x : L) *
      z
⊢ IsInteger B ((y * x) • z)

Tactic:
convert! isIntegral_discr_mul_of_mem_traceDual I hb hx' hz using 1

Premises used: isIntegral_discr_mul_of_mem_traceDual
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)
z : L
hz : z ∈ (↑I : Submodule B L)ᵛ
h : ∀ (w : L), IsInteger B w ↔ IsIntegral A w
⊢ Eq.{u + 1} (α := (a : L) → Prop) (IsInteger B) (IsIntegral A)

Tactic:
ext w
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)
z : L
hz : z ∈ (↑I : Submodule B L)ᵛ
w : L
⊢ IsInteger B w ↔ IsIntegral A w

Tactic:
(IsIntegralClosure.isIntegral_iff (A := B)).symm

Premises used: IsLocalization.IsInteger, Set.Mem, setOf, IsIntegralClosure.isIntegral_iff, Set.range, Iff.symm