How do I get a `cᵢ` according to prove the following goal

Stream: general

[Santiago Mourenza Rivero]

I have been doing this proof and I got stucked in this last step and I don't know how to go on:

γ : Type u_1
I : Type ?u.47344
X : I → Set γ
S : Set γ
F c : Set (WellOrderedSet γ)
h1 : c ⊆ F
h2 : is_chain (WellOrderedSet γ) c
A : Set γ := ⋃ x ∈ c, x.s
R : γ → γ → Prop := fun a b => ∃ cᵢ ∈ c, WellOrderedSet.r cᵢ a b
hR : R = fun a b => ∃ cᵢ ∈ c, WellOrderedSet.r cᵢ a b
Aᵢ : Set ↑A
n : ↑A
hn : n ∈ Aᵢ
m : ↑A
hm : m ∈ Aᵢ
⊢ ∃ cᵢ ∈ c, WellOrderedSet.r cᵢ ↑n ↑m

[Ruben Van de Velde]

One, it's easier for us to help if you share a #mwe

Two, are you asking what the value is mathematically, or do you know already and do you need the syntax to make progress on a lean \exists goal?

[Santiago Mourenza Rivero]

it's a little long but here it is:

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

--variable (α : Type _) [PartialOrder α] --Porque con esto necesito poner el argumento explícito?
variable (γ : Type _)

--Para la familia de conjuntos de los Xᵢ con i ∈ I
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

--(X;R) es un buen orden si ∀ S ∈ X no vacío tiene un mínimo
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 [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)


#check WellOrderedSet.ext

variable (F : Set (WellOrderedSet γ))

instance : PartialOrder (WellOrderedSet γ) where
  le := fun x y => x.s ⊆ y.s ∧ ∀ (a b), x.r a b → y.r a b
  lt := fun x y => x.s ⊂ y.s ∧ ∀ (a b), x.r a b → y.r a b
  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 only
    apply And.intro
    . apply Set.Subset.trans (And.left hxy) (And.left hyz)
    intro a b hxr
    apply And.right hyz a b
    apply And.right hxy a b
    exact 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 hxr
        simp at h
        apply And.right h a b
        exact 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
    . rw[ssubset_def]
      apply And.intro
      . exact h.1.1
      rw[not_subset]
      simp only [not_and, not_forall, exists_prop] at h
      by_contra not_a
      simp only [not_exists, not_and, not_not] at not_a
      have ss : y.s ⊆ x.s := by
        intro a ha
        apply not_a
        apply ha
      obtain ⟨x1, x2, hy, hx⟩ := h.2 ss
      --Esta prueba tiene el problem de que no encuentro la contradicción, preguntar
      --para ver dónde puede estar el fallo
      sorry

      /-have le_xy := h.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.1
      apply Or.elim lt_xy
      . intro this
        exact this
      intro h1
      rw[not_subset]
      refine exists_of_ssubset ?mpr.left.h₂.right.intro.h
      refine ssubset_iff_subset_ne.mpr ?mpr.left.h₂.right.intro.h.a
      apply And.intro
      . exact le_xy.1
      simp only [not_forall, exists_prop] at lt_xy
      simp only [not_forall, exists_prop] at h1
      intro heq
      have hsxy := le_xy.1
      have hsyx : y.s ⊆ x.s := by
        rw[heq]-/
    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, (x.r a b ↔ y.r a b) := by
      intro a b
      apply Iff.intro
      . intro h
        exact le_xy.2 a b h
      intro h
      exact le_yx.2 a b h
    rcases x with ⟨x.s,x.r,x.hwell,x.htriv⟩
    rcases y with ⟨y.s,y.r,y.hwell,y.htriv⟩
    simp only [WellOrderedSet.mk.injEq]
    apply And.intro
    . exact s_eq
    ext a b
    apply r_eq

lemma F_is_inductive : inductive_set F := by
  intro c h1 h2
  let A := ⋃ x ∈ c, x.s
  set R := fun a b => ∃ cᵢ, cᵢ ∈ c ∧ cᵢ.r a b with hR

  let ub : WellOrderedSet γ :={
    s:=A
    r:=R
    h_well:=by
      rw[is_well_ordered]
      intro Aᵢ hAᵢ_ne
      obtain ⟨n,hn⟩ := hAᵢ_ne
      use n
      apply And.intro
      . apply hn
      intro m hm
      rw[hR]
      dsimp only

      sorry
    h_triv := by
      intro a1 a2 h
      simp only [not_exists, not_and]
      intro cᵢ hcᵢ
      have h_triv := cᵢ.h_triv
      apply h_triv
      rw[mem_iUnion,mem_iUnion] at h
      simp only [mem_iUnion, exists_prop, not_exists, not_and] at h
      rcases h with hleft | hright
      . apply Or.intro_left
        apply hleft
        exact hcᵢ
      apply Or.intro_right
      apply hright
      exact hcᵢ
  }
  use ub
  intro y hy
  apply And.intro
  . simp only
    exact subset_biUnion_of_mem hy
  intro a b hyr
  simp only
  use y

[Ruben Van de Velde]

I'm afraid that looks like an example, but not minimal or working

[Santiago Mourenza Rivero]

What exactly I am supposed to send?

[Edward van de Meent]

You could start by replacing irrelevant proofs with sorry, as well as using the extract_goal tactic to summarise the goal you need help with to a single lemma with the goal you need. Then, see if you can remove irrelevant assumptions from the extracted goal, maybe even untill it is merely a question of given statements of shape X, how do i use those to change the goal/context from Y to Z

[Edward van de Meent]

Also, I believe that a key part of the assumption of zorns lemma is that the upper bound of the chain is in the set under consideration, i.e. you're missing the ub \in S part of inductive_set

[Santiago Mourenza Rivero]

okay, thank you for helping me