awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : 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 :
  ∀ (a_1 : B),
    Membership.mem (γ := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) a_1 →
      ∃ x' ∈ a, (algebraMap B L : (a : B) → L) x' = HMul.hMul (β := L) x ((algebraMap B L : (a : B) → L) a_1 : L)
y : A
hy : y ∈ p
hy' :
  Membership.mem.{u_2, u_2} (α := K) (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
obtain :
  ∀ (z : B) (hz : z ∈ a)
    (hz' :
      (algebraMap B L : (a : B) → L) z =
        HMul.hMul (β := L) x ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) y : B) : L)),
    Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
      (HMul.hMul (α := K) (β := K) ((Algebra.trace K L : (a : L) → K) x : K) ((algebraMap A K : (a : A) → K) y : K))
⊢ Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (HMul.hMul (α := K) (β := K) ((Algebra.trace K L : (a : L) → K) x : K) ((algebraMap A K : (a : A) → K) y : K))

Tactic:
obtain ⟨z, hz, hz'⟩ := hx _ (Ideal.mem_map_of_mem _ hy)

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : 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 :
  ∀ (a_1 : B),
    Membership.mem (γ := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) a_1 →
      ∃ x' ∈ a, (algebraMap B L : (a : B) → L) x' = HMul.hMul (β := L) x ((algebraMap B L : (a : B) → L) a_1 : L)
y : A
hy : y ∈ p
hy' :
  Membership.mem.{u_2, u_2} (α := K) (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
z : B
hz : z ∈ a
hz' :
  (algebraMap B L : (a : B) → L) z =
    HMul.hMul (β := L) x ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) y : B) : L)
rw :
  Membership.mem.{u_2, u_2} (α := K) (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) ((intTrace A B : (a : B) → A) z : A) : K)
⊢ Membership.mem.{u_2, u_2} (α := K) (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    ((Algebra.trace K L : (a : L) → K) ((algebraMap B L : (a : B) → L) z : L) : K)

Tactic:
rw [← algebraMap_intTrace (A := A)]

Premises used: Algebra.algebraMap_intTrace
-- 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 : 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 :
  ∀ (a_1 : B),
    Membership.mem (γ := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) a_1 →
      ∃ x' ∈ a, (algebraMap B L : (a : B) → L) x' = HMul.hMul (β := L) x ((algebraMap B L : (a : B) → L) a_1 : L)
y : A
hy : y ∈ p
hy' :
  Membership.mem.{u_2, u_2} (α := K) (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
z : B
hz : z ∈ a
hz' :
  (algebraMap B L : (a : B) → L) z =
    HMul.hMul (β := L) x ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) y : B) : L)
⊢ Membership.mem.{u_2, u_2} (α := K) (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) ((intTrace A B : (a : B) → A) z : A) : K)

Tactic:
⟨intTrace A B z, this z hz, rfl⟩

Premises used: Set.Mem, setOf, Algebra.intTrace, And.intro, Exists.intro, Set.image, DFunLike.coe, 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 : 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 :
  ∀ (a_1 : B),
    Membership.mem (γ := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) a_1 →
      ∃ x' ∈ a, (algebraMap B L : (a : B) → L) x' = HMul.hMul (β := L) x ((algebraMap B L : (a : B) → L) a_1 : L)
y : A
hy : y ∈ p
hy' :
  Membership.mem.{u_2, u_2} (α := K) (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
z : B
hz : z ∈ a
hz' :
  (algebraMap B L : (a : B) → L) z =
    HMul.hMul (β := L) x ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) y : B) : L)
⊢ Membership.mem.{u_2, u_2} (α := K) (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) ((intTrace A B : (a : B) → A) z : A) : K)

Tactic:
exact ⟨intTrace A B z, this z hz, 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 : 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 :
  ∀ (a_1 : B),
    Membership.mem (γ := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) a_1 →
      ∃ x' ∈ a, (algebraMap B L : (a : B) → L) x' = HMul.hMul (β := L) x ((algebraMap B L : (a : B) → L) a_1 : L)
y : A
hy : y ∈ p
hy' :
  Membership.mem.{u_2, u_2} (α := K) (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    ((algebraMap A K : (a : A) → K) y : K)
z : B
hz : z ∈ a
hz' :
  (algebraMap B L : (a : B) → L) z =
    HMul.hMul (β := L) x ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) y : B) : L)
⊢ Membership.mem.{u_2, u_2} (α := K) (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    ((Algebra.trace K L : (a : L) → K) ((algebraMap B L : (a : B) → L) z : L) : K)

Tactic:
have : trace K L (algebraMap B L z) ∈ (p : FractionalIdeal A⁰ K) := by
      rw [← algebraMap_intTrace (A := A)]
      exact ⟨intTrace A B z, this z hz, 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 : 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 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
suffices : ∀ x ∈ a, Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
suffices ∀ x ∈ a, intTrace A B x ∈ p by
    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]
    rw [Ideal.dvd_iff_le, differentialIdeal_le_iff (K := K) (L := L) (pow_ne_zero _ hPbot), hP,
      Submodule.map_le_iff_le_comap]
    intro x hx
    rw [Submodule.restrictScalars_mem, FractionalIdeal.mem_coe,
      FractionalIdeal.mem_div_iff_of_ne_zero (by simpa using hp')] at hx
    rw [Submodule.mem_comap, LinearMap.coe_restrictScalars, ← FractionalIdeal.coe_one,
      ← div_self (G₀ := FractionalIdeal A⁰ K) (a := p) (by simpa using hp),
      FractionalIdeal.mem_coe, FractionalIdeal.mem_div_iff_of_ne_zero (by simpa using hp)]
    simp only [FractionalIdeal.mem_coeIdeal, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂] at hx
    intro y hy'
    obtain ⟨y, hy, rfl : algebraMap A K _ = _⟩ := (FractionalIdeal.mem_coeIdeal _).mp hy'
    obtain ⟨z, hz, hz'⟩ := hx _ (Ideal.mem_map_of_mem _ hy)
    have : trace K L (algebraMap B L z) ∈ (p : FractionalIdeal A⁰ K) := by
      rw [← algebraMap_intTrace (A := A)]
      exact ⟨intTrace A B z, this z hz, rfl⟩
    rwa [mul_comm, ← smul_eq_mul, ← map_smul, Algebra.smul_def, mul_comm,
      ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B L, ← hz']
-- 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 : 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 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
rw :
  IsNilpotent.{u_1} (R := A ⧸ p)
    ((Algebra.trace (A ⧸ p) (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) :
          (a : B ⧸ Ideal.map (algebraMap A B) p) → A ⧸ p)
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p) : (a : B) → B ⧸ Ideal.map (algebraMap A B) p)
          x) :
      A ⧸ p)
⊢ Membership.mem (α := A) p ((intTrace A B : (a : B) → A) x : A)

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, ← trace_quotient_eq_of_isDedekindDomain,
    ← isNilpotent_iff_eq_zero]

Premises used: isNilpotent_iff_eq_zero, Ideal.Quotient.eq_zero_iff_mem, Algebra.trace_quotient_eq_of_isDedekindDomain
-- 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 : 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 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
⊢ IsNilpotent.{u_1} (R := A ⧸ p)
    ((Algebra.trace (A ⧸ p) (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) :
          (a : B ⧸ Ideal.map (algebraMap A B) p) → A ⧸ p)
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p) : (a : B) → B ⧸ Ideal.map (algebraMap A B) p)
          x) :
      A ⧸ p)

Tactic:
isNilpotent_trace_of_isNilpotent ⟨e, ?_⟩

Premises used: Algebra.isNilpotent_trace_of_isNilpotent, Exists.intro
-- 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 : 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 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
refine :
  HPow.hPow (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
      ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p) : (a : B) → B ⧸ Ideal.map (algebraMap A B) p)
          x :
        HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
      e =
    0
⊢ IsNilpotent.{u_1} (R := A ⧸ p)
    ((Algebra.trace (A ⧸ p) (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) :
          (a : B ⧸ Ideal.map (algebraMap A B) p) → A ⧸ p)
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p) : (a : B) → B ⧸ Ideal.map (algebraMap A B) p)
          x) :
      A ⧸ p)

Tactic:
refine isNilpotent_trace_of_isNilpotent ⟨e, ?_⟩
-- 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 : 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 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
rw : Membership.mem (γ := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (x ^ e)
⊢ HPow.hPow (α := HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
      ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p) : (a : B) → B ⧸ Ideal.map (algebraMap A B) p)
          x :
        HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
      e =
    0

Tactic:
rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem]

Premises used: map_pow, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : 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 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
⊢ Membership.mem (γ := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (x ^ e)

Tactic:
(Ideal.dvd_iff_le.mp this) <| Ideal.pow_mem_pow hx _

Premises used: Ideal.dvd_iff_le, Set.Mem, setOf, Iff.mp, Ideal.pow_mem_pow
-- 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 : 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 : Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
x : B
hx : x ∈ a
⊢ Membership.mem (γ := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (x ^ e)

Tactic:
exact (Ideal.dvd_iff_le.mp this) <| Ideal.pow_mem_pow hx _

Premises used: Ideal.dvd_iff_le, Iff.mp, Ideal.pow_mem_pow
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
p : Ideal A
inst_9 : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) (FractionRing B)

Tactic:
have : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
    IsIntegralClosure.isLocalization _ (FractionRing A) _ _