-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_le_lift [IsRefl β s] (f : r ≃r s) :
    Cardinal.lift.{v} (Order.cof r) ≤ Cardinal.lift.{u} (Order.cof s)

Proof state:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
⊢ ∀ b ∈ lift.{u, v} '' {c | ∃ S, (∀ (a : β), ∃ b ∈ S, s a b) ∧ #↑S = c},
    sInf (lift.{v, u} '' {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}) ≤ b

Tactic:
rintro - ⟨-, ⟨u, H, rfl⟩, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b ∈ u, s a b
⊢ sInf (lift.{v, u} '' {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}) ≤ lift.{u, v} #↑u

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b ∈ u, s a b
⊢ sInf (lift.{v, u} '' {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}) ≤ lift.{u, v} #↑u

Tactic:
apply csInf_le'

Result:
case intro.intro.intro.intro.h
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b ∈ u, s a b
⊢ lift.{u, v} #↑u ∈ lift.{v, u} '' {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}

Proof state:
case intro.intro.intro.intro.h.intro.intro
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b ∈ u, s a b
a : α
b : β
hb : b ∈ u
hb' : s (f a) b
⊢ ∃ b ∈ ⇑f.symm '' u, r a b

Tactic:
refine ⟨f.symm b, mem_image_of_mem _ hb, f.map_rel_iff.1 ?_⟩

Result:
case intro.intro.intro.intro.h.intro.intro
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b ∈ u, s a b
a : α
b : β
hb : b ∈ u
hb' : s (f a) b
⊢ s (f a) (f (f.symm b))

Proof state:
case intro.intro.intro.intro.h
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b ∈ u, s a b
a : α
⊢ ∃ b ∈ ⇑f.symm '' u, r a b

Tactic:
rcases H (f a) with ⟨b, hb, hb'⟩

Result:
case intro.intro.intro.intro.h.intro.intro
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b ∈ u, s a b
a : α
b : β
hb : b ∈ u
hb' : s (f a) b
⊢ ∃ b ∈ ⇑f.symm '' u, r a b

Proof state:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
⊢ lift.{v, u} (cof r) ≤ lift.{u, v} (cof s)

Tactic:
rw [Order.cof, Order.cof, lift_sInf, lift_sInf, le_csInf_iff'' ((Order.cof_nonempty s).image _)]

Result:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
⊢ ∀ b ∈ lift.{u, v} '' {c | ∃ S, (∀ (a : β), ∃ b ∈ S, s a b) ∧ #↑S = c},
    sInf (lift.{v, u} '' {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}) ≤ b

Proof state:
case intro.intro.intro.intro.h
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b ∈ u, s a b
⊢ lift.{u, v} #↑u ∈ lift.{v, u} '' {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}

Tactic:
refine ⟨_, ⟨f.symm '' u, fun a => ?_, rfl⟩, lift_mk_eq'.2 ⟨(f.symm.toEquiv.image u).symm⟩⟩

Result:
case intro.intro.intro.intro.h
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b ∈ u, s a b
a : α
⊢ ∃ b ∈ ⇑f.symm '' u, r a b

Proof state:
case intro.intro.intro.intro.h.intro.intro
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : IsRefl β s
f : r ≃r s
u : Set β
H : ∀ (a : β), ∃ b ∈ u, s a b
a : α
b : β
hb : b ∈ u
hb' : s (f a) b
⊢ s (f a) (f (f.symm b))

Tactic:
rwa [RelIso.apply_symm_apply]

Result:
no goals