α✝ β✝ α : Type u
β : Type v
c : Cardinal
f : α → β
hf : ∀ (b : β), lift (#↑(f ⁻¹' {b})) ≤ c
b : β
⊢ ↑(↑Equiv.ulift.symm ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})
α✝ β✝ α : Type u
β : Type v
c : Cardinal
f : α → β
hf : ∀ (b : β), lift (#↑(f ⁻¹' {b})) ≤ c
b : β
⊢ ↑(↑Equiv.ulift '' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})
rw [Equiv.image_eq_preimage]
α✝ β✝ α : Type u
β : Type v
c : Cardinal
f : α → β
hf : ∀ (b : β), lift (#↑(f ⁻¹' {b})) ≤ c
b : β
this : ↑Equiv.ulift.symm = ULift.up
⊢ ↑(↑Equiv.ulift.symm ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})
α✝ β✝ α : Type u
β : Type v
c : Cardinal
f : α → β
hf : ∀ (b : β), lift (#↑(f ⁻¹' {b})) ≤ c
b : β
⊢ ↑(↑Equiv.ulift.symm ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})
have : FunLike.coe (Equiv.symm (Equiv.ulift (α := α))) = ULift.up (α := α) := rfl
α✝ β✝ α : Type u
β : Type v
c : Cardinal
f : α → β
hf : ∀ (b : β), lift (#↑(f ⁻¹' {b})) ≤ c
b : β
this : ↑Equiv.ulift.symm = ULift.up
⊢ ↑(ULift.up ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})
α✝ β✝ α : Type u
β : Type v
c : Cardinal
f : α → β
hf : ∀ (b : β), lift (#↑(f ⁻¹' {b})) ≤ c
b : β
this : ↑Equiv.ulift.symm = ULift.up
⊢ ↑(↑Equiv.ulift.symm ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})
rw [this]
α✝ β✝ α : Type u
β : Type v
c : Cardinal
f : α → β
hf : ∀ (b : β), lift (#↑(f ⁻¹' {b})) ≤ c
b : β
this : ↑Equiv.ulift.symm = ULift.up
⊢ { x // f x = b } ≃ { x // f x = b }
α✝ β✝ α : Type u
β : Type v
c : Cardinal
f : α → β
hf : ∀ (b : β), lift (#↑(f ⁻¹' {b})) ≤ c
b : β
this : ↑Equiv.ulift.symm = ULift.up
⊢ ↑(ULift.up ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})
simp only [preimage, mem_singleton_iff, ULift.up_inj, mem_setOf_eq, coe_setOf]
no goals
α✝ β✝ α : Type u
β : Type v
c : Cardinal
f : α → β
hf : ∀ (b : β), lift (#↑(f ⁻¹' {b})) ≤ c
b : β
this : ↑Equiv.ulift.symm = ULift.up
⊢ { x // f x = b } ≃ { x // f x = b }
exact Equiv.refl _