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.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 :
  HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) (y * x) : L) 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
h₁ :
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) y : L) ((algebraMap B L : (a : B) → L) x : L) * 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
h₂ :
  HMul.hMul (α := L) (β := L)
        ((algebraMap K L : (a : K) → L) (discr.{u_2, u, u} (ι := ↥s) K (B := L) (⇑b : (a : ↥s) → L)) : L)
        ((algebraMap B L : (a : B) → L) x : L) *
      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
h₃ h₄ :
  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 =
    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
⊢ (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

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

Premises used: map_mul, 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
rw :
  (↑(if hI : I = 0 then 0 else Subtype.mk (p := fun (I : Submodule B L) ↦ IsFractional B⁰ I) (↑I : Submodule B L)ᵛ ⋯) :
      Submodule B L) =
    (↑I : Submodule B L)ᵛ
rw₁ :
  (↑(Subtype.mk (p := fun (I : Submodule B L) ↦ IsFractional B⁰ I) (↑I : Submodule B L)ᵛ ⋯) : Submodule B L) =
    (↑I : Submodule B L)ᵛ
rw₂ rw₃ : (↑I : Submodule B L)ᵛ = (↑I : Submodule B L)ᵛ
⊢ (↑(dual A K I) : Submodule B L) = (↑I : Submodule B L)ᵛ

Tactic:
rw [dual, dif_neg hI, coe_mk]

Premises used: FractionalIdeal.dual, FractionalIdeal.coe_mk, dif_neg
-- 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
hI : Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 0
⊢ Eq.{u + 1} (α := Submodule B L) (↑(dual A K 1) : Submodule B L) 1ᵛ

Tactic:
rw [← coe_one, coe_dual]

Premises used: FractionalIdeal.coe_dual, FractionalIdeal.coe_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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
rw :
  Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L)
    (if hI : Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 0 0 then 0
    else Subtype.mk (p := fun (I : Submodule B L) ↦ IsFractional B⁰ I) (↑0 : Submodule B L)ᵛ ⋯)
    0
rw₁ rw₂ : Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 0 0
⊢ Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 0) 0

Tactic:
rw [dual, dif_pos rfl]

Premises used: FractionalIdeal.dual, dif_pos, 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
x : L
rw :
  x ∈ Subtype.mk (p := fun (I : Submodule B L) ↦ IsFractional B⁰ I) (↑I : Submodule B L)ᵛ ⋯ ↔
    ∀ a ∈ I,
      Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K))
        ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) a : K)
⊢ x ∈ dual A K I ↔
    ∀ a ∈ I,
      Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K))
        ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) a : K)

Tactic:
rw [dual, dif_neg hI]

Premises used: FractionalIdeal.dual, dif_neg
-- 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
x : L
⊢ x ∈ Subtype.mk (p := fun (I : Submodule B L) ↦ IsFractional B⁰ I) (↑I : Submodule B L)ᵛ ⋯ ↔
    ∀ a ∈ I,
      Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K))
        ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) a : K)

Tactic:
forall₂_congr fun _ _ ↦ mem_one

Premises used: Set.Mem, setOf, forall₂_congr, 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
x : L
⊢ x ∈ Subtype.mk (p := fun (I : Submodule B L) ↦ IsFractional B⁰ I) (↑I : Submodule B L)ᵛ ⋯ ↔
    ∀ a ∈ I,
      Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K))
        ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) a : K)

Tactic:
exact forall₂_congr fun _ _ ↦ mem_one

Premises used: forall₂_congr, 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
obtain :
  ∀ (b : B) (hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b)
    (hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)), dual A K I ≠ 0
⊢ dual A K I ≠ 0

Tactic:
obtain ⟨b, hb, hb'⟩ := I.prop

Premises used: Subtype.prop
-- 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
this : Membership.mem (α := L) (dual A K I) ((algebraMap B L : (a : B) → L) b : L)
e : dual A K I = 0
⊢ b = 0

Tactic:
rw [e, mem_zero_iff, ← (algebraMap B L).map_zero,
      (IsIntegralClosure.algebraMap_injective B A L).eq_iff] at this

Premises used: Algebra.algebraMap, Function.Injective.eq_iff, IsIntegralClosure.algebraMap_injective, FractionalIdeal.mem_zero_iff, RingHom.map_zero
-- 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
this : Membership.mem (α := L) (dual A K I) ((algebraMap B L : (a : B) → L) b : L)
e : dual A K I = 0
this₁ : b = 0
⊢ dual A K I = 0

Tactic:
rw [e, mem_zero_iff, ← (algebraMap B L).map_zero,
      (IsIntegralClosure.algebraMap_injective B A L).eq_iff] at this

Premises used: Algebra.algebraMap, Function.Injective.eq_iff, IsIntegralClosure.algebraMap_injective, FractionalIdeal.mem_zero_iff, RingHom.map_zero
-- 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
this : b = 0
e : dual A K I = 0
⊢ False

Tactic:
mem_nonZeroDivisors_iff_ne_zero.mp hb this

Premises used: Iff.mp, mem_nonZeroDivisors_iff_ne_zero
-- 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
this : b = 0
e : dual A K I = 0
⊢ False

Tactic:
exact mem_nonZeroDivisors_iff_ne_zero.mp hb this

Premises used: Iff.mp, mem_nonZeroDivisors_iff_ne_zero
-- 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
suffices : Membership.mem (α := L) (dual A K I) ((algebraMap B L : (a : B) → L) b : L)
⊢ dual A K I ≠ 0

Tactic:
suffices algebraMap B L b ∈ dual A K I by
    intro e
    rw [e, mem_zero_iff, ← (algebraMap B L).map_zero,
      (IsIntegralClosure.algebraMap_injective B A L).eq_iff] at this
    exact mem_nonZeroDivisors_iff_ne_zero.mp hb this
-- 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
rw :
  ∀ a ∈ I,
    Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K))
      ((((traceForm K L : (a : L) → L →ₗ[K] K) ((algebraMap B L : (a : B) → L) b) : L →ₗ[K] K) : (a : L) → K) a : K)
⊢ Membership.mem (α := L) (dual A K I) ((algebraMap B L : (a : B) → L) b : L)

Tactic:
rw [mem_dual hI]

Premises used: FractionalIdeal.mem_dual
-- 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
a : L
ha : a ∈ I
apply :
  IsIntegral.{u_1, u_2} A (A := K)
    ((((traceForm K L : (a : L) → L →ₗ[K] K) ((algebraMap B L : (a : B) → L) b) : L →ₗ[K] K) : (a : L) → K) a : K)
⊢ Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K))
    ((((traceForm K L : (a : L) → L →ₗ[K] K) ((algebraMap B L : (a : B) → L) b) : L →ₗ[K] K) : (a : L) → K) a : 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
a : L
ha : a ∈ I
hx :
  IsIntegral A (A := L)
    ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) ((algebraMap B L : (a : B) → L) b : L) : L →ₗ[K] L) :
          (a : L) → L)
        a :
      L)
⊢ IsIntegral.{u_1, u_2} A (A := K)
    ((((traceForm K L : (a : L) → L →ₗ[K] K) ((algebraMap B L : (a : B) → L) b) : L →ₗ[K] K) : (a : L) → K) a : 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
a : L
ha : a ∈ I
hx : IsIntegral A (HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) b : L) a)
⊢ IsIntegral A (A := L)
    ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) ((algebraMap B L : (a : B) → L) b : L) : L →ₗ[K] L) :
          (a : L) → L)
        a :
      L)

Tactic:
dsimp
-- 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
a : L
ha : a ∈ I
⊢ IsInteger B (b • a)

Tactic:
hb' a ha
-- 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
a : L
ha : a ∈ I
h : Eq.{u + 1} (α := (x : L) → Prop) (IsIntegral A) (IsInteger B)
h₁ : HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) b : L) a = b • a
⊢ IsIntegral A (HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) b : L) a)

Tactic:
convert! hb' a ha using 1
-- 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 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsIntegrallyClosed A
inst_18 : IsDedekindDomain B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
a : L
ha : a ∈ I
h : ∀ (w : L), IsIntegral A w ↔ IsInteger B w
⊢ Eq.{u + 1} (α := (x : L) → Prop) (IsIntegral A) (IsInteger B)

Tactic:
ext w