awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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 : ℕ) ⋯
⊢ s.ncard = n
have suffices : s = f' '' univ
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
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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 : ℕ) ⋯
⊢ s = f' '' univ
have h : ∀ (x : α), x ∈ s ↔ x ∈ f' '' univ
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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 ↔ x ∈ f' '' univ
have h : x ∈ s ↔ ∃ (y : Fin n), f' y = x
Tactic: simp only [image_univ, mem_range]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
have h : ∀ (hx : x ∈ s), ∃ (y : Fin n), f' y = x
Tactic: refine ⟨fun hx ↦ ?_, fun ⟨⟨i, hi⟩, hx⟩ ↦ hx ▸ hf' i hi⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ∃ (y : Fin n), f' y = x
have h : ∀ (i : ℕ) (hi : i < n) (hx : f i hi ∈ s), ∃ (y : Fin n), f' y = f i hi
Tactic: obtain ⟨i, hi, rfl⟩ := hf x hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ∃ (y : Fin n), f' y = f i hi
have w : Fin n
Tactic: use ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ∃ (y : Fin n), f' y = f i hi
have h : f' (⟨i, hi⟩ : Fin n) = f i hi
Tactic: use ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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'
have left : Function.Injective f'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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'
⊢ Function.Bijective f'
have right : Function.Surjective f'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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)
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx = Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy
have left : ∀ (hxy : f x sorry = f y sorry), x = y
Tactic: simp only [f', Subtype.mk.injEq] at hxy ⊢
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ∃ (a : (↑s : Type u_1)), f' a = Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy
have 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
Tactic: obtain ⟨a, ha, rfl⟩ := h₃ y hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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 : (↑s : Type u_1)), f' a_1 = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a ha) hy
have 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
Tactic: simp only [Subtype.exists]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
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 : α) ⋯) ⋯
⊢ s.ncard = t.ncard
have hbij : 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⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
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.ncard ≤ t.ncard
have hle : s.encard ≤ t.encard
Tactic: have hle := encard_le_encard_of_injOn hf f_inj
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ s.ncard ≤ t.ncard
have to_encard_tac : LE.le (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
Tactic: to_encard_tac
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ LE.le (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
have rwa : (↑s.ncard : ℕ∞) ≤ t.encard
Tactic: rwa [ht.cast_ncard_eq, (ht.finite_of_encard_le hle).cast_ncard_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Injective f
⊢ (range f).ncard = Nat.card α
have rw : (f '' univ).ncard = Nat.card α
Tactic: rw [← image_univ, ncard_image_of_injective univ hf, ncard_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Injective f
rw : (f '' univ).ncard = Nat.card α
⊢ (range f).ncard = Nat.card α
have rw₁ : ncard.{u_1} (α := α) univ = Nat.card α
Tactic: rw [← image_univ, ncard_image_of_injective univ hf, ncard_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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 α
⊢ (range f).ncard = Nat.card α
have rw₂ : Nat.card α = Nat.card α
Tactic: rw [← image_univ, ncard_image_of_injective univ hf, ncard_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
have by_contra : ∀ (h' : ¬∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y), False
Tactic: by_contra h'
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
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
⊢ False
have h'₁ : ∀ 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'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ n ≤ s.ncard
have rw : n ≤ hs.toFinset (s := s).card
Tactic: rw [ncard_eq_toFinset_card _ hs]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ n ≤ hs.toFinset (s := s).card
have hf₁ : ∀ i < n, f i ∈ hs.toFinset (s := s)
Tactic: apply Finset.le_card_of_inj_on_range
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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)
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx = Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy
have simp : ∀ (hxy : f x sorry = f y sorry), x = y
Tactic: simp only [f', Subtype.mk.injEq] at hxy ⊢
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
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 : α) ⋯) ⋯
⊢ ∃ (a : α) (ha : a ∈ s), b = f a ha
have finj : 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
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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'
⊢ ∃ (a : α) (ha : a ∈ s), b = f a ha
have have : ∀ (hft : Fintype (↑t : Type u_2)), ∃ (a : α) (ha : a ∈ s), b = f a ha
Tactic: have hft := ht.fintype
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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)
⊢ ∃ (a : α) (ha : a ∈ s), b = f a ha
have have : ∀ (hft' : Fintype (↑s : Type u_1)), ∃ (a : α) (ha : a ∈ s), b = f a ha
Tactic: have hft' := Fintype.ofInjective f' finj
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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), b = f a ha
have 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
Tactic: convert! @Finset.surj_on_of_inj_on_of_card_le _ _ _ t.toFinset f'' _ _ _ _ (by simpa) using 1
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ∃ (a : α) (ha : a ∈ s), b = f a ha
have convert_1 : ∀ (a : α) (ha : a ∈ s.toFinset), f'' a ha ∈ t.toFinset
Tactic: convert! @Finset.surj_on_of_inj_on_of_card_le _ _ _ t.toFinset f'' _ _ _ _ (by simpa) using 1
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ∃ (a : α) (ha : a ∈ s), b = f a ha
have convert_2 : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s.toFinset) (ha₂ : a₂ ∈ s.toFinset), f'' a₁ ha₁ = f'' a₂ ha₂ → a₁ = a₂
Tactic: convert! @Finset.surj_on_of_inj_on_of_card_le _ _ _ t.toFinset f'' _ _ _ _ (by simpa) using 1
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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₂
⊢ ∃ (a : α) (ha : a ∈ s), b = f a ha
have convert_3 : t.toFinset.card ≤ s.toFinset.card
Tactic: convert! @Finset.surj_on_of_inj_on_of_card_le _ _ _ t.toFinset f'' _ _ _ _ (by simpa) using 1
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
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₁ = a₂
have ha₃ : a₁ ∈ s
Tactic: rw [mem_toFinset] at ha₁ ha₂
Cleared hypotheses: ha₂, h
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
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₁ = a₂
have ha₅ : a₂ ∈ s
Tactic: rw [mem_toFinset] at ha₁ ha₂
Cleared hypotheses: ha₂, h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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 ⋯
⊢ t.toFinset.card ≤ s.toFinset.card
have convert_3 : t.ncard ≤ s.toFinset.card
Tactic: rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card']
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
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
⊢ ∃ (a : (↑s : Type u_1)), f' a = Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy
have obtain : ∀ (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
Tactic: obtain ⟨a, ha, rfl⟩ := hsurj y hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
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 : (↑s : Type u_1)), f' a_1 = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a ha) hy
have simp : ∃ (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: simp only [Subtype.exists]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
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₁ = a₂
have hsurj₁ : Function.Surjective f'
Tactic: have hsurj : f'.Surjective := by
    rintro ⟨y, hy⟩
    obtain ⟨a, ha, rfl⟩ := hsurj y hy
    simp only [Subtype.exists]
    exact ⟨_, ha, rfl⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
⊢ a₁ = a₂
have haveI : ∀ (this : Fintype (↑s : Type u_1)), a₁ = a₂
Tactic: haveI := hs.fintype
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this : Fintype (↑s : Type u_1)
⊢ a₁ = a₂
have haveI : ∀ (this : Fintype (↑t : Type u_2)), a₁ = a₂
Tactic: haveI := Fintype.ofSurjective _ hsurj
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
a : α
ha : a ∈ s.toFinset
⊢ f'' a ha ∈ t.toFinset
have rw : ∀ (ha_1 : a ∈ s), f'' a ha ∈ t
Tactic: rw [mem_toFinset] at ha ⊢
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
a : α
ha : a ∈ s.toFinset
⊢ f'' a ha ∈ t.toFinset
have rw : ∀ (ha_1 : a ∈ s), f'' a ha ∈ t
Tactic: { rw [mem_toFinset] at ha ⊢; exact hf a ha }