[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ Injective fun f => f.toFun
[PROOFSTEP]
rintro ⟨f, hf⟩ ⟨g, hg⟩ h
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ↪r s
hf : ∀ (a : α) (b : β), s b (↑f a) → ∃ a', ↑f a' = b
g : r ↪r s
hg : ∀ (a : α) (b : β), s b (↑g a) → ∃ a', ↑g a' = b
h : (fun f => f.toFun) { toRelEmbedding := f, init' := hf } = (fun f => f.toFun) { toRelEmbedding := g, init' := hg }
⊢ { toRelEmbedding := f, init' := hf } = { toRelEmbedding := g, init' := hg }
[PROOFSTEP]
congr with x
[GOAL]
case mk.mk.e_toRelEmbedding.h
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ↪r s
hf : ∀ (a : α) (b : β), s b (↑f a) → ∃ a', ↑f a' = b
g : r ↪r s
hg : ∀ (a : α) (b : β), s b (↑g a) → ∃ a', ↑g a' = b
h : (fun f => f.toFun) { toRelEmbedding := f, init' := hf } = (fun f => f.toFun) { toRelEmbedding := g, init' := hg }
x : α
⊢ ↑f x = ↑g x
[PROOFSTEP]
exact congr_fun h x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
a : α
b : β
h : s b (↑f a)
⊢ ∃ a', ↑f a' = b ∧ r a' a
[PROOFSTEP]
rcases f.init h with ⟨a', rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
a a' : α
h : s (↑f a') (↑f a)
⊢ ∃ a'_1, ↑f a'_1 = ↑f a' ∧ r a'_1 a
[PROOFSTEP]
exact ⟨a', rfl, f.map_rel_iff.1 h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
c : γ
h : t c (↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a)
⊢ ∃ a', ↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a' = c
[PROOFSTEP]
simp at h ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
c : γ
h : t c (↑g (↑f a))
⊢ ∃ a', ↑g (↑f a') = c
[PROOFSTEP]
rcases g.2 _ _ h with ⟨b, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
b : β
h : t (↑g.toRelEmbedding b) (↑g (↑f a))
⊢ ∃ a', ↑g (↑f a') = ↑g.toRelEmbedding b
[PROOFSTEP]
have h := g.map_rel_iff.1 h
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
b : β
h✝ : t (↑g.toRelEmbedding b) (↑g (↑f a))
h : s b (↑f a)
⊢ ∃ a', ↑g (↑f a') = ↑g.toRelEmbedding b
[PROOFSTEP]
rcases f.2 _ _ h with ⟨a', rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a a' : α
h✝ : t (↑g.toRelEmbedding (↑f.toRelEmbedding a')) (↑g (↑f a))
h : s (↑f.toRelEmbedding a') (↑f a)
⊢ ∃ a'_1, ↑g (↑f a'_1) = ↑g.toRelEmbedding (↑f.toRelEmbedding a')
[PROOFSTEP]
exact ⟨a', rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝² : IsTrichotomous β s
inst✝¹ : IsIrrefl β s
inst✝ : IsWellFounded α r
f g : r ≼i s
⊢ f = g
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝² : IsTrichotomous β s
inst✝¹ : IsIrrefl β s
inst✝ : IsWellFounded α r
f g : r ≼i s
a : α
⊢ ↑f a = ↑g a
[PROOFSTEP]
refine' IsWellFounded.induction r a fun b IH => extensional_of_trichotomous_of_irrefl s fun x => _
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝² : IsTrichotomous β s
inst✝¹ : IsIrrefl β s
inst✝ : IsWellFounded α r
f g : r ≼i s
a b : α
IH : ∀ (y : α), r y b → ↑f y = ↑g y
x : β
⊢ s x (↑f b) ↔ s x (↑g b)
[PROOFSTEP]
rw [f.init_iff, g.init_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝² : IsTrichotomous β s
inst✝¹ : IsIrrefl β s
inst✝ : IsWellFounded α r
f g : r ≼i s
a b : α
IH : ∀ (y : α), r y b → ↑f y = ↑g y
x : β
⊢ (∃ a', ↑f a' = x ∧ r a' b) ↔ ∃ a', ↑g a' = x ∧ r a' b
[PROOFSTEP]
exact exists_congr fun x => and_congr_left fun hx => IH _ hx ▸ Iff.rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
a : r ≼i s
⊢ ∀ (b : r ≼i s), a = b
[PROOFSTEP]
let _ := a.isWellFounded
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
a : r ≼i s
x✝ : IsWellFounded α r := RelEmbedding.isWellFounded a.toRelEmbedding
⊢ ∀ (b : r ≼i s), a = b
[PROOFSTEP]
exact Subsingleton.elim a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f g : r ≼i s
a : α
⊢ ↑f a = ↑g a
[PROOFSTEP]
rw [Subsingleton.elim f g]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
h : ¬∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x
b x : β
x✝¹ : ∀ (y : β), s y x → Acc s y
IH : ∀ (y : β), s y x → ∃ a, ↑f a = y
hn : ∀ (x_1 : α), ¬↑f x_1 = x
y : β
x✝ : ∃ y_1, ↑f y_1 = y
a : α
e : ↑f a = y
⊢ s y x
[PROOFSTEP]
rw [← e]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
h : ¬∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x
b x : β
x✝¹ : ∀ (y : β), s y x → Acc s y
IH : ∀ (y : β), s y x → ∃ a, ↑f a = y
hn : ∀ (x_1 : α), ¬↑f x_1 = x
y : β
x✝ : ∃ y_1, ↑f y_1 = y
a : α
e : ↑f a = y
⊢ s (↑f a) x
[PROOFSTEP]
exact (trichotomous _ _).resolve_right (not_or_of_not (hn a) fun hl => not_exists.2 hn (f.init hl))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
p : Set β
f : r ≼i s
H : ∀ (a : α), ↑f a ∈ p
a : α
x✝ : ↑p
b : β
m : b ∈ p
h : Subrel s p { val := b, property := m } (↑(RelEmbedding.codRestrict p f.toRelEmbedding H) a)
a' : α
e : ↑f a' = ↑{ val := b, property := m }
⊢ ↑(RelEmbedding.codRestrict p f.toRelEmbedding H) a' = { val := b, property := m }
[PROOFSTEP]
subst e
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
p : Set β
f : r ≼i s
H : ∀ (a : α), ↑f a ∈ p
a : α
x✝ : ↑p
a' : α
m : ↑f a' ∈ p
h : Subrel s p { val := ↑f a', property := m } (↑(RelEmbedding.codRestrict p f.toRelEmbedding H) a)
⊢ ↑(RelEmbedding.codRestrict p f.toRelEmbedding H) a' = { val := ↑f a', property := m }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
a : α
b : α ⊕ β
⊢ Sum.Lex r s b
      (↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
            map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
        a) →
    ∃ a',
      ↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
              map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
          a' =
        b
[PROOFSTEP]
cases b <;> [exact fun _ => ⟨_, rfl⟩; exact False.elim ∘ Sum.lex_inr_inl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
a : α
b : α ⊕ β
⊢ Sum.Lex r s b
      (↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
            map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
        a) →
    ∃ a',
      ↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
              map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
          a' =
        b
[PROOFSTEP]
cases b
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
a val✝ : α
⊢ Sum.Lex r s (Sum.inl val✝)
      (↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
            map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
        a) →
    ∃ a',
      ↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
              map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
          a' =
        Sum.inl val✝
[PROOFSTEP]
exact fun _ => ⟨_, rfl⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
a : α
val✝ : β
⊢ Sum.Lex r s (Sum.inr val✝)
      (↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
            map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
        a) →
    ∃ a',
      ↑{ toEmbedding := { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) },
              map_rel_iff' := (_ : ∀ {a b : α}, Sum.Lex r s (Sum.inl a) (Sum.inl b) ↔ r a b) }
          a' =
        Sum.inr val✝
[PROOFSTEP]
exact False.elim ∘ Sum.lex_inr_inl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
a : α
⊢ Acc r a → Acc s (↑f a)
[PROOFSTEP]
refine' fun h => Acc.recOn h fun a _ ha => Acc.intro _ fun b hb => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
a✝ : α
h : Acc r a✝
a : α
x✝ : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s (↑f y)
b : β
hb : s b (↑f a)
⊢ Acc s b
[PROOFSTEP]
obtain ⟨a', rfl⟩ := f.init hb
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
a✝ : α
h : Acc r a✝
a : α
x✝ : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s (↑f y)
a' : α
hb : s (↑f a') (↑f a)
⊢ Acc s (↑f a')
[PROOFSTEP]
exact ha _ (f.map_rel_iff.mp hb)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
⊢ False
[PROOFSTEP]
have h := f.lt_top f.top
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r (↑f.toRelEmbedding f.top) f.top
⊢ False
[PROOFSTEP]
rw [show f f.top = f.top from InitialSeg.eq (↑f) (InitialSeg.refl r) f.top] at h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r f.top f.top
⊢ False
[PROOFSTEP]
exact _root_.irrefl _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≺i s
g : s ≼i t
a : γ
⊢ t a (↑g f.top) ↔ ∃ a_1, ↑(RelEmbedding.trans f.toRelEmbedding g.toRelEmbedding) a_1 = a
[PROOFSTEP]
simp only [g.init_iff, PrincipalSeg.down, exists_and_left.symm, exists_swap, RelEmbedding.trans_apply, exists_eq_right',
  InitialSeg.coe_coe_fn]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≃r s
g : s ≺i t
c : γ
x✝ : ∃ a, ↑g.toRelEmbedding a = c
b : β
h : ↑g.toRelEmbedding b = c
⊢ ↑g.toRelEmbedding (↑f (↑(RelIso.symm f) b)) = c
[PROOFSTEP]
simp only [h, RelIso.apply_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≃r s
g : s ≺i t
c : γ
this : (∃ a, ↑g.toRelEmbedding a = c) ↔ ∃ a, ↑g.toRelEmbedding (↑f a) = c
⊢ t c g.top ↔ ∃ a, ↑(RelEmbedding.trans (RelIso.toRelEmbedding f) g.toRelEmbedding) a = c
[PROOFSTEP]
simpa [PrincipalSeg.down]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t✝ : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≺i s
g : s ≃r t
⊢ ∀ (b : γ), t b (↑g f.top) ↔ ∃ a, ↑(RelEmbedding.trans f.toRelEmbedding (RelIso.toRelEmbedding g)) a = b
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t✝ : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≺i s
g : s ≃r t
x : γ
⊢ t x (↑g f.top) ↔ ∃ a, ↑(RelEmbedding.trans f.toRelEmbedding (RelIso.toRelEmbedding g)) a = x
[PROOFSTEP]
rw [← g.apply_symm_apply x, g.map_rel_iff, f.down', exists_congr]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t✝ : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≺i s
g : s ≃r t
x : γ
⊢ ∀ (a : α),
    ↑f.toRelEmbedding a = ↑(RelIso.symm g) x ↔
      ↑(RelEmbedding.trans f.toRelEmbedding (RelIso.toRelEmbedding g)) a = ↑g (↑(RelIso.symm g) x)
[PROOFSTEP]
intro y
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t✝ : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≺i s
g : s ≃r t
x : γ
y : α
⊢ ↑f.toRelEmbedding y = ↑(RelIso.symm g) x ↔
    ↑(RelEmbedding.trans f.toRelEmbedding (RelIso.toRelEmbedding g)) y = ↑g (↑(RelIso.symm g) x)
[PROOFSTEP]
exact ⟨congr_arg g, fun h => g.toEquiv.bijective.1 h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f g : r ≺i s
⊢ f = g
[PROOFSTEP]
have ef : (f : α → β) = g := by
  show ((f : r ≼i s) : α → β) = (g : r ≼i s)
  rw [@Subsingleton.elim _ _ (f : r ≼i s) g]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f g : r ≺i s
⊢ ↑f.toRelEmbedding = ↑g.toRelEmbedding
[PROOFSTEP]
show ((f : r ≼i s) : α → β) = (g : r ≼i s)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f g : r ≺i s
⊢ ↑{ toRelEmbedding := f.toRelEmbedding,
        init' := (_ : ∀ (x : α) (x_1 : β), s x_1 (↑f.toRelEmbedding x) → ∃ a', ↑f.toRelEmbedding a' = x_1) } =
    ↑{ toRelEmbedding := g.toRelEmbedding,
        init' := (_ : ∀ (x : α) (x_1 : β), s x_1 (↑g.toRelEmbedding x) → ∃ a', ↑g.toRelEmbedding a' = x_1) }
[PROOFSTEP]
rw [@Subsingleton.elim _ _ (f : r ≼i s) g]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f g : r ≺i s
ef : ↑f.toRelEmbedding = ↑g.toRelEmbedding
⊢ f = g
[PROOFSTEP]
have et : f.top = g.top := by
  refine' extensional_of_trichotomous_of_irrefl s fun x => _
  simp only [PrincipalSeg.down, ef]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f g : r ≺i s
ef : ↑f.toRelEmbedding = ↑g.toRelEmbedding
⊢ f.top = g.top
[PROOFSTEP]
refine' extensional_of_trichotomous_of_irrefl s fun x => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f g : r ≺i s
ef : ↑f.toRelEmbedding = ↑g.toRelEmbedding
x : β
⊢ s x f.top ↔ s x g.top
[PROOFSTEP]
simp only [PrincipalSeg.down, ef]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f g : r ≺i s
ef : ↑f.toRelEmbedding = ↑g.toRelEmbedding
et : f.top = g.top
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
g : r ≺i s
toRelEmbedding✝ : r ↪r s
top✝ : β
down'✝ : ∀ (b : β), s b top✝ ↔ ∃ a, ↑toRelEmbedding✝ a = b
ef : ↑{ toRelEmbedding := toRelEmbedding✝, top := top✝, down' := down'✝ }.toRelEmbedding = ↑g.toRelEmbedding
et : { toRelEmbedding := toRelEmbedding✝, top := top✝, down' := down'✝ }.top = g.top
⊢ { toRelEmbedding := toRelEmbedding✝, top := top✝, down' := down'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
toRelEmbedding✝¹ : r ↪r s
top✝¹ : β
down'✝¹ : ∀ (b : β), s b top✝¹ ↔ ∃ a, ↑toRelEmbedding✝¹ a = b
toRelEmbedding✝ : r ↪r s
top✝ : β
down'✝ : ∀ (b : β), s b top✝ ↔ ∃ a, ↑toRelEmbedding✝ a = b
ef :
  ↑{ toRelEmbedding := toRelEmbedding✝¹, top := top✝¹, down' := down'✝¹ }.toRelEmbedding =
    ↑{ toRelEmbedding := toRelEmbedding✝, top := top✝, down' := down'✝ }.toRelEmbedding
et :
  { toRelEmbedding := toRelEmbedding✝¹, top := top✝¹, down' := down'✝¹ }.top =
    { toRelEmbedding := toRelEmbedding✝, top := top✝, down' := down'✝ }.top
⊢ { toRelEmbedding := toRelEmbedding✝¹, top := top✝¹, down' := down'✝¹ } =
    { toRelEmbedding := toRelEmbedding✝, top := top✝, down' := down'✝ }
[PROOFSTEP]
have := RelEmbedding.coe_fn_injective ef
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
toRelEmbedding✝¹ : r ↪r s
top✝¹ : β
down'✝¹ : ∀ (b : β), s b top✝¹ ↔ ∃ a, ↑toRelEmbedding✝¹ a = b
toRelEmbedding✝ : r ↪r s
top✝ : β
down'✝ : ∀ (b : β), s b top✝ ↔ ∃ a, ↑toRelEmbedding✝ a = b
ef :
  ↑{ toRelEmbedding := toRelEmbedding✝¹, top := top✝¹, down' := down'✝¹ }.toRelEmbedding =
    ↑{ toRelEmbedding := toRelEmbedding✝, top := top✝, down' := down'✝ }.toRelEmbedding
et :
  { toRelEmbedding := toRelEmbedding✝¹, top := top✝¹, down' := down'✝¹ }.top =
    { toRelEmbedding := toRelEmbedding✝, top := top✝, down' := down'✝ }.top
this :
  { toRelEmbedding := toRelEmbedding✝¹, top := top✝¹, down' := down'✝¹ }.toRelEmbedding =
    { toRelEmbedding := toRelEmbedding✝, top := top✝, down' := down'✝ }.toRelEmbedding
⊢ { toRelEmbedding := toRelEmbedding✝¹, top := top✝¹, down' := down'✝¹ } =
    { toRelEmbedding := toRelEmbedding✝, top := top✝, down' := down'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ f.top = g.top
[PROOFSTEP]
rw [Subsingleton.elim f (PrincipalSeg.equivLT e g)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ (equivLT e g).top = g.top
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t✝ : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
f : r ≺i s
g : s ≺i t
h : r ≺i t
⊢ t h.top g.top
[PROOFSTEP]
rw [Subsingleton.elim h (f.trans g)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t✝ : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
f : r ≺i s
g : s ≺i t
h : r ≺i t
⊢ t (PrincipalSeg.trans f g).top g.top
[PROOFSTEP]
apply PrincipalSeg.lt_top
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsEmpty α
b : β
H : ∀ (b' : β), ¬s b' b
src✝ : r ↪r s := RelEmbedding.ofIsEmpty r s
⊢ ∀ (b_1 : β),
    s b_1 b ↔
      ∃ a,
        ↑{ toEmbedding := src✝.toEmbedding,
                map_rel_iff' := (_ : ∀ {a b : α}, s (↑src✝.toEmbedding a) (↑src✝.toEmbedding b) ↔ r a b) }
            a =
          b_1
[PROOFSTEP]
simp [H]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
β : Type u_4
s : β → β → Prop
inst✝ : IsTrans β s
⊢ WellFounded s ↔ ∀ (b : β), WellFounded (Subrel s {b' | s b' b})
[PROOFSTEP]
refine'
  ⟨fun wf b => ⟨fun b' => ((PrincipalSeg.ofElement _ b).acc b').mpr (wf.apply b')⟩, fun wf =>
    ⟨fun b => Acc.intro _ fun b' hb' => _⟩⟩
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
β : Type u_4
s : β → β → Prop
inst✝ : IsTrans β s
wf : ∀ (b : β), WellFounded (Subrel s {b' | s b' b})
b b' : β
hb' : s b' b
⊢ Acc s b'
[PROOFSTEP]
let f := PrincipalSeg.ofElement s b
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
β : Type u_4
s : β → β → Prop
inst✝ : IsTrans β s
wf : ∀ (b : β), WellFounded (Subrel s {b' | s b' b})
b b' : β
hb' : s b' b
f : Subrel s {b_1 | s b_1 b} ≺i s := PrincipalSeg.ofElement s b
⊢ Acc s b'
[PROOFSTEP]
obtain ⟨b', rfl⟩ := f.down.mp ((PrincipalSeg.ofElement_top s b).symm ▸ hb' : s b' f.top)
[GOAL]
case intro
α : Type u_1
β✝ : Type u_2
γ : Type u_3
r : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
β : Type u_4
s : β → β → Prop
inst✝ : IsTrans β s
wf : ∀ (b : β), WellFounded (Subrel s {b' | s b' b})
b : β
f : Subrel s {b_1 | s b_1 b} ≺i s := PrincipalSeg.ofElement s b
b' : ↑{b_1 | s b_1 b}
hb' : s (↑f.toRelEmbedding b') b
⊢ Acc s (↑f.toRelEmbedding b')
[PROOFSTEP]
exact (f.acc b').mp ((wf b).apply b')
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
⊢ (r ≺i s) ⊕ (r ≃r s)
[PROOFSTEP]
by_cases h : Surjective f
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
h : Surjective ↑f
⊢ (r ≺i s) ⊕ (r ≃r s)
[PROOFSTEP]
exact Sum.inr (RelIso.ofSurjective f h)
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
h : ¬Surjective ↑f
⊢ (r ≺i s) ⊕ (r ≃r s)
[PROOFSTEP]
have h' : _ := (InitialSeg.eq_or_principal f).resolve_left h
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
h : ¬Surjective ↑f
h' : ∃ b, ∀ (x : β), s x b ↔ ∃ y, ↑f y = x
⊢ (r ≺i s) ⊕ (r ≃r s)
[PROOFSTEP]
exact Sum.inl ⟨f, Classical.choose h', Classical.choose_spec h'⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ ↑(leLT f g).toRelEmbedding a = ↑g.toRelEmbedding (↑f a)
[PROOFSTEP]
delta InitialSeg.leLT
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ ↑(match ltOrEq f with
          | Sum.inl f' => PrincipalSeg.trans f' g
          | Sum.inr f' => PrincipalSeg.equivLT f' g).toRelEmbedding
      a =
    ↑g.toRelEmbedding (↑f a)
[PROOFSTEP]
cases' h : f.ltOrEq with f' f'
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≺i s
h : ltOrEq f = Sum.inl f'
⊢ ↑(match Sum.inl f' with
          | Sum.inl f' => PrincipalSeg.trans f' g
          | Sum.inr f' => PrincipalSeg.equivLT f' g).toRelEmbedding
      a =
    ↑g.toRelEmbedding (↑f a)
[PROOFSTEP]
simp only [PrincipalSeg.trans_apply, f.ltOrEq_apply_left]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≃r s
h : ltOrEq f = Sum.inr f'
⊢ ↑(match Sum.inr f' with
          | Sum.inl f' => PrincipalSeg.trans f' g
          | Sum.inr f' => PrincipalSeg.equivLT f' g).toRelEmbedding
      a =
    ↑g.toRelEmbedding (↑f a)
[PROOFSTEP]
simp only [PrincipalSeg.equivLT_apply, f.ltOrEq_apply_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
IH : (y : α) → r y a → { b // ¬s (↑f y) b }
⊢ { b // ¬s (↑f a) b }
[PROOFSTEP]
let S := {b | ∀ a h, s (IH a h).1 b}
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
IH : (y : α) → r y a → { b // ¬s (↑f y) b }
S : Set β := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}
⊢ { b // ¬s (↑f a) b }
[PROOFSTEP]
have : f a ∈ S := fun a' h =>
  ((trichotomous _ _).resolve_left fun h' => (IH a' h).2 <| _root_.trans (f.map_rel_iff.2 h) h').resolve_left fun h' =>
    (IH a' h).2 <| h' ▸ f.map_rel_iff.2 h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
IH : (y : α) → r y a → { b // ¬s (↑f y) b }
S : Set β := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}
this : ↑f a ∈ S
⊢ { b // ¬s (↑f a) b }
[PROOFSTEP]
exact ⟨_, IsWellFounded.wf.not_lt_min _ ⟨_, this⟩ this⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a✝ a : α
⊢ r a a✝ → s ↑(collapseF f a) ↑(collapseF f a✝)
[PROOFSTEP]
revert a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ∀ (a_1 : α), r a_1 a → s ↑(collapseF f a_1) ↑(collapseF f a)
[PROOFSTEP]
show (collapseF f a).1 ∈ {b | ∀ (a') (_ : r a' a), s (collapseF f a').1 b}
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(collapseF f a) ∈ {b | ∀ (a' : α), r a' a → s (↑(collapseF f a')) b}
[PROOFSTEP]
unfold collapseF
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(WellFounded.fix (_ : WellFounded r)
        (fun a IH =>
          let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b};
          let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
          { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
            property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
        a) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(WellFounded.fix (_ : WellFounded r)
                (fun a IH =>
                  let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b};
                  let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
                  { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
                    property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
                a'))
            b}
[PROOFSTEP]
rw [WellFounded.fix_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(let S :=
        {b |
          ∀ (a_1 : α) (h : r a_1 a),
            s
              (↑((fun y x =>
                    WellFounded.fix (_ : WellFounded r)
                      (fun a IH =>
                        let S := {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b};
                        let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
                        { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
                          property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
                      y)
                  a_1 h))
              b};
      let_fun this :=
        (_ :
          ∀ (a' : α),
            r a' a →
              s
                (↑(WellFounded.fix (_ : WellFounded r)
                    (fun a IH =>
                      let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b};
                      let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
                      { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
                        property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
                    a'))
                (↑f a));
      { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
        property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) }) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(WellFounded.fix (_ : WellFounded r)
                (fun a IH =>
                  let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b};
                  let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
                  { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
                    property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
                a'))
            b}
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ WellFounded.min (_ : WellFounded s)
      {b |
        ∀ (a_1 : α),
          r a_1 a →
            s
              (↑(WellFounded.fix (_ : WellFounded r)
                  (fun a IH =>
                    {
                      val :=
                        WellFounded.min (_ : WellFounded s) {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                          (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}),
                      property :=
                        (_ :
                          ¬s (↑f a)
                              (WellFounded.min (_ : WellFounded s) {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                                (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}))) })
                  a_1))
              b}
      (_ :
        ∃ x,
          x ∈
            {b |
              ∀ (a_1 : α),
                r a_1 a →
                  s
                    (↑(WellFounded.fix (_ : WellFounded r)
                        (fun a IH =>
                          {
                            val :=
                              WellFounded.min (_ : WellFounded s) {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                                (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}),
                            property :=
                              (_ :
                                ¬s (↑f a)
                                    (WellFounded.min (_ : WellFounded s)
                                      {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                                      (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}))) })
                        a_1))
                    b}) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(WellFounded.fix (_ : WellFounded r)
                (fun a IH =>
                  {
                    val :=
                      WellFounded.min (_ : WellFounded s) {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}
                        (_ : ∃ x, x ∈ {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}),
                    property :=
                      (_ :
                        ¬s (↑f a)
                            (WellFounded.min (_ : WellFounded s) {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}
                              (_ : ∃ x, x ∈ {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}))) })
                a'))
            b}
[PROOFSTEP]
apply WellFounded.min_mem _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b ↑(collapseF f a)
[PROOFSTEP]
unfold collapseF
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      ↑(WellFounded.fix (_ : WellFounded r)
          (fun a IH =>
            let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b};
            let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
            { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
              property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
          a)
[PROOFSTEP]
rw [WellFounded.fix_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      ↑(let S :=
          {b |
            ∀ (a_1 : α) (h : r a_1 a),
              s
                (↑((fun y x =>
                      WellFounded.fix (_ : WellFounded r)
                        (fun a IH =>
                          let S := {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b};
                          let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
                          { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
                            property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
                        y)
                    a_1 h))
                b};
        let_fun this :=
          (_ :
            ∀ (a' : α),
              r a' a →
                s
                  (↑(WellFounded.fix (_ : WellFounded r)
                      (fun a IH =>
                        let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b};
                        let_fun this := (_ : ∀ (a' : α) (h : r a' a), s (↑(IH a' h)) (↑f a));
                        { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
                          property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
                      a'))
                  (↑f a));
        { val := WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S),
          property := (_ : ¬s (↑f a) (WellFounded.min (_ : WellFounded s) S (_ : ∃ x, x ∈ S))) })
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      (WellFounded.min (_ : WellFounded s)
        {b |
          ∀ (a_1 : α),
            r a_1 a →
              s
                (↑(WellFounded.fix (_ : WellFounded r)
                    (fun a IH =>
                      {
                        val :=
                          WellFounded.min (_ : WellFounded s) {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                            (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}),
                        property :=
                          (_ :
                            ¬s (↑f a)
                                (WellFounded.min (_ : WellFounded s) {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                                  (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}))) })
                    a_1))
                b}
        (_ :
          ∃ x,
            x ∈
              {b |
                ∀ (a_1 : α),
                  r a_1 a →
                    s
                      (↑(WellFounded.fix (_ : WellFounded r)
                          (fun a IH =>
                            {
                              val :=
                                WellFounded.min (_ : WellFounded s) {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                                  (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}),
                              property :=
                                (_ :
                                  ¬s (↑f a)
                                      (WellFounded.min (_ : WellFounded s)
                                        {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}
                                        (_ : ∃ x, x ∈ {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}))) })
                          a_1))
                      b}))
[PROOFSTEP]
exact WellFounded.not_lt_min _ _ _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
this : IsWellOrder α r
a✝ : α
b✝ b : β
x✝¹ : ∀ (y : β), s y b → Acc s y
x✝ :
  ∀ (y : β),
    s y b →
      ∀ (x : α),
        s y
            (↑(ofMonotone (fun a => ↑(collapseF f a)) (_ : ∀ (a b : α), r a b → s ↑(collapseF f a) ↑(collapseF f b)))
              x) →
          ∃ a',
            ↑(ofMonotone (fun a => ↑(collapseF f a)) (_ : ∀ (a b : α), r a b → s ↑(collapseF f a) ↑(collapseF f b)))
                a' =
              y
a : α
h : s b (↑(ofMonotone (fun a => ↑(collapseF f a)) (_ : ∀ (a b : α), r a b → s ↑(collapseF f a) ↑(collapseF f b))) a)
⊢ ∃ a', ↑(ofMonotone (fun a => ↑(collapseF f a)) (_ : ∀ (a b : α), r a b → s ↑(collapseF f a) ↑(collapseF f b))) a' = b
[PROOFSTEP]
rcases(@IsWellFounded.wf _ r).has_min {a | ¬s (collapseF f a).1 b} ⟨_, asymm h⟩ with ⟨m, hm, hm'⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
this : IsWellOrder α r
a✝ : α
b✝ b : β
x✝¹ : ∀ (y : β), s y b → Acc s y
x✝ :
  ∀ (y : β),
    s y b →
      ∀ (x : α),
        s y
            (↑(ofMonotone (fun a => ↑(collapseF f a)) (_ : ∀ (a b : α), r a b → s ↑(collapseF f a) ↑(collapseF f b)))
              x) →
          ∃ a',
            ↑(ofMonotone (fun a => ↑(collapseF f a)) (_ : ∀ (a b : α), r a b → s ↑(collapseF f a) ↑(collapseF f b)))
                a' =
              y
a : α
h : s b (↑(ofMonotone (fun a => ↑(collapseF f a)) (_ : ∀ (a b : α), r a b → s ↑(collapseF f a) ↑(collapseF f b))) a)
m : α
hm : m ∈ {a | ¬s (↑(collapseF f a)) b}
hm' : ∀ (x : α), x ∈ {a | ¬s (↑(collapseF f a)) b} → ¬r x m
⊢ ∃ a', ↑(ofMonotone (fun a => ↑(collapseF f a)) (_ : ∀ (a b : α), r a b → s ↑(collapseF f a) ↑(collapseF f b))) a' = b
[PROOFSTEP]
refine' ⟨m, ((@trichotomous _ s _ _ _).resolve_left hm).resolve_right (collapseF.not_lt f _ fun a' h' => _)⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
this : IsWellOrder α r
a✝ : α
b✝ b : β
x✝¹ : ∀ (y : β), s y b → Acc s y
x✝ :
  ∀ (y : β),
    s y b →
      ∀ (x : α),
        s y
            (↑(ofMonotone (fun a => ↑(collapseF f a)) (_ : ∀ (a b : α), r a b → s ↑(collapseF f a) ↑(collapseF f b)))
              x) →
          ∃ a',
            ↑(ofMonotone (fun a => ↑(collapseF f a)) (_ : ∀ (a b : α), r a b → s ↑(collapseF f a) ↑(collapseF f b)))
                a' =
              y
a : α
h : s b (↑(ofMonotone (fun a => ↑(collapseF f a)) (_ : ∀ (a b : α), r a b → s ↑(collapseF f a) ↑(collapseF f b))) a)
m : α
hm : m ∈ {a | ¬s (↑(collapseF f a)) b}
hm' : ∀ (x : α), x ∈ {a | ¬s (↑(collapseF f a)) b} → ¬r x m
a' : α
h' : r a' m
⊢ s (↑(collapseF f a')) b
[PROOFSTEP]
by_contra hn
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
this : IsWellOrder α r
a✝ : α
b✝ b : β
x✝¹ : ∀ (y : β), s y b → Acc s y
x✝ :
  ∀ (y : β),
    s y b →
      ∀ (x : α),
        s y
            (↑(ofMonotone (fun a => ↑(collapseF f a)) (_ : ∀ (a b : α), r a b → s ↑(collapseF f a) ↑(collapseF f b)))
              x) →
          ∃ a',
            ↑(ofMonotone (fun a => ↑(collapseF f a)) (_ : ∀ (a b : α), r a b → s ↑(collapseF f a) ↑(collapseF f b)))
                a' =
              y
a : α
h : s b (↑(ofMonotone (fun a => ↑(collapseF f a)) (_ : ∀ (a b : α), r a b → s ↑(collapseF f a) ↑(collapseF f b))) a)
m : α
hm : m ∈ {a | ¬s (↑(collapseF f a)) b}
hm' : ∀ (x : α), x ∈ {a | ¬s (↑(collapseF f a)) b} → ¬r x m
a' : α
h' : r a' m
hn : ¬s (↑(collapseF f a')) b
⊢ False
[PROOFSTEP]
exact hm' _ hn h'


[GOAL]
α : Type u_1
s : Set α
inst✝¹ : SupSet α
inst✝ : Inhabited ↑s
t : Set ↑s
h : sSup (Subtype.val '' t) ∈ s
⊢ sSup (Subtype.val '' t) = ↑(sSup t)
[PROOFSTEP]
simp [dif_pos h]
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : InfSet α
inst✝ : Inhabited ↑s
t : Set ↑s
h : sInf (Subtype.val '' t) ∈ s
⊢ sInf (Subtype.val '' t) = ↑(sInf t)
[PROOFSTEP]
simp [dif_pos h]
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
⊢ sSup t = sSup univ
[PROOFSTEP]
have A : ∀ (u : Set s), ¬BddAbove u → BddAbove (Subtype.val '' u) → sSup ((↑) '' u : Set α) ∉ s :=
  by
  intro u hu Hu
  contrapose! hu
  refine ⟨⟨_, hu⟩, ?_⟩
  rintro ⟨x, xs⟩ hx
  simp only [Subtype.mk_le_mk]
  apply le_csSup Hu
  exact ⟨⟨x, xs⟩, hx, rfl⟩
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
⊢ ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
[PROOFSTEP]
intro u hu Hu
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
u : Set ↑s
hu : ¬BddAbove u
Hu : BddAbove (Subtype.val '' u)
⊢ ¬sSup (Subtype.val '' u) ∈ s
[PROOFSTEP]
contrapose! hu
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
u : Set ↑s
Hu : BddAbove (Subtype.val '' u)
hu : sSup (Subtype.val '' u) ∈ s
⊢ BddAbove u
[PROOFSTEP]
refine ⟨⟨_, hu⟩, ?_⟩
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
u : Set ↑s
Hu : BddAbove (Subtype.val '' u)
hu : sSup (Subtype.val '' u) ∈ s
⊢ { val := sSup (Subtype.val '' u), property := hu } ∈ upperBounds u
[PROOFSTEP]
rintro ⟨x, xs⟩ hx
[GOAL]
case mk
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
u : Set ↑s
Hu : BddAbove (Subtype.val '' u)
hu : sSup (Subtype.val '' u) ∈ s
x : α
xs : x ∈ s
hx : { val := x, property := xs } ∈ u
⊢ { val := x, property := xs } ≤ { val := sSup (Subtype.val '' u), property := hu }
[PROOFSTEP]
simp only [Subtype.mk_le_mk]
[GOAL]
case mk
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
u : Set ↑s
Hu : BddAbove (Subtype.val '' u)
hu : sSup (Subtype.val '' u) ∈ s
x : α
xs : x ∈ s
hx : { val := x, property := xs } ∈ u
⊢ x ≤ sSup (Subtype.val '' u)
[PROOFSTEP]
apply le_csSup Hu
[GOAL]
case mk
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
u : Set ↑s
Hu : BddAbove (Subtype.val '' u)
hu : sSup (Subtype.val '' u) ∈ s
x : α
xs : x ∈ s
hx : { val := x, property := xs } ∈ u
⊢ x ∈ Subtype.val '' u
[PROOFSTEP]
exact ⟨⟨x, xs⟩, hx, rfl⟩
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
⊢ sSup t = sSup univ
[PROOFSTEP]
by_cases Ht : BddAbove ((↑) '' t : Set α)
[GOAL]
case pos
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
⊢ sSup t = sSup univ
[PROOFSTEP]
have I1 : sSup ((↑) '' t : Set α) ∉ s := A t ht Ht
[GOAL]
case pos
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
⊢ sSup t = sSup univ
[PROOFSTEP]
have I2 : sSup ((↑) '' (univ : Set s) : Set α) ∉ s := by
  apply A
  · contrapose! ht; exact ht.mono (subset_univ _)
  · refine ⟨sSup ((↑) '' t : Set α), ?_⟩
    rintro - ⟨⟨x, hx⟩, -, rfl⟩
    simp [BddAbove, not_nonempty_iff_eq_empty] at ht
    have : ⟨x, hx⟩ ∉ upperBounds t := by simp [ht]
    obtain ⟨⟨y, ys⟩, yt, hy⟩ : ∃ y, y ∈ t ∧ { val := x, property := hx } < y := by
      simpa only [Subtype.mk_le_mk, not_forall, not_le, exists_prop, exists_and_right, mem_upperBounds]
    refine le_trans (le_of_lt hy) ?_
    exact le_csSup Ht ⟨⟨y, ys⟩, yt, rfl⟩
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
⊢ ¬sSup (Subtype.val '' univ) ∈ s
[PROOFSTEP]
apply A
[GOAL]
case a
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
⊢ ¬BddAbove univ
[PROOFSTEP]
contrapose! ht
[GOAL]
case a
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
ht : BddAbove univ
⊢ BddAbove t
[PROOFSTEP]
exact ht.mono (subset_univ _)
[GOAL]
case a
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
⊢ BddAbove (Subtype.val '' univ)
[PROOFSTEP]
refine ⟨sSup ((↑) '' t : Set α), ?_⟩
[GOAL]
case a
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
⊢ sSup (Subtype.val '' t) ∈ upperBounds (Subtype.val '' univ)
[PROOFSTEP]
rintro - ⟨⟨x, hx⟩, -, rfl⟩
[GOAL]
case a.intro.mk.intro
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
x : α
hx : x ∈ s
⊢ ↑{ val := x, property := hx } ≤ sSup (Subtype.val '' t)
[PROOFSTEP]
simp [BddAbove, not_nonempty_iff_eq_empty] at ht
[GOAL]
case a.intro.mk.intro
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
x : α
hx : x ∈ s
ht : upperBounds t = ∅
⊢ ↑{ val := x, property := hx } ≤ sSup (Subtype.val '' t)
[PROOFSTEP]
have : ⟨x, hx⟩ ∉ upperBounds t := by simp [ht]
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
x : α
hx : x ∈ s
ht : upperBounds t = ∅
⊢ ¬{ val := x, property := hx } ∈ upperBounds t
[PROOFSTEP]
simp [ht]
[GOAL]
case a.intro.mk.intro
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
x : α
hx : x ∈ s
ht : upperBounds t = ∅
this : ¬{ val := x, property := hx } ∈ upperBounds t
⊢ ↑{ val := x, property := hx } ≤ sSup (Subtype.val '' t)
[PROOFSTEP]
obtain ⟨⟨y, ys⟩, yt, hy⟩ : ∃ y, y ∈ t ∧ { val := x, property := hx } < y := by
  simpa only [Subtype.mk_le_mk, not_forall, not_le, exists_prop, exists_and_right, mem_upperBounds]
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
x : α
hx : x ∈ s
ht : upperBounds t = ∅
this : ¬{ val := x, property := hx } ∈ upperBounds t
⊢ ∃ y, y ∈ t ∧ { val := x, property := hx } < y
[PROOFSTEP]
simpa only [Subtype.mk_le_mk, not_forall, not_le, exists_prop, exists_and_right, mem_upperBounds]
[GOAL]
case a.intro.mk.intro.intro.mk.intro
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
x : α
hx : x ∈ s
ht : upperBounds t = ∅
this : ¬{ val := x, property := hx } ∈ upperBounds t
y : α
ys : y ∈ s
yt : { val := y, property := ys } ∈ t
hy : { val := x, property := hx } < { val := y, property := ys }
⊢ ↑{ val := x, property := hx } ≤ sSup (Subtype.val '' t)
[PROOFSTEP]
refine le_trans (le_of_lt hy) ?_
[GOAL]
case a.intro.mk.intro.intro.mk.intro
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
x : α
hx : x ∈ s
ht : upperBounds t = ∅
this : ¬{ val := x, property := hx } ∈ upperBounds t
y : α
ys : y ∈ s
yt : { val := y, property := ys } ∈ t
hy : { val := x, property := hx } < { val := y, property := ys }
⊢ ↑{ val := y, property := ys } ≤ sSup (Subtype.val '' t)
[PROOFSTEP]
exact le_csSup Ht ⟨⟨y, ys⟩, yt, rfl⟩
[GOAL]
case pos
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' t)
I1 : ¬sSup (Subtype.val '' t) ∈ s
I2 : ¬sSup (Subtype.val '' univ) ∈ s
⊢ sSup t = sSup univ
[PROOFSTEP]
simp only [sSup, I1, I2, dite_false]
[GOAL]
case neg
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : ¬BddAbove (Subtype.val '' t)
⊢ sSup t = sSup univ
[PROOFSTEP]
have I : ¬BddAbove ((↑) '' (univ : Set s) : Set α) := by contrapose! Ht;
  exact Ht.mono (image_subset Subtype.val (subset_univ _))
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : ¬BddAbove (Subtype.val '' t)
⊢ ¬BddAbove (Subtype.val '' univ)
[PROOFSTEP]
contrapose! Ht
[GOAL]
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : BddAbove (Subtype.val '' univ)
⊢ BddAbove (Subtype.val '' t)
[PROOFSTEP]
exact Ht.mono (image_subset Subtype.val (subset_univ _))
[GOAL]
case neg
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : ¬BddAbove (Subtype.val '' t)
I : ¬BddAbove (Subtype.val '' univ)
⊢ sSup t = sSup univ
[PROOFSTEP]
have X : sSup ((↑) '' t : Set α) = sSup (univ : Set α) := ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ Ht
[GOAL]
case neg
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : ¬BddAbove (Subtype.val '' t)
I : ¬BddAbove (Subtype.val '' univ)
X : sSup (Subtype.val '' t) = sSup univ
⊢ sSup t = sSup univ
[PROOFSTEP]
have Y : sSup ((↑) '' (univ : Set s) : Set α) = sSup (univ : Set α) :=
  ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ I
[GOAL]
case neg
α : Type u_1
s✝ : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
A : ∀ (u : Set ↑s), ¬BddAbove u → BddAbove (Subtype.val '' u) → ¬sSup (Subtype.val '' u) ∈ s
Ht : ¬BddAbove (Subtype.val '' t)
I : ¬BddAbove (Subtype.val '' univ)
X : sSup (Subtype.val '' t) = sSup univ
Y : sSup (Subtype.val '' univ) = sSup univ
⊢ sSup t = sSup univ
[PROOFSTEP]
simp only [sSup, X, Y]
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
⊢ ∀ (s_1 : Set ↑s) (a : ↑s), BddAbove s_1 → a ∈ s_1 → a ≤ sSup s_1
[PROOFSTEP]
rintro t c h_bdd hct
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
c : ↑s
h_bdd : BddAbove t
hct : c ∈ t
⊢ c ≤ sSup t
[PROOFSTEP]
rw [← Subtype.coe_le_coe, ← subset_sSup_of_within s (h_Sup ⟨c, hct⟩ h_bdd)]
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
c : ↑s
h_bdd : BddAbove t
hct : c ∈ t
⊢ ↑c ≤ sSup (Subtype.val '' t)
[PROOFSTEP]
exact (Subtype.mono_coe _).le_csSup_image hct h_bdd
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
⊢ ∀ (s_1 : Set ↑s) (a : ↑s), Set.Nonempty s_1 → a ∈ upperBounds s_1 → sSup s_1 ≤ a
[PROOFSTEP]
rintro t B ht hB
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
B : ↑s
ht : Set.Nonempty t
hB : B ∈ upperBounds t
⊢ sSup t ≤ B
[PROOFSTEP]
rw [← Subtype.coe_le_coe, ← subset_sSup_of_within s (h_Sup ht ⟨B, hB⟩)]
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
B : ↑s
ht : Set.Nonempty t
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ≤ ↑B
[PROOFSTEP]
exact (Subtype.mono_coe s).csSup_image_le ht hB
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
⊢ ∀ (s_1 : Set ↑s) (a : ↑s), BddBelow s_1 → a ∈ s_1 → sInf s_1 ≤ a
[PROOFSTEP]
rintro t c h_bdd hct
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
c : ↑s
h_bdd : BddBelow t
hct : c ∈ t
⊢ sInf t ≤ c
[PROOFSTEP]
rw [← Subtype.coe_le_coe, ← subset_sInf_of_within s (h_Inf ⟨c, hct⟩ h_bdd)]
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
c : ↑s
h_bdd : BddBelow t
hct : c ∈ t
⊢ sInf (Subtype.val '' t) ≤ ↑c
[PROOFSTEP]
exact (Subtype.mono_coe s).csInf_image_le hct h_bdd
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
⊢ ∀ (s_1 : Set ↑s) (a : ↑s), Set.Nonempty s_1 → a ∈ lowerBounds s_1 → a ≤ sInf s_1
[PROOFSTEP]
intro t B ht hB
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
B : ↑s
ht : Set.Nonempty t
hB : B ∈ lowerBounds t
⊢ B ≤ sInf t
[PROOFSTEP]
rw [← Subtype.coe_le_coe, ← subset_sInf_of_within s (h_Inf ht ⟨B, hB⟩)]
[GOAL]
α : Type u_1
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, Set.Nonempty t → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, Set.Nonempty t → BddBelow t → sInf (Subtype.val '' t) ∈ s
src✝³ : SupSet ↑s := subsetSupSet s
src✝² : InfSet ↑s := subsetInfSet s
src✝¹ : Lattice ↑s := DistribLattice.toLattice
src✝ : LinearOrder ↑s := inferInstance
t : Set ↑s
B : ↑s
ht : Set.Nonempty t
hB : B ∈ lowerBounds t
⊢ ↑B ≤ sInf (Subtype.val '' t)
[PROOFSTEP]
exact (Subtype.mono_coe s).le_csInf_image ht hB
[GOAL]
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
ht : Set.Nonempty t
h_bdd : BddAbove t
⊢ sSup (Subtype.val '' t) ∈ s
[PROOFSTEP]
obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
[GOAL]
case intro
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
h_bdd : BddAbove t
c : ↑s
hct : c ∈ t
⊢ sSup (Subtype.val '' t) ∈ s
[PROOFSTEP]
obtain ⟨B, hB⟩ : ∃ B, B ∈ upperBounds t := h_bdd
[GOAL]
case intro.intro
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ∈ s
[PROOFSTEP]
refine' hs.out c.2 B.2 ⟨_, _⟩
[GOAL]
case intro.intro.refine'_1
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ ↑c ≤ sSup (Subtype.val '' t)
[PROOFSTEP]
exact (Subtype.mono_coe s).le_csSup_image hct ⟨B, hB⟩
[GOAL]
case intro.intro.refine'_2
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ≤ ↑B
[PROOFSTEP]
exact (Subtype.mono_coe s).csSup_image_le ⟨c, hct⟩ hB
[GOAL]
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
ht : Set.Nonempty t
h_bdd : BddBelow t
⊢ sInf (Subtype.val '' t) ∈ s
[PROOFSTEP]
obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
[GOAL]
case intro
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
h_bdd : BddBelow t
c : ↑s
hct : c ∈ t
⊢ sInf (Subtype.val '' t) ∈ s
[PROOFSTEP]
obtain ⟨B, hB⟩ : ∃ B, B ∈ lowerBounds t := h_bdd
[GOAL]
case intro.intro
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ sInf (Subtype.val '' t) ∈ s
[PROOFSTEP]
refine' hs.out B.2 c.2 ⟨_, _⟩
[GOAL]
case intro.intro.refine'_1
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ ↑B ≤ sInf (Subtype.val '' t)
[PROOFSTEP]
exact (Subtype.mono_coe s).le_csInf_image ⟨c, hct⟩ hB
[GOAL]
case intro.intro.refine'_2
α : Type u_1
s✝ : Set α
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : OrdConnected s
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ sInf (Subtype.val '' t) ≤ ↑c
[PROOFSTEP]
exact (Subtype.mono_coe s).csInf_image_le hct ⟨B, hB⟩