awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.VecNotation (goal)
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h :
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    vecCons a x ((Equiv.swap i.succ j.succ : (a : Fin (n + 1)) → Fin (n + 1)) k)
h₁ : vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k = vecCons a x k
h₂ :
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n).succ =
    vecCons a x ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h₃ : (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n) = vecCons a x ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h₄ : x ((Equiv.swap i j : (a : Fin n) → Fin n) (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n)) = vecCons a x ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h₅ : x ((Equiv.swap i j : (a : Fin n) → Fin n) (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n)) = x ⟨(↑k : ℕ) - 1, ⋯⟩
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
have h₆ : x (⟨(↑k : ℕ) - 1, sorry⟩ : Fin n) = x ⟨(↑k : ℕ) - 1, sorry⟩
Tactic: rw [Function.comp_apply, Equiv.swap_apply_of_ne_of_ne hki hkj, hk, cons_val_succ,
    Function.comp_apply, cons_val_succ, Equiv.swap_apply_of_ne_of_ne (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.Data.FinEnum.Option (goal)
Goal:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst : FinEnum α
h : card α = 0
x : FinEnum PEmpty.{u + 1}
⊢ recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option) α = congr x inst ⋯ empty
have unfold : (match (motive := ℕ → P α) cardeq : card α with
  | 0 => congr pempty inst cardeq empty
  | n.succ =>
    let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
    have this := sorry;
    congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst sorry
      (option fN
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin n))))) =
  congr x inst sorry empty
Tactic: unfold recEmptyOption
-- Lean 4 proof step from Mathlib.Data.FinEnum.Option (goal)
Goal:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst : FinEnum α
h : card α = 0
x : FinEnum PEmpty.{u + 1}
⊢ (match (motive := ℕ → P α) cardeq : card α with
    | 0 => congr pempty inst cardeq empty
    | n.succ =>
      let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
      have this := ⋯;
      congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
        (option fN
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin n))))) =
    congr x inst ⋯ empty
have h_1 : ∀ (heq : card α = 0), congr pempty inst sorry empty = congr x inst sorry empty
Tactic: split
-- Lean 4 proof step from Mathlib.Data.FinEnum.Option (goal)
Goal:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst : FinEnum α
h : card α = 0
x : FinEnum PEmpty.{u + 1}
h_1 : ∀ (heq : card α = 0), congr pempty inst ⋯ empty = congr x inst ⋯ empty
⊢ (match (motive := ℕ → P α) cardeq : card α with
    | 0 => congr pempty inst cardeq empty
    | n.succ =>
      let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
      have this := ⋯;
      congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
        (option fN
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin n))))) =
    congr x inst ⋯ empty
have h_2 : ∀ (n : ℕ) (heq : card α = n.succ),
  (let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
    have this := sorry;
    congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst sorry
      (option fN
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin n))))) =
    congr x inst sorry empty
Tactic: split
-- Lean 4 proof step from Mathlib.Data.FinEnum.Option (goal)
Goal:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst : FinEnum α
h : card α = 0
x : FinEnum PEmpty.{u + 1}
heq : card α = 0
⊢ congr pempty inst ⋯ empty = congr x inst ⋯ empty
have h_1 : pempty = x
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.FinEnum.Option (goal)
Goal:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst : FinEnum α
h : 0 < card α
| recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option) α =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))
have lhs : recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option) α
Tactic: lhs
-- Lean 4 proof step from Mathlib.Data.FinEnum.Option (goal)
Goal:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst : FinEnum α
h : 0 < card α
| recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option) α
have unfold : (match (motive := ℕ → P α) cardeq : card α with
  | 0 => congr pempty inst cardeq empty
  | n.succ =>
    let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
    have this := sorry;
    congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst sorry
      (option fN
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin n)))) :
  P α)
Tactic: unfold recEmptyOption
-- Lean 4 proof step from Mathlib.Data.FinEnum.Option (goal)
Goal:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst : FinEnum α
h : 0 < card α
| recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option) α =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))
have unfold : (match (motive := ℕ → P α) cardeq : card α with
  | 0 => congr pempty inst cardeq empty
  | n.succ =>
    let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
    have this := sorry;
    congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst sorry
      (option fN
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin n)))) :
  P α)
Tactic: lhs; unfold recEmptyOption
-- Lean 4 proof step from Mathlib.Data.FinEnum.Option (goal)
Goal:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst : FinEnum α
h : 0 < card α
⊢ recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option) α =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))
have conv : (match (motive := ℕ → P α) cardeq : card α with
  | 0 => congr pempty inst cardeq empty
  | n.succ =>
    let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
    have this := sorry;
    congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst sorry
      (option fN
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin n))))) =
  congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
    (insertNone (ULift.{u, 0} (Fin (card α - 1)))
      (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
    inst sorry
    (option ULift.instFinEnum
      (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
        (ULift.{u, 0} (Fin (card α - 1)))))
Tactic: conv => lhs; unfold recEmptyOption
-- Lean 4 proof step from Mathlib.Data.FinEnum.Option (goal)
Goal:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst : FinEnum α
h : 0 < card α
⊢ (match (motive := ℕ → P α) cardeq : card α with
    | 0 => congr pempty inst cardeq empty
    | n.succ =>
      let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
      have this := ⋯;
      congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
        (option fN
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin n))))) =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))
have h_1 : ∀ (heq : card α = 0),
  congr pempty inst sorry empty =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst sorry
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))
Tactic: split
-- Lean 4 proof step from Mathlib.Data.FinEnum.Option (goal)
Goal:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst : FinEnum α
h : 0 < card α
h_1 :
  ∀ (heq : card α = 0),
    congr pempty inst ⋯ empty =
      congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
        (insertNone (ULift.{u, 0} (Fin (card α - 1)))
          (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
        inst ⋯
        (option ULift.instFinEnum
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin (card α - 1)))))
⊢ (match (motive := ℕ → P α) cardeq : card α with
    | 0 => congr pempty inst cardeq empty
    | n.succ =>
      let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
      have this := ⋯;
      congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
        (option fN
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin n))))) =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))
have h_2 : ∀ (n : ℕ) (heq : card α = n.succ),
  (let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
    have this := sorry;
    congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst sorry
      (option fN
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin n))))) =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst sorry
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))
Tactic: split
-- Lean 4 proof step from Mathlib.Data.FinEnum.Option (goal)
Goal:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst : FinEnum α
h : 0 < card α
n : ℕ
heq : card α = n.succ
⊢ (let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
      (option fN
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin n))))) =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))
have h_2 : ∀ (heq : card α = (card α).pred.succ),
  (let fN : FinEnum (ULift.{u, 0} (Fin (card α).pred)) := ULift.instFinEnum;
    have this : card.{u + 1} (ULift.{u, 0} (Fin (card α).pred)) = (card α).pred := sorry;
    congr
      (insertNone (ULift.{u, 0} (Fin (card α).pred))
        (↑(↑(finChoice (card α).pred) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α).pred)) + 1)))
      inst sorry
      (option fN
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α).pred))))) =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst sorry
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))
Tactic: rcases Nat.succ.inj <| (card α).succ_pred_eq_of_pos h |>.trans ‹_› with rfl
Cleared hypotheses: n, heq
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
x : α
⊢ List.idxOf x xs < xs.length
have rw : x ∈ xs
Tactic: rw [List.idxOf_lt_length_iff]
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
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
have h₁ : (↑((fun (x : α) ↦ (⟨List.idxOf x xs, sorry⟩ : Fin xs.length)) (xs.get i)) : ℕ) = (↑i : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
inst : FinEnum α
x : α
⊢ x ∈ toList α
have simp : ∃ (a : Fin (card α)), (Equiv.symm equiv : (a : Fin (card α)) → α) a = x
Tactic: simp only [toList, List.mem_map, List.mem_finRange, true_and]
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
inst : FinEnum α
x : α
⊢ ∃ (a : Fin (card α)), (Equiv.symm equiv : (a : Fin (card α)) → α) a = x
have exists : (Equiv.symm equiv : (a : Fin (card α)) → α) (((equiv : α ≃ Fin (card α)) : (a : α) → Fin (card α)) x : Fin (card α)) = x
Tactic: exists equiv x
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
inst : FinEnum α
⊢ List.Nodup.{u} (α := α)
    (List.map (α := Fin (card α)) (⇑(Equiv.symm equiv) : (a : Fin (card α)) → α) (List.finRange (card α)))
have hf : Injective.{1, u + 1} (α := Fin (card α)) (β := α) (⇑(Equiv.symm equiv) : (a : Fin (card α)) → α)
Tactic: apply List.Nodup.map
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
inst : FinEnum α
hf : Injective.{1, u + 1} (α := Fin (card α)) (β := α) (⇑(Equiv.symm equiv) : (a : Fin (card α)) → α)
⊢ List.Nodup.{u} (α := α)
    (List.map (α := Fin (card α)) (⇑(Equiv.symm equiv) : (a : Fin (card α)) → α) (List.finRange (card α)))
have a : List.Nodup (α := Fin (card α)) (List.finRange (card α))
Tactic: apply List.Nodup.map
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
inst : FinEnum α
⊢ List.Nodup.{u} (α := α)
    (List.map (α := Fin (card α)) (⇑(Equiv.symm equiv) : (a : Fin (card α)) → α) (List.finRange (card α)))
have hf : Injective.{1, u + 1} (α := Fin (card α)) (β := α) (⇑(Equiv.symm equiv) : (a : Fin (card α)) → α)
Tactic: apply List.Nodup.map <;> [apply Equiv.injective; apply List.nodup_finRange]
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
inst : FinEnum α
hf : Injective.{1, u + 1} (α := Fin (card α)) (β := α) (⇑(Equiv.symm equiv) : (a : Fin (card α)) → α)
⊢ List.Nodup.{u} (α := α)
    (List.map (α := Fin (card α)) (⇑(Equiv.symm equiv) : (a : Fin (card α)) → α) (List.finRange (card α)))
have a : List.Nodup (α := Fin (card α)) (List.finRange (card α))
Tactic: apply List.Nodup.map <;> [apply Equiv.injective; apply List.nodup_finRange]
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α_1 : Type u
β_1 : α_1 → Type v
α : Type u_1
β : Type u_2
f : α → β
inst : DecidableEq α
inst_1 : FinEnum β
h : Injective f
x : α
⊢ x ∈ List.filterMap (partialInv f) (toList β)
have simp : ∃ (a : β), partialInv f a = some x
Tactic: simp only [mem_toList, true_and, List.mem_filterMap]
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α_1 : Type u
β_1 : α_1 → Type v
α : Type u_1
β : Type u_2
f : α → β
inst : DecidableEq α
inst_1 : FinEnum β
h : Injective f
x : α
⊢ ∃ (a : β), partialInv f a = some x
have h₁ : partialInv f (f x) = some x
Tactic: use f x
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
β_1 : α → Type v
β : Type u_1
inst : FinEnum α
inst_1 : FinEnum β
x : α × β
⊢ x ∈ toList α ×ˢ toList β
have mk : ∀ (fst : α) (snd : β), (fst, snd) ∈ toList α ×ˢ toList β
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
β_1 : α → Type v
β : Type u_1
inst : FinEnum α
inst_1 : FinEnum β
x : α ⊕ β
⊢ x ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
have inl : ∀ (val : α), Sum.inl val ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
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 β)
⊢ x ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
have inr : ∀ (val : β), Sum.inr val ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
inst : DecidableEq α
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
have cons : (∃ (a : Finset α), (∀ x ∈ a, x ∈ xs) ∧ (s = a ∨ s = insert x a)) ↔ ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs
Tactic: simp only [enum, List.bind_eq_flatMap, List.mem_flatMap, List.mem_cons,
        List.not_mem_nil, or_false, ih]
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
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
have 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))
Tactic: refine ⟨by aesop, fun hs => ⟨s.erase x, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.FinEnum (hypothesis)
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))
have hs₁ : ∀ x_1 ∈ s, ¬x_1 = x → x_1 ∈ xs
Tactic: simp only [or_iff_not_imp_left] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
xs : List α
⊢ s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
have nil : ∀ (s : Finset α), Membership.mem (γ := List (Finset α)) (enum []) s ↔ ∀ x ∈ s, Membership.mem (γ := List α) [] x
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]
Cleared hypotheses: s, xs
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
xs : List α
nil : ∀ (s : Finset α), Membership.mem (γ := List (Finset α)) (enum []) s ↔ ∀ x ∈ s, Membership.mem (γ := List α) [] x
⊢ s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
have 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
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]
Cleared hypotheses: s, xs
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
β_1 β : α → Type v
inst : FinEnum α
inst_1 : (a : α) → FinEnum (β a)
x : Sigma β
⊢ Membership.mem (γ := List (Sigma β))
    (List.flatMap (fun (a : α) ↦ List.map (Sigma.mk (β := β) a) (toList (β a))) (toList α)) x
have mk : ∀ (fst : α) (snd : β fst),
  Membership.mem (γ := List (Sigma β))
    (List.flatMap (fun (a : α) ↦ List.map (Sigma.mk (β := β) a) (toList (β a))) (toList α)) (Sigma.mk (β := β) fst snd)
Tactic: cases x
Cleared hypotheses: x