awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fintype.CardEmbedding (goal)
Goal:
β : Type u_2
inst : Fintype β
⊢ ‖PEmpty.{u_1 + 1} ↪ β‖ = ‖β‖.descFactorial ‖PEmpty.{u_1 + 1}‖
have refine_2 : ∃ (x : PEmpty.{u_1 + 1} ↪ β), ∀ (y : PEmpty.{u_1 + 1} ↪ β), y = x
Tactic: rw [card_pempty, Nat.descFactorial_zero, card_eq_one_iff]
-- Lean 4 proof step from Mathlib.Data.Fintype.CardEmbedding (goal)
Goal:
β : Type u_2
inst : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
⊢ ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = ‖β‖.descFactorial (card.{u_1} (Option γ))
have refine_3 : ∑ i : γ ↪ β, card.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := γ) (⇑i : (a : γ) → β))ᶜ : Type u_2) = (‖β‖ - ‖γ‖) * ‖γ ↪ β‖
Tactic: rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β),
        card_sigma, ← ih]
-- Lean 4 proof step from Mathlib.Data.Fintype.CardEmbedding (goal)
Goal:
β : Type u_2
inst : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
⊢ ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = ‖β‖.descFactorial (card.{u_1} (Option γ))
have refine_3 : ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = ‖β‖.descFactorial (‖γ‖ + 1)
Tactic: classical
    rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β),
        card_sigma, ← ih]
    simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ,
      Nat.nsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Fintype.CardEmbedding (goal)
Goal:
β : Type u_2
inst : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
refine_3 : ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = ‖β‖.descFactorial (‖γ‖ + 1)
⊢ ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = ‖β‖.descFactorial (card.{u_1} (Option γ))
have refine_3₁ : ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = (‖β‖ - ‖γ‖) * ‖β‖.descFactorial ‖γ‖
Tactic: classical
    rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β),
        card_sigma, ← ih]
    simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ,
      Nat.nsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Fintype.CardEmbedding (goal)
Goal:
β : Type u_2
inst : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
refine_3 : ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = ‖β‖.descFactorial (‖γ‖ + 1)
refine_3₁ : ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = (‖β‖ - ‖γ‖) * ‖β‖.descFactorial ‖γ‖
⊢ ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = ‖β‖.descFactorial (card.{u_1} (Option γ))
have refine_3₂ : ‖(f : γ ↪ β) × (↑(Set.range.{u_2, u_1 + 1} (ι := γ) (⇑f : (a : γ) → β))ᶜ : Type u_2)‖ =
  (‖β‖ - ‖γ‖) * ‖β‖.descFactorial ‖γ‖
Tactic: classical
    rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β),
        card_sigma, ← ih]
    simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ,
      Nat.nsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Fintype.CardEmbedding (goal)
Goal:
β : Type u_2
inst : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
refine_3 : ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = ‖β‖.descFactorial (‖γ‖ + 1)
refine_3₁ : ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = (‖β‖ - ‖γ‖) * ‖β‖.descFactorial ‖γ‖
refine_3₂ :
  ‖(f : γ ↪ β) × (↑(Set.range.{u_2, u_1 + 1} (ι := γ) (⇑f : (a : γ) → β))ᶜ : Type u_2)‖ =
    (‖β‖ - ‖γ‖) * ‖β‖.descFactorial ‖γ‖
⊢ ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = ‖β‖.descFactorial (card.{u_1} (Option γ))
have refine_3₃ : ∑ i : γ ↪ β, card.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := γ) (⇑i : (a : γ) → β))ᶜ : Type u_2) =
  (‖β‖ - ‖γ‖) * ‖β‖.descFactorial ‖γ‖
Tactic: classical
    rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β),
        card_sigma, ← ih]
    simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ,
      Nat.nsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Fintype.CardEmbedding (goal)
Goal:
β : Type u_2
inst : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
refine_3 : ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = ‖β‖.descFactorial (‖γ‖ + 1)
refine_3₁ : ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = (‖β‖ - ‖γ‖) * ‖β‖.descFactorial ‖γ‖
refine_3₂ :
  ‖(f : γ ↪ β) × (↑(Set.range.{u_2, u_1 + 1} (ι := γ) (⇑f : (a : γ) → β))ᶜ : Type u_2)‖ =
    (‖β‖ - ‖γ‖) * ‖β‖.descFactorial ‖γ‖
refine_3₃ :
  ∑ i : γ ↪ β, card.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := γ) (⇑i : (a : γ) → β))ᶜ : Type u_2) =
    (‖β‖ - ‖γ‖) * ‖β‖.descFactorial ‖γ‖
⊢ ‖Embedding.{u_1 + 1, u_2 + 1} (Option γ) β‖ = ‖β‖.descFactorial (card.{u_1} (Option γ))
have refine_3₄ : ∑ i : γ ↪ β, card.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := γ) (⇑i : (a : γ) → β))ᶜ : Type u_2) = (‖β‖ - ‖γ‖) * ‖γ ↪ β‖
Tactic: classical
    rw [card_option, Nat.descFactorial_succ, card_congr (Embedding.optionEmbeddingEquiv γ β),
        card_sigma, ← ih]
    simp only [Fintype.card_compl_set, Fintype.card_range, Finset.sum_const, Finset.card_univ,
      Nat.nsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Fintype.Defs (goal)
Goal:
α : Type u_1
inst : Fintype α
⊢ (↑univ : Set α) = Set.univ
have h : ∀ (x : α), x ∈ (↑univ : Set α) ↔ Membership.mem (γ := Set α) Set.univ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Defs (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
⊢ (↑s : Set α) = Set.univ ↔ s = univ
have rw : (↑s : Set α) = (↑univ : Set α) ↔ s = univ
Tactic: rw [← coe_univ, coe_inj]
-- Lean 4 proof step from Mathlib.Data.Fintype.Defs (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
rw : (↑s : Set α) = (↑univ : Set α) ↔ s = univ
⊢ (↑s : Set α) = Set.univ ↔ s = univ
have rw₁ : s = univ ↔ s = univ
Tactic: rw [← coe_univ, coe_inj]
-- Lean 4 proof step from Mathlib.Data.Fintype.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
f : α → β
⊢ (Multiset.map f (val univ)).Nodup ↔ Injective f
have rw : Set.InjOn f (↑univ : Set α) ↔ Injective f
Tactic: rw [nodup_map_iff_injOn, coe_univ, Set.injOn_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
f : α → β
rw : Set.InjOn f (↑univ : Set α) ↔ Injective f
⊢ (Multiset.map f (val univ)).Nodup ↔ Injective f
have rw₁ : Set.InjOn f Set.univ ↔ Injective f
Tactic: rw [nodup_map_iff_injOn, coe_univ, Set.injOn_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
f : α → β
rw : Set.InjOn f (↑univ : Set α) ↔ Injective f
rw₁ : Set.InjOn f Set.univ ↔ Injective f
⊢ (Multiset.map f (val univ)).Nodup ↔ Injective f
have rw₂ : Injective f ↔ Injective f
Tactic: rw [nodup_map_iff_injOn, coe_univ, Set.injOn_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Defs (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
x x_1 : Fintype α
s₁ : Finset α
h₁ : ∀ (x : α), x ∈ s₁
s₂ : Finset α
h₂ : ∀ (x : α), x ∈ s₂
⊢ { elems := s₁, complete := h₁ : Fintype α } = { elems := s₂, complete := h₂ }
have e_elems : s₁ = s₂
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Fintype.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Bool
⊢ x ∈ { val := {true, false}, nodup := fintype._proof_1 : Finset Bool }
have false : false ∈ { val := {true, false}, nodup := fintype._proof_1 : Finset Bool }
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Fintype.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Bool
false : Bool.false ∈ { val := {true, Bool.false}, nodup := fintype._proof_1 : Finset Bool }
⊢ x ∈ { val := {true, Bool.false}, nodup := fintype._proof_1 : Finset Bool }
have true : true ∈ { val := {true, Bool.false}, nodup := fintype._proof_1 : Finset Bool }
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Fintype.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Ordering
⊢ x ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 : Finset Ordering }
have lt : lt ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 : Finset Ordering }
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Fintype.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Ordering
lt : Ordering.lt ∈ { val := {Ordering.lt, eq, gt}, nodup := fintype._proof_1 : Finset Ordering }
⊢ x ∈ { val := {Ordering.lt, eq, gt}, nodup := fintype._proof_1 : Finset Ordering }
have eq : eq ∈ { val := {Ordering.lt, eq, gt}, nodup := fintype._proof_1 : Finset Ordering }
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Fintype.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Ordering
lt : Ordering.lt ∈ { val := {Ordering.lt, Ordering.eq, gt}, nodup := fintype._proof_1 : Finset Ordering }
eq : Ordering.eq ∈ { val := {Ordering.lt, Ordering.eq, gt}, nodup := fintype._proof_1 : Finset Ordering }
⊢ x ∈ { val := {Ordering.lt, Ordering.eq, gt}, nodup := fintype._proof_1 : Finset Ordering }
have gt : gt ∈ { val := {Ordering.lt, Ordering.eq, gt}, nodup := fintype._proof_1 : Finset Ordering }
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Sort u_4
β : Sort u_5
inst : Finite β
f : α → β
H : Injective f
⊢ Finite α
have rcases : ∀ (n : ℕ) (e : β ≃ Fin n), Finite α
Tactic: rcases Finite.exists_equiv_fin β with ⟨n, ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
inst : Fintype α
⊢ card α = 1 ↔ ∃ (x : α), ∀ (y : α), y = x
have rw : Nonempty.{max 1 (u_1 + 1)} (α ≃ Unit) ↔ ∃ (x : α), ∀ (y : α), y = x
Tactic: rw [← card_unit, card_eq]
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
inst : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b : α
⊢ a = b
have let : ∀ (x : α) (hx : ∀ (y : α), y = x), a = b
Tactic: let ⟨x, hx⟩ := card_eq_one_iff.1 ha.symm
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
inst : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b x : α
hx : ∀ (y : α), y = x
⊢ a = b
have rw : x = b
Tactic: rw [hx a, hx b]
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
inst : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b x : α
hx : ∀ (y : α), y = x
rw : x = b
⊢ a = b
have rw₁ : x = x
Tactic: rw [hx a, hx b]
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
n_1 : ℕ := card α
hn : n_1 = card α
n : ℕ
ha : n + 2 = card α
h : card α ≤ 1
⊢ False
have h₁ : n + 2 ≤ 1
Tactic: rw [← ha] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
n_1 : ℕ := card α
hn : n_1 = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ False
have h₁ : (n + 2).le 0
Tactic: cases h with | step h => cases h;
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
inst : Fintype α
⊢ 1 < card α ↔ Nontrivial α
have contrapose! : card α ≤ 1 ↔ Subsingleton α
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
inst : Finite α
e : α ↪ α
⊢ e.equivOfFiniteSelfEmbedding.toEmbedding = e
have h : ∀ (x : α), Eq (α := α) ((e.equivOfFiniteSelfEmbedding.toEmbedding : (a : α) → α) x : α) ((e : (a : α) → α) x : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
s : Finset β
h : Fintype.card α ≤ #s
⊢ ∃ (f : α ↪ β), Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ⊆ (↑s : Set β)
have h₁ : Fintype.card α ≤ Fintype.card.{u_2} ↥s
Tactic: rw [← Fintype.card_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card.{u_2} ↥s
⊢ ∃ (f : α ↪ β), Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ⊆ (↑s : Set β)
have rcases : ∀ (f : Embedding.{u_1 + 1, u_2 + 1} α ↥s),
  ∃ (f : α ↪ β), Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ⊆ (↑s : Set β)
Tactic: rcases nonempty_of_card_le h with ⟨f⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
s : Finset β
hsn : Fintype.card α = #s
⊢ ∃ (f : α ↪ β), map f univ = s
have obtain : ∀ (f : α ↪ β) (hf : Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ⊆ (↑s : Set β)), ∃ (f : α ↪ β), map f univ = s
Tactic: obtain ⟨f : α ↪ β, hf⟩ := exists_of_card_le_finset (Nat.le_of_eq hsn)
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
s : Finset β
hsn : Fintype.card α = #s
f : α ↪ β
hf : Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ⊆ (↑s : Set β)
⊢ ∃ (f : α ↪ β), map f univ = s
have h : map f univ = s
Tactic: use f
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
s : Finset β
hsn : Fintype.card α = #s
f : α ↪ β
hf : Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ⊆ (↑s : Set β)
⊢ map f univ = s
have h : map f univ ⊆ s
Tactic: apply Finset.eq_of_subset_of_card_le
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
s : Finset β
hsn : Fintype.card α = #s
f : α ↪ β
hf : Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ⊆ (↑s : Set β)
h : map f univ ⊆ s
⊢ map f univ = s
have h₁ : #s ≤ #(map f univ)
Tactic: apply Finset.eq_of_subset_of_card_le
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_4
inst : Fintype α
e : α ↪ α
⊢ map e univ = univ
have rw : map e.equivOfFiniteSelfEmbedding.toEmbedding univ = univ
Tactic: rw [← e.toEmbedding_equivOfFiniteSelfEmbedding, univ_map_equiv_to_embedding]
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_4
inst : Fintype α
e : α ↪ α
rw : map e.equivOfFiniteSelfEmbedding.toEmbedding univ = univ
⊢ map e univ = univ
have rw₁ : Eq.{u_4 + 1} (α := Finset α) univ univ
Tactic: rw [← e.toEmbedding_equivOfFiniteSelfEmbedding, univ_map_equiv_to_embedding]
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → (↑s : Type u_1)
hf : Injective f
h : Fintype α
⊢ False
have refine : Fintype.card α < Fintype.card α
Tactic: refine lt_irrefl (Fintype.card α) ?_
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → (↑s : Type u_1)
hf : Injective f
h : Fintype α
⊢ s.toFinset ⊂ univ
have rwa : s ⊂ Set.univ
Tactic: rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → (↑s : Type u_1)
hf : Injective f
h : Fintype α
⊢ False
have refine : Fintype.card α < Fintype.card α
Tactic: classical
      refine lt_irrefl (Fintype.card α) ?_
      calc
        Fintype.card α ≤ Fintype.card s := Fintype.card_le_of_injective f hf
        _ = #s.toFinset := s.toFinset_card.symm
        _ < Fintype.card α :=
          Finset.card_lt_card <| by rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Infinite α
⊢ Infinite.{max 1 (u_1 + 1)} (Equiv.Perm α)
have obtain : ∀ (a : α), Infinite.{max 1 (u_1 + 1)} (Equiv.Perm α)
Tactic: obtain ⟨a : α⟩ := Nontrivial.to_nonempty (α := α)
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Infinite α
⊢ Infinite.{max 1 (u_1 + 1)} (Equiv.Perm α)
have obtain : ∀ (a : α), Infinite.{max 1 (u_1 + 1)} (Equiv.Perm α)
Tactic: classical
  obtain ⟨a : α⟩ := Nontrivial.to_nonempty (α := α)
  exact Infinite.of_injective _ (Equiv.swap_injective_of_left a)
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_4
inst : Infinite α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
⊢ m = n
have inr : ∀ (this : ∀ ⦃m n : ℕ⦄ (h : natEmbeddingAux α m = natEmbeddingAux α n) (hmlen : m ≤ n), m = n) (hmlen : ¬m ≤ n), m = n
Tactic: wlog hmlen : m ≤ n generalizing m n
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_4
inst : Infinite α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
this : DecidableEq α := Classical.decEq α
inr :
  ∀ (this : ∀ ⦃m n : ℕ⦄ (h : natEmbeddingAux α m = natEmbeddingAux α n) (hmlen : m ≤ n), m = n) (hmlen : ¬m ≤ n), m = n
⊢ m = n
have wlog : ∀ ⦃m n : ℕ⦄ (h : natEmbeddingAux α m = natEmbeddingAux α n) (hmlen : m ≤ n), m = n
Tactic: wlog hmlen : m ≤ n generalizing m n
Cleared hypotheses: m, n, h
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_4
inst : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
⊢ m = n
have by_contra : ∀ (hmn : ¬m = n), False
Tactic: by_contra hmn
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (hypothesis)
Goal:
α : Type u_4
inst : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
hmn : ¬m = n
⊢ False
have hmn₁ : m < n
Tactic: have hmn : m < n := lt_of_le_of_ne hmlen hmn
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_4
inst : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
hmn_1 : ¬m = n
hmn : m < n
⊢ False
have refine : Membership.mem (γ := Finset α)
  (Multiset.toFinset
    (Multiset.pmap (p := fun (m : ℕ) ↦ m < n) (fun (m : ℕ) (x : m < n) ↦ natEmbeddingAux α m) (Multiset.range n) sorry))
  (Classical.choose (p := fun (x : α) ↦
    x ∉
      Multiset.toFinset
        (Multiset.pmap (p := fun (m : ℕ) ↦ m < n) (fun (m : ℕ) (x : m < n) ↦ natEmbeddingAux α m) (Multiset.range n) sorry))
    sorry)
Tactic: refine (Classical.choose_spec (exists_notMem_finset
    ((Multiset.range n).pmap (fun m (_ : m < n) ↦ natEmbeddingAux α m)
      (fun _ ↦ Multiset.mem_range.1)).toFinset)) ?_
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_4
inst : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
hmn_1 : ¬m = n
hmn : m < n
⊢ Membership.mem (γ := Finset α)
    (Multiset.toFinset
      (Multiset.pmap (p := fun (m : ℕ) ↦ m < n) (fun (m : ℕ) (x : m < n) ↦ natEmbeddingAux α m) (Multiset.range n) ⋯))
    (Classical.choose (p := fun (x : α) ↦
      x ∉
        Multiset.toFinset
          (Multiset.pmap (p := fun (m : ℕ) ↦ m < n) (fun (m : ℕ) (x : m < n) ↦ natEmbeddingAux α m) (Multiset.range n)
            ⋯))
      ⋯)
have refine : natEmbeddingAux α m =
  Classical.choose (p := fun (x : α) ↦
    x ∉
      Multiset.toFinset
        (Multiset.pmap (p := fun (m : ℕ) ↦ m < n) (fun (m : ℕ) (x : m < n) ↦ natEmbeddingAux α m) (Multiset.range n) sorry))
    sorry
Tactic: refine Multiset.mem_toFinset.2 (Multiset.mem_pmap.2 ⟨m, Multiset.mem_range.2 hmn, ?_⟩)
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_4
inst : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
hmn_1 : ¬m = n
hmn : m < n
⊢ natEmbeddingAux α m =
    Classical.choose (p := fun (x : α) ↦
      x ∉
        Multiset.toFinset
          (Multiset.pmap (p := fun (m : ℕ) ↦ m < n) (fun (m : ℕ) (x : m < n) ↦ natEmbeddingAux α m) (Multiset.range n)
            ⋯))
      ⋯
have rw : natEmbeddingAux α n =
  Classical.choose (p := fun (x : α) ↦
    x ∉
      Multiset.toFinset
        (Multiset.pmap (p := fun (m : ℕ) ↦ m < n) (fun (m : ℕ) (x : m < n) ↦ natEmbeddingAux α m) (Multiset.range n) sorry))
    sorry
Tactic: rw [h, natEmbeddingAux]
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_4
inst : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
hmn_1 : ¬m = n
hmn : m < n
rw :
  natEmbeddingAux α n =
    Classical.choose (p := fun (x : α) ↦
      x ∉
        Multiset.toFinset
          (Multiset.pmap (p := fun (m : ℕ) ↦ m < n) (fun (m : ℕ) (x : m < n) ↦ natEmbeddingAux α m) (Multiset.range n)
            ⋯))
      ⋯
⊢ natEmbeddingAux α m =
    Classical.choose (p := fun (x : α) ↦
      x ∉
        Multiset.toFinset
          (Multiset.pmap (p := fun (m : ℕ) ↦ m < n) (fun (m : ℕ) (x : m < n) ↦ natEmbeddingAux α m) (Multiset.range n)
            ⋯))
      ⋯
have rw₁ : Classical.choose (p := fun (x : α) ↦
    x ∉
      Multiset.toFinset
        (Multiset.pmap (p := fun (m : ℕ) ↦ m < n) (fun (m : ℕ) (x : m < n) ↦ natEmbeddingAux α m) (Multiset.range n) sorry))
    sorry =
  Classical.choose (p := fun (x : α) ↦
    x ∉
      Multiset.toFinset
        (Multiset.pmap (p := fun (m : ℕ) ↦ m < n) (fun (m : ℕ) (x : m < n) ↦ natEmbeddingAux α m) (Multiset.range n) sorry))
    sorry
Tactic: rw [h, natEmbeddingAux]
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_4
inst : Infinite α
n : ℕ
⊢ #(map (natEmbedding α) (range n)) = n
have rw : #(range n) = n
Tactic: rw [card_map, card_range]
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_4
inst : Infinite α
n : ℕ
rw : #(range n) = n
⊢ #(map (natEmbedding α) (range n)) = n
have rw₁ : n = n
Tactic: rw [card_map, card_range]
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
inst : Infinite α
n : ℕ
IH : ∀ (s : Finset α) (hn : #s ≤ n), ∃ (t : Finset α), s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1
have succ : ∀ (hn' : #s = n + 1), ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1
Tactic: rcases hn.eq_or_lt with hn' | hn'
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
inst : Infinite α
n : ℕ
IH : ∀ (s : Finset α) (hn : #s ≤ n), ∃ (t : Finset α), s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
succ : ∀ (hn' : #s = n + 1), ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1
have succ₁ : ∀ (hn' : #s < n + 1), ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1
Tactic: rcases hn.eq_or_lt with hn' | hn'
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
inst : Infinite α
n : ℕ
IH : ∀ (s : Finset α) (hn : #s ≤ n), ∃ (t : Finset α), s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1
have succ : ∀ (t : Finset α) (hs : s ⊆ t) (ht : #t = n), ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1
Tactic: obtain ⟨t, hs, ht⟩ := IH _ (Nat.le_of_lt_succ hn')
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
inst : Infinite α
n : ℕ
IH : ∀ (s : Finset α) (hn : #s ≤ n), ∃ (t : Finset α), s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
t : Finset α
hs : s ⊆ t
ht : #t = n
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1
have succ : ∀ (x : α) (hx : x ∉ t), ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1
Tactic: obtain ⟨x, hx⟩ := exists_notMem_finset t
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
inst : Infinite α
n : ℕ
IH : ∀ (s : Finset α) (hn : #s ≤ n), ∃ (t : Finset α), s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
t : Finset α
hs : s ⊆ t
ht : #t = n
x : α
hx : x ∉ t
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1
have succ : #(cons x t hx) = n + 1
Tactic: refine ⟨Finset.cons x t hx, hs.trans (Finset.subset_cons _), ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.EquivFin (goal)
Goal:
α : Type u_1
inst : Infinite α
s : Finset α
n : ℕ
hn : #s ≤ n
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = n
have zero : ∀ (s : Finset α) (hn : #s ≤ 0), ∃ (t : Finset α), s ⊆ t ∧ #t = 0
Tactic: induction n generalizing s with
  | zero => exact ⟨s, subset_rfl, Nat.eq_zero_of_le_zero hn⟩
  | succ n IH =>
    rcases hn.eq_or_lt with hn' | hn'
    · exact ⟨s, subset_rfl, hn'⟩
    obtain ⟨t, hs, ht⟩ := IH _ (Nat.le_of_lt_succ hn')
    obtain ⟨x, hx⟩ := exists_notMem_finset t
    refine ⟨Finset.cons x t hx, hs.trans (Finset.subset_cons _), ?_⟩
    simp [ht]
Cleared hypotheses: s, n, hn