awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite α
hs : s.ncard + n ≤ Nat.card α
⊢ ∃ (y : Fin n ↪ α), Disjoint s (range (ι := Fin n) (⇑y : (a : Fin n) → α))
have hs₁ : HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
Tactic: apply exists_embedding_disjoint_range_of_add_le_ENat_card
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite α
hs : s.ncard + n ≤ Nat.card α
⊢ HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
have hs₁ : (↑(s.ncard + n) : ℕ∞) ≤ ENat.card α
Tactic: rwa [← ENat.coe_add, ENat.card_eq_coe_natCard, ENat.coe_le_coe]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
Goal:
α : Type u_1
n : ℕ
s : Set α
inst : Finite α
hs : s.ncard + n ≤ Nat.card α
hs₁ : (↑(s.ncard + n) : ℕ∞) ≤ ENat.card α
⊢ HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
have hs₂ : LE.le (α := ℕ∞) (↑(s.ncard + n) : ℕ∞) (↑(Nat.card α) : ℕ∞)
Tactic: rwa [← ENat.coe_add, ENat.card_eq_coe_natCard, ENat.coe_le_coe]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
Goal:
α : Type u_1
m n : ℕ
hn : HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
x : Fin m ↪ α
⊢ ∃ (a : Fin (m + n) ↪ α), (fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x) a = x
have obtain : ∀ (y : Fin n ↪ α)
  (hxy : Disjoint (α := Set α) (range (ι := Fin m) (⇑x : (a : Fin m) → α)) (range (ι := Fin n) (⇑y : (a : Fin n) → α))),
  ∃ (a : Fin (m + n) ↪ α), (fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x) a = x
Tactic: obtain ⟨y, hxy⟩ :=
    exists_embedding_disjoint_range_of_add_le_ENat_card (s := range x)
      (by simpa [← Nat.card_coe_set_eq, Nat.card_range_of_injective x.injective])
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
Goal:
α : Type u_1
m n : ℕ
hn : HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
x : Fin m ↪ α
y : Fin n ↪ α
hxy : Disjoint (α := Set α) (range (ι := Fin m) (⇑x : (a : Fin m) → α)) (range (ι := Fin n) (⇑y : (a : Fin n) → α))
⊢ ∃ (a : Fin (m + n) ↪ α), (fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x) a = x
have h : (fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x) (append hxy) = x
Tactic: use append hxy
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
Goal:
α : Type u_1
m n : ℕ
hn : HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
x : Fin m ↪ α
y : Fin n ↪ α
hxy : Disjoint (α := Set α) (range (ι := Fin m) (⇑x : (a : Fin m) → α)) (range (ι := Fin n) (⇑y : (a : Fin n) → α))
⊢ (fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x) (append hxy) = x
have h : ∀ (i : Fin m),
  Eq (α := α) (((fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x) (append hxy) : (a : Fin m) → α) i : α)
    ((x : (a : Fin m) → α) i : α)
Tactic: ext i
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
Goal:
α : Type u_1
m n : ℕ
hmn : m ≤ n
hn : (↑n : ℕ∞) ≤ ENat.card α
⊢ Surjective (β := Fin m ↪ α) fun (x : Fin n ↪ α) ↦ (castLEEmb hmn).trans x
have obtain : ∀ (k : ℕ) (hmn : m ≤ m + k) (hn : (↑(m + k) : ℕ∞) ≤ ENat.card α),
  Surjective (β := Fin m ↪ α) fun (x : Fin (m + k) ↪ α) ↦ (castLEEmb hmn).trans x
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
Cleared hypotheses: n, hmn, hn
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
Goal:
α : Type u_1
m n : ℕ
inst : Finite α
hn : m + n ≤ Nat.card α
⊢ Surjective (β := Fin m ↪ α) fun (x : Fin (m + n) ↪ α) ↦ Embedding.trans (castAddEmb n) x
have hn₁ : HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
Tactic: apply restrictSurjective_of_add_le_ENatCard
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
Goal:
α : Type u_1
m n : ℕ
inst : Finite α
hn : m + n ≤ Nat.card α
⊢ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
have hn₁ : (↑(m + n) : ℕ∞) ≤ ENat.card α
Tactic: rwa [← ENat.coe_add, ENat.card_eq_coe_natCard, ENat.coe_le_coe]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
Goal:
α : Type u_1
m n : ℕ
inst : Finite α
hn : m + n ≤ Nat.card α
hn₁ : (↑(m + n) : ℕ∞) ≤ ENat.card α
⊢ HAdd.hAdd (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞) ≤ ENat.card α
have hn₂ : LE.le (α := ℕ∞) (↑(m + n) : ℕ∞) (↑(Nat.card α) : ℕ∞)
Tactic: rwa [← ENat.coe_add, ENat.card_eq_coe_natCard, ENat.coe_le_coe]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Embedding (goal)
Goal:
α : Type u_1
m n : ℕ
inst : Finite α
hmn : m ≤ n
hn : n ≤ Nat.card α
⊢ Surjective (β := Fin m ↪ α) fun (x : Fin n ↪ α) ↦ (castLEEmb hmn).trans x
have obtain : ∀ (k : ℕ) (hmn : m ≤ m + k) (hn : m + k ≤ Nat.card α),
  Surjective (β := Fin m ↪ α) fun (x : Fin (m + k) ↪ α) ↦ (castLEEmb hmn).trans x
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
Cleared hypotheses: n, hmn, hn
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
⊢ Nat.card.{u_1} { x : α // p x } = s.card
have rw : Nat.card.{u_1} { x : α // p x } = Fintype.card.{u_1} { x : α // p x }
Tactic: rw [← Fintype.subtype_card s H, Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
rw : Nat.card.{u_1} { x : α // p x } = Fintype.card.{u_1} { x : α // p x }
⊢ Nat.card.{u_1} { x : α // p x } = s.card
have rw₁ : Nat.card.{u_1} { x : α // p x } = Nat.card.{u_1} { x : α // p x }
Tactic: rw [← Fintype.subtype_card s H, Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
inst : Finite α
⊢ (↑(Nat.card α) : Cardinal.{u_1}) = #α
have rw : #α < ℵ₀
Tactic: rw [Nat.card, Cardinal.cast_toNat_of_lt_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (hypothesis)
Goal:
α : Type u
β : Type v
inst : Finite α
f : α → β
hf : Surjective f
⊢ Nat.card β ≤ Nat.card α
have this : lift.{u, v} #β ≤ lift.{v, u} #α
Tactic: have : lift.{u} #β ≤ lift.{v} #α := mk_le_of_surjective (ULift.map_surjective.2 hf)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
⊢ Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β
have rw : Injective f → (Surjective f ↔ Nat.card α = Nat.card β)
Tactic: rw [Bijective, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
h : Injective f
⊢ Surjective f ↔ Nat.card α = Nat.card β
have have : ∀ (this : Fintype β), Surjective f ↔ Nat.card α = Nat.card β
Tactic: have := Fintype.ofFinite β
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
h : Injective f
this : Fintype β
⊢ Surjective f ↔ Nat.card α = Nat.card β
have have : ∀ (this : Fintype α), Surjective f ↔ Nat.card α = Nat.card β
Tactic: have := Fintype.ofInjective f h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
h : Injective f
this_1 : Fintype β
this : Fintype α
⊢ Surjective f ↔ Nat.card α = Nat.card β
have revert : ∀ (h : Injective f), Surjective f ↔ Nat.card α = Nat.card β
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
this_1 : Fintype β
this : Fintype α
⊢ ∀ (h : Injective f), Surjective f ↔ Nat.card α = Nat.card β
have rw : Injective f ∧ Surjective f ↔ Injective f ∧ Nat.card α = Nat.card β
Tactic: rw [← and_congr_right_iff, ← Bijective,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_injective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
this_1 : Fintype β
this : Fintype α
rw : Injective f ∧ Surjective f ↔ Injective f ∧ Nat.card α = Nat.card β
⊢ ∀ (h : Injective f), Surjective f ↔ Nat.card α = Nat.card β
have rw₁ : Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β
Tactic: rw [← and_congr_right_iff, ← Bijective,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_injective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
this_1 : Fintype β
this : Fintype α
rw : Injective f ∧ Surjective f ↔ Injective f ∧ Nat.card α = Nat.card β
rw₁ : Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β
⊢ ∀ (h : Injective f), Surjective f ↔ Nat.card α = Nat.card β
have rw₂ : Bijective f ↔ Injective f ∧ Fintype.card α = Nat.card β
Tactic: rw [← and_congr_right_iff, ← Bijective,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_injective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
this_1 : Fintype β
this : Fintype α
rw : Injective f ∧ Surjective f ↔ Injective f ∧ Nat.card α = Nat.card β
rw₁ : Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β
rw₂ : Bijective f ↔ Injective f ∧ Fintype.card α = Nat.card β
⊢ ∀ (h : Injective f), Surjective f ↔ Nat.card α = Nat.card β
have rw₃ : Bijective f ↔ Injective f ∧ Fintype.card α = Fintype.card β
Tactic: rw [← and_congr_right_iff, ← Bijective,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_injective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
this_1 : Fintype β
this : Fintype α
rw : Injective f ∧ Surjective f ↔ Injective f ∧ Nat.card α = Nat.card β
rw₁ : Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β
rw₂ : Bijective f ↔ Injective f ∧ Fintype.card α = Nat.card β
rw₃ : Bijective f ↔ Injective f ∧ Fintype.card α = Fintype.card β
⊢ ∀ (h : Injective f), Surjective f ↔ Nat.card α = Nat.card β
have rw₄ : Injective f ∧ Fintype.card α = Fintype.card β ↔ Injective f ∧ Fintype.card α = Fintype.card β
Tactic: rw [← and_congr_right_iff, ← Bijective,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_injective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β
have rw : Surjective f → (Injective f ↔ Nat.card α = Nat.card β)
Tactic: rw [_root_.and_comm, Bijective, and_congr_left_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
h : Surjective f
⊢ Injective f ↔ Nat.card α = Nat.card β
have have : ∀ (this : Fintype α), Injective f ↔ Nat.card α = Nat.card β
Tactic: have := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
h : Surjective f
this : Fintype α
⊢ Injective f ↔ Nat.card α = Nat.card β
have have : ∀ (this : Fintype β), Injective f ↔ Nat.card α = Nat.card β
Tactic: have := Fintype.ofSurjective f h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
h : Surjective f
this_1 : Fintype α
this : Fintype β
⊢ Injective f ↔ Nat.card α = Nat.card β
have revert : ∀ (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
this_1 : Fintype α
this : Fintype β
⊢ ∀ (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β
have rw : Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f
Tactic: rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
this_1 : Fintype α
this : Fintype β
rw : Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f
⊢ ∀ (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β
have rw₁ : Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f
Tactic: rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
this_1 : Fintype α
this : Fintype β
rw : Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₁ : Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f
⊢ ∀ (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β
have rw₂ : Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β
Tactic: rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
this_1 : Fintype α
this : Fintype β
rw : Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₁ : Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₂ : Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β
⊢ ∀ (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β
have rw₃ : Bijective f ↔ Surjective f ∧ Fintype.card α = Nat.card β
Tactic: rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
this_1 : Fintype α
this : Fintype β
rw : Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₁ : Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₂ : Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β
rw₃ : Bijective f ↔ Surjective f ∧ Fintype.card α = Nat.card β
⊢ ∀ (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β
have rw₄ : Bijective f ↔ Surjective f ∧ Fintype.card α = Fintype.card β
Tactic: rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
this_1 : Fintype α
this : Fintype β
rw : Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₁ : Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₂ : Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β
rw₃ : Bijective f ↔ Surjective f ∧ Fintype.card α = Nat.card β
rw₄ : Bijective f ↔ Surjective f ∧ Fintype.card α = Fintype.card β
⊢ ∀ (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β
have rw₅ : Surjective f ∧ Fintype.card α = Fintype.card β ↔ Surjective f ∧ Fintype.card α = Fintype.card β
Tactic: rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β
have rw : Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f
Tactic: classical
  rw [_root_.and_comm, Bijective, and_congr_left_iff]
  intro h
  have := Fintype.ofFinite α
  have := Fintype.ofSurjective f h
  revert h
  rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
rw : Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β
have rw₁ : Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f
Tactic: classical
  rw [_root_.and_comm, Bijective, and_congr_left_iff]
  intro h
  have := Fintype.ofFinite α
  have := Fintype.ofSurjective f h
  revert h
  rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
rw : Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₁ : Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β
have rw₂ : Surjective f → (Injective f ↔ Nat.card α = Nat.card β)
Tactic: classical
  rw [_root_.and_comm, Bijective, and_congr_left_iff]
  intro h
  have := Fintype.ofFinite α
  have := Fintype.ofSurjective f h
  revert h
  rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
rw : Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₁ : Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₂ rw₃ rw₄ rw₅ : ∀ (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β
have rw₆ : ∀ (h : Surjective f) (this : Fintype α), Injective f ↔ Nat.card α = Nat.card β
Tactic: classical
  rw [_root_.and_comm, Bijective, and_congr_left_iff]
  intro h
  have := Fintype.ofFinite α
  have := Fintype.ofSurjective f h
  revert h
  rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
rw : Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₁ : Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₂ rw₃ rw₄ rw₅ : ∀ (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β
rw₆ : ∀ (h : Surjective f) (this : Fintype α), Injective f ↔ Nat.card α = Nat.card β
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β
have rw₇ : ∀ (h : Surjective f) (this : Fintype α) (this : Fintype β), Injective f ↔ Nat.card α = Nat.card β
Tactic: classical
  rw [_root_.and_comm, Bijective, and_congr_left_iff]
  intro h
  have := Fintype.ofFinite α
  have := Fintype.ofSurjective f h
  revert h
  rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
rw : Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₁ : Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₂ rw₃ rw₄ rw₅ : ∀ (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β
rw₆ : ∀ (h : Surjective f) (this : Fintype α), Injective f ↔ Nat.card α = Nat.card β
rw₇ : ∀ (h : Surjective f) (this : Fintype α) (this : Fintype β), Injective f ↔ Nat.card α = Nat.card β
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β
have rw₈ : ∀ (this : Fintype α) (this : Fintype β) (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β
Tactic: classical
  rw [_root_.and_comm, Bijective, and_congr_left_iff]
  intro h
  have := Fintype.ofFinite α
  have := Fintype.ofSurjective f h
  revert h
  rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
n : ℕ
⊢ Nat.card (Fin n) = n
have rw : Fintype.card (Fin n) = n
Tactic: rw [Nat.card_eq_fintype_card, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
n : ℕ
rw : Fintype.card (Fin n) = n
⊢ Nat.card (Fin n) = n
have rw₁ : n = n
Tactic: rw [Nat.card_eq_fintype_card, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
have inl : ∀ (hs : s.Finite), Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
Tactic: obtain hs | hs := s.finite_or_infinite
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
inl : ∀ (hs : s.Finite), Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
have inr : ∀ (hs : s.Infinite), Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
Tactic: obtain hs | hs := s.finite_or_infinite
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
have inl : ∀ (this : Fintype (↑s : Type u_1)), Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
Tactic: have := hs.fintype
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
this : Fintype (↑s : Type u_1)
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
have inl : Fintype.card.{u_2} (↑(f '' s) : Type u_2) = Fintype.card.{u_1} (↑s : Type u_1)
Tactic: simp_rw [Nat.card_eq_fintype_card, Set.card_image_of_inj_on hf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
have this : Infinite.{u_1 + 1} (↑s : Type u_1)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
have this₁ : Infinite.{u_2 + 1} (↑(f '' s) : Type u_2)
Tactic: have := (hs.image hf).to_subtype
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
have inl : ∀ (hs : s.Finite), Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
Tactic: classical
  obtain hs | hs := s.finite_or_infinite
  · have := hs.fintype
    simp_rw [Nat.card_eq_fintype_card, Set.card_image_of_inj_on hf]
  · have := hs.to_subtype
    have := (hs.image hf).to_subtype
    simp [Nat.card_eq_zero_of_infinite]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
inl : ∀ (hs : s.Finite), Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
have inr : ∀ (hs : s.Infinite), Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
Tactic: classical
  obtain hs | hs := s.finite_or_infinite
  · have := hs.fintype
    simp_rw [Nat.card_eq_fintype_card, Set.card_image_of_inj_on hf]
  · have := hs.to_subtype
    have := (hs.image hf).to_subtype
    simp [Nat.card_eq_zero_of_infinite]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : InjOn f (f ⁻¹' s)
hsf : s ⊆ range f
⊢ Nat.card.{u_1} (↑(f ⁻¹' s) : Type u_1) = Nat.card.{u_2} (↑s : Type u_2)
have rw : Nat.card.{u_2} (↑(f '' f ⁻¹' s) : Type u_2) = Nat.card.{u_2} (↑s : Type u_2)
Tactic: rw [← Nat.card_image_of_injOn hf, image_preimage_eq_iff.2 hsf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : InjOn f (f ⁻¹' s)
hsf : s ⊆ range f
rw : Nat.card.{u_2} (↑(f '' f ⁻¹' s) : Type u_2) = Nat.card.{u_2} (↑s : Type u_2)
⊢ Nat.card.{u_1} (↑(f ⁻¹' s) : Type u_1) = Nat.card.{u_2} (↑s : Type u_2)
have rw₁ : Nat.card.{u_2} (↑s : Type u_2) = Nat.card.{u_2} (↑s : Type u_2)
Tactic: rw [← Nat.card_image_of_injOn hf, image_preimage_eq_iff.2 hsf]