-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le {α : Type u} {β : Type v} {c : Cardinal}
    (f : α → β) (hf : ∀ b : β, lift.{v} #(f ⁻¹' {b}) ≤ c) : lift.{v} #α ≤ lift.{u} #β * c :=
  (mk_le_mk_mul_of_mk_preimage_le fun x : ULift.{v} α => ULift.up.{u} (f x.1)) <|
    ULift.forall.2 fun b =>
      (mk_congr <|
            (Equiv.ulift.image _).trans
              (Equiv.trans
                (by
                  rw [Equiv.image_eq_preimage]
                  /- Porting note: Need to insert the following `have` b/c bad fun coercion
                   behaviour for Equivs -/
                  have : DFunLike.coe (Equiv.symm (Equiv.ulift (α := α))) = ULift.up (α := α) := rfl
                  rw [this]
                  simp only [preimage, mem_singleton_iff, ULift.up_inj, mem_setOf_eq, coe_setOf]
                  exact Equiv.refl _)
                Equiv.ulift.symm)).trans_le
        (hf b)

Proof state:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
this : ⇑Equiv.ulift.symm = ULift.up
⊢ ↑(ULift.up ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})

Tactic:
simp only [preimage, mem_singleton_iff, ULift.up_inj, mem_setOf_eq, coe_setOf]

Result:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
this : ⇑Equiv.ulift.symm = ULift.up
⊢ { x // f x = b } ≃ { x // f x = b }

Proof state:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
this : ⇑Equiv.ulift.symm = ULift.up
⊢ ↑(⇑Equiv.ulift.symm ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})

Tactic:
rw [this]

Result:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
this : ⇑Equiv.ulift.symm = ULift.up
⊢ ↑(ULift.up ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})

Proof state:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
⊢ ↑(⇑Equiv.ulift '' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})

Tactic:
rw [Equiv.image_eq_preimage]

Result:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
⊢ ↑(⇑Equiv.ulift.symm ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})

Proof state:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
⊢ ↑(⇑Equiv.ulift.symm ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})

Tactic:
have : DFunLike.coe (Equiv.symm (Equiv.ulift (α := α))) = ULift.up (α := α) := rfl

Result:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
this : ⇑Equiv.ulift.symm = ULift.up
⊢ ↑(⇑Equiv.ulift.symm ⁻¹' ((fun x => { down := f x.down }) ⁻¹' {{ down := b }})) ≃ ↑(f ⁻¹' {b})

Proof state:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
this : ⇑Equiv.ulift.symm = ULift.up
⊢ { x // f x = b } ≃ { x // f x = b }

Tactic:
exact Equiv.refl _

Result:
no goals