awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst_4 : CommRing B
inst_5 : IsDedekindDomain B
L : Ideal B
inst_6 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
f_surj :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := A ⧸ J) (⇑(↑f : R ⧸ I →+* A ⧸ J) : (a : R ⧸ I) → A ⧸ J)
fsym_surj :
  Function.Surjective.{u_2 + 1, u_1 + 1} (α := A ⧸ J) (β := R ⧸ I) (⇑(↑f.symm : A ⧸ J →+* R ⧸ I) : (a : A ⧸ J) → R ⧸ I)
⊢ (idealFactorsFunOfQuotHom fsym_surj).comp (idealFactorsFunOfQuotHom f_surj) = OrderHom.id

Tactic:
simpa using idealFactorsFunOfQuotHom_comp f_surj fsym_surj

Premises used: IsDedekindDomain.idealFactorsFunOfQuotHom_comp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
⊢ (idealFactorsEquivOfQuotEquiv f).symm = idealFactorsEquivOfQuotEquiv f.symm

Tactic:
rfl

Premises used: IsDedekindDomain.idealFactorsEquivOfQuotEquiv, Set.Mem, setOf, RelIso.symm, Equiv.symm, RingEquiv.symm, rfl, OrderIso.ofHomInv
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
idealFactorsEquivOfQuotEquiv :
  LE.le.{u_2} (α := (↑{p : Ideal A | p ∣ J} : Type u_2))
      ((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f :
            (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) M hM) :
        (↑{p : Ideal A | p ∣ J} : Type u_2))
      ((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f :
            (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L hL) :
        (↑{p : Ideal A | p ∣ J} : Type u_2)) ↔
    LE.le (α := { x : Ideal R // Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x })
      (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) M hM)
      (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L hL)
⊢ Dvd.dvd.{u_2} (α := Ideal A)
      (↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f :
              (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
            (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L hL)) :
        Ideal A)
      (↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f :
              (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
            (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) M hM)) :
        Ideal A) ↔
    L ∣ M

Tactic:
suffices
    idealFactorsEquivOfQuotEquiv f ⟨M, hM⟩ ≤ idealFactorsEquivOfQuotEquiv f ⟨L, hL⟩ ↔
      (⟨M, hM⟩ : { p : Ideal R | p ∣ I }) ≤ ⟨L, hL⟩
    by rw [dvd_iff_le, dvd_iff_le, Subtype.coe_le_coe, this, Subtype.mk_le_mk]
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
⊢ LE.le.{u_2} (α := (↑{p : Ideal A | p ∣ J} : Type u_2))
      ((idealFactorsEquivOfQuotEquiv f :
            (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) M hM) :
        (↑{p : Ideal A | p ∣ J} : Type u_2))
      ((idealFactorsEquivOfQuotEquiv f :
            (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L hL) :
        (↑{p : Ideal A | p ∣ J} : Type u_2)) ↔
    LE.le (α := { x : Ideal R // Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x })
      (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) M hM)
      (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L hL)

Tactic:
(idealFactorsEquivOfQuotEquiv f).le_iff_le

Premises used: IsDedekindDomain.idealFactorsEquivOfQuotEquiv, OrderIso.le_iff_le
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
L M : Ideal R
hL : L ∣ I
hM : M ∣ I
⊢ LE.le.{u_2} (α := (↑{p : Ideal A | p ∣ J} : Type u_2))
      ((idealFactorsEquivOfQuotEquiv f :
            (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) M hM) :
        (↑{p : Ideal A | p ∣ J} : Type u_2))
      ((idealFactorsEquivOfQuotEquiv f :
            (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L hL) :
        (↑{p : Ideal A | p ∣ J} : Type u_2)) ↔
    LE.le (α := { x : Ideal R // Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x })
      (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) M hM)
      (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L hL)

Tactic:
exact (idealFactorsEquivOfQuotEquiv f).le_iff_le

Premises used: IsDedekindDomain.idealFactorsEquivOfQuotEquiv, OrderIso.le_iff_le
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I = ⊥
⊢ Membership.mem (γ := Multiset (Ideal R)) ∅ L

Tactic:
rw [hI, bot_eq_zero, normalizedFactors_zero, ← Multiset.empty_eq_zero] at hL

Premises used: UniqueFactorizationMonoid.normalizedFactors_zero, Multiset.empty_eq_zero, bot_eq_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I = ⊥
hL₁ : Membership.mem (γ := Multiset (Ideal R)) ∅ L
⊢ I = ⊥

Tactic:
rw [hI, bot_eq_zero, normalizedFactors_zero, ← Multiset.empty_eq_zero] at hL

Premises used: UniqueFactorizationMonoid.normalizedFactors_zero, Multiset.empty_eq_zero, bot_eq_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hJ : J ≠ ⊥
L : Ideal R
hL : Membership.mem (γ := Multiset (Ideal R)) ∅ L
hI : I = ⊥
⊢ False

Tactic:
Finset.notMem_empty _ hL

Premises used: Finset.notMem_empty
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hJ : J ≠ ⊥
L : Ideal R
hL : Membership.mem (γ := Multiset (Ideal R)) ∅ L
hI : I = ⊥
⊢ False

Tactic:
exact Finset.notMem_empty _ hL

Premises used: Finset.notMem_empty
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ I ≠ ⊥

Tactic:
have hI : I ≠ ⊥ := by
    intro hI
    rw [hI, bot_eq_zero, normalizedFactors_zero, ← Multiset.empty_eq_zero] at hL
    exact Finset.notMem_empty _ hL
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I ≠ ⊥
⊢ (↑((idealFactorsEquivOfQuotEquiv f : (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L ⋯)) :
      Ideal A) ∈
    normalizedFactors J

Tactic:
mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors hI hJ hL
    (d := (idealFactorsEquivOfQuotEquiv f).toEquiv) ?_

Premises used: mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I ≠ ⊥
refine :
  ∀ (l l' : { l : Ideal R // l ∣ I }),
    Dvd.dvd.{u_2} (α := Ideal A)
        (↑(((idealFactorsEquivOfQuotEquiv f).toEquiv (r := fun (x1 x2 : (↑{p : Ideal R | p ∣ I} : Type u_1)) ↦ x1 ≤ x2)
                  (s := fun (x1 x2 : (↑{p : Ideal A | p ∣ J} : Type u_2)) ↦ x1 ≤ x2) :
                (a : { l : Ideal R // l ∣ I }) → { l : Ideal A // l ∣ J })
              l) :
          Ideal A)
        (↑(((idealFactorsEquivOfQuotEquiv f).toEquiv (r := fun (x1 x2 : (↑{p : Ideal R | p ∣ I} : Type u_1)) ↦ x1 ≤ x2)
                  (s := fun (x1 x2 : (↑{p : Ideal A | p ∣ J} : Type u_2)) ↦ x1 ≤ x2) :
                (a : { l : Ideal R // l ∣ I }) → { l : Ideal A // l ∣ J })
              l') :
          Ideal A) ↔
      (↑l : Ideal R) ∣ (↑l' : Ideal R)
⊢ (↑((idealFactorsEquivOfQuotEquiv f : (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
          (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x) L ⋯)) :
      Ideal A) ∈
    normalizedFactors J

Tactic:
refine mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors hI hJ hL
    (d := (idealFactorsEquivOfQuotEquiv f).toEquiv) ?_

Premises used: mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I ≠ ⊥
l : Ideal R
hl : l ∣ I
l' : Ideal R
hl' : l' ∣ I
⊢ Dvd.dvd.{u_2} (α := Ideal A)
      (↑(((idealFactorsEquivOfQuotEquiv f).toEquiv (r := fun (x1 x2 : (↑{p : Ideal R | p ∣ I} : Type u_1)) ↦ x1 ≤ x2)
                (s := fun (x1 x2 : (↑{p : Ideal A | p ∣ J} : Type u_2)) ↦ x1 ≤ x2) :
              (a : { l : Ideal R // l ∣ I }) → { l : Ideal A // l ∣ J })
            (Subtype.mk (p := fun (l : Ideal R) ↦ l ∣ I) l hl)) :
        Ideal A)
      (↑(((idealFactorsEquivOfQuotEquiv f).toEquiv (r := fun (x1 x2 : (↑{p : Ideal R | p ∣ I} : Type u_1)) ↦ x1 ≤ x2)
                (s := fun (x1 x2 : (↑{p : Ideal A | p ∣ J} : Type u_2)) ↦ x1 ≤ x2) :
              (a : { l : Ideal R // l ∣ I }) → { l : Ideal A // l ∣ J })
            (Subtype.mk (p := fun (l : Ideal R) ↦ l ∣ I) l' hl')) :
        Ideal A) ↔
    (↑(Subtype.mk (p := fun (l : Ideal R) ↦ l ∣ I) l hl) : Ideal R) ∣
      (↑(Subtype.mk (p := fun (l : Ideal R) ↦ l ∣ I) l' hl') : Ideal R)

Tactic:
apply idealFactorsEquivOfQuotEquiv_is_dvd_iso f

Premises used: IsDedekindDomain.idealFactorsEquivOfQuotEquiv_is_dvd_iso
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst_4 : CommRing B
inst_5 : IsDedekindDomain B
L : Ideal B
inst_6 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hI : I ≠ ⊥
hJ : J ≠ ⊥
j : (↑{M : Ideal A | M ∈ normalizedFactors J} : Type u_2)
⊢ Membership.mem (γ := Set (Ideal R)) {L : Ideal R | L ∈ normalizedFactors I}
    (↑((idealFactorsEquivOfQuotEquiv f.symm :
            (a : (↑{p : Ideal A | p ∣ J} : Type u_2)) → (↑{p : Ideal R | p ∣ I} : Type u_1))
          (Subtype.mk (p := fun (x : Ideal A) ↦ Membership.mem (γ := Set (Ideal A)) {p : Ideal A | p ∣ J} x)
            (↑j : Ideal A) ⋯)) :
      Ideal R)

Tactic:
idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors f.symm hI
          j.prop

Premises used: Set.Mem, setOf, IsDedekindDomain.idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors, Multiset.Mem, Subtype.prop, RingEquiv.symm
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst_4 : CommRing B
inst_5 : IsDedekindDomain B
L : Ideal B
inst_6 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hI : I ≠ ⊥
hJ : J ≠ ⊥
j : (↑{M : Ideal A | M ∈ normalizedFactors J} : Type u_2)
⊢ Membership.mem (γ := Set (Ideal R)) {L : Ideal R | L ∈ normalizedFactors I}
    (↑((idealFactorsEquivOfQuotEquiv f.symm :
            (a : (↑{p : Ideal A | p ∣ J} : Type u_2)) → (↑{p : Ideal R | p ∣ I} : Type u_1))
          (Subtype.mk (p := fun (x : Ideal A) ↦ Membership.mem (γ := Set (Ideal A)) {p : Ideal A | p ∣ J} x)
            (↑j : Ideal A) ⋯)) :
      Ideal R)

Tactic:
exact
        idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors f.symm hI
          j.prop

Premises used: IsDedekindDomain.idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors, Subtype.prop, RingEquiv.symm
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst_4 : CommRing B
inst_5 : IsDedekindDomain B
L : Ideal B
inst_6 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hI : I ≠ ⊥
hJ : J ≠ ⊥
x : (↑{L : Ideal R | L ∈ normalizedFactors I} : Type u_1)
j : Ideal R
hj : Membership.mem (γ := Set (Ideal R)) {L : Ideal R | L ∈ normalizedFactors I} j
⊢ (fun (j : (↑{M : Ideal A | M ∈ normalizedFactors J} : Type u_2)) ↦
        (Subtype.mk (p := fun (x : Ideal R) ↦
            Membership.mem (γ := Set (Ideal R)) {L : Ideal R | L ∈ normalizedFactors I} x)
            (↑(((idealFactorsEquivOfQuotEquiv f).symm :
                    (a : (↑{p : Ideal A | p ∣ J} : Type u_2)) → (↑{p : Ideal R | p ∣ I} : Type u_1))
                  (Subtype.mk (p := fun (x : Ideal A) ↦ Membership.mem (γ := Set (Ideal A)) {p : Ideal A | p ∣ J} x)
                    (↑j : Ideal A) ⋯)) :
              Ideal R)
            ⋯ :
          { x : Ideal R // Membership.mem (γ := Set (Ideal R)) {L : Ideal R | L ∈ normalizedFactors I} x }))
      ((fun (j : (↑{L : Ideal R | L ∈ normalizedFactors I} : Type u_1)) ↦
          (Subtype.mk (p := fun (x : Ideal A) ↦
              Membership.mem (γ := Set (Ideal A)) {M : Ideal A | M ∈ normalizedFactors J} x)
              (↑((idealFactorsEquivOfQuotEquiv f :
                      (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
                    (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x)
                      (↑j : Ideal R) ⋯)) :
                Ideal A)
              ⋯ :
            { x : Ideal A // Membership.mem (γ := Set (Ideal A)) {M : Ideal A | M ∈ normalizedFactors J} x }))
        (Subtype.mk (p := fun (x : Ideal R) ↦
          Membership.mem (γ := Set (Ideal R)) {L : Ideal R | L ∈ normalizedFactors I} x) j hj)) =
    Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {L : Ideal R | L ∈ normalizedFactors I} x)
      j hj

Tactic:
simp
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Field K
inst_3 : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst_4 : CommRing B
inst_5 : IsDedekindDomain B
L : Ideal B
inst_6 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hI : I ≠ ⊥
hJ : J ≠ ⊥
x : (↑{M : Ideal A | M ∈ normalizedFactors J} : Type u_2)
j : Ideal A
hj : Membership.mem (γ := Set (Ideal A)) {M : Ideal A | M ∈ normalizedFactors J} j
⊢ (fun (j : (↑{L : Ideal R | L ∈ normalizedFactors I} : Type u_1)) ↦
        (Subtype.mk (p := fun (x : Ideal A) ↦
            Membership.mem (γ := Set (Ideal A)) {M : Ideal A | M ∈ normalizedFactors J} x)
            (↑((idealFactorsEquivOfQuotEquiv f :
                    (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
                  (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x)
                    (↑j : Ideal R) ⋯)) :
              Ideal A)
            ⋯ :
          { x : Ideal A // Membership.mem (γ := Set (Ideal A)) {M : Ideal A | M ∈ normalizedFactors J} x }))
      ((fun (j : (↑{M : Ideal A | M ∈ normalizedFactors J} : Type u_2)) ↦
          (Subtype.mk (p := fun (x : Ideal R) ↦
              Membership.mem (γ := Set (Ideal R)) {L : Ideal R | L ∈ normalizedFactors I} x)
              (↑(((idealFactorsEquivOfQuotEquiv f).symm :
                      (a : (↑{p : Ideal A | p ∣ J} : Type u_2)) → (↑{p : Ideal R | p ∣ I} : Type u_1))
                    (Subtype.mk (p := fun (x : Ideal A) ↦ Membership.mem (γ := Set (Ideal A)) {p : Ideal A | p ∣ J} x)
                      (↑j : Ideal A) ⋯)) :
                Ideal R)
              ⋯ :
            { x : Ideal R // Membership.mem (γ := Set (Ideal R)) {L : Ideal R | L ∈ normalizedFactors I} x }))
        (Subtype.mk (p := fun (x : Ideal A) ↦
          Membership.mem (γ := Set (Ideal A)) {M : Ideal A | M ∈ normalizedFactors J} x) j hj)) =
    Subtype.mk (p := fun (x : Ideal A) ↦ Membership.mem (γ := Set (Ideal A)) {M : Ideal A | M ∈ normalizedFactors J} x)
      j hj

Tactic:
simp [-Set.coe_setOf]

Premises used: Set.coe_setOf
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ Eq (α :=
    Equiv.{u_2 + 1, u_1 + 1} (↑{M : Ideal A | M ∈ normalizedFactors J} : Type u_2)
      (↑{L : Ideal R | L ∈ normalizedFactors I} : Type u_1))
    (Equiv.symm (normalizedFactorsEquivOfQuotEquiv f hI hJ) :
      Equiv.{u_2 + 1, u_1 + 1} (↑{M : Ideal A | M ∈ normalizedFactors J} : Type u_2)
        (↑{L : Ideal R | L ∈ normalizedFactors I} : Type u_1))
    (normalizedFactorsEquivOfQuotEquiv f.symm hJ hI :
      Equiv.{u_2 + 1, u_1 + 1} (↑{L : Ideal A | L ∈ normalizedFactors J} : Type u_2)
        (↑{M : Ideal R | M ∈ normalizedFactors I} : Type u_1))

Tactic:
rfl

Premises used: IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hI : I ≠ ⊥
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ emultiplicity
      (↑((idealFactorsEquivOfQuotEquiv f :
              (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
            (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x)
              (↑(Subtype.mk (p := fun (x : Ideal R) ↦
                    Membership.mem (γ := Set (Ideal R)) {L : Ideal R | L ∈ normalizedFactors I} x) L hL) :
                Ideal R)
              ⋯)) :
        Ideal A)
      J =
    emultiplicity L I

Tactic:
emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors hI hJ hL
    (d := (idealFactorsEquivOfQuotEquiv f).toEquiv) ?_

Premises used: emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hI : I ≠ ⊥
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
refine :
  ∀ (l l' : { l : Ideal R // l ∣ I }),
    Dvd.dvd.{u_2} (α := Ideal A)
        (↑(((idealFactorsEquivOfQuotEquiv f).toEquiv (r := fun (x1 x2 : (↑{p : Ideal R | p ∣ I} : Type u_1)) ↦ x1 ≤ x2)
                  (s := fun (x1 x2 : (↑{p : Ideal A | p ∣ J} : Type u_2)) ↦ x1 ≤ x2) :
                (a : { l : Ideal R // l ∣ I }) → { l : Ideal A // l ∣ J })
              l) :
          Ideal A)
        (↑(((idealFactorsEquivOfQuotEquiv f).toEquiv (r := fun (x1 x2 : (↑{p : Ideal R | p ∣ I} : Type u_1)) ↦ x1 ≤ x2)
                  (s := fun (x1 x2 : (↑{p : Ideal A | p ∣ J} : Type u_2)) ↦ x1 ≤ x2) :
                (a : { l : Ideal R // l ∣ I }) → { l : Ideal A // l ∣ J })
              l') :
          Ideal A) ↔
      (↑l : Ideal R) ∣ (↑l' : Ideal R)
⊢ emultiplicity
      (↑((idealFactorsEquivOfQuotEquiv f :
              (a : (↑{p : Ideal R | p ∣ I} : Type u_1)) → (↑{p : Ideal A | p ∣ J} : Type u_2))
            (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p ∣ I} x)
              (↑(Subtype.mk (p := fun (x : Ideal R) ↦
                    Membership.mem (γ := Set (Ideal R)) {L : Ideal R | L ∈ normalizedFactors I} x) L hL) :
                Ideal R)
              ⋯)) :
        Ideal A)
      J =
    emultiplicity L I

Tactic:
refine emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors hI hJ hL
    (d := (idealFactorsEquivOfQuotEquiv f).toEquiv) ?_

Premises used: emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst_3 : IsDedekindDomain R
f : RingEquiv.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hI : I ≠ ⊥
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ ∀ (l l' : { l : Ideal R // l ∣ I }),
    Dvd.dvd.{u_2} (α := Ideal A)
        (↑(((idealFactorsEquivOfQuotEquiv f).toEquiv (r := fun (x1 x2 : (↑{p : Ideal R | p ∣ I} : Type u_1)) ↦ x1 ≤ x2)
                  (s := fun (x1 x2 : (↑{p : Ideal A | p ∣ J} : Type u_2)) ↦ x1 ≤ x2) :
                (a : { l : Ideal R // l ∣ I }) → { l : Ideal A // l ∣ J })
              l) :
          Ideal A)
        (↑(((idealFactorsEquivOfQuotEquiv f).toEquiv (r := fun (x1 x2 : (↑{p : Ideal R | p ∣ I} : Type u_1)) ↦ x1 ≤ x2)
                  (s := fun (x1 x2 : (↑{p : Ideal A | p ∣ J} : Type u_2)) ↦ x1 ≤ x2) :
                (a : { l : Ideal R // l ∣ I }) → { l : Ideal A // l ∣ J })
              l') :
          Ideal A) ↔
      (↑l : Ideal R) ∣ (↑l' : Ideal R)

Tactic:
fun ⟨l, hl⟩ ⟨l', hl'⟩ => idealFactorsEquivOfQuotEquiv_is_dvd_iso f hl hl'

Premises used: Dvd.dvd, IsDedekindDomain.idealFactorsEquivOfQuotEquiv, IsDedekindDomain.idealFactorsEquivOfQuotEquiv_is_dvd_iso, Subtype.mk, Iff, _private.0.IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity.match_2, RelIso.toEquiv, Subtype.val, DFunLike.coe