case mk.intro.intro
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
⊢ BddAbove s
α β : Type u
s : Set Cardinal
⊢ Small ↑s → BddAbove s
rintro ⟨ι, ⟨e⟩⟩
case mk.intro.intro
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
⊢ (range fun x => ↑(↑e.symm x)) = s
case mk.intro.intro
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
⊢ BddAbove s
suffices (range fun x : ι => (e.symm x).1) = s by
  rw [← this]
  apply bddAbove_range.{u, u}
case mk.intro.intro.h
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
x : Cardinal
⊢ (x ∈ range fun x => ↑(↑e.symm x)) ↔ x ∈ s
case mk.intro.intro
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
⊢ (range fun x => ↑(↑e.symm x)) = s
ext x
case mk.intro.intro.h.refine'_1
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
x : Cardinal
⊢ (x ∈ range fun x => ↑(↑e.symm x)) → x ∈ s

case mk.intro.intro.h.refine'_2
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
x : Cardinal
hx : x ∈ s
⊢ (fun x => ↑(↑e.symm x)) (↑e { val := x, property := hx }) = x
case mk.intro.intro.h
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
x : Cardinal
⊢ (x ∈ range fun x => ↑(↑e.symm x)) ↔ x ∈ s
refine' ⟨_, fun hx => ⟨e ⟨x, hx⟩, _⟩⟩
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
this : (range fun x => ↑(↑e.symm x)) = s
⊢ BddAbove (range fun x => ↑(↑e.symm x))
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
this : (range fun x => ↑(↑e.symm x)) = s
⊢ BddAbove s
rw [← this]
no goals
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
this : (range fun x => ↑(↑e.symm x)) = s
⊢ BddAbove (range fun x => ↑(↑e.symm x))
apply bddAbove_range.{u, u}
case mk.intro.intro.h.refine'_1.intro
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
a : ι
⊢ (fun x => ↑(↑e.symm x)) a ∈ s
case mk.intro.intro.h.refine'_1
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
x : Cardinal
⊢ (x ∈ range fun x => ↑(↑e.symm x)) → x ∈ s
rintro ⟨a, rfl⟩
no goals
case mk.intro.intro.h.refine'_1.intro
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
a : ι
⊢ (fun x => ↑(↑e.symm x)) a ∈ s
exact (e.symm a).2
no goals
case mk.intro.intro.h.refine'_2
α β : Type u
s : Set Cardinal
ι : Type u
e : ↑s ≃ ι
x : Cardinal
hx : x ∈ s
⊢ (fun x => ↑(↑e.symm x)) (↑e { val := x, property := hx }) = x
simp_rw [Equiv.symm_apply_apply]