awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
hb : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ e * b
ha : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = (P ^ (e - 1) * a) ^ e
⊢ Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
have hb₁ : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = (P ^ e * b) ^ (e - 1)
Tactic: apply_fun (· ^ (e - 1) : Ideal B → _) at hb
Cleared hypotheses: hb
-- 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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = (P ^ (e - 1) * a) ^ e
hb : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = (P ^ e * b) ^ (e - 1)
⊢ Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
have ha₁ : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = P ^ ((e - 1) * e) * a ^ e
Tactic: simp only [mul_pow, ← pow_mul, mul_comm e] at ha hb
Cleared hypotheses: ha, hb
-- 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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = (P ^ (e - 1) * a) ^ e
hb : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = (P ^ e * b) ^ (e - 1)
ha₁ : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = P ^ ((e - 1) * e) * a ^ e
⊢ Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
have hb₁ : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
Tactic: simp only [mul_pow, ← pow_mul, mul_comm e] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = P ^ ((e - 1) * e) * a ^ e
hb : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
| HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e
have rw : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1 + 1)
Tactic: rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he)]
-- 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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = P ^ ((e - 1) * e) * a ^ e
hb : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
⊢ Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
have ha₁ : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1 + 1) = P ^ ((e - 1) * e) * a ^ e
Tactic: conv_lhs at ha => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he)]
Cleared hypotheses: ha, hb
-- 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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1 + 1) = P ^ ((e - 1) * e) * a ^ e
hb : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
⊢ Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
have ha₁ : Ideal.map (F := A →+* B) (algebraMap A B) p * b ^ (e - 1) = a ^ e
Tactic: rw [pow_add, hb, mul_assoc, mul_right_inj' (pow_ne_zero _ hPbot), pow_one, mul_comm] at ha
Cleared hypotheses: ha, hb
-- 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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B
have this : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
Tactic: have : p.map (algebraMap A B) ∣ a ^ e := by
    obtain ⟨b, hb⟩ := hP
    apply_fun (· ^ e : Ideal B → _) at ha
    apply_fun (· ^ (e - 1) : Ideal B → _) at hb
    simp only [mul_pow, ← pow_mul, mul_comm e] at ha hb
    conv_lhs at ha => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he)]
    rw [pow_add, hb, mul_assoc, mul_right_inj' (pow_ne_zero _ hPbot), pow_one, mul_comm] at ha
    exact ⟨_, ha.symm⟩
-- 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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this_1 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)
⊢ (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L)⁻¹ =
    HDiv.hDiv (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L)
      (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)
have a₁ : (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L)⁻¹⁻¹ =
  (HDiv.hDiv (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L)
      (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L))⁻¹
Tactic: apply inv_involutive.injective
-- 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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this_1 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)
⊢ (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L)⁻¹⁻¹ =
    (HDiv.hDiv (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L)
        (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L))⁻¹
have a₁ : (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L) =
  (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L) *
    HDiv.hDiv (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L) (↑a : FractionalIdeal B⁰ L)
Tactic: simp only [inv_inv, ha, FractionalIdeal.coeIdeal_mul, inv_div,
          mul_div_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : 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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this_1 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)
⊢ (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L) =
    (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L) *
      HDiv.hDiv (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L) (↑a : FractionalIdeal B⁰ L)
have a₁ : (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L) =
  HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L) 1
Tactic: rw [div_self (by simpa), mul_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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this_1 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)
a₁ :
  (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L) =
    HMul.hMul (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L) 1
⊢ (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L) =
    (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L) *
      HDiv.hDiv (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L) (↑a : FractionalIdeal B⁰ L)
have a₂ : Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L)
  (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L)
Tactic: rw [div_self (by simpa), mul_one]
-- 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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this_1 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)
⊢ P ^ (e - 1) ∣ differentIdeal A B
have hP₁ : (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L)⁻¹ =
  HDiv.hDiv (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L)
    (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)
Tactic: have hP : ((P ^ (e - 1) :)⁻¹ : FractionalIdeal B⁰ L) = a / p.map (algebraMap A B) := by
      apply inv_involutive.injective
      simp only [inv_inv, ha, FractionalIdeal.coeIdeal_mul, inv_div,
          mul_div_assoc]
      rw [div_self (by simpa), mul_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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP_1 : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this_1 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)
hP :
  (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L)⁻¹ =
    HDiv.hDiv (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L)
      (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)
⊢ P ^ (e - 1) ∣ differentIdeal A B
have rw : LE.le (α := Submodule A L)
  (Submodule.restrictScalars A
    (↑(HDiv.hDiv (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L)
          (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)) :
      Submodule B L))
  (comap
    ((↑A :
        {S : Type u_2} →
          {M : Type u} →
            {M₂ : Type u_2} →
              [inst : Semiring A] →
                [inst_22 : Semiring S] →
                  [inst_23 : AddCommMonoid M] →
                    [inst_24 : AddCommMonoid M₂] →
                      [inst_25 : Module A M] →
                        [inst_26 : Module A M₂] →
                          [inst_27 : Module S M] →
                            [inst_28 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
      (Algebra.trace K L))
    1)
Tactic: rw [Ideal.dvd_iff_le, differentialIdeal_le_iff (K := K) (L := L) (pow_ne_zero _ hPbot), hP,
      Submodule.map_le_iff_le_comap]
-- 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 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP_1 : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this_1 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)
hP :
  (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L)⁻¹ =
    HDiv.hDiv (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L)
      (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)
x : L
hx :
  Membership.mem (γ := Submodule A L)
    (Submodule.restrictScalars A
      (↑(HDiv.hDiv (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L)
            (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)) :
        Submodule B L))
    x
⊢ Membership.mem (γ := Submodule A L)
    (comap
      ((↑A :
          {S : Type u_2} →
            {M : Type u} →
              {M₂ : Type u_2} →
                [inst : Semiring A] →
                  [inst_22 : Semiring S] →
                    [inst_23 : AddCommMonoid M] →
                      [inst_24 : AddCommMonoid M₂] →
                        [inst_25 : Module A M] →
                          [inst_26 : Module A M₂] →
                            [inst_27 : Module S M] →
                              [inst_28 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
        (Algebra.trace K L))
      1)
    x
have hx₁ : ∀ (y : L),
  Membership.mem (γ := FractionalIdeal.{u_3, u} (R := B) B⁰ L)
      (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L) y →
    Membership.mem (γ := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L) (x * y)
Tactic: rw [Submodule.restrictScalars_mem, FractionalIdeal.mem_coe,
      FractionalIdeal.mem_div_iff_of_ne_zero (by simpa using hp')] at hx
Cleared hypotheses: hx