awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
f : RingHom.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := A ⧸ J) (⇑f : (a : R ⧸ I) → A ⧸ J)
X : Ideal R
hX : X ∣ I
Y : Ideal R
hY : Y ∣ I
h :
  LE.le (α := { p : Ideal R // p ∣ I }) (Subtype.mk (p := fun (p : Ideal R) ↦ p ∣ I) X hX)
    (Subtype.mk (p := fun (p : Ideal R) ↦ p ∣ I) Y hY)
⊢ LE.le.{u_2} (α := { p : Ideal A // p ∣ J })
    ((fun (X : { p : Ideal R // p ∣ I }) ↦
        (Subtype.mk (p := fun (p : Ideal A) ↦ p ∣ J)
            (comap (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
              (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑X : Ideal R))))
            ⋯ :
          { p : Ideal A // p ∣ J }))
      (Subtype.mk (p := fun (p : Ideal R) ↦ p ∣ I) X hX))
    ((fun (X : { p : Ideal R // p ∣ I }) ↦
        (Subtype.mk (p := fun (p : Ideal A) ↦ p ∣ J)
            (comap (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
              (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑X : Ideal R))))
            ⋯ :
          { p : Ideal A // p ∣ J }))
      (Subtype.mk (p := fun (p : Ideal R) ↦ p ∣ I) Y hY))
have rw : ∀ (h : X ≤ Y),
  LE.le (α := Ideal A)
    (comap (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
      (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) X)))
    (↑((fun (X : { p : Ideal R // p ∣ I }) ↦
            (Subtype.mk (p := fun (p : Ideal A) ↦ p ∣ J)
                (comap (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
                  (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑X : Ideal R))))
                sorry :
              { p : Ideal A // p ∣ J }))
          (Subtype.mk (p := fun (p : Ideal R) ↦ p ∣ I) Y hY)) :
      Ideal A)
Tactic: rw [← Subtype.coe_le_coe, Subtype.coe_mk, Subtype.coe_mk] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
f : RingHom.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := A ⧸ J) (⇑f : (a : R ⧸ I) → A ⧸ J)
X : Ideal R
hX : X ∣ I
Y : Ideal R
hY : Y ∣ I
h : X ≤ Y
⊢ LE.le (α := Ideal A)
    (comap (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
      (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) X)))
    (↑((fun (X : { p : Ideal R // p ∣ I }) ↦
            (Subtype.mk (p := fun (p : Ideal A) ↦ p ∣ J)
                (comap (F := A →+* A ⧸ J) (Ideal.Quotient.mk J)
                  (map (R := R ⧸ I) f (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (↑X : Ideal R))))
                ⋯ :
              { p : Ideal A // p ∣ J }))
          (Subtype.mk (p := fun (p : Ideal R) ↦ p ∣ I) Y hY)) :
      Ideal A)
have rw : LE.le (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) X)
  (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) Y ⊔ comap f ⊥)
Tactic: rw [Subtype.coe_mk, comap_le_comap_iff_of_surjective (Ideal.Quotient.mk J)
      Ideal.Quotient.mk_surjective, map_le_iff_le_comap, Subtype.coe_mk,
      comap_map_of_surjective _ hf (map (Ideal.Quotient.mk I) Y)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
f : RingHom.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := A ⧸ J) (⇑f : (a : R ⧸ I) → A ⧸ J)
X : Ideal R
hX : X ∣ I
Y : Ideal R
hY : Y ∣ I
h : X ≤ Y
⊢ LE.le (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) X)
    (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) Y ⊔ comap f ⊥)
have suffices : LE.le (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) X)
  (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) Y)
Tactic: suffices map (Ideal.Quotient.mk I) X ≤ map (Ideal.Quotient.mk I) Y by
      exact le_sup_of_le_left this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
f : RingHom.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := A ⧸ J) (⇑f : (a : R ⧸ I) → A ⧸ J)
X : Ideal R
hX : X ∣ I
Y : Ideal R
hY : Y ∣ I
h : X ≤ Y
⊢ LE.le (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) X)
    (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) Y)
have rwa : X ≤ comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) Y)
Tactic: rwa [map_le_iff_le_comap, comap_map_of_surjective (Ideal.Quotient.mk I)
      Ideal.Quotient.mk_surjective, ← RingHom.ker_eq_comap_bot, mk_ker,
      sup_eq_left.mpr <| le_of_dvd hY]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
f : RingHom.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := A ⧸ J) (⇑f : (a : R ⧸ I) → A ⧸ J)
X : Ideal R
hX : X ∣ I
Y : Ideal R
hY : Y ∣ I
h : X ≤ Y
rwa : X ≤ comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) Y)
⊢ LE.le (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) X)
    (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) Y)
have rwa₁ : X ≤ Y ⊔ comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) ⊥
Tactic: rwa [map_le_iff_le_comap, comap_map_of_surjective (Ideal.Quotient.mk I)
      Ideal.Quotient.mk_surjective, ← RingHom.ker_eq_comap_bot, mk_ker,
      sup_eq_left.mpr <| le_of_dvd hY]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
f : RingHom.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := A ⧸ J) (⇑f : (a : R ⧸ I) → A ⧸ J)
X : Ideal R
hX : X ∣ I
Y : Ideal R
hY : Y ∣ I
h : X ≤ Y
rwa : X ≤ comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) Y)
rwa₁ : X ≤ Y ⊔ comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) ⊥
⊢ LE.le (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) X)
    (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) Y)
have rwa₂ : X ≤ Y ⊔ RingHom.ker (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
Tactic: rwa [map_le_iff_le_comap, comap_map_of_surjective (Ideal.Quotient.mk I)
      Ideal.Quotient.mk_surjective, ← RingHom.ker_eq_comap_bot, mk_ker,
      sup_eq_left.mpr <| le_of_dvd hY]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
f : RingHom.{u_1, u_2} (R ⧸ I) (A ⧸ J)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := A ⧸ J) (⇑f : (a : R ⧸ I) → A ⧸ J)
X : Ideal R
hX : X ∣ I
Y : Ideal R
hY : Y ∣ I
h : X ≤ Y
rwa : X ≤ comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) Y)
rwa₁ : X ≤ Y ⊔ comap (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) ⊥
rwa₂ : X ≤ Y ⊔ RingHom.ker (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
⊢ LE.le (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) X)
    (map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) Y)
have rwa₃ : X ≤ Y ⊔ I
Tactic: rwa [map_le_iff_le_comap, comap_map_of_surjective (Ideal.Quotient.mk I)
      Ideal.Quotient.mk_surjective, ← RingHom.ker_eq_comap_bot, mk_ker,
      sup_eq_left.mpr <| le_of_dvd hY]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
B : Type u_4
inst_3 : CommRing B
inst_4 : IsDedekindDomain B
L : Ideal B
f : RingHom.{u_1, u_2} (R ⧸ I) (A ⧸ J)
g : RingHom.{u_2, u_4} (A ⧸ J) (B ⧸ L)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := A ⧸ J) (⇑f : (a : R ⧸ I) → A ⧸ J)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := A ⧸ J) (β := B ⧸ L) (⇑g : (a : A ⧸ J) → B ⧸ L)
⊢ (idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf) = idealFactorsFunOfQuotHom (f := g.comp f) ⋯
have refine : ∀ (x : { p : Ideal R // p ∣ I }),
  Eq.{u_4 + 1} (α := { p : Ideal B // p ∣ L })
    (((idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf) :
          (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L })
        x :
      { p : Ideal B // p ∣ L })
    ((idealFactorsFunOfQuotHom (f := g.comp f) sorry : (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L }) x :
      { p : Ideal B // p ∣ L })
Tactic: refine OrderHom.ext _ _ (funext fun x => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
B : Type u_4
inst_3 : CommRing B
inst_4 : IsDedekindDomain B
L : Ideal B
f : RingHom.{u_1, u_2} (R ⧸ I) (A ⧸ J)
g : RingHom.{u_2, u_4} (A ⧸ J) (B ⧸ L)
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := A ⧸ J) (⇑f : (a : R ⧸ I) → A ⧸ J)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := A ⧸ J) (β := B ⧸ L) (⇑g : (a : A ⧸ J) → B ⧸ L)
x : { p : Ideal R // p ∣ I }
⊢ Eq.{u_4 + 1} (α := { p : Ideal B // p ∣ L })
    (((idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf) :
          (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L })
        x :
      { p : Ideal B // p ∣ L })
    ((idealFactorsFunOfQuotHom (f := g.comp f) ⋯ : (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L }) x :
      { p : Ideal B // p ∣ L })
have rw : Eq.{u_4 + 1} (α := { p : Ideal B // p ∣ L })
  (({
              toFun := fun (X : { p : Ideal A // p ∣ J }) ↦
                Subtype.mk (p := fun (p : Ideal B) ↦ p ∣ L)
                  (comap (F := B →+* B ⧸ L) (Ideal.Quotient.mk L)
                    (map (R := A ⧸ J) g (map (F := A →+* A ⧸ J) (Ideal.Quotient.mk J) (↑X : Ideal A))))
                  sorry,
              monotone' := sorry : OrderHom.{u_2, u_4} { p : Ideal A // p ∣ J } { p : Ideal B // p ∣ L } }.comp
          (idealFactorsFunOfQuotHom hf) :
        (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L })
      x :
    { p : Ideal B // p ∣ L })
  ((idealFactorsFunOfQuotHom (f := g.comp f) sorry : (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L }) x :
    { p : Ideal B // p ∣ L })
Tactic: rw [idealFactorsFunOfQuotHom, idealFactorsFunOfQuotHom, OrderHom.comp_coe, OrderHom.coe_mk,
    OrderHom.coe_mk, Function.comp_apply, idealFactorsFunOfQuotHom, OrderHom.coe_mk,
    Subtype.mk_eq_mk, Subtype.coe_mk, map_comap_of_surjective (Ideal.Quotient.mk J)
    Ideal.Quotient.mk_surjective, map_map]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
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)
⊢ OrderIso.{u_1, u_2} (↑{p : Ideal R | p ∣ I} : Type u_1) (↑{p : Ideal A | p ∣ J} : Type u_2)
have f_surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := A ⧸ J) (⇑(↑f : R ⧸ I →+* A ⧸ J) : (a : R ⧸ I) → A ⧸ J)
Tactic: have f_surj : Function.Surjective (f : R ⧸ I →+* A ⧸ J) := f.surjective
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
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)
⊢ OrderIso.{u_1, u_2} (↑{p : Ideal R | p ∣ I} : Type u_1) (↑{p : Ideal A | p ∣ J} : Type u_2)
have 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)
Tactic: have fsym_surj : Function.Surjective (f.symm : A ⧸ J →+* R ⧸ I) := f.symm.surjective
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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)
⊢ OrderIso.{u_1, u_2} (↑{p : Ideal R | p ∣ I} : Type u_1) (↑{p : Ideal A | p ∣ J} : Type u_2)
have refine_1 : (idealFactorsFunOfQuotHom f_surj).comp (idealFactorsFunOfQuotHom fsym_surj) = OrderHom.id
Tactic: refine OrderIso.ofHomInv (idealFactorsFunOfQuotHom f_surj) (idealFactorsFunOfQuotHom fsym_surj)
    ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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)
refine_1 : (idealFactorsFunOfQuotHom f_surj).comp (idealFactorsFunOfQuotHom fsym_surj) = OrderHom.id
⊢ OrderIso.{u_1, u_2} (↑{p : Ideal R | p ∣ I} : Type u_1) (↑{p : Ideal A | p ∣ J} : Type u_2)
have refine_2 : (idealFactorsFunOfQuotHom fsym_surj).comp (idealFactorsFunOfQuotHom f_surj) = OrderHom.id
Tactic: refine OrderIso.ofHomInv (idealFactorsFunOfQuotHom f_surj) (idealFactorsFunOfQuotHom fsym_surj)
    ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
this :
  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)
⊢ Dvd.dvd.{u_2} (α := Ideal A)
      (↑((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)
      (↑((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
have rw : LE.le.{u_2} (α := Ideal A)
    (↑((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)
    (↑((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) ↔
  L ∣ M
Tactic: rw [dvd_iff_le, dvd_iff_le, Subtype.coe_le_coe, this, Subtype.mk_le_mk]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
this :
  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)
rw :
  LE.le.{u_2} (α := Ideal A)
      (↑((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)
      (↑((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) ↔
    L ∣ M
⊢ Dvd.dvd.{u_2} (α := Ideal A)
      (↑((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)
      (↑((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
have rw₁ : LE.le.{u_2} (α := Ideal A)
    (↑((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)
    (↑((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) ↔
  M ≤ L
Tactic: rw [dvd_iff_le, dvd_iff_le, Subtype.coe_le_coe, this, Subtype.mk_le_mk]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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
⊢ Dvd.dvd.{u_2} (α := Ideal A)
      (↑((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)
      (↑((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
have idealFactorsEquivOfQuotEquiv : 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: 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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
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 = ⊥
⊢ False
have hL₁ : Membership.mem (γ := Multiset (Ideal R)) ∅ L
Tactic: rw [hI, bot_eq_zero, normalizedFactors_zero, ← Multiset.empty_eq_zero] at hL
Cleared hypotheses: hL, hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
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
⊢ (↑((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
have hI : 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