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.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)
⊢ y ≠ 0
have refine_1 : discr.{u_2, u, u} (ι := ↥s) K (B := L) (⇑b : (a : ↥s) → L) ≠ 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]
-- 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)
z : L
hz : z ∈ (↑I : Submodule B L)ᵛ
⊢ IsInteger B ((y * x) • z)
have h : Eq.{u + 1} (α := (a : L) → Prop) (IsInteger B) (IsIntegral A)
Tactic: convert! isIntegral_discr_mul_of_mem_traceDual I hb hx' hz using 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.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)
⊢ IsInteger B ((y * x) • z)
have 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
Tactic: convert! isIntegral_discr_mul_of_mem_traceDual I hb hx' hz using 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.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)ᵛ
⊢ Eq.{u + 1} (α := (a : L) → Prop) (IsInteger B) (IsIntegral A)
have h : ∀ (w : L), IsInteger B w ↔ IsIntegral A w
Tactic: ext w
-- 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)
z : L
hz : z ∈ (↑I : Submodule B L)ᵛ
⊢ (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
have 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
Tactic: rw [Algebra.smul_def, map_mul, 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
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
⊢ (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
have 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
Tactic: rw [Algebra.smul_def, map_mul, 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
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
⊢ (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
have 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
Tactic: rw [Algebra.smul_def, map_mul, 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
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
⊢ (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
have 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
Tactic: rw [Algebra.smul_def, map_mul, 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_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
inst_16 : IsDomain A
inst_17 : IsFractionRing B L
inst_18 : Nontrivial B
inst_19 : NoZeroDivisors B
I : FractionalIdeal.{u_3, u} (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: classical
    have ⟨s, b, hb⟩ := FiniteDimensional.exists_is_basis_integral A K L
    obtain ⟨x, hx, hx'⟩ := exists_ne_zero_mem_isInteger hI
    have ⟨y, hy⟩ := (IsIntegralClosure.isIntegral_iff (A := B)).mp
      (IsIntegral.algebraMap (B := L) (discr_isIntegral K hb))
    refine ⟨y * x, mem_nonZeroDivisors_iff_ne_zero.mpr (mul_ne_zero ?_ hx), fun z hz ↦ ?_⟩
    · rw [← (IsIntegralClosure.algebraMap_injective B A L).ne_iff, hy, map_zero,
        ← (algebraMap K L).map_zero, (algebraMap K L).injective.ne_iff]
      exact discr_not_zero_of_basis K b
    · convert! isIntegral_discr_mul_of_mem_traceDual I hb hx' hz using 1
      · ext w; exact (IsIntegralClosure.isIntegral_iff (A := B)).symm
      · rw [Algebra.smul_def, map_mul, 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_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
inst_16 : IsDomain A
inst_17 : IsFractionRing B L
inst_18 : Nontrivial B
inst_19 : NoZeroDivisors B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : ¬I = 0
have 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)ᵛ
⊢ 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)) (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: classical
    have ⟨s, b, hb⟩ := FiniteDimensional.exists_is_basis_integral A K L
    obtain ⟨x, hx, hx'⟩ := exists_ne_zero_mem_isInteger hI
    have ⟨y, hy⟩ := (IsIntegralClosure.isIntegral_iff (A := B)).mp
      (IsIntegral.algebraMap (B := L) (discr_isIntegral K hb))
    refine ⟨y * x, mem_nonZeroDivisors_iff_ne_zero.mpr (mul_ne_zero ?_ hx), fun z hz ↦ ?_⟩
    · rw [← (IsIntegralClosure.algebraMap_injective B A L).ne_iff, hy, map_zero,
        ← (algebraMap K L).map_zero, (algebraMap K L).injective.ne_iff]
      exact discr_not_zero_of_basis K b
    · convert! isIntegral_discr_mul_of_mem_traceDual I hb hx' hz using 1
      · ext w; exact (IsIntegralClosure.isIntegral_iff (A := B)).symm
      · rw [Algebra.smul_def, map_mul, 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_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
inst_16 : IsDomain A
inst_17 : IsFractionRing B L
inst_18 : Nontrivial B
inst_19 : NoZeroDivisors B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : ¬I = 0
have 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)ᵛ
have₃ :
  ∀ (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)ᵛ
⊢ 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)) (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: classical
    have ⟨s, b, hb⟩ := FiniteDimensional.exists_is_basis_integral A K L
    obtain ⟨x, hx, hx'⟩ := exists_ne_zero_mem_isInteger hI
    have ⟨y, hy⟩ := (IsIntegralClosure.isIntegral_iff (A := B)).mp
      (IsIntegral.algebraMap (B := L) (discr_isIntegral K hb))
    refine ⟨y * x, mem_nonZeroDivisors_iff_ne_zero.mpr (mul_ne_zero ?_ hx), fun z hz ↦ ?_⟩
    · rw [← (IsIntegralClosure.algebraMap_injective B A L).ne_iff, hy, map_zero,
        ← (algebraMap K L).map_zero, (algebraMap K L).injective.ne_iff]
      exact discr_not_zero_of_basis K b
    · convert! isIntegral_discr_mul_of_mem_traceDual I hb hx' hz using 1
      · ext w; exact (IsIntegralClosure.isIntegral_iff (A := B)).symm
      · rw [Algebra.smul_def, map_mul, 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_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
inst_16 : IsDomain A
inst_17 : IsFractionRing B L
inst_18 : Nontrivial B
inst_19 : NoZeroDivisors B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : ¬I = 0
have 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)ᵛ
have₃ :
  ∀ (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₄ :
  ∀ (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)ᵛ
⊢ IsFractional B⁰ (↑I : Submodule B L)ᵛ
have refine_1 : ∀ (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)),
  y ≠ 0
Tactic: classical
    have ⟨s, b, hb⟩ := FiniteDimensional.exists_is_basis_integral A K L
    obtain ⟨x, hx, hx'⟩ := exists_ne_zero_mem_isInteger hI
    have ⟨y, hy⟩ := (IsIntegralClosure.isIntegral_iff (A := B)).mp
      (IsIntegral.algebraMap (B := L) (discr_isIntegral K hb))
    refine ⟨y * x, mem_nonZeroDivisors_iff_ne_zero.mpr (mul_ne_zero ?_ hx), fun z hz ↦ ?_⟩
    · rw [← (IsIntegralClosure.algebraMap_injective B A L).ne_iff, hy, map_zero,
        ← (algebraMap K L).map_zero, (algebraMap K L).injective.ne_iff]
      exact discr_not_zero_of_basis K b
    · convert! isIntegral_discr_mul_of_mem_traceDual I hb hx' hz using 1
      · ext w; exact (IsIntegralClosure.isIntegral_iff (A := B)).symm
      · rw [Algebra.smul_def, map_mul, 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_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
⊢ (↑(dual A K I) : Submodule B L) = (↑I : Submodule B L)ᵛ
have rw : (↑(if hI : I = 0 then 0 else Subtype.mk (p := fun (I : Submodule B L) ↦ IsFractional B⁰ I) (↑I : Submodule B L)ᵛ sorry) :
    Submodule B L) =
  (↑I : Submodule B L)ᵛ
Tactic: rw [dual, dif_neg hI, coe_mk]
-- 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 : 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)ᵛ
⊢ (↑(dual A K I) : Submodule B L) = (↑I : Submodule B L)ᵛ
have rw₁ : (↑(Subtype.mk (p := fun (I : Submodule B L) ↦ IsFractional B⁰ I) (↑I : Submodule B L)ᵛ sorry) : Submodule B L) =
  (↑I : Submodule B L)ᵛ
Tactic: rw [dual, dif_neg hI, coe_mk]