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 : 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)⁻¹⁻¹ =
    (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)) : 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

Premises used: Function.Involutive.injective, inv_involutive
-- 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_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) =
    (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L) *
      HDiv.hDiv (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L) (↑a : FractionalIdeal B⁰ L)
⊢ (↑(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:
simp only [inv_inv, ha, FractionalIdeal.coeIdeal_mul, inv_div,
          mul_div_assoc]

Premises used: mul_div_assoc, FractionalIdeal.coeIdeal_mul, inv_inv, inv_div
-- 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_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)
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑a : FractionalIdeal B⁰ L) 0

Tactic:
simpa
-- 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_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
a₂ a₃ :
  Eq.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L)
    (↑(P ^ (e - 1)) : FractionalIdeal B⁰ L)
⊢ (↑(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:
rw [div_self (by simpa), mul_one]

Premises used: mul_one, div_self
-- 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_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)

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]
-- 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)
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)
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
rw [Ideal.dvd_iff_le, differentialIdeal_le_iff (K := K) (L := L) (pow_ne_zero _ hPbot), hP,
      Submodule.map_le_iff_le_comap]

Premises used: Ideal.dvd_iff_le, pow_ne_zero, differentialIdeal_le_iff, Submodule.map_le_iff_le_comap
-- 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 :
  x ∈
    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)
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L)
    (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L) 0

Tactic:
simpa using hp'
-- 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 :
  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
⊢ ∀ (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

Premises used: Submodule.restrictScalars_mem, FractionalIdeal.mem_coe, FractionalIdeal.mem_div_iff_of_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : 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 :
  ∀ (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)
⊢ Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K) 0

Tactic:
simpa using hp
-- 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 :
  ∀ (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)
rw :
  ∀ (y : K),
    Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K) y →
      Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
        (HMul.hMul (α := K) ((Algebra.trace K L : (a : L) → K) x : K) y)
⊢ 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

Tactic:
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)]

Premises used: Submodule.mem_comap, LinearMap.coe_restrictScalars, FractionalIdeal.coe_one, FractionalIdeal.mem_coe, div_self, FractionalIdeal.mem_div_iff_of_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : 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 :
  ∀ (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)
⊢ ∀ (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)

Tactic:
simp only [FractionalIdeal.mem_coeIdeal, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂] at hx

Premises used: and_imp, forall_exists_index, FractionalIdeal.mem_coeIdeal, forall_apply_eq_imp_iff₂
-- 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 : K
hy' : Membership.mem (γ := FractionalIdeal.{u_1, u_2} (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K) y
obtain :
  ∀ (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)),
    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) ((Algebra.trace K L : (a : L) → K) x : K) y)

Tactic:
obtain ⟨y, hy, rfl : algebraMap A K _ = _⟩ := (FractionalIdeal.mem_coeIdeal _).mp hy'

Premises used: Algebra.algebraMap, FractionalIdeal.mem_coeIdeal, Iff.mp, DFunLike.coe, rfl