-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_compl_eq_mk_compl_finite_lift {α : Type u} {β : Type v} [Finite α] {s : Set α}
    {t : Set β} (h1 : (lift.{max v w, u} #α) = (lift.{max u w, v} #β))
    (h2 : lift.{max v w, u} #s = lift.{max u w, v} #t) :
    lift.{max v w} #(sᶜ : Set α) = lift.{max u w} #(tᶜ : Set β)

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h2 : lift.{max v w, u} #↑s = lift.{max u w, v} #↑t
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
⊢ lift.{max v w, u} #↑sᶜ = lift.{max u w, v} #↑tᶜ

Tactic:
lift s to Finset α using s.toFinite

Result:
case intro.intro.intro
α : Type u
β : Type v
inst✝ : Finite α
t : Set β
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
s : Finset α
h2 : lift.{max v w, u} #↑↑s = lift.{max u w, v} #↑t
⊢ lift.{max v w, u} #↑(↑s)ᶜ = lift.{max u w, v} #↑tᶜ

Proof state:
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift.{max v w, u} #α = lift.{max u w, v} #β
h2 : lift.{max v w, u} #↑s = lift.{max u w, v} #↑t
val✝ : Fintype α
⊢ lift.{max v w, u} #↑sᶜ = lift.{max u w, v} #↑tᶜ

Tactic:
rcases lift_mk_eq.{u, v, w}.1 h1 with ⟨e⟩

Result:
case intro.intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift.{max v w, u} #α = lift.{max u w, v} #β
h2 : lift.{max v w, u} #↑s = lift.{max u w, v} #↑t
val✝ : Fintype α
e : α ≃ β
⊢ lift.{max v w, u} #↑sᶜ = lift.{max u w, v} #↑tᶜ

Proof state:
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift.{max v w, u} #α = lift.{max u w, v} #β
h2 : lift.{max v w, u} #↑s = lift.{max u w, v} #↑t
⊢ lift.{max v w, u} #↑sᶜ = lift.{max u w, v} #↑tᶜ

Tactic:
cases nonempty_fintype α

Result:
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift.{max v w, u} #α = lift.{max u w, v} #β
h2 : lift.{max v w, u} #↑s = lift.{max u w, v} #↑t
val✝ : Fintype α
⊢ lift.{max v w, u} #↑sᶜ = lift.{max u w, v} #↑tᶜ

Proof state:
case intro.intro.intro
α : Type u
β : Type v
inst✝ : Finite α
t : Set β
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
s : Finset α
h2 : lift.{max v w, u} #↑↑s = lift.{max u w, v} #↑t
⊢ lift.{max v w, u} #↑(↑s)ᶜ = lift.{max u w, v} #↑tᶜ

Tactic:
lift t to Finset β using t.toFinite

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : Finite α
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
s : Finset α
t : Finset β
h2 : lift.{max v w, u} #↑↑s = lift.{max u w, v} #↑↑t
⊢ lift.{max v w, u} #↑(↑s)ᶜ = lift.{max u w, v} #↑(↑t)ᶜ

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift.{max v w, u} #α = lift.{max u w, v} #β
h2 : lift.{max v w, u} #↑s = lift.{max u w, v} #↑t
val✝ : Fintype α
e : α ≃ β
⊢ lift.{max v w, u} #↑sᶜ = lift.{max u w, v} #↑tᶜ

Tactic:
letI : Fintype β := Fintype.ofEquiv α e

Result:
case intro.intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift.{max v w, u} #α = lift.{max u w, v} #β
h2 : lift.{max v w, u} #↑s = lift.{max u w, v} #↑t
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
⊢ lift.{max v w, u} #↑sᶜ = lift.{max u w, v} #↑tᶜ

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h2 : lift.{max v w, u} #↑s = lift.{max u w, v} #↑t
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
⊢ lift.{max v w, u} #↑sᶜ = lift.{max u w, v} #↑tᶜ

Tactic:
classical
  lift s to Finset α using s.toFinite
  lift t to Finset β using t.toFinite
  simp only [Finset.coe_sort_coe, mk_fintype, Fintype.card_coe, lift_natCast, Nat.cast_inj] at h2
  simp only [← Finset.coe_compl, Finset.coe_sort_coe, mk_coe_finset, Finset.card_compl,
    lift_natCast, Nat.cast_inj, h1, h2]

Result:
no goals

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift.{max v w, u} #α = lift.{max u w, v} #β
h2 : lift.{max v w, u} #↑s = lift.{max u w, v} #↑t
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
⊢ lift.{max v w, u} #↑sᶜ = lift.{max u w, v} #↑tᶜ

Tactic:
replace h1 : Fintype.card α = Fintype.card β := (Fintype.ofEquiv_card _).symm

Result:
case intro.intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h2 : lift.{max v w, u} #↑s = lift.{max u w, v} #↑t
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
⊢ lift.{max v w, u} #↑sᶜ = lift.{max u w, v} #↑tᶜ

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : Finite α
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
s : Finset α
t : Finset β
h2 : s.card = t.card
⊢ lift.{max v w, u} #↑(↑s)ᶜ = lift.{max u w, v} #↑(↑t)ᶜ

Tactic:
simp only [← Finset.coe_compl, Finset.coe_sort_coe, mk_coe_finset, Finset.card_compl,
  lift_natCast, Nat.cast_inj, h1, h2]

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : Finite α
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
s : Finset α
t : Finset β
h2 : lift.{max v w, u} #↑↑s = lift.{max u w, v} #↑↑t
⊢ lift.{max v w, u} #↑(↑s)ᶜ = lift.{max u w, v} #↑(↑t)ᶜ

Tactic:
simp only [Finset.coe_sort_coe, mk_fintype, Fintype.card_coe, lift_natCast, Nat.cast_inj] at h2

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : Finite α
val✝ : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
s : Finset α
t : Finset β
h2 : s.card = t.card
⊢ lift.{max v w, u} #↑(↑s)ᶜ = lift.{max u w, v} #↑(↑t)ᶜ