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 : 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)ᵛ
⊢ (↑(dual A K I) : Submodule B L) = (↑I : Submodule B L)ᵛ
have rw₂ : (↑I : 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
⊢ Eq.{u + 1} (α := Submodule B L) (↑(dual A K 1) : Submodule B L) 1ᵛ
have hI : Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 0
Tactic: rw [← coe_one, coe_dual]
-- 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
⊢ Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 0) 0
have 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)ᵛ sorry)
  0
Tactic: rw [dual, dif_pos rfl]
-- 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
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
⊢ Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (dual A K 0) 0
have rw₁ : Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 0 0
Tactic: rw [dual, dif_pos rfl]
-- 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
x : L
⊢ 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)
have rw : x ∈ Subtype.mk (p := fun (I : Submodule B L) ↦ IsFractional B⁰ I) (↑I : Submodule B L)ᵛ sorry ↔
  ∀ 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]
-- 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 ≠ 0
have 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
Tactic: obtain ⟨b, hb, hb'⟩ := I.prop
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : 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
⊢ False
have this₁ : b = 0
Tactic: rw [e, mem_zero_iff, ← (algebraMap B L).map_zero,
      (IsIntegralClosure.algebraMap_injective B A L).eq_iff] at this
Cleared hypotheses: this, e
-- 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
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
have suffices : Membership.mem (α := L) (dual A K I) ((algebraMap B L : (a : B) → L) b : L)
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
-- 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
b : B
hb : Membership.mem (γ := Submonoid B) (B⁰ : Submonoid B) b
hb' : ∀ b_1 ∈ (↑I : Submodule B L), IsInteger B (b • b_1)
⊢ Membership.mem (α := L) (dual A K I) ((algebraMap B L : (a : B) → L) b : L)
have 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)
Tactic: rw [mem_dual 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_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
⊢ 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)
have 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)
Tactic: apply IsIntegrallyClosed.isIntegral_iff.mp
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : 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
⊢ 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)
have 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)
Tactic: apply isIntegral_trace
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : 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
⊢ 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)
have hx : IsIntegral A (HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) b : L) a)
Tactic: dsimp
-- 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
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
⊢ IsIntegral A (HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) b : L) a)
have h : Eq.{u + 1} (α := (x : L) → Prop) (IsIntegral A) (IsInteger B)
Tactic: convert! hb' a ha 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_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)
⊢ IsIntegral A (HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) b : L) a)
have h₁ : HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) b : L) a = b • a
Tactic: convert! hb' a ha 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_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
⊢ Eq.{u + 1} (α := (x : L) → Prop) (IsIntegral A) (IsInteger B)
have h : ∀ (w : L), IsIntegral A w ↔ IsInteger B 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_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 J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
⊢ J ≤ dual A K I
have rw : J ≤ Subtype.mk (p := fun (I : Submodule B L) ↦ IsFractional B⁰ I) (↑I : Submodule B L)ᵛ sorry
Tactic: rw [dual, dif_neg 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_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 J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : Membership.mem (γ := Submodule A L) (Submodule.restrictScalars A (↑I : Submodule B L)) y
⊢ Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1
    ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
have rw : ∃ (y_1 : A),
  Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y_1 : K)
    ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
Tactic: rw [mem_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : 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 J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : Membership.mem (γ := Submodule A L) (Submodule.restrictScalars A (↑I : Submodule B L)) y
⊢ ∃ (y_1 : A),
    Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) y_1 : K)
      ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
have apply : IsIntegral.{u_1, u_2} A (A := K) ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
Tactic: apply IsIntegrallyClosed.isIntegral_iff.mp
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : 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 J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : Membership.mem (γ := Submodule A L) (Submodule.restrictScalars A (↑I : Submodule B L)) y
⊢ IsIntegral.{u_1, u_2} A (A := K) ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
have hx₁ : IsIntegral A (A := L) ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) x : L →ₗ[K] L) : (a : L) → L) y : L)
Tactic: apply isIntegral_trace
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : 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 J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : Membership.mem (γ := Submodule A L) (Submodule.restrictScalars A (↑I : Submodule B L)) y
⊢ IsIntegral A (A := L) ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) x : L →ₗ[K] L) : (a : L) → L) y : L)
have hx₁ : ∃ (y_1 : B),
  Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y_1 : L)
    ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) x : L →ₗ[K] L) : (a : L) → L) y : L)
Tactic: rw [IsIntegralClosure.isIntegral_iff (A := B)]
-- 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 J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : Membership.mem (γ := Submodule A L) (Submodule.restrictScalars A (↑I : Submodule B L)) y
⊢ ∃ (y_1 : B),
    Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y_1 : L)
      ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) x : L →ₗ[K] L) : (a : L) → L) y : L)
have hx₁ : ∀ z ∈ (↑⊤ : Set B),
  ∀ (hz : (Algebra.linearMap B L : (a : B) → L) z = y * x),
    ∃ (y_1 : B),
      Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y_1 : L)
        ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) x : L →ₗ[K] L) : (a : L) → L) y : L)
Tactic: have ⟨z, _, hz⟩ := hIJ (FractionalIdeal.mul_mem_mul hy hx)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : 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 J : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : I ≠ 0
hIJ : I * J ≤ 1
x : L
hx : x ∈ J
y : L
hy : Membership.mem (γ := Submodule A L) (Submodule.restrictScalars A (↑I : Submodule B L)) y
z : B
left : z ∈ (↑⊤ : Set B)
hz : (Algebra.linearMap B L : (a : B) → L) z = y * x
⊢ ∃ (y_1 : B),
    Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y_1 : L)
      ((((AlgHom.toLinearMap (lmul K L) : (a : L) → L →ₗ[K] L) x : L →ₗ[K] L) : (a : L) → L) y : L)
have hz₁ : (Algebra.linearMap B L : (a : B) → L) z = x * y
Tactic: rw [mul_comm] at hz
Cleared hypotheses: 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_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
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 1 ≤ 1
have rw : LE.le.{u} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 1
Tactic: rw [one_mul]