awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
cons : ∀ (hm : x ∈ xs), (s(x, x) :: (map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2
cons₁ : ∀ (hm : x ∉ xs), (s(x, x) :: (map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2
⊢ (s(x, x) :: (map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2

Tactic:
obtain hm | hm := Decidable.em (x ∈ xs)

Premises used: Membership.mem, Decidable.em
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
cons : s(x, x) ∈ map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2
⊢ (s(x, x) :: (map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2

Tactic:
rw [dedup_cons_of_mem hm, ← ih, dedup_cons_of_mem,
        List.Subset.dedup_append_right (map_mk_sublist_sym2 _ _ hm).subset]

Premises used: List.Subset.dedup_append_right, List.Sublist.subset, List.map_mk_sublist_sym2, List.dedup_cons_of_mem
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ s(x, x) ∈ map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2

Tactic:
mem_append_left _ ?_

Premises used: List.mem_append_left
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
cons : Membership.mem (γ := List (Sym2 α)) (map (fun (y : α) ↦ s(x, y)) xs) s(x, x)
⊢ s(x, x) ∈ map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2

Tactic:
refine mem_append_left _ ?_

Premises used: List.mem_append_left
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
cons : ∃ a ∈ xs, s(x, a) = s(x, x)
⊢ Membership.mem (γ := List (Sym2 α)) (map (fun (y : α) ↦ s(x, y)) xs) s(x, x)

Tactic:
rw [mem_map]

Premises used: List.mem_map
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ ∃ a ∈ xs, s(x, a) = s(x, x)

Tactic:
⟨_, hm, Sym2.eq_swap⟩

Premises used: Sym2.eq_swap, And.intro, Exists.intro
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ ∃ a ∈ xs, s(x, a) = s(x, x)

Tactic:
exact ⟨_, hm, Sym2.eq_swap⟩
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
cons : Function.Injective (β := Sym2 α) fun (y : α) ↦ s(x, y)
cons₁ : Disjoint (map (fun (y : α) ↦ s(x, y)) xs) xs.sym2
cons₂ : s(x, x) ∉ map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2
⊢ (s(x, x) :: (map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2

Tactic:
rw [dedup_cons_of_notMem hm, List.sym2, map_cons, ← ih, dedup_cons_of_notMem, cons_append,
        List.Disjoint.dedup_append, dedup_map_of_injective]

Premises used: List.Disjoint.dedup_append, List.map_cons, List.dedup_cons_of_notMem, List.sym2, List.cons_append, List.dedup_map_of_injective
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ Function.Injective (β := Sym2 α) fun (y : α) ↦ s(x, y)

Tactic:
(Sym2.mkEmbedding _).injective

Premises used: Function.Embedding.injective, Sym2.mkEmbedding
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ Function.Injective (β := Sym2 α) fun (y : α) ↦ s(x, y)

Tactic:
exact (Sym2.mkEmbedding _).injective

Premises used: Function.Embedding.injective, Sym2.mkEmbedding
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ Disjoint (map (fun (y : α) ↦ s(x, y)) xs) xs.sym2

Tactic:
map_mk_disjoint_sym2 x xs hm

Premises used: List.map_mk_disjoint_sym2
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ Disjoint (map (fun (y : α) ↦ s(x, y)) xs) xs.sym2

Tactic:
exact map_mk_disjoint_sym2 x xs hm

Premises used: List.map_mk_disjoint_sym2
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ s(x, x) ∉ map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2

Tactic:
simp [hm, mem_sym2_iff]

Premises used: List.mem_sym2_iff
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
nil : Eq.{u_1 + 1} (α := List (Sym2 α)) (dedup (List.sym2 [])) (List.sym2 (dedup []))
cons : ∀ (x : α) (xs : List α) (ih : xs.sym2.dedup = xs.dedup.sym2), (x :: xs).sym2.dedup = (x :: xs).dedup.sym2
⊢ xs.sym2.dedup = xs.dedup.sym2

Tactic:
induction xs with
  | nil => simp only [List.sym2, dedup_nil]
  | cons x xs ih =>
    simp only [List.sym2, map_cons, cons_append]
    obtain hm | hm := Decidable.em (x ∈ xs)
    · rw [dedup_cons_of_mem hm, ← ih, dedup_cons_of_mem,
        List.Subset.dedup_append_right (map_mk_sublist_sym2 _ _ hm).subset]
      refine mem_append_left _ ?_
      rw [mem_map]
      exact ⟨_, hm, Sym2.eq_swap⟩
    · rw [dedup_cons_of_notMem hm, List.sym2, map_cons, ← ih, dedup_cons_of_notMem, cons_append,
        List.Disjoint.dedup_append, dedup_map_of_injective]
      · exact (Sym2.mkEmbedding _).injective
      · exact map_mk_disjoint_sym2 x xs hm
      · simp [hm, mem_sym2_iff]

Premises used: List.Disjoint.dedup_append, List.dedup_nil, List.map_cons, List.dedup_cons_of_notMem, List.mem_append_left, List.cons, List.sym2, Function.Embedding.injective, List.dedup_cons_of_mem, List.mem_map, List.mem_sym2_iff, List.cons_append, List.dedup_map_of_injective, Sym2.mkEmbedding, List.nil
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys : List α
⊢ Perm.{u_1} (α := Sym2 α) (List.sym2 []) (List.sym2 [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys : List α
x : α
l₁ l₂ : List α
h : l₁ ~ l₂
ih : l₁.sym2 ~ l₂.sym2
cons : List.map (fun (y : α) ↦ s(x, y)) l₁ ++ l₁.sym2 ~ List.map (fun (y : α) ↦ s(x, y)) l₂ ++ l₂.sym2
⊢ (x :: l₁).sym2 ~ (x :: l₂).sym2

Tactic:
simp only [List.sym2, map_cons, cons_append, perm_cons]

Premises used: List.map_cons, List.perm_cons, List.sym2, List.cons_append
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys : List α
x : α
l₁ l₂ : List α
h : l₁ ~ l₂
ih : l₁.sym2 ~ l₂.sym2
⊢ List.map (fun (y : α) ↦ s(x, y)) l₁ ++ l₁.sym2 ~ List.map (fun (y : α) ↦ s(x, y)) l₂ ++ l₂.sym2

Tactic:
(h.map _).append ih

Premises used: List.Perm.append, List.Perm.map
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys : List α
x : α
l₁ l₂ : List α
h : l₁ ~ l₂
ih : l₁.sym2 ~ l₂.sym2
⊢ List.map (fun (y : α) ↦ s(x, y)) l₁ ++ l₁.sym2 ~ List.map (fun (y : α) ↦ s(x, y)) l₂ ++ l₂.sym2

Tactic:
exact (h.map _).append ih

Premises used: List.Perm.append, List.Perm.map
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs_1 ys : List α
x y : α
xs : List α
enter : s(y, x)
| s(y, y) ::
      s(y, x) ::
        (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) ::
      s(x, y) ::
        (List.map (fun (y : α) ↦ s(x, y)) xs ++ s(y, y) :: (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ xs.sym2))

Tactic:
enter [1, 2, 1]
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs_1 ys : List α
x y : α
xs : List α
rw : s(x, y)
| s(y, x)

Tactic:
rw [Sym2.eq_swap]

Premises used: Sym2.eq_swap
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs_1 ys : List α
x y : α
xs : List α
enter : s(x, y)
| s(y, y) ::
      s(y, x) ::
        (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) ::
      s(x, y) ::
        (List.map (fun (y : α) ↦ s(x, y)) xs ++ s(y, y) :: (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ xs.sym2))

Tactic:
enter [1, 2, 1]; rw [Sym2.eq_swap]

Premises used: Sym2.eq_swap
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs_1 ys : List α
x y : α
xs : List α
swap :
  s(y, y) ::
      s(x, y) ::
        (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) ::
      s(x, y) ::
        (List.map (fun (y : α) ↦ s(x, y)) xs ++ s(y, y) :: (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ xs.sym2))
⊢ s(y, y) ::
      s(y, x) ::
        (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) ::
      s(x, y) ::
        (List.map (fun (y : α) ↦ s(x, y)) xs ++ s(y, y) :: (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ xs.sym2))

Tactic:
conv => enter [1, 2, 1]; rw [Sym2.eq_swap]

Premises used: Sym2.eq_swap
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs_1 ys : List α
x y : α
xs : List α
⊢ s(y, y) ::
      s(x, y) ::
        (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) ::
      s(x, y) ::
        (List.map (fun (y : α) ↦ s(x, y)) xs ++ s(y, y) :: (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ xs.sym2))

Tactic:
Perm.trans (Perm.swap ..) (Perm.trans (Perm.cons _ ?_) (Perm.swap ..))

Premises used: List.Perm.cons, List.Perm.swap, List.Perm.trans
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs_1 ys : List α
x y : α
xs : List α
swap :
  s(y, y) :: (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) :: (List.map (fun (y : α) ↦ s(x, y)) xs ++ s(y, y) :: (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ xs.sym2))
⊢ s(y, y) ::
      s(x, y) ::
        (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) ::
      s(x, y) ::
        (List.map (fun (y : α) ↦ s(x, y)) xs ++ s(y, y) :: (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ xs.sym2))

Tactic:
refine Perm.trans (Perm.swap ..) (Perm.trans (Perm.cons _ ?_) (Perm.swap ..))

Premises used: List.Perm.cons, List.Perm.swap, List.Perm.trans
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs_1 ys : List α
x y : α
xs : List α
swap :
  {s(y, y)} +
      ((↑(List.map (fun (y_1 : α) ↦ s(y, y_1)) xs) : Multiset (Sym2 α)) +
        ({s(x, x)} + ((↑(List.map (fun (y : α) ↦ s(x, y)) xs) : Multiset (Sym2 α)) + (↑xs.sym2 : Multiset (Sym2 α))))) =
    {s(x, x)} +
      ((↑(List.map (fun (y : α) ↦ s(x, y)) xs) : Multiset (Sym2 α)) +
        ({s(y, y)} +
          ((↑(List.map (fun (y_1 : α) ↦ s(y, y_1)) xs) : Multiset (Sym2 α)) + (↑xs.sym2 : Multiset (Sym2 α)))))
⊢ s(y, y) :: (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) :: (List.map (fun (y : α) ↦ s(x, y)) xs ++ s(y, y) :: (List.map (fun (y_1 : α) ↦ s(y, y_1)) xs ++ xs.sym2))

Tactic:
simp only [← Multiset.coe_eq_coe, ← Multiset.cons_coe,
      ← Multiset.coe_add, ← Multiset.singleton_add]

Premises used: Multiset.coe_add, Multiset.singleton_add, Multiset.coe_eq_coe, Multiset.cons_coe
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs_1 ys : List α
x y : α
xs : List α
⊢ {s(y, y)} +
      ((↑(List.map (fun (y_1 : α) ↦ s(y, y_1)) xs) : Multiset (Sym2 α)) +
        ({s(x, x)} + ((↑(List.map (fun (y : α) ↦ s(x, y)) xs) : Multiset (Sym2 α)) + (↑xs.sym2 : Multiset (Sym2 α))))) =
    {s(x, x)} +
      ((↑(List.map (fun (y : α) ↦ s(x, y)) xs) : Multiset (Sym2 α)) +
        ({s(y, y)} +
          ((↑(List.map (fun (y_1 : α) ↦ s(y, y_1)) xs) : Multiset (Sym2 α)) + (↑xs.sym2 : Multiset (Sym2 α)))))

Tactic:
simp only [add_left_comm]

Premises used: add_left_comm
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys l₁ l₂ l₃ : List α
h : l₁ ~ l₂
h_1 : l₂ ~ l₃
ih1 : l₁.sym2 ~ l₂.sym2
ih2 : l₂.sym2 ~ l₃.sym2
⊢ l₁.sym2 ~ l₃.sym2

Tactic:
ih1.trans ih2

Premises used: List.Perm.trans
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys l₁ l₂ l₃ : List α
h : l₁ ~ l₂
h_1 : l₂ ~ l₃
ih1 : l₁.sym2 ~ l₂.sym2
ih2 : l₂.sym2 ~ l₃.sym2
⊢ l₁.sym2 ~ l₃.sym2

Tactic:
exact ih1.trans ih2

Premises used: List.Perm.trans
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys : List α
h : xs ~ ys
nil : Perm.{u_1} (α := Sym2 α) (List.sym2 []) (List.sym2 [])
cons : ∀ (x : α) {l₁ l₂ : List α} (h : l₁ ~ l₂) (ih : l₁.sym2 ~ l₂.sym2), (x :: l₁).sym2 ~ (x :: l₂).sym2
swap : ∀ (x y : α) (xs : List α), (y :: x :: xs).sym2 ~ (x :: y :: xs).sym2
trans :
  ∀ {l₁ l₂ l₃ : List α}, l₁ ~ l₂ → l₂ ~ l₃ → ∀ (ih1 : l₁.sym2 ~ l₂.sym2) (ih2 : l₂.sym2 ~ l₃.sym2), l₁.sym2 ~ l₃.sym2
⊢ xs.sym2 ~ ys.sym2

Tactic:
induction h with
  | nil => rfl
  | cons x h ih =>
    simp only [List.sym2, map_cons, cons_append, perm_cons]
    exact (h.map _).append ih
  | swap x y xs =>
    simp only [List.sym2, map_cons, cons_append]
    conv => enter [1, 2, 1]; rw [Sym2.eq_swap]
    -- Explicit permutation to speed up simps that follow.
    refine Perm.trans (Perm.swap ..) (Perm.trans (Perm.cons _ ?_) (Perm.swap ..))
    simp only [← Multiset.coe_eq_coe, ← Multiset.cons_coe,
      ← Multiset.coe_add, ← Multiset.singleton_add]
    simp only [add_left_comm]
  | trans _ _ ih1 ih2 => exact ih1.trans ih2

Premises used: Multiset.coe_add, Multiset.singleton_add, List.map_cons, add_left_comm, List.Perm.cons, Multiset.coe_eq_coe, List.Perm.swap, List.Perm.trans, Sym2.eq_swap, List.perm_cons, List.sym2, Multiset.cons_coe, List.Perm.nil, List.cons_append
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys : List α
⊢ Sublist.{u_1} (α := Sym2 α) (List.sym2 []) (List.sym2 [])

Tactic:
apply slnil

Premises used: List.Sublist.slnil
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys l₁ l₂ : List α
a : α
h : l₁ <+ l₂
ih : l₁.sym2 <+ l₂.sym2
⊢ l₁.sym2 <+ map (fun (y : α) ↦ s(a, y)) (a :: l₂) ++ l₂.sym2

Tactic:
Sublist.append (nil_sublist _) ih

Premises used: List.append, List.nil_sublist, List.Sublist.append
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys l₁ l₂ : List α
a : α
h : l₁ <+ l₂
ih : l₁.sym2 <+ l₂.sym2
⊢ l₁.sym2 <+ map (fun (y : α) ↦ s(a, y)) (a :: l₂) ++ l₂.sym2

Tactic:
exact Sublist.append (nil_sublist _) ih

Premises used: List.nil_sublist, List.Sublist.append
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys l₁ l₂ : List α
a : α
h : l₁ <+ l₂
ih : l₁.sym2 <+ l₂.sym2
⊢ s(a, a) :: (map (fun (y : α) ↦ s(a, y)) l₁ ++ l₁.sym2) <+ s(a, a) :: (map (fun (y : α) ↦ s(a, y)) l₂ ++ l₂.sym2)

Tactic:
cons_cons _ (append (Sublist.map _ h) ih)

Premises used: List.Sublist.map, List.Sublist.cons_cons, List.Sublist.append
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys l₁ l₂ : List α
a : α
h : l₁ <+ l₂
ih : l₁.sym2 <+ l₂.sym2
⊢ s(a, a) :: (map (fun (y : α) ↦ s(a, y)) l₁ ++ l₁.sym2) <+ s(a, a) :: (map (fun (y : α) ↦ s(a, y)) l₂ ++ l₂.sym2)

Tactic:
exact cons_cons _ (append (Sublist.map _ h) ih)

Premises used: List.Sublist.map, List.Sublist.cons_cons, List.Sublist.append
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys : List α
h : xs <+ ys
slnil : Sublist.{u_1} (α := Sym2 α) (List.sym2 []) (List.sym2 [])
cons : ∀ {l₁ l₂ : List α} (a : α) (h : l₁ <+ l₂) (ih : l₁.sym2 <+ l₂.sym2), l₁.sym2 <+ (a :: l₂).sym2
cons_cons : ∀ {l₁ l₂ : List α} (a : α) (h : l₁ <+ l₂) (ih : l₁.sym2 <+ l₂.sym2), (a :: l₁).sym2 <+ (a :: l₂).sym2
⊢ xs.sym2 <+ ys.sym2

Tactic:
induction h with
  | slnil => apply slnil
  | cons a h ih =>
    simp only [List.sym2]
    exact Sublist.append (nil_sublist _) ih
  | cons_cons a h ih =>
    simp only [List.sym2, map_cons, cons_append]
    exact cons_cons _ (append (Sublist.map _ h) ih)

Premises used: List.map_cons, List.Sublist.cons_cons, List.Sublist.slnil, List.sym2, List.Sublist.cons, List.cons_append
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys : List α
h : xs <+~ ys
obtain : ∀ (xs' : List α) (hx : xs' ~ xs) (h : xs' <+ ys), xs.sym2 <+~ ys.sym2
⊢ xs.sym2 <+~ ys.sym2

Tactic:
obtain ⟨xs', hx, h⟩ := h
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys xs' : List α
hx : xs' ~ xs
h : xs' <+ ys
⊢ xs.sym2 <+~ ys.sym2

Tactic:
hx.sym2.symm.subperm.trans h.sym2.subperm

Premises used: List.Perm.sym2, List.Sublist.sym2, List.Subperm.trans, List.Perm.subperm, List.Perm.symm, List.Sublist.subperm
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs ys xs' : List α
hx : xs' ~ xs
h : xs' <+ ys
⊢ xs.sym2 <+~ ys.sym2

Tactic:
exact hx.sym2.symm.subperm.trans h.sym2.subperm

Premises used: List.Perm.sym2, List.Sublist.sym2, List.Subperm.trans, List.Perm.subperm, List.Perm.symm, List.Sublist.subperm
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
⊢ length.{u_1} (α := Sym2 α) (List.sym2 []) = (length.{u_1} (α := α) [] + 1).choose 2

Tactic:
rfl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
ih : xs.sym2.length = (xs.length + 1).choose 2
cons : (map (fun (y : α) ↦ s(x, y)) (x :: xs) ++ xs.sym2).length = ((x :: xs).length + 1).choose 2
cons₁ : length (α := Sym2 α) (map (fun (y : α) ↦ s(x, y)) (x :: xs)) + xs.sym2.length = ((x :: xs).length + 1).choose 2
cons₂ : (x :: xs).length + xs.sym2.length = ((x :: xs).length + 1).choose 2
cons₃ : xs.length + 1 + xs.sym2.length = (xs.length + 1 + 1).choose 2
cons₄ : xs.length + 1 + xs.sym2.length = (xs.length + 1).choose 1 + (xs.length + 1).choose (Nat.succ 1)
cons₅ : xs.length + 1 + xs.sym2.length = (xs.length + 1).choose 1 + xs.sym2.length
cons₆ cons₇ : xs.length + 1 + xs.sym2.length = xs.length + 1 + xs.sym2.length
⊢ (x :: xs).sym2.length = ((x :: xs).length + 1).choose 2

Tactic:
rw [List.sym2, length_append, length_map, length_cons,
        Nat.choose_succ_succ, ← ih, Nat.choose_one_right]

Premises used: List.length_cons, Nat.choose_succ_succ, List.length_append, Nat.choose_one_right, List.sym2, List.length_map
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
nil : length.{u_1} (α := Sym2 α) (List.sym2 []) = (length.{u_1} (α := α) [] + 1).choose 2
cons :
  ∀ (x : α) (xs : List α) (ih : xs.sym2.length = (xs.length + 1).choose 2),
    (x :: xs).sym2.length = ((x :: xs).length + 1).choose 2
⊢ xs.sym2.length = (xs.length + 1).choose 2

Tactic:
induction xs with
  | nil => rfl
  | cons x xs ih =>
    rw [List.sym2, length_append, length_map, length_cons,
        Nat.choose_succ_succ, ← ih, Nat.choose_one_right]

Premises used: List.length_cons, Nat.choose_succ_succ, List.length_append, Nat.choose_one_right, List.cons, List.sym2, List.length_map, List.nil
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
⊢ Eq.{u_1 + 1} (α := List (Sym α 1)) (List.sym 1 []) (map (fun (x : α) ↦ x ::ₛ Sym.nil) [])

Tactic:
simp only [List.sym, Nat.succ_eq_add_one, Nat.reduceAdd, map_nil]

Premises used: Nat.succ_eq_add_one, Nat.reduceAdd, List.sym, List.map_nil
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs_1 : List α
x : α
xs : List α
ih : Eq (α := List (Sym α 1)) (List.sym 1 xs) (map (fun (x : α) ↦ x ::ₛ Sym.nil) xs)
cons : List.sym 1 (x :: xs) = (x ::ₛ Sym.nil) :: map (fun (x : α) ↦ x ::ₛ Sym.nil) xs
cons₁ : List.sym 1 (x :: xs) = (x ::ₛ Sym.nil) :: List.sym 1 xs
cons₂ :
  HAppend.hAppend (α := List (Sym α (Nat.succ 0))) (map (fun (p : Sym α 0) ↦ x ::ₛ p) (List.sym 0 (x :: xs)))
      (List.sym (HAdd.hAdd (α := ℕ) 0 1) xs) =
    (x ::ₛ Sym.nil) :: List.sym 1 xs
cons₃ :
  HAppend.hAppend (α := List (Sym α (Nat.succ 0))) (map (fun (p : Sym α 0) ↦ x ::ₛ p) [Sym.nil])
      (List.sym (HAdd.hAdd (α := ℕ) 0 1) xs) =
    (x ::ₛ Sym.nil) :: List.sym 1 xs
cons₄ : [x ::ₛ Sym.nil] ++ List.sym (HAdd.hAdd (α := ℕ) 0 1) xs = (x ::ₛ Sym.nil) :: List.sym 1 xs
cons₅ cons₆ : (x ::ₛ Sym.nil) :: List.sym (HAdd.hAdd (α := ℕ) 0 1) xs = (x ::ₛ Sym.nil) :: List.sym 1 xs
⊢ Eq (α := List (Sym α 1)) (List.sym 1 (x :: xs)) (map (fun (x : α) ↦ x ::ₛ Sym.nil) (x :: xs))

Tactic:
rw [map_cons, ← ih, List.sym, List.sym, map_singleton, singleton_append]

Premises used: List.map_cons, List.map_singleton, List.singleton_append, List.sym
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
nil : Eq.{u_1 + 1} (α := List (Sym α 1)) (List.sym 1 []) (map (fun (x : α) ↦ x ::ₛ Sym.nil) [])
cons :
  ∀ (x : α) (xs : List α) (ih : Eq (α := List (Sym α 1)) (List.sym 1 xs) (map (fun (x : α) ↦ x ::ₛ Sym.nil) xs)),
    Eq (α := List (Sym α 1)) (List.sym 1 (x :: xs)) (map (fun (x : α) ↦ x ::ₛ Sym.nil) (x :: xs))
⊢ Eq (α := List (Sym α 1)) (List.sym 1 xs) (map (fun (x : α) ↦ x ::ₛ Sym.nil) xs)

Tactic:
induction xs with
  | nil => simp only [List.sym, Nat.succ_eq_add_one, Nat.reduceAdd, map_nil]
  | cons x xs ih =>
    rw [map_cons, ← ih, List.sym, List.sym, map_singleton, singleton_append]

Premises used: Nat.succ_eq_add_one, List.map_cons, List.map_singleton, Nat.reduceAdd, List.cons, List.singleton_append, List.sym, List.map_nil, List.nil
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
⊢ Eq (α := List (Sym α 2)) (map (α := Sym2 α) (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) (List.sym2 []))
    (List.sym 2 [])

Tactic:
simp only [List.sym, map_eq_nil_iff, sym2_eq_nil_iff]

Premises used: List.map_eq_nil_iff, List.sym, List.sym2_eq_nil_iff
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs_1 : List α
x : α
xs : List α
ih : Eq (α := List (Sym α 2)) (map (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) xs.sym2) (List.sym 2 xs)
cons :
  HAppend.hAppend (α := List (Sym α 2))
      (map (Function.comp (β := Sym2 α) (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) fun (y : α) ↦ s(x, y)) (x :: xs))
      (map (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) xs.sym2) =
    HAppend.hAppend (α := List (Sym α (Nat.succ 1)))
      (map ((fun (p : Sym α 1) ↦ x ::ₛ p) ∘ fun (x : α) ↦ x ::ₛ Sym.nil) (x :: xs))
      (map (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) xs.sym2)
⊢ Eq (α := List (Sym α 2)) (map (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) (x :: xs).sym2) (List.sym 2 (x :: xs))

Tactic:
rw [List.sym, ← ih, sym_one_eq, map_map, List.sym2, map_append, map_map]

Premises used: List.map_map, List.sym2, List.sym, List.sym_one_eq, List.map_append
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs_1 : List α
x : α
xs : List α
ih : Eq (α := List (Sym α 2)) (map (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) xs.sym2) (List.sym 2 xs)
⊢ HAppend.hAppend (α := List (Sym α 2))
      (map (Function.comp (β := Sym2 α) (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) fun (y : α) ↦ s(x, y)) (x :: xs))
      (map (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) xs.sym2) =
    HAppend.hAppend (α := List (Sym α (Nat.succ 1)))
      (map ((fun (p : Sym α 1) ↦ x ::ₛ p) ∘ fun (x : α) ↦ x ::ₛ Sym.nil) (x :: xs))
      (map (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) xs.sym2)

Tactic:
rfl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
nil :
  Eq (α := List (Sym α 2)) (map (α := Sym2 α) (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) (List.sym2 []))
    (List.sym 2 [])
cons :
  ∀ (x : α) (xs : List α)
    (ih : Eq (α := List (Sym α 2)) (map (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) xs.sym2) (List.sym 2 xs)),
    Eq (α := List (Sym α 2)) (map (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) (x :: xs).sym2) (List.sym 2 (x :: xs))
⊢ Eq (α := List (Sym α 2)) (map (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) xs.sym2) (List.sym 2 xs)

Tactic:
induction xs with
  | nil => simp only [List.sym, map_eq_nil_iff, sym2_eq_nil_iff]
  | cons x xs ih =>
    rw [List.sym, ← ih, sym_one_eq, map_map, List.sym2, map_append, map_map]
    rfl

Premises used: List.map_eq_nil_iff, List.map_map, List.cons, List.sym2, List.sym, List.sym_one_eq, List.map_append, List.sym2_eq_nil_iff, List.nil
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
β : Type u_3
f : α → β
n : ℕ
xs x : List α
simp : [Sym.nil] = map (Sym.map f) [Sym.nil]
⊢ Eq (α := List (Sym β 0)) (List.sym 0 (map f x)) (map (Sym.map f) (List.sym 0 x))

Tactic:
simp only [List.sym]

Premises used: List.sym
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
β : Type u_3
f : α → β
n : ℕ
xs x : List α
⊢ [Sym.nil] = map (Sym.map f) [Sym.nil]

Tactic:
rfl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
β : Type u_3
f : α → β
n_1 : ℕ
xs : List α
n : ℕ
⊢ Eq (α := List (Sym β (n + 1))) (List.sym (n + 1) (map f [])) (map (Sym.map f) (List.sym (n + 1) []))

Tactic:
simp [List.sym]

Premises used: List.sym