awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ P)
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this_2 : IsScalarTower.{u_1, u_1, u_3} A (A ⧸ p) (B ⧸ Q)
this : Module.Finite.{u_1, u_3} (A ⧸ p) (B ⧸ Q)
e : AlgEquiv.{u_1, u_3, u_3} (A ⧸ p)
  (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) ((B ⧸ P) × B ⧸ Q) :=
  let __spread.0 :
    HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ≃+* (B ⧸ P) × B ⧸ Q :=
    RingEquiv.trans (Ideal.quotEquivOfEq ⋯) (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ ∃ (x : B ⧸ P), Ne.{u_1 + 1} (α := A ⧸ p) ((Algebra.trace (A ⧸ p) (B ⧸ P) : (a : B ⧸ P) → A ⧸ p) x : A ⧸ p) (0 : A ⧸ p)

Tactic:
simpa [LinearMap.ext_iff] using Algebra.trace_ne_zero (A ⧸ p) (B ⧸ P)

Premises used: LinearMap.ext_iff, HasQuotient.Quotient, Algebra.trace_ne_zero
-- 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 Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ P)
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this_2 : IsScalarTower.{u_1, u_1, u_3} A (A ⧸ p) (B ⧸ Q)
this : Module.Finite.{u_1, u_3} (A ⧸ p) (B ⧸ Q)
e : AlgEquiv.{u_1, u_3, u_3} (A ⧸ p)
  (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) ((B ⧸ P) × B ⧸ Q) :=
  let __spread.0 :
    HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ≃+* (B ⧸ P) × B ⧸ Q :=
    RingEquiv.trans (Ideal.quotEquivOfEq ⋯) (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
obtain :
  ∀ (x : B ⧸ P)
    (hx : Ne.{u_1 + 1} (α := A ⧸ p) ((Algebra.trace (A ⧸ p) (B ⧸ P) : (a : B ⧸ P) → A ⧸ p) x : A ⧸ p) (0 : A ⧸ p)),
    ¬P ∣ differentIdeal A B
⊢ ¬P ∣ differentIdeal A B

Tactic:
obtain ⟨x, hx⟩ : ∃ x, Algebra.trace (A ⧸ p) (B ⧸ P) x ≠ 0 := by
    simpa [LinearMap.ext_iff] using Algebra.trace_ne_zero (A ⧸ p) (B ⧸ P)
-- 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 Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ P)
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this_2 : IsScalarTower.{u_1, u_1, u_3} A (A ⧸ p) (B ⧸ Q)
this : Module.Finite.{u_1, u_3} (A ⧸ p) (B ⧸ Q)
e : AlgEquiv.{u_1, u_3, u_3} (A ⧸ p)
  (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) ((B ⧸ P) × B ⧸ Q) :=
  let __spread.0 :
    HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ≃+* (B ⧸ P) × B ⧸ Q :=
    RingEquiv.trans (Ideal.quotEquivOfEq ⋯) (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : Ne.{u_1 + 1} (α := A ⧸ p) ((Algebra.trace (A ⧸ p) (B ⧸ P) : (a : B ⧸ P) → A ⧸ p) x : A ⧸ p) (0 : A ⧸ p)
obtain :
  ∀ (y : B)
    (hy :
      Eq (α := 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)
            y :
          HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
        ((e.symm : (a : (B ⧸ P) × B ⧸ Q) → B ⧸ Ideal.map (algebraMap A B) p) (x, 0) :
          HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))),
    ¬P ∣ differentIdeal A B
⊢ ¬P ∣ differentIdeal A B

Tactic:
obtain ⟨y, hy⟩ := Ideal.Quotient.mk_surjective (e.symm (x, 0))

Premises used: AlgEquiv.symm, Prod.mk, Ideal.Quotient.mk_surjective, OfNat.ofNat, DFunLike.coe
-- 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 Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ P)
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this_2 : IsScalarTower.{u_1, u_1, u_3} A (A ⧸ p) (B ⧸ Q)
this : Module.Finite.{u_1, u_3} (A ⧸ p) (B ⧸ Q)
e : AlgEquiv.{u_1, u_3, u_3} (A ⧸ p)
  (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) ((B ⧸ P) × B ⧸ Q) :=
  let __spread.0 :
    HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ≃+* (B ⧸ P) × B ⧸ Q :=
    RingEquiv.trans (Ideal.quotEquivOfEq ⋯) (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : Ne.{u_1 + 1} (α := A ⧸ p) ((Algebra.trace (A ⧸ p) (B ⧸ P) : (a : B ⧸ P) → A ⧸ p) x : A ⧸ p) (0 : A ⧸ p)
y : B
hy :
  Eq (α := 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) y :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
    ((e.symm : (a : (B ⧸ P) × B ⧸ Q) → B ⧸ Ideal.map (algebraMap A B) p) (x, 0) :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
⊢ ¬P ∣ differentIdeal A B

Tactic:
not_dvd_differentIdeal_of_intTrace_not_mem A P Q hP y ?_ ?_

Premises used: not_dvd_differentIdeal_of_intTrace_not_mem
-- 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 Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ P)
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this_2 : IsScalarTower.{u_1, u_1, u_3} A (A ⧸ p) (B ⧸ Q)
this : Module.Finite.{u_1, u_3} (A ⧸ p) (B ⧸ Q)
e : AlgEquiv.{u_1, u_3, u_3} (A ⧸ p)
  (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) ((B ⧸ P) × B ⧸ Q) :=
  let __spread.0 :
    HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ≃+* (B ⧸ P) × B ⧸ Q :=
    RingEquiv.trans (Ideal.quotEquivOfEq ⋯) (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : Ne.{u_1 + 1} (α := A ⧸ p) ((Algebra.trace (A ⧸ p) (B ⧸ P) : (a : B ⧸ P) → A ⧸ p) x : A ⧸ p) (0 : A ⧸ p)
y : B
hy :
  Eq (α := 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) y :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
    ((e.symm : (a : (B ⧸ P) × B ⧸ Q) → B ⧸ Ideal.map (algebraMap A B) p) (x, 0) :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
refine_1 : y ∈ Q
refine_2 : ((intTrace A B : (a : B) → A) y : A) ∉ p
⊢ ¬P ∣ differentIdeal A B

Tactic:
refine not_dvd_differentIdeal_of_intTrace_not_mem A P Q hP y ?_ ?_

Premises used: not_dvd_differentIdeal_of_intTrace_not_mem
-- 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 Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ P)
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this_2 : IsScalarTower.{u_1, u_1, u_3} A (A ⧸ p) (B ⧸ Q)
this : Module.Finite.{u_1, u_3} (A ⧸ p) (B ⧸ Q)
e : AlgEquiv.{u_1, u_3, u_3} (A ⧸ p)
  (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) ((B ⧸ P) × B ⧸ Q) :=
  let __spread.0 :
    HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ≃+* (B ⧸ P) × B ⧸ Q :=
    RingEquiv.trans (Ideal.quotEquivOfEq ⋯) (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : Ne.{u_1 + 1} (α := A ⧸ p) ((Algebra.trace (A ⧸ p) (B ⧸ P) : (a : B ⧸ P) → A ⧸ p) x : A ⧸ p) (0 : A ⧸ p)
y : B
hy :
  Eq (α := 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) y :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
    ((e.symm : (a : (B ⧸ P) × B ⧸ Q) → B ⧸ Ideal.map (algebraMap A B) p) (x, 0) :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
⊢ Eq.{u_3 + 1} (α := B ⧸ Q)
    ((e : (a : B ⧸ Ideal.map (algebraMap A B) p) → (B ⧸ P) × B ⧸ Q)
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p) : (a : B) → B ⧸ Ideal.map (algebraMap A B) p)
            y :
          HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))).2
    ((e : (a : B ⧸ Ideal.map (algebraMap A B) p) → (B ⧸ P) × B ⧸ Q)
        ((e.symm : (a : (B ⧸ P) × B ⧸ Q) → B ⧸ Ideal.map (algebraMap A B) p) (x, 0) :
          HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))).2

Tactic:
have := congr((e $hy).2)
-- 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 Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ P)
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this_2 : IsScalarTower.{u_1, u_1, u_3} A (A ⧸ p) (B ⧸ Q)
this_3 : Module.Finite.{u_1, u_3} (A ⧸ p) (B ⧸ Q)
e : AlgEquiv.{u_1, u_3, u_3} (A ⧸ p)
  (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) ((B ⧸ P) × B ⧸ Q) :=
  let __spread.0 :
    HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ≃+* (B ⧸ P) × B ⧸ Q :=
    RingEquiv.trans (Ideal.quotEquivOfEq ⋯) (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : Ne.{u_1 + 1} (α := A ⧸ p) ((Algebra.trace (A ⧸ p) (B ⧸ P) : (a : B ⧸ P) → A ⧸ p) x : A ⧸ p) (0 : A ⧸ p)
y : B
hy :
  Eq (α := 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) y :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
    ((e.symm : (a : (B ⧸ P) × B ⧸ Q) → B ⧸ Ideal.map (algebraMap A B) p) (x, 0) :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
this :
  Eq.{u_3 + 1} (α := B ⧸ Q)
    ((e : (a : B ⧸ Ideal.map (algebraMap A B) p) → (B ⧸ P) × B ⧸ Q)
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p) : (a : B) → B ⧸ Ideal.map (algebraMap A B) p)
            y :
          HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))).2
    ((e : (a : B ⧸ Ideal.map (algebraMap A B) p) → (B ⧸ P) × B ⧸ Q)
        ((e.symm : (a : (B ⧸ P) × B ⧸ Q) → B ⧸ Ideal.map (algebraMap A B) p) (x, 0) :
          HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))).2
⊢ Eq.{u_3 + 1} (α := B ⧸ Q)
    ((e : (a : B ⧸ Ideal.map (algebraMap A B) p) → (B ⧸ P) × B ⧸ Q)
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p) : (a : B) → B ⧸ Ideal.map (algebraMap A B) p)
            y :
          HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))).2
    0

Tactic:
simp at this
-- 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 Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ P)
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this_2 : IsScalarTower.{u_1, u_1, u_3} A (A ⧸ p) (B ⧸ Q)
this_3 : Module.Finite.{u_1, u_3} (A ⧸ p) (B ⧸ Q)
e : AlgEquiv.{u_1, u_3, u_3} (A ⧸ p)
  (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) ((B ⧸ P) × B ⧸ Q) :=
  let __spread.0 :
    HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ≃+* (B ⧸ P) × B ⧸ Q :=
    RingEquiv.trans (Ideal.quotEquivOfEq ⋯) (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : Ne.{u_1 + 1} (α := A ⧸ p) ((Algebra.trace (A ⧸ p) (B ⧸ P) : (a : B ⧸ P) → A ⧸ p) x : A ⧸ p) (0 : A ⧸ p)
y : B
hy :
  Eq (α := 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) y :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
    ((e.symm : (a : (B ⧸ P) × B ⧸ Q) → B ⧸ Ideal.map (algebraMap A B) p) (x, 0) :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
this :
  Eq.{u_3 + 1} (α := B ⧸ Q)
    ((e : (a : B ⧸ Ideal.map (algebraMap A B) p) → (B ⧸ P) × B ⧸ Q)
        ((Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p) : (a : B) → B ⧸ Ideal.map (algebraMap A B) p)
            y :
          HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))).2
    0
⊢ y ∈ Q

Tactic:
simpa [e, Ideal.Quotient.eq_zero_iff_mem] using this

Premises used: Ideal.Quotient.eq_zero_iff_mem
-- 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 Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ P)
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this_2 : IsScalarTower.{u_1, u_1, u_3} A (A ⧸ p) (B ⧸ Q)
this : Module.Finite.{u_1, u_3} (A ⧸ p) (B ⧸ Q)
e : AlgEquiv.{u_1, u_3, u_3} (A ⧸ p)
  (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) ((B ⧸ P) × B ⧸ Q) :=
  let __spread.0 :
    HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ≃+* (B ⧸ P) × B ⧸ Q :=
    RingEquiv.trans (Ideal.quotEquivOfEq ⋯) (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : Ne.{u_1 + 1} (α := A ⧸ p) ((Algebra.trace (A ⧸ p) (B ⧸ P) : (a : B ⧸ P) → A ⧸ p) x : A ⧸ p) (0 : A ⧸ p)
y : B
hy :
  Eq (α := 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) y :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
    ((e.symm : (a : (B ⧸ P) × B ⧸ Q) → B ⧸ Ideal.map (algebraMap A B) p) (x, 0) :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
refine_2 :
  ¬HAdd.hAdd (α := A ⧸ p) (β := A ⧸ p) ((Algebra.trace (A ⧸ p) (B ⧸ P) : (a : B ⧸ P) → A ⧸ p) (x, 0).1 : A ⧸ p)
        ((Algebra.trace (A ⧸ p) (B ⧸ Q) : (a : B ⧸ Q) → A ⧸ p) (x, 0).2 : A ⧸ p) =
      0
⊢ ((intTrace A B : (a : B) → A) y : A) ∉ p

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, ← Algebra.trace_quotient_eq_of_isDedekindDomain,
      hy, Algebra.trace_eq_of_algEquiv, Algebra.trace_prod_apply]

Premises used: Algebra.trace_eq_of_algEquiv, Ideal.Quotient.eq_zero_iff_mem, Algebra.trace_quotient_eq_of_isDedekindDomain, Algebra.trace_prod_apply
-- 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 Q : Ideal B
inst_10 : P.IsMaximal
inst_11 : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
inst_12 : Algebra.IsSeparable.{u_1, u_3} (A ⧸ p) (B ⧸ P)
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this_2 : IsScalarTower.{u_1, u_1, u_3} A (A ⧸ p) (B ⧸ Q)
this : Module.Finite.{u_1, u_3} (A ⧸ p) (B ⧸ Q)
e : AlgEquiv.{u_1, u_3, u_3} (A ⧸ p)
  (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)) ((B ⧸ P) × B ⧸ Q) :=
  let __spread.0 :
    HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ≃+* (B ⧸ P) × B ⧸ Q :=
    RingEquiv.trans (Ideal.quotEquivOfEq ⋯) (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : Ne.{u_1 + 1} (α := A ⧸ p) ((Algebra.trace (A ⧸ p) (B ⧸ P) : (a : B ⧸ P) → A ⧸ p) x : A ⧸ p) (0 : A ⧸ p)
y : B
hy :
  Eq (α := 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) y :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
    ((e.symm : (a : (B ⧸ P) × B ⧸ Q) → B ⧸ Ideal.map (algebraMap A B) p) (x, 0) :
      HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
⊢ ¬HAdd.hAdd (α := A ⧸ p) (β := A ⧸ p) ((Algebra.trace (A ⧸ p) (B ⧸ P) : (a : B ⧸ P) → A ⧸ p) (x, 0).1 : A ⧸ p)
        ((Algebra.trace (A ⧸ p) (B ⧸ Q) : (a : B ⧸ Q) → A ⧸ p) (x, 0).2 : A ⧸ p) =
      0

Tactic:
simpa
-- 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
inst_10 : Finite.{u_1 + 1} (A ⧸ p)
P Q : Ideal B
inst_11 : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
over : p = Ideal.under A P
⊢ P.LiesOver p

Tactic:
constructor
-- 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
inst_10 : Finite.{u_1 + 1} (A ⧸ p)
P Q : Ideal B
inst_11 : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
⊢ p = Ideal.under A P

Tactic:
‹p.IsMaximal›.eq_of_le ?_ ?_

Premises used: Ideal.IsMaximal.eq_of_le
-- 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
inst_10 : Finite.{u_1 + 1} (A ⧸ p)
P Q : Ideal B
inst_11 : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
over : Ne (α := Ideal A) (Ideal.under A P) ⊤
over₁ : p ≤ Ideal.under A P
⊢ p = Ideal.under A P

Tactic:
refine ‹p.IsMaximal›.eq_of_le ?_ ?_

Premises used: Ideal.IsMaximal.eq_of_le
-- 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
inst_10 : Finite.{u_1 + 1} (A ⧸ p)
P Q : Ideal B
inst_11 : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
⊢ Ne (α := Ideal A) (Ideal.under A P) ⊤

Tactic:
simpa using ‹P.IsMaximal›.ne_top

Premises used: Ideal.IsMaximal.ne_top
-- 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
inst_10 : Finite.{u_1 + 1} (A ⧸ p)
P Q : Ideal B
inst_11 : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
over : P * Q ≤ P
⊢ p ≤ Ideal.under A P

Tactic:
rw [← Ideal.map_le_iff_le_comap, ← hP]

Premises used: Ideal.map_le_iff_le_comap