α✝ : Type ?u.1813
r✝ : α✝ → α✝ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
⊢ ∀ (b : Cardinal),
    b ∈ Cardinal.lift '' {c | ∃ S, (∀ (a : β), ∃ b, b ∈ S ∧ s a b) ∧ (#↑S) = c} →
      sInf (Cardinal.lift '' {c | ∃ S, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) ∧ (#↑S) = c}) ≤ b
α✝ : Type ?u.1813
r✝ : α✝ → α✝ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
⊢ Cardinal.lift (cof r) ≤ Cardinal.lift (cof s)
rw [Order.cof, Order.cof, lift_sInf, lift_sInf,
  le_csInf_iff'' (nonempty_image_iff.2 (Order.cof_nonempty s))]
case intro.intro.intro.intro
α✝ : Type ?u.1813
r✝ : α✝ → α✝ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b, b ∈ u ∧ s a b
⊢ sInf (Cardinal.lift '' {c | ∃ S, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) ∧ (#↑S) = c}) ≤ Cardinal.lift (#↑u)
α✝ : Type ?u.1813
r✝ : α✝ → α✝ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
⊢ ∀ (b : Cardinal),
    b ∈ Cardinal.lift '' {c | ∃ S, (∀ (a : β), ∃ b, b ∈ S ∧ s a b) ∧ (#↑S) = c} →
      sInf (Cardinal.lift '' {c | ∃ S, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) ∧ (#↑S) = c}) ≤ b
rintro - ⟨-, ⟨u, H, rfl⟩, rfl⟩
case intro.intro.intro.intro.h
α✝ : Type ?u.1813
r✝ : α✝ → α✝ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b, b ∈ u ∧ s a b
⊢ Cardinal.lift (#↑u) ∈ Cardinal.lift '' {c | ∃ S, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) ∧ (#↑S) = c}
case intro.intro.intro.intro
α✝ : Type ?u.1813
r✝ : α✝ → α✝ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b, b ∈ u ∧ s a b
⊢ sInf (Cardinal.lift '' {c | ∃ S, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) ∧ (#↑S) = c}) ≤ Cardinal.lift (#↑u)
apply csInf_le'
case intro.intro.intro.intro.h
α✝ : Type ?u.1813
r✝ : α✝ → α✝ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b, b ∈ u ∧ s a b
a : α
⊢ ∃ b, b ∈ ↑(RelIso.symm f) '' u ∧ r a b
case intro.intro.intro.intro.h
α✝ : Type ?u.1813
r✝ : α✝ → α✝ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b, b ∈ u ∧ s a b
⊢ Cardinal.lift (#↑u) ∈ Cardinal.lift '' {c | ∃ S, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) ∧ (#↑S) = c}
refine'
  ⟨_, ⟨f.symm '' u, fun a => _, rfl⟩,
    lift_mk_eq.{u, v, max u v}.2 ⟨(f.symm.toEquiv.image u).symm⟩⟩
case intro.intro.intro.intro.h.intro.intro
α✝ : Type ?u.1813
r✝ : α✝ → α✝ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b, b ∈ u ∧ s a b
a : α
b : β
hb : b ∈ u
hb' : s (↑f a) b
⊢ ∃ b, b ∈ ↑(RelIso.symm f) '' u ∧ r a b
case intro.intro.intro.intro.h
α✝ : Type ?u.1813
r✝ : α✝ → α✝ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b, b ∈ u ∧ s a b
a : α
⊢ ∃ b, b ∈ ↑(RelIso.symm f) '' u ∧ r a b
rcases H (f a) with ⟨b, hb, hb'⟩
case intro.intro.intro.intro.h.intro.intro
α✝ : Type ?u.1813
r✝ : α✝ → α✝ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b, b ∈ u ∧ s a b
a : α
b : β
hb : b ∈ u
hb' : s (↑f a) b
⊢ s (↑f a) (↑f (↑(RelIso.symm f) b))
case intro.intro.intro.intro.h.intro.intro
α✝ : Type ?u.1813
r✝ : α✝ → α✝ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b, b ∈ u ∧ s a b
a : α
b : β
hb : b ∈ u
hb' : s (↑f a) b
⊢ ∃ b, b ∈ ↑(RelIso.symm f) '' u ∧ r a b
refine' ⟨f.symm b, mem_image_of_mem _ hb, f.map_rel_iff.1 _⟩
no goals
case intro.intro.intro.intro.h.intro.intro
α✝ : Type ?u.1813
r✝ : α✝ → α✝ → Prop
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b, b ∈ u ∧ s a b
a : α
b : β
hb : b ∈ u
hb' : s (↑f a) b
⊢ s (↑f a) (↑f (↑(RelIso.symm f) b))
rwa [RelIso.apply_symm_apply]