case mk
P : Type u_1
inst✝ : LE P
I J s t✝ : Ideal P
x y : P
t : Ideal P
toLowerSet✝ : LowerSet P
nonempty'✝ : Set.Nonempty toLowerSet✝.carrier
directed'✝ : DirectedOn (fun x x_1 => x ≤ x_1) toLowerSet✝.carrier
x✝ : { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet = t.toLowerSet
⊢ { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ } = t
P : Type u_1
inst✝ : LE P
I J s✝ t✝ : Ideal P
x y : P
s t : Ideal P
x✝ : s.toLowerSet = t.toLowerSet
⊢ s = t
cases s
case mk.mk
P : Type u_1
inst✝ : LE P
I J s t : Ideal P
x y : P
toLowerSet✝¹ : LowerSet P
nonempty'✝¹ : Set.Nonempty toLowerSet✝¹.carrier
directed'✝¹ : DirectedOn (fun x x_1 => x ≤ x_1) toLowerSet✝¹.carrier
toLowerSet✝ : LowerSet P
nonempty'✝ : Set.Nonempty toLowerSet✝.carrier
directed'✝ : DirectedOn (fun x x_1 => x ≤ x_1) toLowerSet✝.carrier
x✝ :
  { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ }.toLowerSet =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet
⊢ { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ } =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }
case mk
P : Type u_1
inst✝ : LE P
I J s t✝ : Ideal P
x y : P
t : Ideal P
toLowerSet✝ : LowerSet P
nonempty'✝ : Set.Nonempty toLowerSet✝.carrier
directed'✝ : DirectedOn (fun x x_1 => x ≤ x_1) toLowerSet✝.carrier
x✝ : { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet = t.toLowerSet
⊢ { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ } = t
cases t
no goals
case mk.mk
P : Type u_1
inst✝ : LE P
I J s t : Ideal P
x y : P
toLowerSet✝¹ : LowerSet P
nonempty'✝¹ : Set.Nonempty toLowerSet✝¹.carrier
directed'✝¹ : DirectedOn (fun x x_1 => x ≤ x_1) toLowerSet✝¹.carrier
toLowerSet✝ : LowerSet P
nonempty'✝ : Set.Nonempty toLowerSet✝.carrier
directed'✝ : DirectedOn (fun x x_1 => x ≤ x_1) toLowerSet✝.carrier
x✝ :
  { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ }.toLowerSet =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet
⊢ { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ } =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }
congr