How can I finish this instance of `PartialOrder`?

Stream: general

[Santiago Mourenza Rivero]

In order to prove that Zorn's Lemma implies the Well-Ordering Principle, I need to demonstrate that a set F is inductive. To do this, I have to define a WellOrderedSet structure and F as a set of this type. Now, in order to find an upper bound, I have to order the elements of F, and for this, I must create an instance of PartialOrder, but I am unable to complete the proof. I will leave here what I have so far:

import Mathlib.Tactic
import Mathlib.Init.Order.Defs

variable (α : Type _) [PartialOrder α]
variable (γ : Type _)

variable {β I : Type _}
variable (X : I → Set γ)
variable (S : Set γ )

open Set
open Classical


def is_chain [PartialOrder γ] (c : Set γ) : Prop := ∀ (x y : γ), x ∈ c → y ∈ c → x ≤ y ∨ y ≤ x

def is_well_ordered (R : γ  → γ → Prop) : Prop := ∀ (A : Set γ), Nonempty A → ∃ n ∈ A, ∀ m ∈ A, R n m
def well_ordered_principle : Prop := ∃ (R : γ  → γ → Prop), is_well_ordered γ R

variable {γ}

def axiom_of_choice : Prop := (∀ (i : I), Nonempty (X i)) → ∃ (f : (I → ⋃ i, X i)), ∀ (i : I), (f i).1 ∈ X i

--def inductive_set (S : Set α) : Prop := ∀ (c : Set α), c ⊆ S → (∀ (x y : α), x ∈ c → y ∈ c → x ≤ y ∨ y ≤ x) → ∃ (ub : α), ∀ (x : α), x ∈ c → x ≤ ub
def inductive_set [PartialOrder γ] (S : Set γ) : Prop := ∀ (c : Set γ), c ⊆ S → is_chain γ c → ∃ (ub : γ), ∀ (x : γ ), x ∈ c → x ≤ ub
def zorn [PartialOrder γ] (_ : inductive_set S ) : Prop := ∃ (m : γ), m ∈ S ∧ ∀ (x : γ), x ∈ S → x < m

structure WellOrderedSet (γ : Type _) :=
  (s : Set γ)
  (r : s → s → Prop)
  (h_well : is_well_ordered s r)

variable (F : Set (WellOrderedSet γ))

instance : PartialOrder (WellOrderedSet γ) where
  le := fun x y => x.s ⊆ y.s ∧ ∀ (a b), (ha : a ∈ x.s) → (ha' : a ∈ y.s) → (hb : b ∈ x.s) → (hb' : b ∈ y.s) → x.r ⟨a,ha⟩ ⟨b,hb⟩ → y.r ⟨a,ha'⟩ ⟨b,hb'⟩
  lt := fun x y => x.s ⊂ y.s ∧ (∀ (a b), (ha : a ∈ x.s) → (ha' : a ∈ y.s) → (hb : b ∈ x.s) → (hb' : b ∈ y.s) → x.r ⟨a,ha⟩ ⟨b,hb⟩ → y.r ⟨a,ha'⟩ ⟨b,hb'⟩)
  le_refl := by
    intro x
    simp only [imp_self, implies_true]
    apply And.intro
    . apply Set.Subset.refl
    trivial

  le_trans := by
    intro x y z hxy hyz
    dsimp at *
    apply And.intro
    . apply Set.Subset.trans (And.left hxy) (And.left hyz)
    intro a b ha ha' hb hb' hxr
    apply And.right hyz a b (And.left hxy ha) ha' (And.left hxy hb) hb'
    exact And.right hxy a b ha (And.left hxy ha) hb (And.left hxy hb) hxr

  lt_iff_le_not_le := by
    intro x y
    apply Iff.intro
    . intro h
      apply And.intro
      . apply And.intro
        . simp at h
          exact And.left h.1
        intro a b ha ha' hb hb' hxr
        simp at h
        exact And.right h a b ha (And.left h.1 ha) hb (And.left h.1 hb) hxr
      intro h_le_yx
      have not_h_s := And.right (And.left h)
      have h_s := And.left h_le_yx
      contradiction
    intro h
    apply And.intro
    . have le_xy := h.1.1
      have lt_xy := h.2
      dsimp at lt_xy
      rw[not_and_or] at lt_xy
      apply HasSubset.Subset.ssubset_of_not_subset
      apply le_xy
      apply Or.elim lt_xy
      . intro this
        exact this
      sorry
    exact h.1.2

  le_antisymm := by
    intro x y le_xy le_yx
    have s_eq : x.s = y.s := Set.Subset.antisymm le_xy.1 le_yx.1
    have r_eq : ∀ a b, a ∈ x.s → b ∈ x.s → (x.r a b ↔ y.r a b) := by
      intro a b ha hb
      apply Iff.intro
      . intro h
        exact le_xy.2 a b ha hb h
      exact le_yx.2 a b (le_xy.1 ha) (le_xy.1 hb)

    rcases x with ⟨x.s,x.r⟩
    rcases y with ⟨y.s,y.r⟩
    simp at *
    congr
    apply And.intro
    exact s_eq
    sorry

If I manage to make progress in any aspect, I will update the information accordingly.