awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
β : Type u_3
f : α → β
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
rw :
  HAppend.hAppend (α := List (Sym β n.succ))
      (map (fun (p : Sym β n) ↦ f x ::ₛ p) (map (Sym.map f) (List.sym n (x :: xs))))
      (map (Sym.map f) (List.sym (n + 1) xs)) =
    map (Sym.map f) (List.sym (n + 1) (x :: xs))
⊢ Eq (α := List (Sym β (n + 1))) (List.sym (n + 1) (map f (x :: xs))) (map (Sym.map f) (List.sym (n + 1) (x :: xs)))

Tactic:
rw [map_cons, List.sym, ← map_cons, sym_map f n (x :: xs), sym_map f (n + 1) xs]

Premises used: List.map_cons, List.cons, HAdd.hAdd, List.sym, OfNat.ofNat
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
β : Type u_3
f : α → β
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
simp :
  Eq (α := List (Sym β n.succ)) (map ((fun (p : Sym β n) ↦ f x ::ₛ p) ∘ Sym.map f) (List.sym n (x :: xs)))
    (map (Sym.map f ∘ fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs)))
⊢ HAppend.hAppend (α := List (Sym β n.succ))
      (map (fun (p : Sym β n) ↦ f x ::ₛ p) (map (Sym.map f) (List.sym n (x :: xs))))
      (map (Sym.map f) (List.sym (n + 1) xs)) =
    map (Sym.map f) (List.sym (n + 1) (x :: xs))

Tactic:
simp only [map_map, List.sym, map_append, append_cancel_right_eq]

Premises used: List.map_map, List.sym, List.append_cancel_right_eq, List.map_append
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
β : Type u_3
f : α → β
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
e_f :
  Eq (α := Sym α n → Sym β n.succ) ((fun (p : Sym β n) ↦ f x ::ₛ p) ∘ Sym.map f)
    (Sym.map f ∘ fun (p : Sym α n) ↦ x ::ₛ p)
⊢ Eq (α := List (Sym β n.succ)) (map ((fun (p : Sym β n) ↦ f x ::ₛ p) ∘ Sym.map f) (List.sym n (x :: xs)))
    (map (Sym.map f ∘ fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs)))

Tactic:
congr
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
β : Type u_3
f : α → β
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
e_f :
  ∀ (s : Sym α n),
    (↑(((fun (p : Sym β n) ↦ f x ::ₛ p) ∘ Sym.map f) s) : Multiset β) =
      (↑((Sym.map f ∘ fun (p : Sym α n) ↦ x ::ₛ p) s) : Multiset β)
⊢ Eq (α := Sym α n → Sym β n.succ) ((fun (p : Sym β n) ↦ f x ::ₛ p) ∘ Sym.map f)
    (Sym.map f ∘ fun (p : Sym α n) ↦ x ::ₛ p)

Tactic:
ext s
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
β : Type u_3
f : α → β
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
s : Sym α n
⊢ (↑(((fun (p : Sym β n) ↦ f x ::ₛ p) ∘ Sym.map f) s) : Multiset β) =
    (↑((Sym.map f ∘ fun (p : Sym α n) ↦ x ::ₛ p) s) : Multiset β)

Tactic:
simp only [Function.comp_apply, Sym.map_cons]

Premises used: Function.comp_apply, Sym.map_cons
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n : ℕ
xs_1 ys_1 : List α
h : xs_1 <+ ys_1
ys xs : List α
h_1 : xs <+ ys
⊢ Sublist (α := Sym α 0) (List.sym 0 xs) (List.sym 0 ys)

Tactic:
simp [List.sym]

Premises used: List.sym
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs ys : List α
h : xs <+ ys
n : ℕ
⊢ Sublist.{u_1} (α := Sym α (n + 1)) (List.sym (n + 1) []) (List.sym (n + 1) [])

Tactic:
simp only [refl]

Premises used: List.Sublist.refl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 ys : List α
h_1 : xs_1 <+ ys
xs : List α
n : ℕ
l₂ : List α
a : α
h : xs <+ l₂
rw :
  HAppend.hAppend (α := List (Sym α (n + 1))) [] (List.sym (n + 1) xs) <+
    HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₂)))
      (List.sym (n + 1) l₂)
⊢ Sublist (α := Sym α (n + 1)) (List.sym (n + 1) xs) (List.sym (n + 1) (a :: l₂))

Tactic:
rw [List.sym, ← nil_append (List.sym (n + 1) xs)]

Premises used: HAdd.hAdd, List.nil_append, List.sym, OfNat.ofNat
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 ys : List α
h_1 : xs_1 <+ ys
xs : List α
n : ℕ
l₂ : List α
a : α
h : xs <+ l₂
apply : Sublist (α := Sym α (n + 1)) (List.sym (n + 1) xs) (List.sym (n + 1) l₂)
⊢ HAppend.hAppend (α := List (Sym α (n + 1))) [] (List.sym (n + 1) xs) <+
    HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₂)))
      (List.sym (n + 1) l₂)

Tactic:
apply Sublist.append (nil_sublist _)

Premises used: List.nil_sublist, List.Sublist.append
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 ys : List α
h_1 : xs_1 <+ ys
xs : List α
n : ℕ
l₂ : List α
a : α
h : xs <+ l₂
⊢ Sublist (α := Sym α (n + 1)) (List.sym (n + 1) xs) (List.sym (n + 1) l₂)

Tactic:
h.sym (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 ys : List α
h_1 : xs_1 <+ ys
xs : List α
n : ℕ
l₂ : List α
a : α
h : xs <+ l₂
⊢ Sublist (α := Sym α (n + 1)) (List.sym (n + 1) xs) (List.sym (n + 1) l₂)

Tactic:
exact h.sym (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs ys : List α
h_1 : xs <+ ys
n : ℕ
l₁ l₂ : List α
a : α
h : l₁ <+ l₂
rw :
  HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₁)))
      (List.sym (n + 1) l₁) <+
    HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₂)))
      (List.sym (n + 1) l₂)
⊢ Sublist (α := Sym α (n + 1)) (List.sym (n + 1) (a :: l₁)) (List.sym (n + 1) (a :: l₂))

Tactic:
rw [List.sym, List.sym]

Premises used: List.sym
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs ys : List α
h_1 : xs <+ ys
n : ℕ
l₁ l₂ : List α
a : α
h : l₁ <+ l₂
hl :
  Sublist (α := Sym α (n + 1)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₁)))
    (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₂)))
hr : Sublist (α := Sym α (n + 1)) (List.sym (n + 1) l₁) (List.sym (n + 1) l₂)
⊢ HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₁)))
      (List.sym (n + 1) l₁) <+
    HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₂)))
      (List.sym (n + 1) l₂)

Tactic:
apply Sublist.append

Premises used: List.Sublist.append
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs ys : List α
h_1 : xs <+ ys
n : ℕ
l₁ l₂ : List α
a : α
h : l₁ <+ l₂
⊢ Sublist (α := Sym α (n + 1)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₁)))
    (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₂)))

Tactic:
((cons_cons a h).sym n).map _

Premises used: List.Sublist.map, List.Sublist.cons_cons
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs ys : List α
h_1 : xs <+ ys
n : ℕ
l₁ l₂ : List α
a : α
h : l₁ <+ l₂
⊢ Sublist (α := Sym α (n + 1)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₁)))
    (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₂)))

Tactic:
exact ((cons_cons a h).sym n).map _

Premises used: List.Sublist.map, List.Sublist.cons_cons
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs ys : List α
h_1 : xs <+ ys
n : ℕ
l₁ l₂ : List α
a : α
h : l₁ <+ l₂
⊢ Sublist (α := Sym α (n + 1)) (List.sym (n + 1) l₁) (List.sym (n + 1) l₂)

Tactic:
h.sym (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs ys : List α
h_1 : xs <+ ys
n : ℕ
l₁ l₂ : List α
a : α
h : l₁ <+ l₂
⊢ Sublist (α := Sym α (n + 1)) (List.sym (n + 1) l₁) (List.sym (n + 1) l₂)

Tactic:
exact h.sym (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
n : ℕ
a : α
⊢ List.sym n xs <+ List.sym n (a :: xs)

Tactic:
(sublist_cons_self a xs).sym n

Premises used: List.Sublist.sym, List.sublist_cons_self
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n : ℕ
xs_1 : List α
a : α
xs : List α
z : Sym α 0
ha : a ∈ z
hz : Membership.mem (γ := List (Sym α 0)) (List.sym 0 xs) z
⊢ Membership.mem (γ := Sym α 0) Sym.nil a

Tactic:
cases Sym.eq_nil_of_card_zero z

Premises used: Sym.eq_nil_of_card_zero
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n : ℕ
xs_1 : List α
a : α
xs : List α
z : Sym α 0
ha : a ∈ z
hz : Membership.mem (γ := List (Sym α 0)) (List.sym 0 xs) z
ha₁ : Membership.mem (γ := Sym α 0) Sym.nil a
⊢ Membership.mem (γ := List (Sym α 0)) (List.sym 0 xs) Sym.nil

Tactic:
cases Sym.eq_nil_of_card_zero z

Premises used: Sym.eq_nil_of_card_zero
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n : ℕ
xs_1 : List α
a : α
xs : List α
ha : Membership.mem (γ := Sym α 0) Sym.nil a
hz : Membership.mem (γ := List (Sym α 0)) (List.sym 0 xs) Sym.nil
⊢ a ∈ xs

Tactic:
simp at ha
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs : List α
a : α
n : ℕ
z : Sym α (n + 1)
ha : a ∈ z
hz : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) []) z
⊢ Membership.mem (γ := List α) [] a

Tactic:
simp [List.sym] at hz

Premises used: List.sym
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) (x :: xs)) z
⊢ (∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z) ∨ Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z

Tactic:
rw [List.sym, mem_append, mem_map] at hz

Premises used: List.mem_append, List.sym, List.mem_map
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : (∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z) ∨ Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
inl : ∀ (z : Sym α n) (hz : z ∈ List.sym n (x :: xs)) (ha : a ∈ x ::ₛ z), a ∈ x :: xs
inr : ∀ (hz : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z), a ∈ x :: xs
⊢ a ∈ x :: xs

Tactic:
obtain ⟨z, hz, rfl⟩ | hz := hz

Premises used: rfl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a ∈ x ::ₛ z
⊢ a = x ∨ a ∈ z

Tactic:
rw [Sym.mem_cons] at ha

Premises used: Sym.mem_cons
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a = x ∨ a ∈ z
inl : ∀ (hz : z ∈ List.sym n (a :: xs)), a ∈ a :: xs
inl₁ : ∀ (ha : a ∈ z), a ∈ x :: xs
⊢ a ∈ x :: xs

Tactic:
obtain rfl | ha := ha

Premises used: rfl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
xs : List α
z : Sym α n
hz : z ∈ List.sym n (a :: xs)
⊢ a ∈ a :: xs

Tactic:
simp
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a ∈ z
⊢ a ∈ x :: xs

Tactic:
mem_of_mem_of_mem_sym ha hz
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a ∈ z
⊢ a ∈ x :: xs

Tactic:
exact mem_of_mem_of_mem_sym ha hz
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
inr : a = x ∨ a ∈ xs
⊢ a ∈ x :: xs

Tactic:
rw [mem_cons]

Premises used: List.mem_cons
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
inr : a ∈ xs
⊢ a = x ∨ a ∈ xs

Tactic:
right
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
⊢ a ∈ xs

Tactic:
mem_of_mem_of_mem_sym ha hz
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
⊢ a ∈ xs

Tactic:
exact mem_of_mem_of_mem_sym ha hz
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
n : ℕ
a : α
z : Sym α n
h : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) (a ::ₛ z)
⊢ a ∈ xs

Tactic:
mem_of_mem_of_mem_sym (Sym.mem_cons_self a z) h

Premises used: Sym.mem_cons_self, List.mem_of_mem_of_mem_sym
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n : ℕ
xs x : List α
h : x.Nodup
⊢ Nodup (α := Sym α 0) (List.sym 0 x)

Tactic:
simp [List.sym]

Premises used: List.sym
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs : List α
n : ℕ
h : Nodup.{u_1} (α := α) []
⊢ Nodup.{u_1} (α := Sym α (n + 1)) (List.sym (n + 1) [])

Tactic:
simp [List.sym]

Premises used: List.sym
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
rw :
  (HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs)))
      (List.sym (n + 1) xs)).Nodup
⊢ Nodup (α := Sym α (n + 1)) (List.sym (n + 1) (x :: xs))

Tactic:
rw [List.sym]

Premises used: List.sym
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs)))
      (List.sym (n + 1) xs)).Nodup

Tactic:
Nodup.append (Nodup.map ?inj (Nodup.sym n h)) (Nodup.sym (n + 1) h.of_cons) ?disj

Premises used: List.Nodup.append, List.Nodup.map, HAdd.hAdd, List.Nodup.of_cons, OfNat.ofNat
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
refine : Function.Injective (β := Sym α (n + 1)) fun (p : Sym α n) ↦ x ::ₛ p
refine₁ : Disjoint (α := Sym α (n + 1)) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) (List.sym (n + 1) xs)
⊢ (HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs)))
      (List.sym (n + 1) xs)).Nodup

Tactic:
refine Nodup.append (Nodup.map ?inj (Nodup.sym n h)) (Nodup.sym (n + 1) h.of_cons) ?disj

Premises used: List.Nodup.append, List.Nodup.map, HAdd.hAdd, List.Nodup.of_cons, OfNat.ofNat
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z z' : Sym α n
⊢ Eq.{u_1 + 1} (α := Sym α (n + 1)) ((fun (p : Sym α n) ↦ x ::ₛ p) z) ((fun (p : Sym α n) ↦ x ::ₛ p) z') → z = z'

Tactic:
simp
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ Function.Injective (β := Sym α (n + 1)) fun (p : Sym α n) ↦ x ::ₛ p

Tactic:
case inj =>
      intro z z'
      simp
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : Membership.mem (γ := List (Sym α (n + 1))) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) z
hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
⊢ ∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z

Tactic:
rw [mem_map] at hz

Premises used: List.mem_map
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : Membership.mem (γ := List (Sym α (n + 1))) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) z
hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
hz₁ : ∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z
⊢ Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z

Tactic:
rw [mem_map] at hz

Premises used: List.mem_map
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : ∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z
hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
obtain :
  ∀ (z : Sym α n) (_hz : z ∈ List.sym n (x :: xs))
    (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) (x ::ₛ z)), False
⊢ False

Tactic:
obtain ⟨z, _hz, rfl⟩ := hz

Premises used: rfl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α n
_hz : z ∈ List.sym n (x :: xs)
hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) (x ::ₛ z)
⊢ x ∈ xs

Tactic:
have := first_mem_of_cons_mem_sym hz'
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α n
_hz : z ∈ List.sym n (x :: xs)
hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) (x ::ₛ z)
this : x ∈ xs
⊢ False

Tactic:
simp only [nodup_cons, this, not_true_eq_false, false_and] at h

Premises used: false_and, not_true_eq_false, List.nodup_cons
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
case case₁ case₂ :
  ∀ ⦃z : Sym α (n + 1)⦄
    (hz : Membership.mem (γ := List (Sym α (n + 1))) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) z)
    (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z), False
case₃ :
  ∀ ⦃z : Sym α (n + 1)⦄ (hz : ∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z)
    (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z), False
case₄ :
  ∀ (z : Sym α n) (_hz : z ∈ List.sym n (x :: xs))
    (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) (x ::ₛ z)), False
case₅ :
  ∀ (z : Sym α n) (_hz : z ∈ List.sym n (x :: xs))
    (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) (x ::ₛ z)) (this : x ∈ xs), False
⊢ Disjoint (α := Sym α (n + 1)) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) (List.sym (n + 1) xs)

Tactic:
case disj =>
      intro z hz hz'
      rw [mem_map] at hz
      obtain ⟨z, _hz, rfl⟩ := hz
      have := first_mem_of_cons_mem_sym hz'
      simp only [nodup_cons, this, not_true_eq_false, false_and] at h

Premises used: false_and, not_true_eq_false, List.nodup_cons, List.mem_map, rfl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n : ℕ
xs x : List α
rw : length.{u_1} (α := Sym α 0) [Sym.nil] = 1
⊢ length (α := Sym α 0) (List.sym 0 x) = x.length.multichoose 0

Tactic:
rw [List.sym, Nat.multichoose]

Premises used: List.sym, Nat.multichoose
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n : ℕ
xs x : List α
⊢ length.{u_1} (α := Sym α 0) [Sym.nil] = 1

Tactic:
rfl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs : List α
n : ℕ
⊢ length.{u_1} (α := Sym α (n + 1)) (List.sym (n + 1) []) = (length.{u_1} (α := α) []).multichoose (n + 1)

Tactic:
simp [List.sym]

Premises used: List.sym
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
rw :
  (List.sym n (x :: xs)).length + length (α := Sym α (n + 1)) (List.sym (n + 1) xs) =
    (xs.length + 1).multichoose (n + 1)
⊢ length (α := Sym α (n + 1)) (List.sym (n + 1) (x :: xs)) = (x :: xs).length.multichoose (n + 1)

Tactic:
rw [List.sym, length_append, length_map, length_cons]

Premises used: List.length_cons, List.length_append, List.length_map, List.sym
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
rw : (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) = (xs.length + 1).multichoose (n + 1)
⊢ (List.sym n (x :: xs)).length + length (α := Sym α (n + 1)) (List.sym (n + 1) xs) =
    (xs.length + 1).multichoose (n + 1)

Tactic:
rw [@length_sym n (x :: xs), @length_sym (n + 1) xs]
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
rw :
  (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) =
    xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n
rw₁ :
  (xs.length + 1).multichoose n + xs.length.multichoose (n + 1) =
    xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n
rw₂ rw₃ :
  xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n =
    xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n
⊢ (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) = (xs.length + 1).multichoose (n + 1)

Tactic:
rw [Nat.multichoose_succ_succ, length_cons, add_comm]

Premises used: List.length_cons, add_comm, Nat.multichoose_succ_succ
-- Module: Mathlib.Data.List.TFAE
Goal:
⊢ TFAE []

Tactic:
forall_mem_nil _

Premises used: List.TFAE, List.forall_mem_nil
-- Module: Mathlib.Data.List.TFAE
Goal:
p : Prop
⊢ [p].TFAE

Tactic:
simp [TFAE, -eq_iff_iff]

Premises used: List.TFAE, eq_iff_iff
-- Module: Mathlib.Data.List.TFAE
Goal:
a b : Prop
l : List Prop
h : b ∈ l
H : (a :: l).TFAE
⊢ a ∈ a :: l

Tactic:
simp
-- Module: Mathlib.Data.List.TFAE
Goal:
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
⊢ a ↔ a

Tactic:
rfl
-- Module: Mathlib.Data.List.TFAE
Goal:
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
q : Prop
hq : Mem q l
⊢ a ↔ q

Tactic:
ab.trans (H _ h _ hq)

Premises used: Iff.trans
-- Module: Mathlib.Data.List.TFAE
Goal:
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
q : Prop
hq : Mem q l
⊢ a ↔ q

Tactic:
exact ab.trans (H _ h _ hq)

Premises used: Iff.trans
-- Module: Mathlib.Data.List.TFAE
Goal:
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
⊢ p ↔ a

Tactic:
(ab.trans (H _ h _ hp)).symm

Premises used: Iff.trans, Iff.symm
-- Module: Mathlib.Data.List.TFAE
Goal:
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
⊢ p ↔ a

Tactic:
exact (ab.trans (H _ h _ hp)).symm

Premises used: Iff.trans, Iff.symm
-- Module: Mathlib.Data.List.TFAE
Goal:
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
q : Prop
hq : Mem q l
⊢ p ↔ q

Tactic:
H _ hp _ hq
-- Module: Mathlib.Data.List.TFAE
Goal:
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
p : Prop
hp : Mem p l
q : Prop
hq : Mem q l
⊢ p ↔ q

Tactic:
exact H _ hp _ hq
-- Module: Mathlib.Data.List.TFAE
Goal:
a b : Prop
l : List Prop
⊢ (a :: b :: l).TFAE ↔ (a ↔ b) ∧ (b :: l).TFAE

Tactic:
tfae_cons_of_mem (Mem.head _)

Premises used: List.tfae_cons_of_mem, List.Mem.head
-- Module: Mathlib.Data.List.TFAE
Goal:
a : Prop
l : List Prop
⊢ (a :: a :: l).TFAE ↔ (a :: l).TFAE

Tactic:
simp [tfae_cons_cons]

Premises used: List.tfae_cons_cons
-- Module: Mathlib.Data.List.TFAE
Goal:
b : Prop
l : List Prop
h : ∀ (a : Prop), a ∈ l → (a ↔ b)
⊢ l.TFAE

Tactic:
fun _a₁ h₁ _a₂ h₂ => (h _ h₁).trans (h _ h₂).symm

Premises used: List.TFAE, Iff.trans, Iff.symm
-- Module: Mathlib.Data.List.TFAE
Goal:
a b : Prop
h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) [a, b]
h_last : getLastD [] b → a
⊢ [a, b].TFAE

Tactic:
simp_all [tfae_cons_cons, iff_def]

Premises used: iff_def, List.tfae_cons_cons
-- Module: Mathlib.Data.List.TFAE
Goal:
c : Prop
l : List Prop
IH :
  ∀ {a b : Prop} (h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (a :: b :: l)) (h_last : l.getLastD b → a),
    (a :: b :: l).TFAE
a b : Prop
h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (a :: b :: c :: l)
h_last : (c :: l).getLastD b → a
cons :
  ∀
    (IH :
      ∀ {a b : Prop} (h_chain : (a → b) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (b :: l)) (h_last : l.getLastD b → a),
        (a ↔ b) ∧ (b :: l).TFAE)
    (h_chain : (a → b) ∧ (b → c) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (c :: l)) (h_last : l.getLastD c → a),
    (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE
⊢ (a :: b :: c :: l).TFAE

Tactic:
simp only [tfae_cons_cons, getLastD_cons, isChain_cons_cons] at *

Premises used: List.isChain_cons_cons, List.tfae_cons_cons, List.getLastD_cons
-- Module: Mathlib.Data.List.TFAE
Goal:
c : Prop
l : List Prop
a b : Prop
IH :
  ∀ {a b : Prop} (h_chain : (a → b) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (b :: l)) (h_last : l.getLastD b → a),
    (a ↔ b) ∧ (b :: l).TFAE
h_chain : (a → b) ∧ (b → c) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (c :: l)
h_last : l.getLastD c → a
⊢ a → b

Tactic:
rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩
-- Module: Mathlib.Data.List.TFAE
Goal:
c : Prop
l : List Prop
a b : Prop
IH :
  ∀ {a b : Prop} (h_chain : (a → b) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (b :: l)) (h_last : l.getLastD b → a),
    (a ↔ b) ∧ (b :: l).TFAE
h_chain : (a → b) ∧ (b → c) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (c :: l)
h_last : l.getLastD c → a
ab : a → b
⊢ b → c

Tactic:
rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩