no goals
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
⊢ card s = card t
classical calc
    s.card = s.attach.card := card_attach.symm
    _ = (s.attach.image fun a : { a // a ∈ s } => f a.1 a.2).card :=
      Eq.symm ((card_image_of_injective _) fun a b h => Subtype.eq <| h₂ _ _ _ _ h)
    _ = t.card :=
      congr_arg card
        (Finset.ext fun b =>
          ⟨fun h =>
            let ⟨a, _, ha₂⟩ := mem_image.1 h
            ha₂ ▸ h₁ _ _,
            fun h =>
            let ⟨a, ha₁, ha₂⟩ := h₃ b h
            mem_image.2 ⟨⟨a, ha₁⟩, by simp [ha₂]⟩⟩)
no goals
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
⊢ card s = card t
calc
s.card = s.attach.card := card_attach.symm
_ = (s.attach.image fun a : { a // a ∈ s } => f a.1 a.2).card :=
Eq.symm ((card_image_of_injective _) fun a b h => Subtype.eq <| h₂ _ _ _ _ h)
_ = t.card :=
congr_arg card
(Finset.ext fun b =>
⟨fun h =>
  let ⟨a, _, ha₂⟩ := mem_image.1 h
  ha₂ ▸ h₁ _ _,
  fun h =>
  let ⟨a, ha₁, ha₂⟩ := h₃ b h
  mem_image.2 ⟨⟨a, ha₁⟩, by simp [ha₂]⟩⟩)
no goals
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
b : β
h : b ∈ t
a : α
ha₁ : a ∈ s
ha₂ : f a ha₁ = b
⊢ { val := a, property := ha₁ } ∈ attach s ∧
    f ↑{ val := a, property := ha₁ } (_ : ↑{ val := a, property := ha₁ } ∈ s) = b
simp [ha₂]