awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
x : α
rw : x ∈ xs
⊢ List.idxOf x xs < xs.length

Tactic:
rw [List.idxOf_lt_length_iff]

Premises used: List.idxOf_lt_length_iff
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
x : α
⊢ x ∈ xs

Tactic:
apply h
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
x : α
⊢ xs.get ((fun (x : α) ↦ (⟨List.idxOf x xs, ⋯⟩ : Fin xs.length)) x) = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
i : Fin xs.length
h₁ : (↑((fun (x : α) ↦ (⟨List.idxOf x xs, ⋯⟩ : Fin xs.length)) (xs.get i)) : ℕ) = (↑i : ℕ)
⊢ (fun (x : α) ↦ (⟨List.idxOf x xs, ⋯⟩ : Fin xs.length)) (xs.get i) = i

Tactic:
ext
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
i : Fin xs.length
⊢ (↑((fun (x : α) ↦ (⟨List.idxOf x xs, ⋯⟩ : Fin xs.length)) (xs.get i)) : ℕ) = (↑i : ℕ)

Tactic:
simp [h'.idxOf_getElem]

Premises used: List.Nodup.idxOf_getElem
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
⊢ ∀ (x : α), x ∈ xs.dedup

Tactic:
simp [*]
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
⊢ card α = xs.dedup.length

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
x : α
simp : ∃ (a : Fin (card α)), (Equiv.symm equiv : (a : Fin (card α)) → α) a = x
⊢ x ∈ toList α

Tactic:
simp only [toList, List.mem_map, List.mem_finRange, true_and]

Premises used: FinEnum.toList, List.mem_finRange, List.mem_map, true_and
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
x : α
exists :
  (Equiv.symm equiv : (a : Fin (card α)) → α) (((equiv : α ≃ Fin (card α)) : (a : α) → Fin (card α)) x : Fin (card α)) =
    x
⊢ ∃ (a : Fin (card α)), (Equiv.symm equiv : (a : Fin (card α)) → α) a = x

Tactic:
exists equiv x

Premises used: DFunLike.coe, FinEnum.equiv
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
x : α
⊢ (Equiv.symm equiv : (a : Fin (card α)) → α) (((equiv : α ≃ Fin (card α)) : (a : α) → Fin (card α)) x : Fin (card α)) =
    x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
hf : Injective.{1, u + 1} (α := Fin (card α)) (β := α) (⇑(Equiv.symm equiv) : (a : Fin (card α)) → α)
a : List.Nodup (α := Fin (card α)) (List.finRange (card α))
⊢ List.Nodup.{u} (α := α)
    (List.map (α := Fin (card α)) (⇑(Equiv.symm equiv) : (a : Fin (card α)) → α) (List.finRange (card α)))

Tactic:
apply List.Nodup.map

Premises used: List.Nodup.map
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
⊢ Injective.{1, u + 1} (α := Fin (card α)) (β := α) (⇑(Equiv.symm equiv) : (a : Fin (card α)) → α)

Tactic:
apply Equiv.injective

Premises used: Equiv.injective
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
⊢ List.Nodup (α := Fin (card α)) (List.finRange (card α))

Tactic:
apply List.nodup_finRange

Premises used: List.nodup_finRange
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
hf : Injective.{1, u + 1} (α := Fin (card α)) (β := α) (⇑(Equiv.symm equiv) : (a : Fin (card α)) → α)
a : List.Nodup (α := Fin (card α)) (List.finRange (card α))
hf₁ : Injective.{1, u + 1} (α := Fin (card α)) (β := α) (⇑(Equiv.symm equiv) : (a : Fin (card α)) → α)
a₁ : List.Nodup (α := Fin (card α)) (List.finRange (card α))
⊢ List.Nodup.{u} (α := α)
    (List.map (α := Fin (card α)) (⇑(Equiv.symm equiv) : (a : Fin (card α)) → α) (List.finRange (card α)))

Tactic:
apply List.Nodup.map <;> [apply Equiv.injective; apply List.nodup_finRange]

Premises used: List.Nodup.map, List.nodup_finRange, Equiv.injective
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β_1 : α → Type v
β : Type u_1
f : β → α
inst : DecidableEq α
inst_1 : FinEnum β
h : Surjective f
x : α
⊢ x ∈ List.map f (toList β)

Tactic:
simpa using h _
-- Module: Mathlib.Data.FinEnum
Goal:
α_1 : Type u
β_1 : α_1 → Type v
α : Type u_1
β : Type u_2
f : α → β
inst : DecidableEq α
inst_1 : FinEnum β
h : Injective f
x : α
simp : ∃ (a : β), partialInv f a = some x
⊢ x ∈ List.filterMap (partialInv f) (toList β)

Tactic:
simp only [mem_toList, true_and, List.mem_filterMap]

Premises used: FinEnum.mem_toList, List.mem_filterMap, true_and
-- Module: Mathlib.Data.FinEnum
Goal:
α_1 : Type u
β_1 : α_1 → Type v
α : Type u_1
β : Type u_2
f : α → β
inst : DecidableEq α
inst_1 : FinEnum β
h : Injective f
x : α
h₁ : partialInv f (f x) = some x
⊢ ∃ (a : β), partialInv f a = some x

Tactic:
use f x
-- Module: Mathlib.Data.FinEnum
Goal:
α_1 : Type u
β_1 : α_1 → Type v
α : Type u_1
β : Type u_2
f : α → β
inst : DecidableEq α
inst_1 : FinEnum β
h : Injective f
x : α
⊢ partialInv f (f x) = some x

Tactic:
simp only [h, Function.partialInv_left]

Premises used: Function.partialInv_left
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum (ULift.{u_1, u} α)
inst_1 : FinEnum α
⊢ card (ULift.{u_1, u} α) = card α

Tactic:
Fin.equiv_iff_eq.mp ⟨equiv.symm.trans Equiv.ulift |>.trans equiv⟩

Premises used: Equiv.trans, Equiv.ulift, Nonempty.intro, Iff.mp, Fin.equiv_iff_eq, Equiv.symm, FinEnum.equiv
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
a : α
⊢ Eq (α := Fin (card (ULift.{u_1, u} α)))
    (((equiv : ULift.{u_1, u} α ≃ Fin (card (ULift.{u_1, u} α))) :
          (a : ULift.{u_1, u} α) → Fin (card (ULift.{u_1, u} α)))
        { down := a } :
      Fin (card (ULift.{u_1, u} α)))
    (((equiv : α ≃ Fin (card α)) : (a : α) → Fin (card α)) a : Fin (card α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
a' : ULift.{u_1, u} α
⊢ Eq (α := Fin (card α)) (((equiv : α ≃ Fin (card α)) : (a : α) → Fin (card α)) a'.down : Fin (card α))
    (((equiv : ULift.{u_1, u} α ≃ Fin (card (ULift.{u_1, u} α))) :
          (a : ULift.{u_1, u} α) → Fin (card (ULift.{u_1, u} α)))
        a' :
      Fin (card (ULift.{u_1, u} α)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
i : Fin (card α)
⊢ Eq (α := ULift.{u_1, u} α) ({ down := (Equiv.symm equiv : (a : Fin (card α)) → α) i } : ULift.{u_1, u} α)
    ((Equiv.symm equiv : (a : Fin (card (ULift.{u_1, u} α))) → ULift.{u_1, u} α) i : ULift.{u_1, u} α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
i : Fin (card α)
⊢ Eq.{u + 1} (α := α)
    (ULift.down.{u_1, u} ((Equiv.symm equiv : (a : Fin (card (ULift.{u_1, u} α))) → ULift.{u_1, u} α) i) : α)
    ((Equiv.symm equiv : (a : Fin (card α)) → α) i : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
⊢ card PEmpty.{u_1 + 1} = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
⊢ card Empty = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : PUnit.{u_1 + 1}
⊢ x ∈ [PUnit.unit]

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
⊢ card PUnit.{u_1 + 1} = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β_1 : α → Type v
β : Type u_1
inst : FinEnum α
inst_1 : FinEnum β
x : α × β
mk : ∀ (fst : α) (snd : β), (fst, snd) ∈ toList α ×ˢ toList β
⊢ x ∈ toList α ×ˢ toList β

Tactic:
cases x
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β_1 : α → Type v
β : Type u_1
inst : FinEnum α
inst_1 : FinEnum β
fst : α
snd : β
⊢ (fst, snd) ∈ toList α ×ˢ toList β

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β_1 : α → Type v
β : Type u_1
inst : FinEnum α
inst_1 : FinEnum β
x : α ⊕ β
inl : ∀ (val : α), Sum.inl val ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
inr : ∀ (val : β), Sum.inr val ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
⊢ x ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)

Tactic:
cases x
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β_1 : α → Type v
β : Type u_1
inst : FinEnum α
inst_1 : FinEnum β
val : α
⊢ Sum.inl val ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β_1 : α → Type v
β : Type u_1
inst : FinEnum α
inst_1 : FinEnum β
val : β
⊢ Sum.inr val ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
n : ℕ
⊢ ∀ (x : Fin n), x ∈ List.finRange n

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
n : ℕ
inst : FinEnum (Fin n)
⊢ card (Fin n) = n

Tactic:
Fin.equiv_iff_eq.mp ⟨equiv.symm⟩

Premises used: Nonempty.intro, Iff.mp, Fin.equiv_iff_eq, Equiv.symm, FinEnum.equiv
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
⊢ Membership.mem (γ := List (Finset α)) (enum []) s ↔ ∀ x ∈ s, Membership.mem (γ := List α) [] x

Tactic:
simp [enum, eq_empty_iff_forall_notMem]

Premises used: Finset.eq_empty_iff_forall_notMem, FinEnum.Finset.enum
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
cons : (∃ (a : Finset α), (∀ x ∈ a, x ∈ xs) ∧ (s = a ∨ s = insert x a)) ↔ ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs
⊢ s ∈ enum (x :: xs) ↔ ∀ x_1 ∈ s, x_1 ∈ x :: xs

Tactic:
simp only [enum, List.bind_eq_flatMap, List.mem_flatMap, List.mem_cons,
        List.not_mem_nil, or_false, ih]

Premises used: FinEnum.Finset.enum, List.bind_eq_flatMap, or_false, List.mem_flatMap, List.mem_cons, List.not_mem_nil
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
⊢ (∃ (a : Finset α), (∀ x ∈ a, x ∈ xs) ∧ (s = a ∨ s = insert x a)) → ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs

Tactic:
aesop
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
cons :
  ∀ (hs : ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs), (∀ x_1 ∈ s.erase x, x_1 ∈ xs) ∧ (s = s.erase x ∨ s = insert x (s.erase x))
⊢ (∃ (a : Finset α), (∀ x ∈ a, x ∈ xs) ∧ (s = a ∨ s = insert x a)) ↔ ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs

Tactic:
refine ⟨by aesop, fun hs => ⟨s.erase x, ?_⟩⟩
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
hs : ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs
⊢ ∀ x_1 ∈ s, ¬x_1 = x → x_1 ∈ xs

Tactic:
simp only [or_iff_not_imp_left] at hs

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
hs : ∀ x_1 ∈ s, ¬x_1 = x → x_1 ∈ xs
⊢ (∀ x_1 ∈ s.erase x, x_1 ∈ xs) ∧ (s = s.erase x ∨ s = insert x (s.erase x))

Tactic:
simp +contextual [eq_comm (a := s), or_iff_not_imp_left, hs]

Premises used: eq_comm, Classical.or_iff_not_imp_left
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
xs : List α
nil : ∀ (s : Finset α), Membership.mem (γ := List (Finset α)) (enum []) s ↔ ∀ x ∈ s, Membership.mem (γ := List α) [] x
cons :
  ∀ (x : α) (xs : List α) (ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs) (s : Finset α),
    s ∈ enum (x :: xs) ↔ ∀ x_1 ∈ s, x_1 ∈ x :: xs
⊢ s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs

Tactic:
induction xs generalizing s with
  | nil => simp [enum, eq_empty_iff_forall_notMem]
  | cons x xs ih =>
      simp only [enum, List.bind_eq_flatMap, List.mem_flatMap, List.mem_cons,
        List.not_mem_nil, or_false, ih]
      refine ⟨by aesop, fun hs => ⟨s.erase x, ?_⟩⟩
      simp only [or_iff_not_imp_left] at hs
      simp +contextual [eq_comm (a := s), or_iff_not_imp_left, hs]

Premises used: Finset.cons, Finset.eq_empty_iff_forall_notMem, eq_comm, FinEnum.Finset.enum, List.bind_eq_flatMap, Classical.or_iff_not_imp_left, or_false, List.mem_flatMap, List.mem_cons, List.not_mem_nil
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : FinEnum α
⊢ ∀ (x : Finset α), x ∈ enum (toList α)

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : FinEnum α
p : α → Prop
inst_1 : DecidablePred p
x : α
h : p x
⊢ Membership.mem (γ := List { x : α // p x })
    (List.filterMap (fun (x : α) ↦ if h : p x then some (Subtype.mk (p := fun (x : α) ↦ p x) x h) else none) (toList α))
    (Subtype.mk (p := fun (x : α) ↦ p x) x h)

Tactic:
simpa
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β_1 β : α → Type v
inst : FinEnum α
inst_1 : (a : α) → FinEnum (β a)
x : Sigma β
mk :
  ∀ (fst : α) (snd : β fst),
    Membership.mem (γ := List (Sigma β))
      (List.flatMap (fun (a : α) ↦ List.map (Sigma.mk (β := β) a) (toList (β a))) (toList α))
      (Sigma.mk (β := β) fst snd)
⊢ Membership.mem (γ := List (Sigma β))
    (List.flatMap (fun (a : α) ↦ List.map (Sigma.mk (β := β) a) (toList (β a))) (toList α)) x

Tactic:
cases x
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β_1 β : α → Type v
inst : FinEnum α
inst_1 : (a : α) → FinEnum (β a)
fst : α
snd : β fst
⊢ Membership.mem (γ := List (Sigma β))
    (List.flatMap (fun (a : α) ↦ List.map (Sigma.mk (β := β) a) (toList (β a))) (toList α)) (Sigma.mk (β := β) fst snd)

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α_1 : Type u
β_1 : α_1 → Type v
α : Prop
β : α → Type v
inst : (a : α) → FinEnum (β a)
inst_1 : Decidable α
h : α
x : (a : α) ×' β a
a : α
Ba : β a
⊢ Membership.mem (γ := List ((a : α) ×' β a)) (List.map (PSigma.mk (β := fun (a : α) ↦ β a) h) (toList (β h)))
    (PSigma.mk (β := fun (a : α) ↦ β a) a Ba)

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α_1 : Type u
β_1 : α_1 → Type v
α : Prop
β : α → Prop
inst : Decidable α
inst_1 : (a : α) → Decidable (β a)
h : ∃ (a : α), β a
⊢ ∀ (x : (a : α) ×' β a), x ∈ [PSigma.mk (β := fun (a : α) ↦ β a) ⋯ ⋯]

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
xs : List α
⊢ ∀ (x : { x : α // x ∈ xs }), x ∈ xs.attach

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : FinEnum α
x : α
⊢ Membership.mem (γ := Finset α) (map (α := Fin (card α)) (Equiv.toEmbedding (Equiv.symm equiv)) univ) x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
inst_1 : Fintype α
⊢ card α = Fintype.card α

Tactic:
Fintype.truncEquivFin α |>.inductionOn (fun h ↦ Fin.equiv_iff_eq.mp ⟨equiv.symm.trans h⟩)

Premises used: Fintype.truncEquivFin, Quotient.inductionOn
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
e₁ e₂ : FinEnum α
⊢ card α = card α

Tactic:
calc _
  _ = _ := @card_eq_fintypeCard _ e₁ inferInstance
  _ = _ := Fintype.card_congr' rfl
  _ = _ := @card_eq_fintypeCard _ e₂ inferInstance |>.symm

Premises used: Trans.trans, Eq.symm, Fintype.card_congr', rfl, FinEnum.card_eq_fintypeCard
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
⊢ card α = 0 ↔ IsEmpty α

Tactic:
Eq.congr_left card_eq_fintypeCard |>.trans Fintype.card_eq_zero_iff

Premises used: Eq.congr_left, Fintype.card_eq_zero_iff, Iff.trans, FinEnum.card_eq_fintypeCard
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
inst_1 : IsEmpty α
⊢ card α = 0

Tactic:
card_eq_zero_iff.mpr ‹_›

Premises used: Iff.mpr, FinEnum.card_eq_zero_iff
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
⊢ 0 < card α ↔ Nonempty α

Tactic:
card_eq_fintypeCard (α := α) ▸ Fintype.card_pos_iff

Premises used: Eq.rec, Eq.symm, Fintype.card_pos_iff, FinEnum.card_eq_fintypeCard
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u_1
inst : FinEnum α
inst_1 : Nonempty α
⊢ 0 < card α

Tactic:
card_pos_iff.mpr ‹_›

Premises used: Iff.mpr, FinEnum.card_pos_iff
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u_1
inst : FinEnum α
inst_1 : Nonempty α
⊢ card α ≠ 0

Tactic:
card_pos.ne'

Premises used: FinEnum.card_pos, LT.lt.ne'
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
inst : FinEnum α
inst_1 : Unique α
⊢ card α = 1

Tactic:
card_eq_fintypeCard.trans <| Fintype.card_eq_one_iff_nonempty_unique.mpr ⟨‹_›⟩

Premises used: Iff.mpr, Fintype.card_eq_one_iff_nonempty_unique, Nonempty.intro, Eq.trans, FinEnum.card_eq_fintypeCard
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
change :
  { card := card α, equiv := equiv, decEq := fun (a b : α) ↦ decEq a b } =
    { card := 0, equiv := Equiv.equivOfIsEmpty α (Fin 0), decEq := fun (a b : α) ↦ decidableEq_of_subsingleton a b :
      FinEnum α }
⊢ e = { card := 0, equiv := Equiv.equivOfIsEmpty α (Fin 0), decEq := fun (a b : α) ↦ decidableEq_of_subsingleton a b }

Tactic:
change FinEnum.mk e.1 e.2 = _

Premises used: FinEnum.card, FinEnum.mk, FinEnum.equiv
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
h : card α = 0
h₁ : HEq (α := α ≃ Fin (card α)) equiv (β := α ≃ Fin 0) (Equiv.equivOfIsEmpty α (Fin 0))
h₂ : Eq.{u + 1} (α := DecidableEq α) (fun (a b : α) ↦ decEq a b) fun (a b : α) ↦ decidableEq_of_subsingleton a b
⊢ { card := card α, equiv := equiv, decEq := fun (a b : α) ↦ decEq a b } =
    { card := 0, equiv := Equiv.equivOfIsEmpty α (Fin 0), decEq := fun (a b : α) ↦ decidableEq_of_subsingleton a b :
      FinEnum α }

Tactic:
congr 1
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
⊢ card α = 0

Tactic:
card_eq_zero

Premises used: FinEnum.card_eq_zero
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
⊢ card α = 0

Tactic:
exact card_eq_zero

Premises used: FinEnum.card_eq_zero
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
⊢ HEq (α := α ≃ Fin (card α)) equiv (β := α ≃ Fin 0) (Equiv.equivOfIsEmpty α (Fin 0))

Tactic:
heq_of_cast_eq ?_ (Subsingleton.allEq _ _)

Premises used: Subsingleton.allEq, heq_of_cast_eq
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
h : (α ≃ Fin (card α)) = (α ≃ Fin 0)
⊢ HEq (α := α ≃ Fin (card α)) equiv (β := α ≃ Fin 0) (Equiv.equivOfIsEmpty α (Fin 0))

Tactic:
refine heq_of_cast_eq ?_ (Subsingleton.allEq _ _)

Premises used: Subsingleton.allEq, heq_of_cast_eq
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
⊢ (α ≃ Fin (card α)) = (α ≃ Fin 0)

Tactic:
congrArg (α ≃ Fin ·) <| card_eq_zero

Premises used: congrArg, Equiv, Fin, FinEnum.card_eq_zero
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
⊢ (α ≃ Fin (card α)) = (α ≃ Fin 0)

Tactic:
exact congrArg (α ≃ Fin ·) <| card_eq_zero

Premises used: congrArg, Equiv, Fin, FinEnum.card_eq_zero
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
h :
  ∀ (x : α),
    Eq.{u + 1} (α := (b : α) → Decidable (x = b)) (fun (b : α) ↦ decEq x b) fun (b : α) ↦
      decidableEq_of_subsingleton x b
⊢ Eq.{u + 1} (α := DecidableEq α) (fun (a b : α) ↦ decEq a b) fun (a b : α) ↦ decidableEq_of_subsingleton a b

Tactic:
funext x
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
x : α
⊢ Eq.{u + 1} (α := (b : α) → Decidable (x = b)) (fun (b : α) ↦ decEq x b) fun (b : α) ↦ decidableEq_of_subsingleton x b

Tactic:
‹IsEmpty α›.elim x

Premises used: IsEmpty.elim
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
x : α
⊢ Eq.{u + 1} (α := (b : α) → Decidable (x = b)) (fun (b : α) ↦ decEq x b) fun (b : α) ↦ decidableEq_of_subsingleton x b

Tactic:
exact ‹IsEmpty α›.elim x
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : Unique α
e : FinEnum α
change :
  { card := card α, equiv := equiv, decEq := fun (a b : α) ↦ decEq a b } =
    { card := 1, equiv := Equiv.ofUnique α (Fin 1), decEq := fun (a b : α) ↦ decidableEq_of_subsingleton a b :
      FinEnum α }
⊢ e = { card := 1, equiv := Equiv.ofUnique α (Fin 1), decEq := fun (a b : α) ↦ decidableEq_of_subsingleton a b }

Tactic:
change FinEnum.mk e.1 e.2 = _

Premises used: FinEnum.card, FinEnum.mk, FinEnum.equiv
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : Unique α
e : FinEnum α
h : card α = 1
h₁ : HEq (α := α ≃ Fin (card α)) equiv (β := α ≃ Fin 1) (Equiv.ofUnique α (Fin 1))
h₂ : Eq.{u + 1} (α := DecidableEq α) (fun (a b : α) ↦ decEq a b) fun (a b : α) ↦ decidableEq_of_subsingleton a b
⊢ { card := card α, equiv := equiv, decEq := fun (a b : α) ↦ decEq a b } =
    { card := 1, equiv := Equiv.ofUnique α (Fin 1), decEq := fun (a b : α) ↦ decidableEq_of_subsingleton a b :
      FinEnum α }

Tactic:
congr 1
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : Unique α
e : FinEnum α
⊢ card α = 1

Tactic:
card_eq_one α

Premises used: FinEnum.card_eq_one
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : Unique α
e : FinEnum α
⊢ card α = 1

Tactic:
exact card_eq_one α

Premises used: FinEnum.card_eq_one
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : Unique α
e : FinEnum α
⊢ HEq (α := α ≃ Fin (card α)) equiv (β := α ≃ Fin 1) (Equiv.ofUnique α (Fin 1))

Tactic:
heq_of_cast_eq ?_ (Subsingleton.allEq _ _)

Premises used: Subsingleton.allEq, heq_of_cast_eq
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : Unique α
e : FinEnum α
h : (α ≃ Fin (card α)) = (α ≃ Fin 1)
⊢ HEq (α := α ≃ Fin (card α)) equiv (β := α ≃ Fin 1) (Equiv.ofUnique α (Fin 1))

Tactic:
refine heq_of_cast_eq ?_ (Subsingleton.allEq _ _)

Premises used: Subsingleton.allEq, heq_of_cast_eq
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : Unique α
e : FinEnum α
⊢ (α ≃ Fin (card α)) = (α ≃ Fin 1)

Tactic:
congrArg (α ≃ Fin ·) <| card_eq_one α

Premises used: congrArg, Equiv, FinEnum.card_eq_one, Fin
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : Unique α
e : FinEnum α
⊢ (α ≃ Fin (card α)) = (α ≃ Fin 1)

Tactic:
exact congrArg (α ≃ Fin ·) <| card_eq_one α

Premises used: congrArg, Equiv, FinEnum.card_eq_one, Fin
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
inst : Unique α
e : FinEnum α
⊢ Eq.{u + 1} (α := DecidableEq α) (fun (a b : α) ↦ decEq a b) fun (a b : α) ↦ decidableEq_of_subsingleton a b

Tactic:
subsingleton
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : UInt8
⊢ UInt8.ofFin x.toFin = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : Fin (HPow.hPow (α := ℕ) (β := ℕ) 2 8)
⊢ (UInt8.ofFin x).toFin = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : UInt16
⊢ UInt16.ofFin x.toFin = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : Fin (HPow.hPow (α := ℕ) (β := ℕ) 2 16)
⊢ (UInt16.ofFin x).toFin = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : UInt32
⊢ UInt32.ofFin x.toFin = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : Fin (HPow.hPow (α := ℕ) (β := ℕ) 2 32)
⊢ (UInt32.ofFin x).toFin = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : UInt64
⊢ UInt64.ofFin x.toFin = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : Fin (HPow.hPow (α := ℕ) (β := ℕ) 2 64)
⊢ (UInt64.ofFin x).toFin = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : Int8
⊢ (Int8.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int8.toBitVec) x) = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : Fin (HPow.hPow (α := ℕ) (β := ℕ) 2 8)
⊢ (BitVec.toFin ∘ Int8.toBitVec) ((Int8.ofBitVec ∘ BitVec.ofFin) x) = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : Int16
⊢ (Int16.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int16.toBitVec) x) = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : Fin (HPow.hPow (α := ℕ) (β := ℕ) 2 16)
⊢ (BitVec.toFin ∘ Int16.toBitVec) ((Int16.ofBitVec ∘ BitVec.ofFin) x) = x

Tactic:
simp
-- Module: Mathlib.Data.FinEnum
Goal:
α : Type u
β : α → Type v
x : Int32
⊢ (Int32.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int32.toBitVec) x) = x

Tactic:
simp