α✝ : Type ?u.112496
β✝ : Type ?u.112499
γ : Type ?u.112502
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal
b : Ordinal
h : card b ≤ Cardinal.lift a
c : Cardinal
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
e' : Nonempty (α ≃ β)
⊢ ∃ a', lift a' = type s
α✝ : Type ?u.112496
β✝ : Type ?u.112499
γ : Type ?u.112502
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal
b : Ordinal
h : card b ≤ Cardinal.lift a
c : Cardinal
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
e' : Cardinal.lift (#α) = card (type s)
⊢ ∃ a', lift a' = type s
rw [card_type, ← Cardinal.lift_id'.{max u v, u} (#β), ← Cardinal.lift_umax.{u, v},
  lift_mk_eq.{u, max u v, max u v}] at e'
case intro
α✝ : Type ?u.112496
β✝ : Type ?u.112499
γ : Type ?u.112502
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal
b : Ordinal
h : card b ≤ Cardinal.lift a
c : Cardinal
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
⊢ ∃ a', lift a' = type s
α✝ : Type ?u.112496
β✝ : Type ?u.112499
γ : Type ?u.112502
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal
b : Ordinal
h : card b ≤ Cardinal.lift a
c : Cardinal
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
e' : Nonempty (α ≃ β)
⊢ ∃ a', lift a' = type s
cases' e' with f
case intro
α✝ : Type ?u.112496
β✝ : Type ?u.112499
γ : Type ?u.112502
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal
b : Ordinal
h : card b ≤ Cardinal.lift a
c : Cardinal
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
g : ↑f ⁻¹'o s ≃r s
⊢ ∃ a', lift a' = type s
case intro
α✝ : Type ?u.112496
β✝ : Type ?u.112499
γ : Type ?u.112502
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal
b : Ordinal
h : card b ≤ Cardinal.lift a
c : Cardinal
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
⊢ ∃ a', lift a' = type s
have g := RelIso.preimage f s
case intro
α✝ : Type ?u.112496
β✝ : Type ?u.112499
γ : Type ?u.112502
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal
b : Ordinal
h : card b ≤ Cardinal.lift a
c : Cardinal
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
g : ↑f ⁻¹'o s ≃r s
this : IsWellOrder α (↑f ⁻¹'o s)
⊢ ∃ a', lift a' = type s
case intro
α✝ : Type ?u.112496
β✝ : Type ?u.112499
γ : Type ?u.112502
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal
b : Ordinal
h : card b ≤ Cardinal.lift a
c : Cardinal
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
g : ↑f ⁻¹'o s ≃r s
⊢ ∃ a', lift a' = type s
haveI := (g : f ⁻¹'o s ↪r s).isWellOrder
case intro
α✝ : Type ?u.112496
β✝ : Type ?u.112499
γ : Type ?u.112502
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal
b : Ordinal
h : card b ≤ Cardinal.lift a
c : Cardinal
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
g : ↑f ⁻¹'o s ≃r s
this✝ : IsWellOrder α (↑f ⁻¹'o s)
this : lift (type (↑f ⁻¹'o s)) = lift (type s)
⊢ ∃ a', lift a' = type s
case intro
α✝ : Type ?u.112496
β✝ : Type ?u.112499
γ : Type ?u.112502
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal
b : Ordinal
h : card b ≤ Cardinal.lift a
c : Cardinal
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
g : ↑f ⁻¹'o s ≃r s
this : IsWellOrder α (↑f ⁻¹'o s)
⊢ ∃ a', lift a' = type s
have := lift_type_eq.{u, max u v, max u v}.2 ⟨g⟩
case intro
α✝ : Type ?u.112496
β✝ : Type ?u.112499
γ : Type ?u.112502
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal
b : Ordinal
h : card b ≤ Cardinal.lift a
c : Cardinal
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
g : ↑f ⁻¹'o s ≃r s
this✝ : IsWellOrder α (↑f ⁻¹'o s)
this : lift (type (↑f ⁻¹'o s)) = type s
⊢ ∃ a', lift a' = type s
case intro
α✝ : Type ?u.112496
β✝ : Type ?u.112499
γ : Type ?u.112502
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal
b : Ordinal
h : card b ≤ Cardinal.lift a
c : Cardinal
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
g : ↑f ⁻¹'o s ≃r s
this✝ : IsWellOrder α (↑f ⁻¹'o s)
this : lift (type (↑f ⁻¹'o s)) = lift (type s)
⊢ ∃ a', lift a' = type s
rw [lift_id, lift_umax.{u, v}] at this
no goals
case intro
α✝ : Type ?u.112496
β✝ : Type ?u.112499
γ : Type ?u.112502
r : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Cardinal
b : Ordinal
h : card b ≤ Cardinal.lift a
c : Cardinal
e : Cardinal.lift c = card b
α : Type u
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : α ≃ β
g : ↑f ⁻¹'o s ≃r s
this✝ : IsWellOrder α (↑f ⁻¹'o s)
this : lift (type (↑f ⁻¹'o s)) = type s
⊢ ∃ a', lift a' = type s
exact ⟨_, this⟩