-- Mathlib/Data/Set/Card.lean
theorem ncard_congr {t : Set β} (f : ∀ a ∈ s, β) (h₁ : ∀ a ha, f a ha ∈ t)
    (h₂ : ∀ a b ha hb, f a ha = f b hb → a = b) (h₃ : ∀ b ∈ t, ∃ a ha, f a ha = b) :
    s.ncard = t.ncard

Proof state:
case right.mk.intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1, f' a_1 = ⟨f a ha, hy⟩

Tactic:
simp only [Subtype.mk.injEq, Subtype.exists]

Result:
case right.mk.intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1, ∃ (b : a_1 ∈ s), f' ⟨a_1, b⟩ = ⟨f a ha, hy⟩

Proof state:
case right
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
⊢ Function.Surjective f'

Tactic:
rintro ⟨y, hy⟩

Result:
case right.mk
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
y : β
hy : y ∈ t
⊢ ∃ a, f' a = ⟨y, hy⟩

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
⊢ Function.Bijective f'

Tactic:
constructor

Result:
case left
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
⊢ Function.Injective f'

case right
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
⊢ Function.Surjective f'

Proof state:
case left.mk.mk
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x ⋯ = f y ⋯
⊢ x = y

Tactic:
exact h₂ _ _ hx hy hxy

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
⊢ s.ncard = t.ncard

Tactic:
set f' : s → t := fun x ↦ ⟨f x.1 x.2, h₁ _ _⟩

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
⊢ s.ncard = t.ncard

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
hbij : Function.Bijective f'
⊢ Nat.card ↑s = Nat.card ↑t

Tactic:
exact Nat.card_congr (Equiv.ofBijective f' hbij)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
hbij : Function.Bijective f'
⊢ s.ncard = t.ncard

Tactic:
simp_rw [← Nat.card_coe_set_eq]

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
hbij : Function.Bijective f'
⊢ Nat.card ↑s = Nat.card ↑t

Proof state:
case right.mk.intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1, ∃ (b : a_1 ∈ s), f' ⟨a_1, b⟩ = ⟨f a ha, hy⟩

Tactic:
exact ⟨_, ha, rfl⟩

Result:
no goals

Proof state:
case left.mk.mk
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f' ⟨x, hx⟩ = f' ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
simp only [f', Subtype.mk.injEq] at hxy ⊢

Result:
case left.mk.mk
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x ⋯ = f y ⋯
⊢ x = y

Proof state:
case right.mk
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
y : β
hy : y ∈ t
⊢ ∃ a, f' a = ⟨y, hy⟩

Tactic:
obtain ⟨a, ha, rfl⟩ := h₃ y hy

Result:
case right.mk.intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1, f' a_1 = ⟨f a ha, hy⟩

Proof state:
case left
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
⊢ Function.Injective f'

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy

Result:
case left.mk.mk
α : Type u_1
β : Type u_2
s : Set α
t : Set β
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 ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x => ⟨f ↑x ⋯, ⋯⟩
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f' ⟨x, hx⟩ = f' ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩