awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
hst : s ⊆ t
⊢ #t ≤ #s ↔ t = s

Tactic:
(eq_iff_card_le_of_subset hst).trans eq_comm

Premises used: eq_comm, Iff.trans, Finset.eq_iff_card_le_of_subset
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
h : #t ≤ #s
⊢ s ⊆ t ↔ s = t

Tactic:
⟨fun hst => eq_of_subset_of_card_le hst h, Eq.subset⟩

Premises used: Eq.subset, Iff.intro, Finset.eq_of_subset_of_card_le
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
f : α ↪ α
hs : map f s ⊆ s
⊢ map f s = s

Tactic:
eq_of_subset_of_card_le hs (card_map _).ge

Premises used: Eq.ge, Finset.card_map, Finset.eq_of_subset_of_card_le
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
p : α → Prop
inst : DecidablePred p
rw : #s ≤ #(filter p s) ↔ ∀ x ∈ s, p x
rw₁ : filter p s = s ↔ ∀ x ∈ s, p x
rw₂ rw₃ : (∀ x ∈ s, p x) ↔ ∀ x ∈ s, p x
⊢ #(filter p s) = #s ↔ ∀ x ∈ s, p x

Tactic:
rw [← (card_filter_le s p).ge_iff_eq, eq_iff_card_le_of_subset (filter_subset p s),
    filter_eq_self]

Premises used: Finset.filter_subset, Finset.filter_eq_self, LE.le.ge_iff_eq, Finset.card_filter_le, Finset.eq_iff_card_le_of_subset
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
p : α → Prop
inst : DecidablePred p
rw : filter p s = ∅ ↔ ∀ x ∈ s, ¬p x
rw₁ rw₂ : (∀ ⦃x : α⦄, x ∈ s → ¬p x) ↔ ∀ x ∈ s, ¬p x
⊢ #(filter p s) = 0 ↔ ∀ x ∈ s, ¬p x

Tactic:
rw [card_eq_zero, filter_eq_empty_iff]

Premises used: Finset.filter_eq_empty_iff, Finset.card_eq_zero
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
h : s ⊂ t
⊢ #s < #t

Tactic:
card_lt_card <| val_lt_iff.2 h

Premises used: Iff.mpr, Finset.val_lt_iff, Finset.card, Multiset.card_lt_card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
⊢ StrictMono.{u_1, 0} (α := Finset α) card

Tactic:
fun _ _ ↦ card_lt_card

Premises used: StrictMono, Set.Subset, Finset.card_lt_card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
h : ∀ (a : α), a ∈ s ↔ Membership.mem (γ := Finset α) (image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach) a
⊢ s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach

Tactic:
ext a
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
h : a ∈ s ↔ ∃ (i : ℕ) (hi : i ∈ range n), f i ⋯ = a
⊢ a ∈ s ↔ Membership.mem (γ := Finset α) (image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach) a

Tactic:
simpa only [mem_image, mem_attach, true_and, Subtype.exists]

Premises used: Finset.mem_image, Finset.mem_attach, Subtype.exists, true_and
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
h : a ∈ s ↔ ∃ (i : ℕ) (hi : i ∈ range n), f i ⋯ = a
⊢ a ∈ s ↔ Membership.mem (γ := Finset α) (image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach) a

Tactic:
suffices _ : a ∈ s ↔ ∃ (i : _) (hi : i ∈ range n), f i (mem_range.1 hi) = a by
      simpa only [mem_image, mem_attach, true_and, Subtype.exists]
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
h : a ∈ s → ∃ (i : ℕ) (hi : i ∈ range n), f i ⋯ = a
h₁ : (∃ (i : ℕ) (hi : i ∈ range n), f i ⋯ = a) → a ∈ s
⊢ a ∈ s ↔ ∃ (i : ℕ) (hi : i ∈ range n), f i ⋯ = a

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
ha : a ∈ s
h : ∀ (i : ℕ) (hi : i < n) (ha : f i hi ∈ s), ∃ (i_1 : ℕ) (hi_1 : i_1 ∈ range n), f i_1 ⋯ = f i hi
⊢ ∃ (i : ℕ) (hi : i ∈ range n), f i ⋯ = a

Tactic:
obtain ⟨i, hi, rfl⟩ := hf a ha

Premises used: rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
i : ℕ
hi : i < n
ha : f i hi ∈ s
w : ℕ
w₁ : i ∈ range n
h : f i ⋯ = f i hi
⊢ ∃ (i_1 : ℕ) (hi_1 : i_1 ∈ range n), f i_1 ⋯ = f i hi

Tactic:
use i, mem_range.2 hi

Premises used: Iff.mpr, Finset.mem_range
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
i : ℕ
hi : i ∈ range n
⊢ f i ⋯ ∈ s

Tactic:
apply hf'
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
⊢ s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach

Tactic:
have : s = (range n).attach.image fun i => f i.1 (mem_range.1 i.2) := by
    ext a
    suffices _ : a ∈ s ↔ ∃ (i : _) (hi : i ∈ range n), f i (mem_range.1 hi) = a by
      simpa only [mem_image, mem_attach, true_and, Subtype.exists]
    constructor
    · intro ha; obtain ⟨i, hi, rfl⟩ := hf a ha; use i, mem_range.2 hi
    · rintro ⟨i, hi, rfl⟩; apply hf'
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach
rw rw₁ :
  card.{u_1} (α := α) (image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach) =
    card.{u_1} (α := α) (image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach)
⊢ #s = card.{u_1} (α := α) (image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach)

Tactic:
rw [this]
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach
⊢ card.{u_1} (α := α) (image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach) = #(range n).attach

Tactic:
?_
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach
⊢ #(range n).attach = #(range n)

Tactic:
card_attach

Premises used: Finset.card_attach
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach
⊢ #(range n) = n

Tactic:
card_range n

Premises used: Finset.card_range
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach
fun : card.{u_1} (α := α) (image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach) = #(range n).attach
⊢ #s = n

Tactic:
calc
    #s = #((range n).attach.image fun i => f i.1 (mem_range.1 i.2)) := by rw [this]
    _ = #(range n).attach := ?_
    _ = #(range n) := card_attach
    _ = n := card_range n

Premises used: Finset.card_range, Finset.mem_range, Finset.range, Finset.card_attach, Finset.attach, Iff.mp, Finset.image
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach
H : Injective.{1, u_1 + 1} (β := α) fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯
⊢ card.{u_1} (α := α) (image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach) = #(range n).attach

Tactic:
apply card_image_of_injective

Premises used: Finset.card_image_of_injective
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach
i : ℕ
hi : i ∈ range n
H :
  ∀ (j : ℕ) (hj : j ∈ range n),
    Eq.{u_1 + 1} (α := α) ((fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) i hi))
        ((fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) j hj)) →
      Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) i hi = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) j hj
⊢ ∀ ⦃a₂ : ↥(range n)⦄,
    Eq.{u_1 + 1} (α := α) ((fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) i hi))
        ((fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) a₂) →
      Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) i hi = a₂

Tactic:
⟨j, hj⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach
i : ℕ
hi : i ∈ range n
j : ℕ
hj : j ∈ range n
eq :
  Eq.{u_1 + 1} (α := α) ((fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) i hi))
    ((fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) j hj))
⊢ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) i hi = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) j hj

Tactic:
Subtype.ext <| f_inj i j (mem_range.1 hi) (mem_range.1 hj) eq

Premises used: Finset.mem_range, Iff.mp, Subtype.ext
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach
i : ℕ
hi : i ∈ range n
j : ℕ
hj : j ∈ range n
eq :
  Eq.{u_1 + 1} (α := α) ((fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) i hi))
    ((fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) j hj))
⊢ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) i hi = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) j hj

Tactic:
exact Subtype.ext <| f_inj i j (mem_range.1 hi) (mem_range.1 hj) eq

Premises used: Finset.mem_range, Iff.mp, Subtype.ext
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ (i : ℕ) (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
have : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach
have₁ : ∀ (this : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach), #s = n
have₂ : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach
have₃ have₄ : ∀ (this : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach), #s = n
have₅ :
  ∀ (this : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach),
    card.{u_1} (α := α) (image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach) = #(range n).attach
H :
  ∀ (this : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach),
    Injective.{1, u_1 + 1} (β := α) fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯
H₁ :
  ∀ (this : s = image (fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (range n).attach) (i : ℕ) (hi : i ∈ range n) (j : ℕ)
    (hj : j ∈ range n)
    (eq :
      Eq.{u_1 + 1} (α := α) ((fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) i hi))
        ((fun (i : ↥(range n)) ↦ f (↑i : ℕ) ⋯) (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) j hj))),
    Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) i hi = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ range n) j hj
⊢ #s = n

Tactic:
classical
  have : s = (range n).attach.image fun i => f i.1 (mem_range.1 i.2) := by
    ext a
    suffices _ : a ∈ s ↔ ∃ (i : _) (hi : i ∈ range n), f i (mem_range.1 hi) = a by
      simpa only [mem_image, mem_attach, true_and, Subtype.exists]
    constructor
    · intro ha; obtain ⟨i, hi, rfl⟩ := hf a ha; use i, mem_range.2 hi
    · rintro ⟨i, hi, rfl⟩; apply hf'
  calc
    #s = #((range n).attach.image fun i => f i.1 (mem_range.1 i.2)) := by rw [this]
    _ = #(range n).attach := ?_
    _ = #(range n) := card_attach
    _ = n := card_range n
  apply card_image_of_injective
  intro ⟨i, hi⟩ ⟨j, hj⟩ eq
  exact Subtype.ext <| f_inj i j (mem_range.1 hi) (mem_range.1 hj) eq

Premises used: Finset.card_range, Finset.card_image_of_injective, Finset.range, Finset.card_attach, Finset.attach, Subtype.ext
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
⊢ #s = #s.attach

Tactic:
card_attach.symm

Premises used: Finset.card_attach, Eq.symm
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
⊢ #s.attach = card.{u_2} (α := β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach)

Tactic:
Eq.symm ?_

Premises used: Eq.symm
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
⊢ card.{u_2} (α := β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) = #t

Tactic:
?_
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
calc_1 : card.{u_2} (α := β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) = #s.attach
calc_2 : card.{u_2} (α := β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) = #t
⊢ #s = #t

Tactic:
calc
    #s = #s.attach := card_attach.symm
    _ = #(s.attach.image fun a ↦ i a.1 a.2) := Eq.symm ?_
    _ = #t := ?_

Premises used: Finset.card_attach, Finset.attach, Eq.symm, Finset.image
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
calc_1 : Injective.{u_1 + 1, u_2 + 1} (β := β) fun (a : ↥s) ↦ i (↑a : α) ⋯
⊢ card.{u_2} (α := β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) = #s.attach

Tactic:
apply card_image_of_injective

Premises used: Finset.card_image_of_injective
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
val : α
property : val ∈ s
calc_1 :
  ∀ (val_1 : α) (property_1 : val_1 ∈ s),
    Eq.{u_2 + 1} (α := β) ((fun (a : ↥s) ↦ i (↑a : α) ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) val property))
        ((fun (a : ↥s) ↦ i (↑a : α) ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) val_1 property_1)) →
      Subtype.mk (p := fun (x : α) ↦ x ∈ s) val property = Subtype.mk (p := fun (x : α) ↦ x ∈ s) val_1 property_1
⊢ ∀ ⦃a₂ : ↥s⦄,
    Eq.{u_2 + 1} (α := β) ((fun (a : ↥s) ↦ i (↑a : α) ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) val property))
        ((fun (a : ↥s) ↦ i (↑a : α) ⋯) a₂) →
      Subtype.mk (p := fun (x : α) ↦ x ∈ s) val property = a₂

Tactic:
⟨_, _⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
val : α
property : val ∈ s
val_1 : α
property_1 : val_1 ∈ s
h :
  Eq.{u_2 + 1} (α := β) ((fun (a : ↥s) ↦ i (↑a : α) ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) val property))
    ((fun (a : ↥s) ↦ i (↑a : α) ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) val_1 property_1))
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) val property = Subtype.mk (p := fun (x : α) ↦ x ∈ s) val_1 property_1

Tactic:
simpa using i_inj _ _ _ _ h
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
calc_2 : image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach = t
⊢ card.{u_2} (α := β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) = #t

Tactic:
congr 1
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
calc_2 : ∀ (b : β), Membership.mem (γ := Finset β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) b ↔ b ∈ t
⊢ image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach = t

Tactic:
ext b
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
b : β
calc_2 : Membership.mem (γ := Finset β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) b → b ∈ t
calc_2₁ : b ∈ t → Membership.mem (γ := Finset β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) b
⊢ Membership.mem (γ := Finset β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) b ↔ b ∈ t

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
b : β
h : Membership.mem (γ := Finset β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) b
calc_2 :
  ∀ w ∈ s.attach,
    ∀ (h : Membership.mem (γ := Finset β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) (i (↑w : α) ⋯)),
      i (↑w : α) ⋯ ∈ t
⊢ b ∈ t

Tactic:
obtain ⟨_, _, rfl⟩ := mem_image.1 h

Premises used: Finset.mem_image, Iff.mp, rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
w : ↥s
left : w ∈ s.attach
h : Membership.mem (γ := Finset β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) (i (↑w : α) ⋯)
⊢ i (↑w : α) ⋯ ∈ t

Tactic:
apply hi
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
b : β
h : b ∈ t
calc_2 :
  ∀ (a : α) (ha : a ∈ s) (h : i a ha ∈ t),
    Membership.mem (γ := Finset β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) (i a ha)
⊢ Membership.mem (γ := Finset β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) b

Tactic:
obtain ⟨a, ha, rfl⟩ := i_surj b h

Premises used: rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
a : α
ha : a ∈ s
h : i a ha ∈ t
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha ∈ s.attach ∧
    i (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) : α) ⋯ = i a ha

Tactic:
simp
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
a : α
ha : a ∈ s
h : i a ha ∈ t
⊢ Membership.mem (γ := Finset β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) (i a ha)

Tactic:
exact mem_image.2 ⟨⟨a, ha⟩, by simp⟩

Premises used: Iff.mpr, Finset.mem_image, Exists.intro
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), i a ha = b
calc_1 : card.{u_2} (α := β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) = #s.attach
calc_2 calc_2₁ : card.{u_2} (α := β) (image (fun (a : ↥s) ↦ i (↑a : α) ⋯) s.attach) = #t
⊢ #s = #t

Tactic:
classical
  calc
    #s = #s.attach := card_attach.symm
    _ = #(s.attach.image fun a ↦ i a.1 a.2) := Eq.symm ?_
    _ = #t := ?_
  · apply card_image_of_injective
    intro ⟨_, _⟩ ⟨_, _⟩ h
    simpa using i_inj _ _ _ _ h
  · congr 1
    ext b
    constructor <;> intro h
    · obtain ⟨_, _, rfl⟩ := mem_image.1 h; apply hi
    · obtain ⟨a, ha, rfl⟩ := i_surj b h; exact mem_image.2 ⟨⟨a, ha⟩, by simp⟩

Premises used: Iff.mpr, Finset.mem_image, Finset.card_image_of_injective, Finset.card_attach, Finset.attach, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
⊢ #s = #t

Tactic:
card_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩)

Premises used: Finset.card_bij, Exists.intro
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
refine : ∀ (a1 : α) (h1 : a1 ∈ s) (a2 : α) (h2 : a2 ∈ s) (eq : i a1 h1 = i a2 h2), a1 = a2
⊢ #s = #t

Tactic:
refine card_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩)

Premises used: Finset.card_bij, Exists.intro