-- Mathlib/RingTheory/UniqueFactorizationDomain/Ideal.lean
/-- The ascending chain condition on principal ideals holds in a `WfDvdMonoid` domain. -/
lemma Ideal.setOf_isPrincipal_wellFoundedOn_gt [CommSemiring α] [WfDvdMonoid α] [IsDomain α] :
    {I : Ideal α | I.IsPrincipal}.WellFoundedOn (· > ·)

Proof state:
case h
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
x✝ : Ideal α
⊢ x✝ ∈ {I | Submodule.IsPrincipal I} ↔ x✝ ∈ (fun a => span {a}) '' Set.univ

Tactic:
simp [Submodule.isPrincipal_iff, eq_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a => span {a}) '' Set.univ
⊢ WellFounded (Function.onFun (fun x1 x2 => x1 > x2) fun a => span {a})

Tactic:
convert wellFounded_dvdNotUnit (α := α)

Result:
case h.e'_2
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a => span {a}) '' Set.univ
⊢ (Function.onFun (fun x1 x2 => x1 > x2) fun a => span {a}) = DvdNotUnit

Proof state:
case h.e'_2
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a => span {a}) '' Set.univ
⊢ (Function.onFun (fun x1 x2 => x1 > x2) fun a => span {a}) = DvdNotUnit

Tactic:
ext

Result:
case h.e'_2.h.h.a
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a => span {a}) '' Set.univ
x✝¹ x✝ : α
⊢ Function.onFun (fun x1 x2 => x1 > x2) (fun a => span {a}) x✝¹ x✝ ↔ DvdNotUnit x✝¹ x✝

Proof state:
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
⊢ {I | Submodule.IsPrincipal I} = (fun a => span {a}) '' Set.univ

Tactic:
ext

Result:
case h
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
x✝ : Ideal α
⊢ x✝ ∈ {I | Submodule.IsPrincipal I} ↔ x✝ ∈ (fun a => span {a}) '' Set.univ

Proof state:
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a => span {a}) '' Set.univ
⊢ {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2

Tactic:
rw [this, Set.wellFoundedOn_image, Set.wellFoundedOn_univ]

Result:
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a => span {a}) '' Set.univ
⊢ WellFounded (Function.onFun (fun x1 x2 => x1 > x2) fun a => span {a})

Proof state:
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
⊢ {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2

Tactic:
have : {I : Ideal α | I.IsPrincipal} = ((fun a ↦ Ideal.span {a}) '' Set.univ) := by
  ext
  simp [Submodule.isPrincipal_iff, eq_comm]

Result:
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a => span {a}) '' Set.univ
⊢ {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2

Proof state:
case h.e'_2.h.h.a
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a => span {a}) '' Set.univ
x✝¹ x✝ : α
⊢ Function.onFun (fun x1 x2 => x1 > x2) (fun a => span {a}) x✝¹ x✝ ↔ DvdNotUnit x✝¹ x✝

Tactic:
exact Ideal.span_singleton_lt_span_singleton

Result:
no goals