awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
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
f' : Fin n → α := fun (i : Fin n) ↦ f (↑i : ℕ) ⋯
himage : s = f' '' univ
⊢ (f' '' univ).ncard = ncard (α := Fin n) univ

Tactic:
exact InjOn.ncard_image <| fun i _hi j _hj h ↦ Fin.ext <| f_inj i.val j.val i.is_lt j.is_lt h

Premises used: Fin.ext, Set.InjOn.ncard_image
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
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
f' : Fin n → α := fun (i : Fin n) ↦ f (↑i : ℕ) ⋯
suffices : s = f' '' univ
⊢ s.ncard = n

Tactic:
suffices himage : s = f' '' Set.univ by
    rw [← Fintype.card_fin n, ← Nat.card_eq_fintype_card, ← Set.ncard_univ, himage]
    exact InjOn.ncard_image <| fun i _hi j _hj h ↦ Fin.ext <| f_inj i.val j.val i.is_lt j.is_lt h
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
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
f' : Fin n → α := fun (i : Fin n) ↦ f (↑i : ℕ) ⋯
h : ∀ (x : α), x ∈ s ↔ x ∈ f' '' univ
⊢ s = f' '' univ

Tactic:
ext x
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
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
f' : Fin n → α := fun (i : Fin n) ↦ f (↑i : ℕ) ⋯
x : α
h : x ∈ s ↔ ∃ (y : Fin n), f' y = x
⊢ x ∈ s ↔ x ∈ f' '' univ

Tactic:
simp only [image_univ, mem_range]

Premises used: Set.image_univ, Set.mem_range
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
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
f' : Fin n → α := fun (i : Fin n) ↦ f (↑i : ℕ) ⋯
x : α
⊢ x ∈ s ↔ ∃ (y : Fin n), f' y = x

Tactic:
⟨fun hx ↦ ?_, fun ⟨⟨i, hi⟩, hx⟩ ↦ hx ▸ hf' i hi⟩

Premises used: Membership.mem, Eq.rec, _private.0.Set.ncard_eq_of_bijective.match_1, Iff.intro
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
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
f' : Fin n → α := fun (i : Fin n) ↦ f (↑i : ℕ) ⋯
x : α
h : ∀ (hx : x ∈ s), ∃ (y : Fin n), f' y = x
⊢ x ∈ s ↔ ∃ (y : Fin n), f' y = x

Tactic:
refine ⟨fun hx ↦ ?_, fun ⟨⟨i, hi⟩, hx⟩ ↦ hx ▸ hf' i hi⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
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
f' : Fin n → α := fun (i : Fin n) ↦ f (↑i : ℕ) ⋯
x : α
hx : x ∈ s
h : ∀ (i : ℕ) (hi : i < n) (hx : f i hi ∈ s), ∃ (y : Fin n), f' y = f i hi
⊢ ∃ (y : Fin n), f' y = x

Tactic:
obtain ⟨i, hi, rfl⟩ := hf x hx

Premises used: rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
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
f' : Fin n → α := fun (i : Fin n) ↦ f (↑i : ℕ) ⋯
i : ℕ
hi : i < n
hx : f i hi ∈ s
w : Fin n
h : f' (⟨i, hi⟩ : Fin n) = f i hi
⊢ ∃ (y : Fin n), f' y = f i hi

Tactic:
use ⟨i, hi⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : 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 : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
left : Function.Injective f'
right : Function.Surjective f'
⊢ Function.Bijective f'

Tactic:
constructor
-- Module: Mathlib.Data.Set.Card
Goal:
α : 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 : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f' (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) = f' (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
left : ∀ (hxy : f x ⋯ = f y ⋯), x = y
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx = Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy

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

Premises used: Subtype.mk.injEq
-- Module: Mathlib.Data.Set.Card
Goal:
α : 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 : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x ⋯ = f y ⋯
⊢ x = y

Tactic:
h₂ _ _ hx hy hxy
-- Module: Mathlib.Data.Set.Card
Goal:
α : 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 : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x ⋯ = f y ⋯
⊢ x = y

Tactic:
exact h₂ _ _ hx hy hxy
-- Module: Mathlib.Data.Set.Card
Goal:
α : 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 : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
y : β
hy : y ∈ t
right :
  ∀ (a : α) (ha : a ∈ s) (hy : f a ha ∈ t),
    ∃ (a_1 : (↑s : Type u_1)), f' a_1 = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a ha) hy
⊢ ∃ (a : (↑s : Type u_1)), f' a = Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy

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

Premises used: rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : 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 : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
a : α
ha : a ∈ s
hy : f a ha ∈ t
right :
  ∃ (a_1 : α) (b : a_1 ∈ s),
    f' (Subtype.mk (p := fun (a : α) ↦ a ∈ s) a_1 b) = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a ha) hy
⊢ ∃ (a_1 : (↑s : Type u_1)), f' a_1 = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a ha) hy

Tactic:
simp only [Subtype.exists]

Premises used: Subtype.exists
-- Module: Mathlib.Data.Set.Card
Goal:
α : 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 : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ (a_1 : α) (b : a_1 ∈ s),
    f' (Subtype.mk (p := fun (a : α) ↦ a ∈ s) a_1 b) = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a ha) hy

Tactic:
⟨_, ha, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : 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 : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ (a_1 : α) (b : a_1 ∈ s),
    f' (Subtype.mk (p := fun (a : α) ↦ a ∈ s) a_1 b) = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a ha) hy

Tactic:
exact ⟨_, ha, rfl⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : 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 : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
⊢ Function.Bijective f'

Tactic:
have hbij : f'.Bijective := by
    constructor
    · rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
      simp only [f', Subtype.mk.injEq] at hxy ⊢
      exact h₂ _ _ hx hy hxy
    rintro ⟨y, hy⟩
    obtain ⟨a, ha, rfl⟩ := h₃ y hy
    simp only [Subtype.exists]
    exact ⟨_, ha, rfl⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : 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 : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hbij : Function.Bijective f'
⊢ Nat.card.{u_1} (↑s : Type u_1) = Nat.card.{u_2} (↑t : Type u_2)

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

Premises used: Nat.card_congr, Equiv.ofBijective
-- Module: Mathlib.Data.Set.Card
Goal:
α : 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 : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hbij : Function.Bijective f'
⊢ Nat.card.{u_1} (↑s : Type u_1) = Nat.card.{u_2} (↑t : Type u_2)

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

Premises used: Nat.card_congr, Equiv.ofBijective
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
S : Set α
T : Set β
f : Equiv.{u_1 + 1, u_2 + 1} (↑S : Type u_1) (↑T : Type u_2)
⊢ S.ncard = T.ncard

Tactic:
Cardinal.toNat_congr f

Premises used: Set.encard, Cardinal.toNat_congr, dite, Function.extend, ENat.toNat, WithTop.untopD, Set.ncard, WithTop.recTopCoe, ENat.card, Cardinal.toENatAux
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
⊢ s.encard ≤ t.encard

Tactic:
have hle := encard_le_encard_of_injOn hf f_inj
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
hle : s.encard ≤ t.encard
to_encard_tac : LE.le (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
⊢ s.ncard ≤ t.ncard

Tactic:
to_encard_tac
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
hle : s.encard ≤ t.encard
rwa : (↑s.ncard : ℕ∞) ≤ t.encard
rwa₁ rwa₂ rwa₃ rwa₄ : s.encard ≤ t.encard
⊢ LE.le (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)

Tactic:
rwa [ht.cast_ncard_eq, (ht.finite_of_encard_le hle).cast_ncard_eq]

Premises used: Set.Finite.finite_of_encard_le, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Injective f
rw : (f '' univ).ncard = Nat.card α
rw₁ : ncard.{u_1} (α := α) univ = Nat.card α
rw₂ rw₃ : Nat.card α = Nat.card α
⊢ (range f).ncard = Nat.card α

Tactic:
rw [← image_univ, ncard_image_of_injective univ hf, ncard_univ]

Premises used: Set.image_univ, Set.univ, Set.ncard_image_of_injective, Set.ncard_univ
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set β
h : BijOn f s t
⊢ s.ncard = t.ncard

Tactic:
ncard_congr' h.equiv

Premises used: Set.ncard_congr', Set.BijOn.equiv
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hc : t.ncard < s.ncard
f : α → β
hf : ∀ a ∈ s, f a ∈ t
ht : t.Finite
by_contra : ∀ (h' : ¬∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y), False
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Tactic:
by_contra h'
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hc : t.ncard < s.ncard
f : α → β
hf : ∀ a ∈ s, f a ∈ t
ht : t.Finite
h' : ¬∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
⊢ ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1 → x = x_1

Tactic:
simp only [Ne, not_exists, not_and, not_imp_not] at h'

Premises used: not_exists, Ne, not_and, not_imp_not
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hc : t.ncard < s.ncard
f : α → β
hf : ∀ a ∈ s, f a ∈ t
ht : t.Finite
h' : ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1 → x = x_1
⊢ False

Tactic:
(ncard_le_ncard_of_injOn f hf h' ht).not_gt hc

Premises used: LE.le.not_gt, Set.ncard_le_ncard_of_injOn
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hc : t.ncard < s.ncard
f : α → β
hf : ∀ a ∈ s, f a ∈ t
ht : t.Finite
h' : ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1 → x = x_1
⊢ False

Tactic:
exact (ncard_le_ncard_of_injOn f hf h' ht).not_gt hc

Premises used: LE.le.not_gt, Set.ncard_le_ncard_of_injOn
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
hs : s.Finite
rw : n ≤ hs.toFinset (s := s).card
⊢ n ≤ s.ncard

Tactic:
rw [ncard_eq_toFinset_card _ hs]

Premises used: Set.ncard_eq_toFinset_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
hs : s.Finite
hf₁ : ∀ i < n, f i ∈ hs.toFinset (s := s)
f_inj₁ : ∀ i < n, ∀ j < n, f i = f j → i = j
f₁ : ℕ → α
⊢ n ≤ hs.toFinset (s := s).card

Tactic:
apply Finset.le_card_of_inj_on_range

Premises used: Finset.le_card_of_inj_on_range
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
hs : s.Finite
⊢ ∀ i < n, f i ∈ hs.toFinset (s := s)

Tactic:
simpa
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
hs : s.Finite
⊢ ∀ i < n, ∀ j < n, f i = f j → i = j

Tactic:
simpa
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f' (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) = f' (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
simp : ∀ (hxy : f x ⋯ = f y ⋯), x = y
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx = Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy

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

Premises used: Subtype.mk.injEq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x ⋯ = f y ⋯
⊢ x = y

Tactic:
apply hinj _ _ hx hy hxy
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
⊢ Function.Injective f'

Tactic:
have finj : f'.Injective := by
    rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
    simp only [f', Subtype.mk.injEq] at hxy ⊢
    apply hinj _ _ hx hy hxy
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
finj : Function.Injective f'
have : ∀ (hft : Fintype (↑t : Type u_2)), ∃ (a : α) (ha : a ∈ s), b = f a ha
⊢ ∃ (a : α) (ha : a ∈ s), b = f a ha

Tactic:
have hft := ht.fintype
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
finj : Function.Injective f'
hft : Fintype (↑t : Type u_2)
have : ∀ (hft' : Fintype (↑s : Type u_1)), ∃ (a : α) (ha : a ∈ s), b = f a ha
⊢ ∃ (a : α) (ha : a ∈ s), b = f a ha

Tactic:
have hft' := Fintype.ofInjective f' finj
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
finj : Function.Injective f'
hft : Fintype (↑t : Type u_2)
hft' : Fintype (↑s : Type u_1)
a : α
h : a ∈ s.toFinset
⊢ a ∈ s

Tactic:
simpa using h
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
finj : Function.Injective f'
hft : Fintype (↑t : Type u_2)
hft' : Fintype (↑s : Type u_1)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
⊢ b ∈ t.toFinset

Tactic:
simpa
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
finj : Function.Injective f'
hft : Fintype (↑t : Type u_2)
hft' : Fintype (↑s : Type u_1)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
h :
  Eq.{u_1 + 1} (α := α → Prop) (fun (a : α) ↦ ∃ (ha : a ∈ s), b = f a ha) fun (a : α) ↦
    ∃ (ha : a ∈ s.toFinset), b = f'' a ha
convert_1 : ∀ (a : α) (ha : a ∈ s.toFinset), f'' a ha ∈ t.toFinset
convert_2 : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s.toFinset) (ha₂ : a₂ ∈ s.toFinset), f'' a₁ ha₁ = f'' a₂ ha₂ → a₁ = a₂
convert_3 : t.toFinset.card ≤ s.toFinset.card
⊢ ∃ (a : α) (ha : a ∈ s), b = f a ha

Tactic:
convert! @Finset.surj_on_of_inj_on_of_card_le _ _ _ t.toFinset f'' _ _ _ _ (by simpa) using 1

Premises used: Finset.surj_on_of_inj_on_of_card_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
finj : Function.Injective f'
hft : Fintype (↑t : Type u_2)
hft' : Fintype (↑s : Type u_1)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
⊢ Eq.{u_1 + 1} (α := α → Prop) (fun (a : α) ↦ ∃ (ha : a ∈ s), b = f a ha) fun (a : α) ↦
    ∃ (ha : a ∈ s.toFinset), b = f'' a ha

Tactic:
simp [f'']
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
finj : Function.Injective f'
hft : Fintype (↑t : Type u_2)
hft' : Fintype (↑s : Type u_1)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
⊢ ∀ (a : α) (ha : a ∈ s.toFinset), f'' a ha ∈ t.toFinset

Tactic:
simp [f'', hf]
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
finj : Function.Injective f'
hft : Fintype (↑t : Type u_2)
hft' : Fintype (↑s : Type u_1)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
a₁ a₂ : α
ha₁ : a₁ ∈ s.toFinset
ha₂ : a₂ ∈ s.toFinset
h : f'' a₁ ha₁ = f'' a₂ ha₂
⊢ a₁ ∈ s

Tactic:
rw [mem_toFinset] at ha₁ ha₂

Premises used: Set.mem_toFinset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
finj : Function.Injective f'
hft : Fintype (↑t : Type u_2)
hft' : Fintype (↑s : Type u_1)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
a₁ a₂ : α
ha₁ : a₁ ∈ s.toFinset
ha₂ : a₂ ∈ s.toFinset
h : f'' a₁ ha₁ = f'' a₂ ha₂
ha₃ : a₁ ∈ s
⊢ a₂ ∈ s.toFinset

Tactic:
rw [mem_toFinset] at ha₁ ha₂

Premises used: Set.mem_toFinset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
finj : Function.Injective f'
hft : Fintype (↑t : Type u_2)
hft' : Fintype (↑s : Type u_1)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
a₁ a₂ : α
ha₁ : a₁ ∈ s.toFinset
ha₂ : a₂ ∈ s.toFinset
h : f'' a₁ ha₁ = f'' a₂ ha₂
ha₃ : a₁ ∈ s
ha₄ : a₂ ∈ s.toFinset
⊢ a₂ ∈ s

Tactic:
rw [mem_toFinset] at ha₁ ha₂

Premises used: Set.mem_toFinset