How to use Equiv.Set.univ

Stream: general

[Santiago Mourenza Rivero]

I'm trying to finish a result where I need to use that the set m.s = univ, the problem is that the types don't unify as I expected and I wanted to use this equivalence but I am not sure how to do it. The last line (where I comment what I am looking for) is where I'm working:

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

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

@[ext]structure WellOrderedSet (γ : Type _) :=
(s : Set γ)
(r : γ  → γ  → Prop)
(h_well : is_well_ordered s (fun x y => r x.val y.val))
(h_triv : ∀ (x y : γ) (_ : x ∉ s ∨ y ∉ s), ¬ r x y)

variable (F : Set (WellOrderedSet γ))

instance : PartialOrder (WellOrderedSet γ) where
  le := sorry
  lt := sorry
  le_refl := sorry
  le_trans := sorry
  lt_iff_le_not_le := sorry
  le_antisymm := sorry

lemma F_is_inductive : inductive_set F := by sorry

theorem zorn_implies_wop : zorn F (F_is_inductive F) → well_ordered_principle γ := by
  intro hZ
  rw[zorn] at hZ
  rw[well_ordered_principle]
  obtain ⟨m, hm⟩ := hZ
  have : m.s = Set.univ := sorry
  use m.r
  have h3 := m.3
  --Here is where I need to use Equiv.Set.univ and using h3 I can finish the result
  sorry