-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_1)
h : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑t : Type u_1)
let let₁ let₂ let₃ : (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₄ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₅ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  let ft : Finset α :=
    Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) → (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₆ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  let ft : Finset α :=
    Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) →
    (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) →
      (hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₇ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  let ft : Finset α :=
    Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) →
    (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) →
      (hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t) →
        (hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
let₈ :
  let fs : Finset α :=
    Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
  let ft : Finset α :=
    Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
  (hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) →
    (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) →
      (hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t) →
        (hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s) →
          (hc : fs.card = ft.card) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
⊢ (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
have let₉ : let fs : Finset α := Finset.map (α := { x : α // x ∈ s }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) Finset.univ;
let ft : Finset α := Finset.map (α := { x : α // x ∈ t }) (Function.Embedding.subtype fun (x : α) ↦ x ∈ t) Finset.univ;
(hs : ∀ (x : α), x ∈ fs ↔ x ∈ s) →
  (ht : ∀ (x : α), x ∈ ft ↔ x ∈ t) →
    (hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t) →
      (hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s) →
        (hc : (fs \ ft).card = (ft \ fs).card) → (↑(s \ t) : Type u_1) ≃ (↑(t \ s) : Type u_1)
Tactic: classical
  let fs : Finset α := Finset.univ.map (Function.Embedding.subtype (· ∈ s))
  let ft : Finset α := Finset.univ.map (Function.Embedding.subtype (· ∈ t))
  have hs (x : α) : x ∈ fs ↔ x ∈ s := by simp [fs]
  have ht (x : α) : x ∈ ft ↔ x ∈ t := by simp [ft]
  have hst (x : α) : x ∈ fs \ ft ↔ x ∈ s \ t := by simp [hs, ht]
  have hts (x : α) : x ∈ ft \ fs ↔ x ∈ t \ s := by simp [hs, ht]
  have hc : fs.card = ft.card := by
    rw [← Fintype.subtype_card fs hs, ← Fintype.subtype_card ft ht]; convert! h
  replace hc := Finset.card_sdiff_comm hc
  rw [← Fintype.subtype_card (fs \ ft) hst, ← Fintype.subtype_card (ft \ fs) hts] at hc
  exact ((Fintype.card_eq (_F := (_)) (_G := (_))).mp hc).some