awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
rw : (↑s : Set α) = (↑univ : Set α) ↔ s = univ
rw₁ rw₂ : s = univ ↔ s = univ
⊢ (↑s : Set α) = Set.univ ↔ s = univ

Tactic:
rw [← coe_univ, coe_inj]

Premises used: Finset.coe_univ, Finset.coe_inj
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
⊢ s ⊆ univ

Tactic:
fun a _ => mem_univ a

Premises used: Finset.mem_univ
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
⊢ ∀ (x : α), x ∈ filter p univ ↔ p x

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
α : Type u_5
β : α → Type u_4
inst : (a : α) → DecidableEq (β a)
inst_1 : Fintype α
f g : (a : α) → β a
⊢ (∀ (a : α), Membership.mem (γ := Finset α) univ a → f a = g a) ↔ f = g

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst : DecidablePred p
inst_1 : Fintype α
⊢ (∀ (a : α), Membership.mem (γ := Finset α) univ a → p a) ↔ ∀ (a : α), p a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst : DecidablePred p
inst_1 : Fintype α
⊢ (∃ (a : α), Membership.mem (γ := Finset α) univ a ∧ p a) ↔ ∃ (a : α), p a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Defs
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
rw₂ rw₃ : Injective f ↔ Injective f
⊢ (Multiset.map f (val univ)).Nodup ↔ Injective f

Tactic:
rw [nodup_map_iff_injOn, coe_univ, Set.injOn_univ]

Premises used: Finset.coe_univ, Finset.nodup_map_iff_injOn, Set.injOn_univ
-- Module: Mathlib.Data.Fintype.Defs
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₂
e_elems : s₁ = s₂
⊢ { elems := s₁, complete := h₁ : Fintype α } = { elems := s₂, complete := h₂ }

Tactic:
congr
-- Module: Mathlib.Data.Fintype.Defs
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₂
⊢ s₁ = s₂

Tactic:
simp [Finset.ext_iff, h₁, h₂]

Premises used: Finset.ext_iff
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
⊢ Lean.Meta.FastSubsingleton.{u_4 + 1} (Fintype α)

Tactic:

Premises used: Lean.Meta.FastSubsingleton.mk
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ Multiset.Nodup (α := Bool) {true, false}

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Bool
false : Bool.false ∈ { val := {Bool.true, Bool.false}, nodup := fintype._proof_1 : Finset Bool }
true : Bool.true ∈ { val := {Bool.true, Bool.false}, nodup := fintype._proof_1 : Finset Bool }
⊢ x ∈ { val := {Bool.true, Bool.false}, nodup := fintype._proof_1 : Finset Bool }

Tactic:
cases x
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ false ∈ { val := {true, false}, nodup := fintype._proof_1 : Finset Bool }

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ true ∈ { val := {true, false}, nodup := fintype._proof_1 : Finset Bool }

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ Multiset.Nodup (α := Ordering) {lt, eq, gt}

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Ordering
lt : Ordering.lt ∈ { val := {Ordering.lt, Ordering.eq, Ordering.gt}, nodup := fintype._proof_1 : Finset Ordering }
eq : Ordering.eq ∈ { val := {Ordering.lt, Ordering.eq, Ordering.gt}, nodup := fintype._proof_1 : Finset Ordering }
gt : Ordering.gt ∈ { val := {Ordering.lt, Ordering.eq, Ordering.gt}, nodup := fintype._proof_1 : Finset Ordering }
⊢ x ∈ { val := {Ordering.lt, Ordering.eq, Ordering.gt}, nodup := fintype._proof_1 : Finset Ordering }

Tactic:
cases x
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ lt ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 : Finset Ordering }

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ eq ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 : Finset Ordering }

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ gt ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 : Finset Ordering }

Tactic:
simp
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst : DecidableEq α
inst_1 : Fintype α
⊢ Trunc (α ≃ Fin (Multiset.card.{u_4} (α := α) (val univ)))

Tactic:
exact
    Quot.recOnSubsingleton
      (motive := fun s : Multiset α =>
        (∀ x : α, x ∈ s) → s.Nodup → Trunc (α ≃ Fin (Multiset.card s)))
      univ.val
      (fun l (h : ∀ x : α, x ∈ l) (nd : l.Nodup) => Trunc.mk (nd.getEquivOfForallMemList _ h).symm)
      mem_univ_val univ.2

Premises used: Finset.univ, Finset.mem_univ_val, Quot.recOnSubsingleton, Finset.nodup, Finset.val, Trunc.mk, Equiv.symm, List.Nodup.getEquivOfForallMemList
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst : Fintype α
⊢ Trunc { f : Fin (Multiset.card.{u_4} (α := α) (val univ)) → α // Bijective f }

Tactic:
refine
    Quot.recOnSubsingleton
      (motive := fun s : Multiset α =>
        (∀ x : α, x ∈ s) → s.Nodup → Trunc {f : Fin (Multiset.card s) → α // Bijective f})
      univ.val
      (fun l (h : ∀ x : α, x ∈ l) (nd : l.Nodup) => Trunc.mk (nd.getBijectionOfForallMemList _ h))
      mem_univ_val univ.2

Premises used: Finset.univ, Finset.mem_univ_val, Quot.recOnSubsingleton, Finset.nodup, Finset.val, Trunc.mk, List.Nodup.getBijectionOfForallMemList
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Fintype α
inst_1 : Fintype β
h : card α = card β
this_1 : DecidableEq α := Classical.decEq α
this : DecidableEq β := Classical.decEq β
⊢ α ≃ β

Tactic:
exact (truncEquivOfCardEq h).out

Premises used: Fintype.truncEquivOfCardEq, Trunc.out
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_4
β : Type u_5
_F : Fintype α
_G : Fintype β
⊢ card α = card β ↔ Nonempty (α ≃ β)

Tactic:
⟨fun h =>
    haveI := Classical.propDecidable
    (truncEquivOfCardEq h).nonempty,
    fun ⟨f⟩ => card_congr f⟩

Premises used: Fintype.card_congr, _private.0.Fintype.card_eq.match_1, Fintype.card, Iff.intro, Trunc.nonempty, Eq, Fintype.truncEquivOfCardEq
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_4
_inst : Fintype α
⊢ Finite α

Tactic:
⟨Fintype.equivFin α⟩

Premises used: Finite.intro, Fintype.equivFin
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst : Fintype α
⊢ Finite α

Tactic:
Fintype.finite ‹_›

Premises used: Fintype.finite
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_4
⊢ Finite α ↔ Nonempty.{u_4 + 1} (Fintype α)

Tactic:
⟨fun _ => nonempty_fintype α, fun ⟨_⟩ => inferInstance⟩

Premises used: Finite, inferInstance, nonempty_fintype, Iff.intro, _private.0.finite_iff_nonempty_fintype.match_1
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Sort u_4
β : Sort u_5
inst : Finite β
f : α → β
H : Injective f
rcases : ∀ (n : ℕ) (e : β ≃ Fin n), Finite α
⊢ Finite α

Tactic:
rcases Finite.exists_equiv_fin β with ⟨n, ⟨e⟩⟩

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Sort u_4
β : Sort u_5
inst : Finite β
f : α → β
H : Injective f
n : ℕ
e : β ≃ Fin n
⊢ Finite α

Tactic:
.of_equiv (Set.range (e ∘ f)) (Equiv.ofInjective _ (e.injective.comp H)).symm

Premises used: Finite.of_equiv, Function.comp, Set.Elem, Equiv.ofInjective, Function.Injective.comp, Equiv.injective, Set.range, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Sort u_4
β : Sort u_5
inst : Finite β
f : α → β
H : Injective f
n : ℕ
e : β ≃ Fin n
⊢ Finite α

Tactic:
exact .of_equiv (Set.range (e ∘ f)) (Equiv.ofInjective _ (e.injective.comp H)).symm
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Sort u_4
β : Sort u_5
inst : Finite β
f : α → β
H : Injective f
n : ℕ
e : β ≃ Fin n
⊢ Finite α

Tactic:
classical exact .of_equiv (Set.range (e ∘ f)) (Equiv.ofInjective _ (e.injective.comp H)).symm
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Sort u_4
inst : Subsingleton α
⊢ Finite α

Tactic:
Finite.of_injective (Function.const α ()) <| Function.injective_of_subsingleton _

Premises used: Unit.unit, Function.injective_of_subsingleton, Function.const, Finite.of_injective
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
⊢ Finite p

Tactic:
Finite.of_subsingleton

Premises used: Finite.of_subsingleton
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Sort u_4
inst : Finite α
p : α → Prop
⊢ Finite.{max 1 u_4} { x : α // p x }

Tactic:
Finite.of_injective Subtype.val Subtype.coe_injective

Premises used: Subtype.coe_injective, Subtype.val, Finite.of_injective
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Sort u_4
β : Sort u_5
inst : Finite α
f : α → β
H : Surjective f
⊢ Finite β

Tactic:
Finite.of_injective _ <| injective_surjInv H

Premises used: Function.injective_surjInv, Finite.of_injective
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Sort u_4
inst : Finite α
r : α → α → Prop
⊢ Finite.{u_4} (Quot r)

Tactic:
Finite.of_surjective _ Quot.mk_surjective

Premises used: Quot.mk_surjective, Finite.of_surjective
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Sort u_4
inst : Finite α
s : Setoid α
⊢ Finite.{u_4} (Quotient s)

Tactic:
Quot.finite _

Premises used: Quot.finite, Quotient
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
rw : Nonempty.{max 1 (u_1 + 1)} (α ≃ Unit) ↔ ∃ (x : α), ∀ (y : α), y = x
⊢ card α = 1 ↔ ∃ (x : α), ∀ (y : α), y = x

Tactic:
rw [← card_unit, card_eq]

Premises used: Fintype.card_eq, Fintype.card_unit
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
⊢ Nonempty.{max 1 (u_1 + 1)} (α ≃ Unit) ↔ ∃ (x : α), ∀ (y : α), y = x

Tactic:
⟨fun ⟨a⟩ => ⟨a.symm (), fun y => a.injective (Subsingleton.elim _ _)⟩,
     fun ⟨x, hx⟩ =>
      ⟨⟨fun _ => (), fun _ => x, fun _ => (hx _).trans (hx _).symm, fun _ =>
          Subsingleton.elim _ _⟩⟩⟩

Premises used: Unit.unit, _private.0.Fintype.card_eq_one_iff.match_2, Exists, Equiv.mk, Equiv, Nonempty.intro, Unit, Iff.intro, Exists.intro, Nonempty, Equiv.injective, Equiv.symm, Subsingleton.elim, Eq.symm, DFunLike.coe, _private.0.Fintype.card_eq_one_iff.match_1, Eq.trans
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
⊢ Nonempty.{max 1 (u_1 + 1)} (α ≃ Unit) ↔ ∃ (x : α), ∀ (y : α), y = x

Tactic:
exact
    ⟨fun ⟨a⟩ => ⟨a.symm (), fun y => a.injective (Subsingleton.elim _ _)⟩,
     fun ⟨x, hx⟩ =>
      ⟨⟨fun _ => (), fun _ => x, fun _ => (hx _).trans (hx _).symm, fun _ =>
          Subsingleton.elim _ _⟩⟩⟩
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
⊢ card α = 1 ↔ Nonempty.{max 1 (u_1 + 1)} (Unique α)

Tactic:
⟨fun h =>
    let ⟨d, h⟩ := Fintype.card_eq_one_iff.mp h
    ⟨{  default := d
        uniq := h }⟩,
    fun ⟨_h⟩ => Fintype.card_unique⟩

Premises used: Unique.mk, Unique, _private.0.Fintype.card_eq_one_iff.match_2, Fintype.card, Nonempty.intro, Fintype.card_unique, Iff.intro, Iff.mp, Nonempty, OfNat.ofNat, Eq, Fintype.card_eq_one_iff, _private.0.Fintype.card_eq_one_iff_nonempty_unique.match_1, Inhabited.mk
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b : α
let : ∀ (x : α) (hx : ∀ (y : α), y = x), a = b
⊢ a = b

Tactic:
let ⟨x, hx⟩ := card_eq_one_iff.1 ha.symm
-- Module: Mathlib.Data.Fintype.EquivFin
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
rw₁ rw₂ : x = x
⊢ a = b

Tactic:
rw [hx a, hx b]
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
n_1 : ℕ := card α
hn : n_1 = card α
n : ℕ
ha : n + 2 = card α
h : card α ≤ 1
⊢ n + 2 ≤ 1

Tactic:
rw [← ha] at h
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
n_1 : ℕ := card α
hn : n_1 = card α
n : ℕ
ha : n + 2 = card α
h : (n + 2).le 0
⊢ False

Tactic:
cases h
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
n_1 : ℕ := card α
hn : n_1 = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ (n + 2).le 0

Tactic:
cases h with | step h => cases h;
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
⊢ card α ≤ 1 ↔ Subsingleton α

Tactic:
card_le_one_iff.trans subsingleton_iff.symm

Premises used: subsingleton_iff, Fintype.card_le_one_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
contrapose! : card α ≤ 1 ↔ Subsingleton α
⊢ 1 < card α ↔ Nontrivial α

Tactic:
contrapose!
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
⊢ card α ≤ 1 ↔ Subsingleton α

Tactic:
card_le_one_iff_subsingleton

Premises used: Fintype.card_le_one_iff_subsingleton
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
⊢ card α ≤ 1 ↔ Subsingleton α

Tactic:
exact card_le_one_iff_subsingleton

Premises used: Fintype.card_le_one_iff_subsingleton
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
h : 1 < card α
a : α
⊢ ∃ (b : α), b ≠ a

Tactic:
haveI : Nontrivial α := one_lt_card_iff_nontrivial.1 h
  exists_ne a

Premises used: exists_ne
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
h : 1 < card α
⊢ ∃ (a : α) (b : α), a ≠ b

Tactic:
haveI : Nontrivial α := one_lt_card_iff_nontrivial.1 h
  exists_pair_ne α

Premises used: exists_pair_ne
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
i : α
h : ∀ (j : α), j = i
⊢ card α = 1

Tactic:
Fintype.card_eq_one_iff.2 ⟨i, h⟩

Premises used: Iff.mpr, Exists.intro, Fintype.card_eq_one_iff
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
h : Nontrivial α
⊢ 1 < card α

Tactic:
Fintype.one_lt_card_iff_nontrivial.mpr h

Premises used: Iff.mpr, Fintype.one_lt_card_iff_nontrivial
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Fintype α
⊢ 1 < card α ↔ ∃ (a : α) (b : α), a ≠ b

Tactic:
one_lt_card_iff_nontrivial.trans nontrivial_iff

Premises used: Fintype.one_lt_card_iff_nontrivial, nontrivial_iff, Iff.trans
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
⊢ Bijective f ↔ Injective f ∧ card α = card β

Tactic:
⟨fun h => ⟨h.1, card_of_bijective h⟩, fun h =>
    ⟨h.1, h.1.surjective_of_finite <| equivOfCardEq h.2⟩⟩

Premises used: Function.Injective.surjective_of_finite, Fintype.card_of_bijective, And.right, And.left, And.intro, Iff.intro, Fintype.equivOfCardEq
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
⊢ Bijective f ↔ Surjective f ∧ card α = card β

Tactic:
⟨fun h => ⟨h.2, card_of_bijective h⟩, fun h =>
    ⟨h.1.injective_of_finite <| equivOfCardEq h.2, h.1⟩⟩

Premises used: Fintype.card_of_bijective, And.right, Function.Surjective.injective_of_finite, And.left, And.intro, Iff.intro, Fintype.equivOfCardEq
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
g : β → α
hfg : LeftInverse f g
hcard : card α ≤ card β
⊢ RightInverse f g

Tactic:
have hsurj : Surjective f := surjective_iff_hasRightInverse.2 ⟨g, hfg⟩
  rightInverse_of_injective_of_leftInverse
    ((bijective_iff_surjective_and_card _).2
        ⟨hsurj, le_antisymm hcard (card_le_of_surjective f hsurj)⟩).1
    hfg

Premises used: Iff.mpr, Function.surjective_iff_hasRightInverse, Function.rightInverse_of_injective_of_leftInverse, Fintype.bijective_iff_surjective_and_card, le_antisymm, And.left, And.intro, Exists.intro, Fintype.card_le_of_surjective
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
g : β → α
hfg : RightInverse f g
hcard : card β ≤ card α
⊢ LeftInverse f g

Tactic:
Function.LeftInverse.rightInverse_of_card_le hfg hcard

Premises used: Function.LeftInverse.rightInverse_of_card_le, Function.RightInverse
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
s : Finset α
n : ℕ
i : ↥s ≃ Fin n
⊢ #s = n

Tactic:
Fin.equiv_iff_eq.1 ⟨s.equivFin.symm.trans i⟩

Premises used: Finset.equivFin, Equiv.trans, Nonempty.intro, Iff.mp, Fin.equiv_iff_eq, Equiv.symm
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
s : Finset α
inst : Fintype β
i : Equiv.{u_1 + 1, u_2 + 1} (↥s) β
⊢ #s = Fintype.card β

Tactic:
card_eq_of_equiv_fin <| i.trans <| Fintype.equivFin β

Premises used: Equiv.trans, Fintype.equivFin, Finset.card_eq_of_equiv_fin
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : Equiv.{u_1 + 1, u_2 + 1} ↥s ↥t
⊢ #s = #t

Tactic:
(card_eq_of_equiv_fintype i).trans (Fintype.card_coe _)

Premises used: Finset.card_eq_of_equiv_fintype, Fintype.card_coe, Eq.trans
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Finite α
e : α ↪ α
h : ∀ (x : α), Eq (α := α) ((e.equivOfFiniteSelfEmbedding.toEmbedding : (a : α) → α) x : α) ((e : (a : α) → α) x : α)
⊢ e.equivOfFiniteSelfEmbedding.toEmbedding = e

Tactic:
ext
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Finite α
e : α ↪ α
x : α
⊢ Eq (α := α) ((e.equivOfFiniteSelfEmbedding.toEmbedding : (a : α) → α) x : α) ((e : (a : α) → α) x : α)

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
h : Fintype.card α ≤ Fintype.card β
⊢ Nonempty (α ↪ β)

Tactic:
(truncOfCardLE h).nonempty

Premises used: Function.Embedding.truncOfCardLE, Trunc.nonempty
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
h : Fintype.card α ≤ Fintype.card β
⊢ Nonempty (α ↪ β)

Tactic:
exact (truncOfCardLE h).nonempty

Premises used: Function.Embedding.truncOfCardLE, Trunc.nonempty
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
h : Fintype.card α ≤ Fintype.card β
⊢ Nonempty (α ↪ β)

Tactic:
classical exact (truncOfCardLE h).nonempty
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
⊢ Nonempty (α ↪ β) ↔ Fintype.card α ≤ Fintype.card β

Tactic:
⟨fun ⟨e⟩ => Fintype.card_le_of_embedding e, nonempty_of_card_le⟩

Premises used: _private.0.Function.Embedding.nonempty_iff_card_le.match_1, Fintype.card, LE.le, Iff.intro, Fintype.card_le_of_embedding, Function.Embedding.nonempty_of_card_le
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
s : Finset β
h : Fintype.card α ≤ #s
⊢ Fintype.card α ≤ Fintype.card.{u_2} ↥s

Tactic:
rw [← Fintype.card_coe] at h

Premises used: Fintype.card_coe
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card.{u_2} ↥s
rcases :
  ∀ (f : Embedding.{u_1 + 1, u_2 + 1} α ↥s),
    ∃ (f : α ↪ β), Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ⊆ (↑s : Set β)
⊢ ∃ (f : α ↪ β), Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ⊆ (↑s : Set β)

Tactic:
rcases nonempty_of_card_le h with ⟨f⟩

Premises used: Function.Embedding.nonempty_of_card_le
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card.{u_2} ↥s
f : Embedding.{u_1 + 1, u_2 + 1} α ↥s
⊢ Set.range.{u_2, u_1 + 1} (ι := α) (⇑(f.trans (subtype fun (x : β) ↦ x ∈ s)) : (a : α) → β) ⊆ (↑s : Set β)

Tactic:
simp [Set.range_subset_iff]

Premises used: Set.range_subset_iff
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card.{u_2} ↥s
f : Embedding.{u_1 + 1, u_2 + 1} α ↥s
⊢ ∃ (f : α ↪ β), Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ⊆ (↑s : Set β)

Tactic:
exact ⟨f.trans (Embedding.subtype _), by simp [Set.range_subset_iff]⟩
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
s : Finset β
hsn : Fintype.card α = #s
obtain :
  ∀ (f : α ↪ β) (hf : Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ⊆ (↑s : Set β)),
    ∃ (f : α ↪ β), map f univ = s
⊢ ∃ (f : α ↪ β), map f univ = s

Tactic:
obtain ⟨f : α ↪ β, hf⟩ := exists_of_card_le_finset (Nat.le_of_eq hsn)

Premises used: Function.Embedding.exists_of_card_le_finset, Nat.le_of_eq
-- Module: Mathlib.Data.Fintype.EquivFin
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
⊢ ∃ (f : α ↪ β), map f univ = s

Tactic:
use f
-- Module: Mathlib.Data.Fintype.EquivFin
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
h₁ : #s ≤ #(map f univ)
⊢ map f univ = s

Tactic:
apply Finset.eq_of_subset_of_card_le

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

Tactic:
simp [← coe_subset, hf]

Premises used: Finset.coe_subset
-- Module: Mathlib.Data.Fintype.EquivFin
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 β)
⊢ #s ≤ #(map f univ)

Tactic:
simp [← hsn]
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_4
inst : Fintype α
e : α ↪ α
rw : map e.equivOfFiniteSelfEmbedding.toEmbedding univ = univ
rw₁ rw₂ : Eq.{u_4 + 1} (α := Finset α) univ univ
⊢ map e univ = univ

Tactic:
rw [← e.toEmbedding_equivOfFiniteSelfEmbedding, univ_map_equiv_to_embedding]

Premises used: Finset.univ_map_equiv_to_embedding, Function.Embedding.toEmbedding_equivOfFiniteSelfEmbedding
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
h : Surjective f
h' : ¬Injective f
⊢ card β < card α

Tactic:
card_lt_of_injective_not_surjective _ (Function.injective_surjInv h) fun hg =>
    have w : Function.Bijective (Function.surjInv h) := ⟨Function.injective_surjInv h, hg⟩
    h' <| h.injective_of_finite (Equiv.ofBijective _ w).symm

Premises used: Function.surjInv, Function.Surjective.injective_of_finite, And.intro, Equiv.ofBijective, Equiv.symm, Function.injective_surjInv, Fintype.card_lt_of_injective_not_surjective
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
inst : Infinite α
_h : Fintype α
⊢ False

Tactic:
not_finite α

Premises used: not_finite
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_4
⊢ IsEmpty.{u_4 + 1} (Fintype α) ↔ Infinite α

Tactic:
⟨fun ⟨h⟩ => ⟨fun h' => (@nonempty_fintype α h').elim h⟩, fun ⟨h⟩ => ⟨fun h' => h h'.finite⟩⟩

Premises used: Nonempty.elim, Fintype.finite, _private.0.isEmpty_fintype.match_1, Infinite.mk, _private.0.isEmpty_fintype.match_2, IsEmpty, IsEmpty.mk, nonempty_fintype, Fintype, Iff.intro, Infinite
-- Module: Mathlib.Data.Fintype.EquivFin
Goal:
α : Type u_1
h : ∀ (a : Fintype α), False
⊢ Infinite α

Tactic:
isEmpty_fintype.mp ⟨h⟩

Premises used: IsEmpty.mk, Iff.mp, isEmpty_fintype
-- 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 α
⊢ False

Tactic:
lt_irrefl (Fintype.card α) ?_

Premises used: lt_irrefl, Fintype.card