awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → (↑s : Type u_1)
hf : Injective f
h : Fintype α
refine : Fintype.card α < Fintype.card α
⊢ False

Tactic:
refine lt_irrefl (Fintype.card α) ?_

Premises used: lt_irrefl, Fintype.card
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → (↑s : Type u_1)
hf : Injective f
h : Fintype α
⊢ Fintype.card α ≤ Fintype.card.{u_1} (↑s : Type u_1)

Tactic:
Fintype.card_le_of_injective f hf

Premises used: Fintype.card_le_of_injective
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → (↑s : Type u_1)
hf : Injective f
h : Fintype α
⊢ Fintype.card.{u_1} (↑s : Type u_1) = #s.toFinset

Tactic:
s.toFinset_card.symm

Premises used: Set.toFinset_card, Eq.symm
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → (↑s : Type u_1)
hf : Injective f
h : Fintype α
rwa : s ⊂ Set.univ
rwa₁ rwa₂ rwa₃ rwa₄ : s ≠ Set.univ
⊢ s.toFinset ⊂ univ

Tactic:
rwa [Set.toFinset_ssubset_univ, Set.ssubset_univ_iff]

Premises used: Set.toFinset_ssubset_univ, Set.ssubset_univ_iff
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → (↑s : Type u_1)
hf : Injective f
h : Fintype α
⊢ Fintype.card α < Fintype.card α

Tactic:
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]

Premises used: Fintype.card_le_of_injective, Set.Elem, Fintype.card, Set.toFinset_card, Set.toFinset, Finset.card_lt_card, Eq.symm
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : α → (↑s : Type u_1)
hf : Injective f
h : Fintype α
refine : Fintype.card α < Fintype.card α
⊢ False

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]

Premises used: lt_irrefl, Fintype.card, Finset.card_lt_card
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
s : Set α
hs : s ≠ Set.univ
f : (↑s : Type u_1) → α
hf : Surjective f
⊢ Infinite α

Tactic:
of_injective_to_set hs (injective_surjInv hf)

Premises used: Infinite.of_injective_to_set, Function.injective_surjInv
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Infinite α
s : Finset α
⊢ ∃ (x : α), x ∉ s

Tactic:
not_forall.1 fun h => Fintype.false ⟨s, h⟩

Premises used: Fintype.false, Fintype.mk, Iff.mp, Classical.not_forall
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst : Infinite α
x : α
_hx : x ∉ ∅
y : α
hy : y ∉ {x}
⊢ y ≠ x

Tactic:
simpa only [mem_singleton] using hy

Premises used: Finset.mem_singleton
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_4
inst : Infinite α
⊢ Nonempty α

Tactic:
infer_instance
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Sort u_4
β : Sort u_5
inst : Infinite β
f : β → α
hf : Injective f
⊢ Infinite α

Tactic:
⟨fun _I => (Finite.of_injective f hf).false⟩

Premises used: Finite.false, Infinite.mk, Finite.of_injective
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Sort u_4
β : Sort u_5
inst : Infinite β
f : α → β
hf : Surjective f
⊢ Infinite α

Tactic:
⟨fun _I => (Finite.of_surjective f hf).false⟩

Premises used: Finite.false, Infinite.mk, Finite.of_surjective
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β_1 : Type u_2
γ : Type u_3
β : α → Type u_4
inst : Infinite α
inst_1 : ∀ (a : α), Nonempty.{u_4 + 1} (β a)
⊢ Infinite ((a : α) × β a)

Tactic:
Infinite.of_surjective Sigma.fst Sigma.fst_surjective

Premises used: Sigma.fst_surjective, Sigma.fst, Infinite.of_surjective
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : α → Type u_4
a : α
inst : Infinite.{u_4 + 1} (β a)
x x_1 : β a
⊢ Eq (α := (a : α) × β a) ((fun (x : β a) ↦ Sigma.mk (β := fun (a : α) ↦ β a) a x) x)
      ((fun (x : β a) ↦ Sigma.mk (β := fun (a : α) ↦ β a) a x) x_1) →
    x = x_1

Tactic:
simp
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β_1 : Type u_2
γ : Type u_3
β : α → Type u_4
inst : Nonempty α
inst_1 : ∀ (a : α), Infinite.{u_4 + 1} (β a)
⊢ Infinite ((a : α) × β a)

Tactic:
Infinite.sigma_of_right (a := Classical.arbitrary α)

Premises used: Infinite.sigma_of_right
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : Fintype ℕ
⊢ False

Tactic:
(Finset.range _).card_le_univ.not_gt ((Nat.lt_succ_self _).trans_eq (card_range _).symm)

Premises used: Finset.card_range, Nat.lt_succ_self, LT.lt.trans_eq, Finset.range, LE.le.not_gt, Finset.card_le_univ, Eq.symm
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : Fintype ℕ
⊢ False

Tactic:
exact (Finset.range _).card_le_univ.not_gt ((Nat.lt_succ_self _).trans_eq (card_range _).symm)

Premises used: Finset.card_range, Nat.lt_succ_self, LT.lt.trans_eq, Finset.range, LE.le.not_gt, Finset.card_le_univ, Eq.symm
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ Infinite ℤ

Tactic:
Infinite.of_injective Int.ofNat fun _ _ => Int.ofNat.inj

Premises used: Infinite.of_injective, Int.ofNat.inj, Int.ofNat
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
⊢ Infinite.{u_1 + 1} (Multiset α)

Tactic:
let ⟨x⟩ := ‹Nonempty α›
  Infinite.of_injective (fun n => Multiset.replicate n x) (Multiset.replicate_left_injective _)

Premises used: Infinite.of_injective, Multiset.replicate_left_injective, Multiset, _private.0.instInfiniteMultisetOfNonempty.match_1, Infinite, Multiset.replicate
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
⊢ Infinite.{u_1 + 1} (List α)

Tactic:
Infinite.of_surjective ((↑) : List α → Multiset α) Quot.mk_surjective

Premises used: Multiset.ofList, Quot.mk_surjective, Infinite.of_surjective
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ Infinite String

Tactic:
Infinite.of_injective String.ofList (fun _ _ => String.ofList_injective)

Premises used: Infinite.of_injective, String.ofList_injective, String.ofList
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Infinite α
⊢ Infinite.{u_1 + 1} (Set α)

Tactic:
Infinite.of_injective singleton Set.singleton_injective

Premises used: Infinite.of_injective, Set.singleton_injective, Singleton.singleton
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Infinite α
⊢ Infinite.{u_1 + 1} (Finset α)

Tactic:
Infinite.of_injective singleton Finset.singleton_injective

Premises used: Infinite.of_injective, Finset.singleton_injective, Singleton.singleton
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Infinite α
⊢ Infinite.{u_1 + 1} (Option α)

Tactic:
Infinite.of_injective some (Option.some_injective α)

Premises used: Infinite.of_injective, Option.some, Option.some_injective
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Infinite α
⊢ Infinite (α ⊕ β)

Tactic:
Infinite.of_injective Sum.inl Sum.inl_injective

Premises used: Infinite.of_injective, Sum.inl_injective, Sum.inl
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Infinite β
⊢ Infinite (α ⊕ β)

Tactic:
Infinite.of_injective Sum.inr Sum.inr_injective

Premises used: Infinite.of_injective, Sum.inr_injective, Sum.inr
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty α
inst_1 : Infinite β
⊢ Infinite (α × β)

Tactic:
Infinite.of_surjective Prod.snd Prod.snd_surjective

Premises used: Prod.snd_surjective, Infinite.of_surjective, Prod.snd
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Infinite α
inst_1 : Nonempty β
⊢ Infinite (α × β)

Tactic:
Infinite.of_surjective Prod.fst Prod.fst_surjective

Premises used: Prod.fst_surjective, Prod.fst, Infinite.of_surjective
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Infinite α
obtain : ∀ (a : α), Infinite.{max 1 (u_1 + 1)} (Equiv.Perm α)
⊢ Infinite.{max 1 (u_1 + 1)} (Equiv.Perm α)

Tactic:
obtain ⟨a : α⟩ := Nontrivial.to_nonempty (α := α)

Premises used: Nontrivial.to_nonempty
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Infinite α
a : α
⊢ Infinite.{max 1 (u_1 + 1)} (Equiv.Perm α)

Tactic:
Infinite.of_injective _ (Equiv.swap_injective_of_left a)

Premises used: Infinite.of_injective, Equiv.swap_injective_of_left
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Infinite α
a : α
⊢ Infinite.{max 1 (u_1 + 1)} (Equiv.Perm α)

Tactic:
exact Infinite.of_injective _ (Equiv.swap_injective_of_left a)

Premises used: Infinite.of_injective, Equiv.swap_injective_of_left
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Infinite α
obtain : ∀ (a : α), Infinite.{max 1 (u_1 + 1)} (Equiv.Perm α)
⊢ 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)

Premises used: Nontrivial.to_nonempty
-- Module: Mathlib.Data.Fintype.EquivFin
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
wlog : ∀ ⦃m n : ℕ⦄ (h : natEmbeddingAux α m = natEmbeddingAux α n) (hmlen : m ≤ n), m = n
⊢ m = n

Tactic:
wlog hmlen : m ≤ n generalizing m n
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_4
inst : Infinite α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
this_1 : DecidableEq α := Classical.decEq α
this : ∀ ⦃m n : ℕ⦄ (h : natEmbeddingAux α m = natEmbeddingAux α n) (hmlen : m ≤ n), m = n
hmlen : ¬m ≤ n
⊢ m = n

Tactic:
(this h.symm <| le_of_not_ge hmlen).symm

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_4
inst : Infinite α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
this_1 : DecidableEq α := Classical.decEq α
this : ∀ ⦃m n : ℕ⦄ (h : natEmbeddingAux α m = natEmbeddingAux α n) (hmlen : m ≤ n), m = n
hmlen : ¬m ≤ n
⊢ m = n

Tactic:
exact (this h.symm <| le_of_not_ge hmlen).symm

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_4
inst : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
by_contra : ∀ (hmn : ¬m = n), False
⊢ m = n

Tactic:
by_contra hmn
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_4
inst : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
hmn : ¬m = n
⊢ m < n

Tactic:
have hmn : m < n := lt_of_le_of_ne hmlen hmn
-- Module: Mathlib.Data.Fintype.EquivFin
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

Tactic:
(Classical.choose_spec (exists_notMem_finset
    ((Multiset.range n).pmap (fun m (_ : m < n) ↦ natEmbeddingAux α m)
      (fun _ ↦ Multiset.mem_range.1)).toFinset)) ?_

Premises used: Multiset.toFinset, Multiset.mem_range, Classical.choose_spec, Infinite.exists_notMem_finset, Multiset.pmap, Iff.mp, Multiset.range, _private.0.Infinite.natEmbeddingAux
-- Module: Mathlib.Data.Fintype.EquivFin
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
refine :
  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)
            ⋯))
      ⋯)
⊢ False

Tactic:
refine (Classical.choose_spec (exists_notMem_finset
    ((Multiset.range n).pmap (fun m (_ : m < n) ↦ natEmbeddingAux α m)
      (fun _ ↦ Multiset.mem_range.1)).toFinset)) ?_

Premises used: Multiset.toFinset, Multiset.mem_range, Classical.choose_spec, Infinite.exists_notMem_finset, Multiset.pmap, Iff.mp, Multiset.range, _private.0.Infinite.natEmbeddingAux
-- Module: Mathlib.Data.Fintype.EquivFin
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)
            ⋯))
      ⋯)

Tactic:
Multiset.mem_toFinset.2 (Multiset.mem_pmap.2 ⟨m, Multiset.mem_range.2 hmn, ?_⟩)

Premises used: Iff.mpr, Multiset.mem_range, Exists.intro, Multiset.mem_toFinset, Multiset.mem_pmap
-- Module: Mathlib.Data.Fintype.EquivFin
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
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)
            ⋯))
      ⋯
⊢ 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)
            ⋯))
      ⋯)

Tactic:
refine Multiset.mem_toFinset.2 (Multiset.mem_pmap.2 ⟨m, Multiset.mem_range.2 hmn, ?_⟩)

Premises used: Iff.mpr, Multiset.mem_range, Exists.intro, Multiset.mem_toFinset, Multiset.mem_pmap
-- Module: Mathlib.Data.Fintype.EquivFin
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)
            ⋯))
      ⋯
rw₁ 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)
            ⋯))
      ⋯ =
    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)
            ⋯))
      ⋯

Tactic:
rw [h, natEmbeddingAux]

Premises used: _private.0.Infinite.natEmbeddingAux
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_4
inst : Infinite α
n : ℕ
rw : #(range n) = n
rw₁ rw₂ : n = n
⊢ #(map (natEmbedding α) (range n)) = n

Tactic:
rw [card_map, card_range]

Premises used: Finset.card_map, Finset.card_range
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Infinite α
s : Finset α
hn : #s ≤ 0
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = 0

Tactic:
⟨s, subset_rfl, Nat.eq_zero_of_le_zero hn⟩

Premises used: And.intro, Exists.intro, subset_rfl, Nat.eq_zero_of_le_zero
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Infinite α
s : Finset α
hn : #s ≤ 0
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = 0

Tactic:
exact ⟨s, subset_rfl, Nat.eq_zero_of_le_zero hn⟩
-- Module: Mathlib.Data.Fintype.EquivFin
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
succ₁ : ∀ (hn' : #s < n + 1), ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1

Tactic:
rcases hn.eq_or_lt with hn' | hn'

Premises used: LE.le.eq_or_lt
-- Module: Mathlib.Data.Fintype.EquivFin
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

Tactic:
⟨s, subset_rfl, hn'⟩

Premises used: And.intro, Exists.intro, subset_rfl
-- Module: Mathlib.Data.Fintype.EquivFin
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

Tactic:
exact ⟨s, subset_rfl, hn'⟩
-- Module: Mathlib.Data.Fintype.EquivFin
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
succ : ∀ (t : Finset α) (hs : s ⊆ t) (ht : #t = n), ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1

Tactic:
obtain ⟨t, hs, ht⟩ := IH _ (Nat.le_of_lt_succ hn')

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.Data.Fintype.EquivFin
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
succ : ∀ (x : α) (hx : x ∉ t), ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1

Tactic:
obtain ⟨x, hx⟩ := exists_notMem_finset t

Premises used: Infinite.exists_notMem_finset
-- Module: Mathlib.Data.Fintype.EquivFin
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

Tactic:
⟨Finset.cons x t hx, hs.trans (Finset.subset_cons _), ?_⟩

Premises used: Finset.cons, HasSubset.Subset.trans, Finset.subset_cons, And.intro, Exists.intro
-- Module: Mathlib.Data.Fintype.EquivFin
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
succ : #(cons x t hx) = n + 1
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = n + 1

Tactic:
refine ⟨Finset.cons x t hx, hs.trans (Finset.subset_cons _), ?_⟩
-- Module: Mathlib.Data.Fintype.EquivFin
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
⊢ #(cons x t hx) = n + 1

Tactic:
simp [ht]
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Infinite α
s : Finset α
n : ℕ
hn : #s ≤ n
zero : ∀ (s : Finset α) (hn : #s ≤ 0), ∃ (t : Finset α), s ⊆ t ∧ #t = 0
succ :
  ∀ (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
⊢ ∃ (t : Finset α), s ⊆ t ∧ #t = n

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]

Premises used: LE.le.eq_or_lt
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), #s ≤ n
h : ¬Infinite ι
⊢ Fintype ι

Tactic:
apply fintypeOfNotInfinite

Premises used: fintypeOfNotInfinite
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), #s ≤ n
i : Infinite ι
h : ∀ (s : Finset ι) (c : #s = n + 1), False
⊢ False

Tactic:
obtain ⟨s, c⟩ := Infinite.exists_subset_card_eq ι (n + 1)

Premises used: Infinite.exists_subset_card_eq, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), #s ≤ n
i : Infinite ι
s : Finset ι
c : #s = n + 1
⊢ #s ≤ n

Tactic:
specialize w s
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
i : Infinite ι
s : Finset ι
c : #s = n + 1
w : #s ≤ n
⊢ n + 1 ≤ n

Tactic:
rw [c] at w
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
i : Infinite ι
s : Finset ι
c : #s = n + 1
w : n + 1 ≤ n
⊢ False

Tactic:
Nat.not_succ_le_self n w

Premises used: Nat.not_succ_le_self
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
i : Infinite ι
s : Finset ι
c : #s = n + 1
w : n + 1 ≤ n
⊢ False

Tactic:
exact Nat.not_succ_le_self n w

Premises used: Nat.not_succ_le_self
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Sort u_4
β : Sort u_5
inst : Infinite α
inst_1 : Finite β
f : α → β
⊢ ¬Injective f

Tactic:
fun hf => (Finite.of_injective f hf).false

Premises used: Finite.false, Not, Finite.of_injective
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
α : Sort u_4
β : Sort u_5
inst : Infinite α
inst_1 : Finite β
⊢ IsEmpty (α ↪ β)

Tactic:
⟨fun f => not_injective_infinite_finite f f.2⟩

Premises used: not_injective_infinite_finite, Function.Embedding.inj', IsEmpty.mk, DFunLike.coe
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Sort u_4
β : Sort u_5
inst : Finite α
inst_1 : Infinite β
f : α → β
⊢ ¬Surjective f

Tactic:
fun hf => (Infinite.of_surjective f hf).not_finite ‹_›

Premises used: Infinite.not_finite, Not
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n : ℕ
h : ∀ (a : ℕ), a ∈ map (α := Fin n) valEmbedding univ ↔ a ∈ Iio n
⊢ map (α := Fin n) valEmbedding univ = Iio n

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n a : ℕ
⊢ a ∈ map (α := Fin n) valEmbedding univ ↔ a ∈ Iio n

Tactic:
simp [orderIsoSubtype.symm.surjective.exists, OrderIso.symm]

Premises used: Function.Surjective.exists, OrderIso.surjective, OrderIso.symm, Fin.orderIsoSubtype
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n : ℕ
h : ∀ (x : Fin n.succ), x ∈ (↑(Ioi 0) : Set (Fin n.succ)) ↔ x ∈ (↑(map (succEmb n) univ) : Set (Fin n.succ))
⊢ (↑(Ioi 0) : Set (Fin n.succ)) = (↑(map (succEmb n) univ) : Set (Fin n.succ))

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n : ℕ
x : Fin n.succ
⊢ x ∈ (↑(Ioi 0) : Set (Fin n.succ)) ↔ x ∈ (↑(map (succEmb n) univ) : Set (Fin n.succ))

Tactic:
simp [pos_iff_ne_zero]

Premises used: Fin.pos_iff_ne_zero
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n : ℕ
h : ∀ (x : Fin (n + 1)), x ∈ (↑(Iio (last n)) : Set (Fin (n + 1))) ↔ x ∈ (↑(map castSuccEmb univ) : Set (Fin (n + 1)))
⊢ (↑(Iio (last n)) : Set (Fin (n + 1))) = (↑(map castSuccEmb univ) : Set (Fin (n + 1)))

Tactic:
ext
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n : ℕ
x : Fin (n + 1)
⊢ x ∈ (↑(Iio (last n)) : Set (Fin (n + 1))) ↔ x ∈ (↑(map castSuccEmb univ) : Set (Fin (n + 1)))

Tactic:
simp [lt_def]

Premises used: Fin.lt_def
-- Module: Mathlib.Data.Fintype.Fin
Goal:
n : ℕ
i : Fin n
⊢ Ioi i.succ = map (succEmb n) (Ioi i)

Tactic:
simp