α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
⊢ ∃ S, Unbounded r S ∧ type (Subrel r S) = ord (cof (type r))
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ ∃ S, Unbounded r S ∧ type (Subrel r S) = ord (cof (type r))
let ⟨S, hS, e⟩ := cof_eq r
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
⊢ ∃ S, Unbounded r S ∧ type (Subrel r S) = ord (cof (type r))
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
⊢ ∃ S, Unbounded r S ∧ type (Subrel r S) = ord (cof (type r))
let ⟨s, _, e'⟩ := Cardinal.ord_eq S
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
⊢ ∃ S, Unbounded r S ∧ type (Subrel r S) = ord (cof (type r))
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
⊢ ∃ S, Unbounded r S ∧ type (Subrel r S) = ord (cof (type r))
let T : Set α := { a | ∃ aS : a ∈ S, ∀ b : S, s b ⟨_, aS⟩ → r b a }
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
⊢ ∃ S, Unbounded r S ∧ type (Subrel r S) = ord (cof (type r))

case this
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
⊢ Unbounded r T
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
⊢ ∃ S, Unbounded r S ∧ type (Subrel r S) = ord (cof (type r))
suffices : Unbounded r T
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
⊢ type (Subrel r T) ≤ ord (cof (type r))
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
⊢ ∃ S, Unbounded r S ∧ type (Subrel r S) = ord (cof (type r))
refine' ⟨T, this, le_antisymm _ (Cardinal.ord_le.2 <| cof_type_le this)⟩
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
⊢ type (Subrel r T) ≤ type s
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
⊢ type (Subrel r T) ≤ ord (cof (type r))
rw [← e, e']
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a b : ↑T
h : Subrel r T a b
⊢ s ((fun a => { val := ↑a, property := (_ : ↑a ∈ S) }) a) ((fun a => { val := ↑a, property := (_ : ↑a ∈ S) }) b)
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
⊢ type (Subrel r T) ≤ type s
refine'
  (RelEmbedding.ofMonotone
      (fun a : T =>
        (⟨a,
            let ⟨aS, _⟩ := a.2
            aS⟩ :
          S))
      fun a b h => _).ordinal_type_le
case mk.intro
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
b : ↑T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
h : Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) } b
⊢ s
    ((fun a => { val := ↑a, property := (_ : ↑a ∈ S) })
      { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) })
    ((fun a => { val := ↑a, property := (_ : ↑a ∈ S) }) b)
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a b : ↑T
h : Subrel r T a b
⊢ s ((fun a => { val := ↑a, property := (_ : ↑a ∈ S) }) a) ((fun a => { val := ↑a, property := (_ : ↑a ∈ S) }) b)
rcases a with ⟨a, aS, ha⟩
case mk.intro.mk.intro
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 { val := b, property := bS } → r (↑b_1) b
h :
  Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
    { val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) }
⊢ s
    ((fun a => { val := ↑a, property := (_ : ↑a ∈ S) })
      { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) })
    ((fun a => { val := ↑a, property := (_ : ↑a ∈ S) })
      { val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) })
case mk.intro
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
b : ↑T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
h : Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) } b
⊢ s
    ((fun a => { val := ↑a, property := (_ : ↑a ∈ S) })
      { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) })
    ((fun a => { val := ↑a, property := (_ : ↑a ∈ S) }) b)
rcases b with ⟨b, bS, hb⟩
case mk.intro.mk.intro
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 { val := b, property := bS } → r (↑b_1) b
h :
  Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
    { val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) }
⊢ s
    { val := a,
      property :=
        (_ : ↑{ val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) } ∈ S) }
    { val := b,
      property :=
        (_ : ↑{ val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) } ∈ S) }
case mk.intro.mk.intro
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 { val := b, property := bS } → r (↑b_1) b
h :
  Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
    { val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) }
⊢ s
    ((fun a => { val := ↑a, property := (_ : ↑a ∈ S) })
      { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) })
    ((fun a => { val := ↑a, property := (_ : ↑a ∈ S) })
      { val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) })
change s ⟨a, _⟩ ⟨b, _⟩
case mk.intro.mk.intro.refine'_1
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 { val := b, property := bS } → r (↑b_1) b
h :
  Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
    { val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) }
hn :
  s
    { val := b,
      property :=
        (_ : ↑{ val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) } ∈ S) }
    { val := a,
      property :=
        (_ : ↑{ val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) } ∈ S) }
⊢ False

case mk.intro.mk.intro.refine'_2
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 { val := b, property := bS } → r (↑b_1) b
h :
  Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
    { val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) }
⊢ ¬{ val := b,
        property :=
          (_ :
            ↑{ val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) } ∈
              S) } =
      { val := a,
        property :=
          (_ : ↑{ val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) } ∈ S) }
case mk.intro.mk.intro
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 { val := b, property := bS } → r (↑b_1) b
h :
  Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
    { val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) }
⊢ s
    { val := a,
      property :=
        (_ : ↑{ val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) } ∈ S) }
    { val := b,
      property :=
        (_ : ↑{ val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) } ∈ S) }
refine' ((trichotomous_of s _ _).resolve_left fun hn => _).resolve_left _
no goals
case mk.intro.mk.intro.refine'_1
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 { val := b, property := bS } → r (↑b_1) b
h :
  Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
    { val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) }
hn :
  s
    { val := b,
      property :=
        (_ : ↑{ val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) } ∈ S) }
    { val := a,
      property :=
        (_ : ↑{ val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) } ∈ S) }
⊢ False
exact asymm h (ha _ hn)
case mk.intro.mk.intro.refine'_2
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e✝ : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 { val := b, property := bS } → r (↑b_1) b
h :
  Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
    { val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) }
e :
  { val := b,
      property :=
        (_ :
          ↑{ val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) } ∈ S) } =
    { val := a,
      property :=
        (_ : ↑{ val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) } ∈ S) }
⊢ False
case mk.intro.mk.intro.refine'_2
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 { val := b, property := bS } → r (↑b_1) b
h :
  Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
    { val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) }
⊢ ¬{ val := b,
        property :=
          (_ :
            ↑{ val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) } ∈
              S) } =
      { val := a,
        property :=
          (_ : ↑{ val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) } ∈ S) }
intro e
case mk.intro.mk.intro.refine'_2
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e✝ : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 { val := b, property := bS } → r (↑b_1) b
h :
  Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
    { val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) }
e : b = a
⊢ False
case mk.intro.mk.intro.refine'_2
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e✝ : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 { val := b, property := bS } → r (↑b_1) b
h :
  Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
    { val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) }
e :
  { val := b,
      property :=
        (_ :
          ↑{ val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) } ∈ S) } =
    { val := a,
      property :=
        (_ : ↑{ val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) } ∈ S) }
⊢ False
injection e with e
case mk.intro.mk.intro.refine'_2
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
bS : a ∈ S
hb : ∀ (b : ↑S), s b { val := a, property := bS } → r (↑b) a
h :
  Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
    { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
⊢ False
case mk.intro.mk.intro.refine'_2
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e✝ : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
b : α
bS : b ∈ S
hb : ∀ (b_1 : ↑S), s b_1 { val := b, property := bS } → r (↑b_1) b
h :
  Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
    { val := b, property := (_ : ∃ aS, ∀ (b_1 : ↑S), s b_1 { val := b, property := aS } → r (↑b_1) b) }
e : b = a
⊢ False
subst b
no goals
case mk.intro.mk.intro.refine'_2
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
this : Unbounded r T
a : α
aS : a ∈ S
ha : ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a
bS : a ∈ S
hb : ∀ (b : ↑S), s b { val := a, property := bS } → r (↑b) a
h :
  Subrel r T { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
    { val := a, property := (_ : ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a) }
⊢ False
exact irrefl _ h
case this
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
⊢ ∃ b, b ∈ T ∧ ¬r b a
case this
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
⊢ Unbounded r T
intro a
case this
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
⊢ ∃ b, b ∈ T ∧ ¬r b a
case this
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
⊢ ∃ b, b ∈ T ∧ ¬r b a
have : { b : S | ¬r b a }.Nonempty :=
  let ⟨b, bS, ba⟩ := hS a
  ⟨⟨b, bS⟩, ba⟩
case this
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
b : ↑S := WellFounded.min (_ : WellFounded s) {b | ¬r (↑b) a} this
⊢ ∃ b, b ∈ T ∧ ¬r b a
case this
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
⊢ ∃ b, b ∈ T ∧ ¬r b a
let b := (IsWellFounded.wf : WellFounded s).min _ this
case this
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
b : ↑S := WellFounded.min (_ : WellFounded s) {b | ¬r (↑b) a} this
ba : ¬r (↑b) a
⊢ ∃ b, b ∈ T ∧ ¬r b a
case this
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
b : ↑S := WellFounded.min (_ : WellFounded s) {b | ¬r (↑b) a} this
⊢ ∃ b, b ∈ T ∧ ¬r b a
have ba : ¬r b a := IsWellFounded.wf.min_mem _ this
case this
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
b : ↑S := WellFounded.min (_ : WellFounded s) {b | ¬r (↑b) a} this
ba : ¬r (↑b) a
c : ↑S
h : ¬r ↑c ↑b
⊢ ¬s c { val := ↑b, property := (_ : ↑b ∈ S) }
case this
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
b : ↑S := WellFounded.min (_ : WellFounded s) {b | ¬r (↑b) a} this
ba : ¬r (↑b) a
⊢ ∃ b, b ∈ T ∧ ¬r b a
refine' ⟨b, ⟨b.2, fun c => not_imp_not.1 fun h => _⟩, ba⟩
case this
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
b : ↑S := WellFounded.min (_ : WellFounded s) {b | ¬r (↑b) a} this
ba : ¬r (↑b) a
c : ↑S
h : ¬r ↑c ↑b
⊢ ¬s c b
case this
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
b : ↑S := WellFounded.min (_ : WellFounded s) {b | ¬r (↑b) a} this
ba : ¬r (↑b) a
c : ↑S
h : ¬r ↑c ↑b
⊢ ¬s c { val := ↑b, property := (_ : ↑b ∈ S) }
rw [show ∀ b : S, (⟨b, b.2⟩ : S) = b by intro b; cases b; rfl]
no goals
case this
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
b : ↑S := WellFounded.min (_ : WellFounded s) {b | ¬r (↑b) a} this
ba : ¬r (↑b) a
c : ↑S
h : ¬r ↑c ↑b
⊢ ¬s c b
exact IsWellFounded.wf.not_lt_min _ this (IsOrderConnected.neg_trans h ba)
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
b✝ : ↑S := WellFounded.min (_ : WellFounded s) {b | ¬r (↑b) a} this
ba : ¬r (↑b✝) a
c : ↑S
h : ¬r ↑c ↑b✝
b : ↑S
⊢ { val := ↑b, property := (_ : ↑b ∈ S) } = b
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
b : ↑S := WellFounded.min (_ : WellFounded s) {b | ¬r (↑b) a} this
ba : ¬r (↑b) a
c : ↑S
h : ¬r ↑c ↑b
⊢ ∀ (b : ↑S), { val := ↑b, property := (_ : ↑b ∈ S) } = b
intro b
case mk
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
b : ↑S := WellFounded.min (_ : WellFounded s) {b | ¬r (↑b) a} this
ba : ¬r (↑b) a
c : ↑S
h : ¬r ↑c ↑b
val✝ : α
property✝ : val✝ ∈ S
⊢ { val := ↑{ val := val✝, property := property✝ }, property := (_ : ↑{ val := val✝, property := property✝ } ∈ S) } =
    { val := val✝, property := property✝ }
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
b✝ : ↑S := WellFounded.min (_ : WellFounded s) {b | ¬r (↑b) a} this
ba : ¬r (↑b✝) a
c : ↑S
h : ¬r ↑c ↑b✝
b : ↑S
⊢ { val := ↑b, property := (_ : ↑b ∈ S) } = b
cases b
no goals
case mk
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
hS : Unbounded r S
e : (#↑S) = cof (type r)
s : ↑S → ↑S → Prop
w✝ : IsWellOrder (↑S) s
e' : ord (#↑S) = type s
T : Set α := {a | ∃ aS, ∀ (b : ↑S), s b { val := a, property := aS } → r (↑b) a}
a : α
this : Set.Nonempty {b | ¬r (↑b) a}
b : ↑S := WellFounded.min (_ : WellFounded s) {b | ¬r (↑b) a} this
ba : ¬r (↑b) a
c : ↑S
h : ¬r ↑c ↑b
val✝ : α
property✝ : val✝ ∈ S
⊢ { val := ↑{ val := val✝, property := property✝ }, property := (_ : ↑{ val := val✝, property := property✝ } ∈ S) } =
    { val := val✝, property := property✝ }
rfl