awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsDedekindDomain R
inst_3 : Algebra R K
hK : IsFractionRing R K
x : K
hR : ¬IsField R
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    ∀ (i : MaximalSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x

Tactic:
fun hx ⟨v, hv⟩ => hx ((equivMaximalSpectrum hR).symm ⟨v, hv⟩)

Premises used: MaximalSpectrum.asIdeal, Localization.subalgebra.ofField, MaximalSpectrum.mk, _private.0.IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot.match_1, Membership.mem, IsDedekindDomain.HeightOneSpectrum.equivMaximalSpectrum, Ideal.primeCompl_le_nonZeroDivisors, Ideal.primeCompl, Equiv.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsDedekindDomain R
inst_3 : Algebra R K
hK : IsFractionRing R K
x : K
hR : ¬IsField R
⊢ (∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    ∀ (i : MaximalSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x

Tactic:
exact fun hx ⟨v, hv⟩ => hx ((equivMaximalSpectrum hR).symm ⟨v, hv⟩)
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsDedekindDomain R
inst_3 : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    ∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x

Tactic:
fun hx ⟨v, hv, hbot⟩ => hx ⟨v, hv.isMaximal hbot⟩

Premises used: Localization.subalgebra.ofField, Ideal.IsPrime.isMaximal, MaximalSpectrum.mk, Membership.mem, IsDedekindDomain.HeightOneSpectrum.asIdeal, _private.0.IsDedekindDomain.HeightOneSpectrum.ext.match_1, Ideal.primeCompl_le_nonZeroDivisors, Ideal.primeCompl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsDedekindDomain R
inst_3 : Algebra R K
hK : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x) →
    ∀ (i : HeightOneSpectrum R),
      Membership.mem (γ := Subalgebra R K) (Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) x

Tactic:
exact fun hx ⟨v, hv, hbot⟩ => hx ⟨v, hv.isMaximal hbot⟩
-- 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 R
v : HeightOneSpectrum R
S : Type u_4
inst_4 : CommRing S
e : R ≃+* S
x : HeightOneSpectrum R
asIdeal :
  ∀ (x_1 : R),
    Membership.mem (γ := Ideal R) (HeightOneSpectrum.asIdeal (comap (↑e : R →+* S) ⋯ (comap (↑e.symm : S →+* R) ⋯ x)))
        x_1 ↔
      x_1 ∈ x.asIdeal
⊢ comap (↑e : R →+* S) ⋯ (comap (↑e.symm : S →+* R) ⋯ x) = x

Tactic:
ext
-- 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 R
v : HeightOneSpectrum R
S : Type u_4
inst_4 : CommRing S
e : R ≃+* S
x : HeightOneSpectrum R
x_1 : R
⊢ Membership.mem (γ := Ideal R) (asIdeal (comap (↑e : R →+* S) ⋯ (comap (↑e.symm : S →+* R) ⋯ x))) x_1 ↔ x_1 ∈ x.asIdeal

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 R
v : HeightOneSpectrum R
S : Type u_4
inst_4 : CommRing S
e : R ≃+* S
x : HeightOneSpectrum S
asIdeal :
  ∀ (x_1 : S),
    Membership.mem (γ := Ideal S) (HeightOneSpectrum.asIdeal (comap (↑e.symm : S →+* R) ⋯ (comap (↑e : R →+* S) ⋯ x)))
        x_1 ↔
      x_1 ∈ x.asIdeal
⊢ comap (↑e.symm : S →+* R) ⋯ (comap (↑e : R →+* S) ⋯ x) = x

Tactic:
ext
-- 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 R
v : HeightOneSpectrum R
S : Type u_4
inst_4 : CommRing S
e : R ≃+* S
x : HeightOneSpectrum S
x_1 : S
asIdeal :
  Membership.mem (γ := Ideal S) (HeightOneSpectrum.asIdeal (comap (↑e.symm : S →+* R) ⋯ (comap (↑e : R →+* S) ⋯ x)))
      x_1 ↔
    Membership.mem (γ := Ideal S) (Ideal.map e (Ideal.comap e x.asIdeal)) x_1
⊢ Membership.mem (γ := Ideal S) (HeightOneSpectrum.asIdeal (comap (↑e.symm : S →+* R) ⋯ (comap (↑e : R →+* S) ⋯ x)))
      x_1 ↔
    x_1 ∈ x.asIdeal

Tactic:
rw [← Ideal.map_comap_eq_self_of_equiv e x.asIdeal]

Premises used: IsDedekindDomain.HeightOneSpectrum.asIdeal, Ideal.map_comap_eq_self_of_equiv
-- 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 R
v : HeightOneSpectrum R
S : Type u_4
inst_4 : CommRing S
e : R ≃+* S
x : HeightOneSpectrum S
x_1 : S
asIdeal :
  Membership.mem (γ := Ideal S) (Ideal.map e (Ideal.comap (F := R →+* S) (↑e : R →+* S) x.asIdeal)) x_1 ↔
    Membership.mem (γ := Ideal S) (Ideal.map e (Ideal.comap e x.asIdeal)) x_1
⊢ Membership.mem (γ := Ideal S) (HeightOneSpectrum.asIdeal (comap (↑e.symm : S →+* R) ⋯ (comap (↑e : R →+* S) ⋯ x)))
      x_1 ↔
    Membership.mem (γ := Ideal S) (Ideal.map e (Ideal.comap e x.asIdeal)) x_1

Tactic:
simp only [comap_asIdeal, Ideal.mem_comap, RingHom.coe_coe, Ideal.symm_apply_mem_of_equiv_iff]

Premises used: RingHom.coe_coe, Ideal.symm_apply_mem_of_equiv_iff, Ideal.mem_comap, IsDedekindDomain.HeightOneSpectrum.comap_asIdeal
-- 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 R
v : HeightOneSpectrum R
S : Type u_4
inst_4 : CommRing S
e : R ≃+* S
x : HeightOneSpectrum S
x_1 : S
⊢ Membership.mem (γ := Ideal S) (Ideal.map e (Ideal.comap (F := R →+* S) (↑e : R →+* S) x.asIdeal)) x_1 ↔
    Membership.mem (γ := Ideal S) (Ideal.map e (Ideal.comap e x.asIdeal)) x_1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- 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 R
v : HeightOneSpectrum R
S : Type u_4
inst_4 : CommRing S
e : R ≃+* S
x : HeightOneSpectrum S
x_1 : S
⊢ Membership.mem (γ := Ideal S) (Ideal.map e (Ideal.comap (F := R →+* S) (↑e : R →+* S) x.asIdeal)) x_1 ↔
    Membership.mem (γ := Ideal S) (Ideal.map e (Ideal.comap e x.asIdeal)) x_1

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
R : Type u_5
S : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : Nontrivial.{u_6} (HeightOneSpectrum S)
e : R ≃+* S
⊢ Nontrivial.{u_5} (HeightOneSpectrum R)

Tactic:
(equivOfRingEquiv e).surjective.nontrivial

Premises used: IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv, Function.Surjective.nontrivial, Equiv.surjective
-- 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
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 : { p : Ideal R // p ∣ I }
⊢ LE.le (α := Ideal A) (RingHom.ker (F := A →+* A ⧸ J) (Ideal.Quotient.mk 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))))

Tactic:
have : RingHom.ker (Ideal.Quotient.mk J) ≤
        comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) X)) :=
      ker_le_comap (Ideal.Quotient.mk J)
-- 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
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 : { p : Ideal R // p ∣ I }
this :
  LE.le (α := Ideal A) (RingHom.ker (F := A →+* A ⧸ J) (Ideal.Quotient.mk 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))))
⊢ 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)))

Tactic:
rw [mk_ker] at this

Premises used: Ideal.mk_ker
-- 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
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 : { p : Ideal R // p ∣ I }
this :
  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)))
⊢ 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))) ∣
    J

Tactic:
dvd_iff_le.mpr this

Premises used: Iff.mpr, Ideal.dvd_iff_le
-- 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
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 : { p : Ideal R // p ∣ I }
this :
  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)))
⊢ 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))) ∣
    J

Tactic:
exact dvd_iff_le.mpr this

Premises used: Iff.mpr, Ideal.dvd_iff_le
-- 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
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)
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))))
                  ⋯ :
                { p : Ideal A // p ∣ J }))
            (Subtype.mk (p := fun (p : Ideal R) ↦ p ∣ I) Y hY)) :
        Ideal A)
⊢ 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))

Tactic:
rw [← Subtype.coe_le_coe, Subtype.coe_mk, Subtype.coe_mk] at h ⊢

Premises used: Subtype.coe_mk, Subtype.coe_le_coe
-- 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
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
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 ⊥)
⊢ 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)

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

Premises used: Subtype.coe_mk, Ideal.Quotient.mk, Ideal.map, Ideal.comap_le_comap_iff_of_surjective, Ideal.Quotient.mk_surjective, Ideal.map_le_iff_le_comap, Ideal.comap_map_of_surjective
-- 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
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
this :
  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)
⊢ 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:
le_sup_of_le_left this

Premises used: Set.Mem, le_sup_of_le_left
-- 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
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
this :
  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)
⊢ 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:
exact le_sup_of_le_left this

Premises used: le_sup_of_le_left
-- 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
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
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)
⊢ 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:
suffices map (Ideal.Quotient.mk I) X ≤ map (Ideal.Quotient.mk I) Y by
      exact le_sup_of_le_left this
-- 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
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)
rwa₃ : X ≤ Y ⊔ I
rwa₄ rwa₅ rwa₆ rwa₇ : 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)

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]

Premises used: Iff.mpr, Ideal.Quotient.mk, Ideal.le_of_dvd, sup_eq_left, Ideal.Quotient.mk_surjective, Ideal.map_le_iff_le_comap, Ideal.comap_map_of_surjective, RingHom.ker_eq_comap_bot, Ideal.mk_ker
-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Goal:
A : Type u_2
inst : CommRing A
inst_1 : IsDedekindDomain A
J : Ideal A
X : { p : Ideal A // p ∣ J }
⊢ Eq (α := { p : Ideal A // p ∣ J })
    ((idealFactorsFunOfQuotHom (f := RingHom.id (A ⧸ J)) ⋯ : (a : { p : Ideal A // p ∣ J }) → { p : Ideal A // p ∣ J })
        X :
      { p : Ideal A // p ∣ J })
    ((OrderHom.id : (a : { p : Ideal A // p ∣ J }) → { p : Ideal A // p ∣ J }) X : { p : Ideal A // p ∣ J })

Tactic:
simp only [idealFactorsFunOfQuotHom, map_id, OrderHom.coe_mk, OrderHom.id_coe, id,
        comap_map_of_surjective (Ideal.Quotient.mk J) Ideal.Quotient.mk_surjective, ←
        RingHom.ker_eq_comap_bot (Ideal.Quotient.mk J), mk_ker,
        sup_eq_left.mpr (dvd_iff_le.mp X.prop), Subtype.coe_eta]

Premises used: Iff.mpr, Ideal.dvd_iff_le, OrderHom.id_coe, Ideal.Quotient.mk, Ideal.map_id, IsDedekindDomain.idealFactorsFunOfQuotHom, id, sup_eq_left, OrderHom.coe_mk, Ideal.Quotient.mk_surjective, Ideal.comap_map_of_surjective, RingHom.ker_eq_comap_bot, Subtype.coe_eta, Subtype.prop, Iff.mp, Ideal.mk_ker
-- 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
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) ⋯

Tactic:
OrderHom.ext _ _ (funext fun x => ?_)

Premises used: funext, OrderHom.ext
-- 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
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)
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) ⋯ : (a : { p : Ideal R // p ∣ I }) → { p : Ideal B // p ∣ L }) x :
        { p : Ideal B // p ∣ L })
⊢ (idealFactorsFunOfQuotHom hg).comp (idealFactorsFunOfQuotHom hf) = idealFactorsFunOfQuotHom (f := g.comp f) ⋯

Tactic:
refine OrderHom.ext _ _ (funext fun x => ?_)

Premises used: funext, OrderHom.ext
-- 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)
⊢ 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
-- 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)
⊢ 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
-- 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)
refine_1 : (idealFactorsFunOfQuotHom f_surj).comp (idealFactorsFunOfQuotHom fsym_surj) = OrderHom.id
refine_2 : (idealFactorsFunOfQuotHom fsym_surj).comp (idealFactorsFunOfQuotHom f_surj) = OrderHom.id
⊢ OrderIso.{u_1, u_2} (↑{p : Ideal R | p ∣ I} : Type u_1) (↑{p : Ideal A | p ∣ J} : Type u_2)

Tactic:
refine OrderIso.ofHomInv (idealFactorsFunOfQuotHom f_surj) (idealFactorsFunOfQuotHom fsym_surj)
    ?_ ?_

Premises used: IsDedekindDomain.idealFactorsFunOfQuotHom, OrderIso.ofHomInv
-- 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 f_surj).comp (idealFactorsFunOfQuotHom fsym_surj) = OrderHom.id

Tactic:
simpa using idealFactorsFunOfQuotHom_comp fsym_surj f_surj

Premises used: IsDedekindDomain.idealFactorsFunOfQuotHom_comp