awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x_1 : B
hxQ : x_1 ∈ Q
hx_1 : ((intTrace A B : (a : B) → A) x_1 : A) ∉ p
hp : ¬p = ⊥
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this_2 : IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) L
this : FiniteDimensional K L
H :
  (↑Q : FractionalIdeal B⁰ L) ≤
    HMul.hMul (α := FractionalIdeal (R := B) B⁰ L) (β := FractionalIdeal (R := B) B⁰ L)
      (FractionalIdeal.dual A K 1 : FractionalIdeal (R := B) B⁰ L)
      (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)
hne : Ne.{u_3 + 1} (α := FractionalIdeal (R := B) B⁰ L) 1 0
x : L
hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x
y : B
hy : y ∈ (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : Set B)
neg :
  ∀ (y : B) (h : Membership.mem (γ := Set B) ((⇑(algebraMap A B) : (a : A) → B) '' (↑p : Set A)) y) (x : L)
    (hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x),
    Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
      (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
          (HMul.hMul (β := L) x ((Algebra.linearMap B L : (a : B) → L) y : L)) :
        K)
⊢ Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K)
        (HMul.hMul (β := L) x ((Algebra.linearMap B L : (a : B) → L) y : L)) :
      K)
have neg₁ : ∀ (x : L) (hx : Membership.mem (γ := FractionalIdeal (R := B) B⁰ L) (FractionalIdeal.dual A K 1) x),
  Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
    (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) (x * (Algebra.linearMap B L : (a : B) → L) 0) : K)
Tactic: induction hy using Submodule.span_induction generalizing x with
    | mem y h =>
      obtain ⟨y, hy, rfl⟩ := h
      obtain ⟨z, hz⟩ :=
        (FractionalIdeal.mem_dual (by simp)).mp hx 1 ⟨1, trivial, (algebraMap B L).map_one⟩
      simp only [Algebra.traceForm_apply, mul_one] at hz
      refine ⟨z * y, Ideal.mul_mem_left _ _ hy, ?_⟩
      rw [Algebra.linearMap_apply, Algebra.linearMap_apply, mul_comm x,
        ← IsScalarTower.algebraMap_apply,
        ← Algebra.smul_def, LinearMap.map_smul_of_tower, ← hz,
        Algebra.smul_def, map_mul, mul_comm]
    | zero => simp
    | add y z _ _ hy hz =>
      simp only [map_add, mul_add]
      exact Submodule.add_mem _ (hy x hx) (hz x hx)
    | smul y z hz IH =>
      simpa [Algebra.smul_def, mul_assoc, -FractionalIdeal.mem_coeIdeal, mul_left_comm x] using
        IH _ (Submodule.smul_mem _ y hx)
Cleared hypotheses: x, hx, hy
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
P Q : Ideal B
hP : P * Q = Ideal.map (F := A →+* B) (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : ((intTrace A B : (a : B) → A) x : A) ∉ p
hp : ¬p = ⊥
this_1 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this_2 : IsLocalization (algebraMapSubmonoid.{u_1, u_3} (R := A) B A⁰) L
this : FiniteDimensional K L
H :
  (↑Q : FractionalIdeal B⁰ L) ≤
    HMul.hMul (α := FractionalIdeal (R := B) B⁰ L) (β := FractionalIdeal (R := B) B⁰ L)
      (FractionalIdeal.dual A K 1 : FractionalIdeal (R := B) B⁰ L)
      (↑(Ideal.map (F := A →+* B) (algebraMap A B) p) : FractionalIdeal B⁰ L)
hne : Ne.{u_3 + 1} (α := FractionalIdeal (R := B) B⁰ L) 1 0
⊢ ∀ (x y : L),
    Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
        (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) x : K) →
      Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
          (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) y : K) →
        Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
          (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) (x + y) : K)
have neg : ∀ (x y : L),
  Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
      (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) x : K) →
    Membership.mem (α := K) (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
        (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) y : K) →
      Membership.mem (γ := FractionalIdeal (R := A) A⁰ K) (↑p : FractionalIdeal A⁰ K)
        (HAdd.hAdd (α := K) (β := K) (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) x : K)
          (((Algebra.trace K L : L →ₗ[K] K) : (a : L) → K) y : K))
Tactic: simp only [map_add]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
⊢ p ≤ Ideal.comap (F := A →+* B) (algebraMap A B) Q
have rw : P * Q ≤ Q
Tactic: rw [← Ideal.map_le_iff_le_comap, ← hP]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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 : Algebra.{u_1, u_3} (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
⊢ ¬P ∣ differentIdeal A B
have this₁ : IsScalarTower.{u_1, u_1, u_3} A (A ⧸ p) (B ⧸ Q)
Tactic: have : IsScalarTower A (A ⧸ p) (B ⧸ Q) := .of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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 : IsScalarTower.{u_1, u_1, u_3} A (A ⧸ p) (B ⧸ Q)
⊢ ¬P ∣ differentIdeal A B
have this₁ : Module.Finite.{u_1, u_3} (A ⧸ p) (B ⧸ Q)
Tactic: have : Module.Finite (A ⧸ p) (B ⧸ Q) :=
    Module.Finite.of_restrictScalars_finite A (A ⧸ p) (B ⧸ Q)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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' := ⋯ }
⊢ ¬P ∣ differentIdeal A B
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
⊢ ¬P ∣ differentIdeal A B
have 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
Tactic: obtain ⟨y, hy⟩ := Ideal.Quotient.mk_surjective (e.symm (x, 0))
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
have refine_1 : y ∈ Q
Tactic: refine not_dvd_differentIdeal_of_intTrace_not_mem A P Q hP y ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
⊢ ¬P ∣ differentIdeal A B
have refine_2 : ((intTrace A B : (a : B) → A) y : A) ∉ p
Tactic: refine not_dvd_differentIdeal_of_intTrace_not_mem A P Q hP y ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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))
⊢ y ∈ Q
have 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
Tactic: have := congr((e $hy).2)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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
⊢ y ∈ Q
have 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
Tactic: simp at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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))
⊢ ((intTrace A B : (a : B) → A) y : A) ∉ p
have 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
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, ← Algebra.trace_quotient_eq_of_isDedekindDomain,
      hy, Algebra.trace_eq_of_algEquiv, Algebra.trace_prod_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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.LiesOver p
have over : p = Ideal.under A P
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
have over : Ne (α := Ideal A) (Ideal.under A P) ⊤
Tactic: refine ‹p.IsMaximal›.eq_of_le ?_ ?_