awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
nil :
  Perm.{u} (α := List α) (flatMap (fun (n : ℕ) ↦ sublistsLen n []) (range (length.{u} (α := α) [] + 1))) (sublists' [])
cons :
  ∀ (h : α) (tl : List α) (l_ih : flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'),
    flatMap (fun (n : ℕ) ↦ sublistsLen n (h :: tl)) (range ((h :: tl).length + 1)) ~ (h :: tl).sublists'
⊢ flatMap (fun (n : ℕ) ↦ sublistsLen n l) (range (l.length + 1)) ~ l.sublists'

Tactic:
induction l with
  | nil => simp [range_succ]
  | cons h tl l_ih =>
    simp_rw [range_succ_eq_map, length, flatMap_cons, flatMap_map, sublistsLen_succ_cons,
      sublists'_cons, List.sublistsLen_zero, List.singleton_append]
    refine ((flatMap_append_perm (range (tl.length + 1)) _ _).symm.cons _).trans ?_
    simp_rw [← List.map_flatMap, ← cons_append]
    rw [← List.singleton_append, ← List.sublistsLen_zero tl]
    refine Perm.append ?_ (l_ih.map _)
    rw [List.range_succ, flatMap_append, flatMap_singleton,
      sublistsLen_of_length_lt (Nat.lt_succ_self _), append_nil,
      ← List.flatMap_map Nat.succ fun n => sublistsLen n tl,
      ← flatMap_cons (f := fun n => sublistsLen n tl), ← range_succ_eq_map]
    exact l_ih

Premises used: Nat.lt_succ_self, List.sublists'_cons, List.sublistsLen_succ_cons, List.range_succ_eq_map, List.append_nil, List.cons, List.flatMap_cons, List.sublistsLen_of_length_lt, List.singleton_append, List.flatMap_map, List.map_flatMap, List.flatMap_singleton, List.length, List.cons_append, List.flatMap_append, List.range_succ, List.nil, List.sublistsLen_zero
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ (map f []).sym2 = map (Sym2.map f) (List.sym2 [])

Tactic:
simp [List.sym2]

Premises used: List.sym2
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : α
xs : List α
ih : (map f xs).sym2 = map (Sym2.map f) xs.sym2
⊢ (map f (x :: xs)).sym2 = map (Sym2.map f) (x :: xs).sym2

Tactic:
simp [List.sym2, ih, Function.comp]

Premises used: Function.comp, List.sym2
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
β : Type u_2
f : α → β
xs : List α
nil : (map f []).sym2 = map (Sym2.map f) (List.sym2 [])
cons :
  ∀ (x : α) (xs : List α) (ih : (map f xs).sym2 = map (Sym2.map f) xs.sym2),
    (map f (x :: xs)).sym2 = map (Sym2.map f) (x :: xs).sym2
⊢ (map f xs).sym2 = map (Sym2.map f) xs.sym2

Tactic:
induction xs with
  | nil => simp [List.sym2]
  | cons x xs ih => simp [List.sym2, ih, Function.comp]

Premises used: Function.comp, List.cons, List.sym2, List.nil
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
z : Sym2 α
simp : z = s(x, x) ∨ (∃ a ∈ xs, s(x, a) = z) ∨ z ∈ xs.sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2
⊢ z ∈ (x :: xs).sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2

Tactic:
simp only [List.sym2, map_cons, cons_append, mem_cons, mem_append, mem_map]

Premises used: List.map_cons, List.mem_append, List.sym2, List.mem_cons, List.mem_map, List.cons_append
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
z : Sym2 α
⊢ z = s(x, x) ∨ (∃ a ∈ xs, s(x, a) = z) ∨ z ∈ xs.sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2

Tactic:
simp only [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
nil : Eq.{u_1 + 1} (α := List (Sym2 α)) (List.sym2 []) [] ↔ Eq.{u_1 + 1} (α := List α) [] []
cons : ∀ (head : α) (tail : List α), (head :: tail).sym2 = [] ↔ head :: tail = []
⊢ xs.sym2 = [] ↔ xs = []

Tactic:
cases xs
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List (Sym2 α)) (List.sym2 []) [] ↔ Eq.{u_1 + 1} (α := List α) [] []

Tactic:
simp [List.sym2]

Premises used: List.sym2
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
head : α
tail : List α
⊢ (head :: tail).sym2 = [] ↔ head :: tail = []

Tactic:
simp [List.sym2]

Premises used: List.sym2
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b : α
h : Membership.mem (γ := List (Sym2 α)) (List.sym2 []) s(a, b)
⊢ Membership.mem (γ := List α) [] a

Tactic:
(not_mem_nil h).elim

Premises used: False.elim, List.not_mem_nil
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b : α
h : Membership.mem (γ := List (Sym2 α)) (List.sym2 []) s(a, b)
⊢ Membership.mem (γ := List α) [] a

Tactic:
exact (not_mem_nil h).elim

Premises used: False.elim, List.not_mem_nil
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b x : α
xs : List α
ih : ∀ (h : s(a, b) ∈ xs.sym2), a ∈ xs
h : s(a, b) ∈ (x :: xs).sym2
cons : 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
a b x : α
xs : List α
ih : ∀ (h : s(a, b) ∈ xs.sym2), a ∈ xs
h : s(a, b) ∈ (x :: xs).sym2
⊢ s(a, b) = s(x, x) ∨ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2

Tactic:
rw [mem_sym2_cons_iff] at h

Premises used: List.mem_sym2_cons_iff
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b x : α
xs : List α
ih : ∀ (h : s(a, b) ∈ xs.sym2), a ∈ xs
h : s(a, b) = s(x, x) ∨ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2
cons : ∀ (h : s(a, b) = s(x, x)), a = x ∨ a ∈ xs
cons₁ : ∀ (c : α) (hc : c ∈ xs) (h : s(a, b) = s(x, c)), a = x ∨ a ∈ xs
cons₂ : ∀ (h : s(a, b) ∈ xs.sym2), a = x ∨ a ∈ xs
⊢ a = x ∨ a ∈ xs

Tactic:
obtain (h | ⟨c, hc, h⟩ | h) := h
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b x : α
xs : List α
ih : ∀ (h : s(a, b) ∈ xs.sym2), a ∈ xs
h : s(a, b) = s(x, x)
⊢ a = x ∧ (b = x ∨ b = x)

Tactic:
rw [Sym2.eq_iff, ← and_or_left] at h

Premises used: and_or_left, Sym2.eq_iff
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b x : α
xs : List α
ih : ∀ (h : s(a, b) ∈ xs.sym2), a ∈ xs
h : a = x ∧ (b = x ∨ b = x)
⊢ a = x ∨ a ∈ xs

Tactic:
.inl h.1

Premises used: And.left, Or.inl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b x : α
xs : List α
ih : ∀ (h : s(a, b) ∈ xs.sym2), a ∈ xs
h : a = x ∧ (b = x ∨ b = x)
⊢ a = x ∨ a ∈ xs

Tactic:
exact .inl h.1
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b x : α
xs : List α
ih : ∀ (h : s(a, b) ∈ xs.sym2), a ∈ xs
c : α
hc : c ∈ xs
h : s(a, b) = s(x, c)
⊢ a = x ∧ b = c ∨ a = c ∧ b = x

Tactic:
rw [Sym2.eq_iff] at h

Premises used: Sym2.eq_iff
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b x : α
xs : List α
ih : ∀ (h : s(a, b) ∈ xs.sym2), a ∈ xs
c : α
hc : c ∈ xs
h : a = x ∧ b = c ∨ a = c ∧ b = x
cons : ∀ (hc : b ∈ xs), a = a ∨ a ∈ xs
cons₁ : ∀ (hc : a ∈ xs), a = b ∨ a ∈ xs
⊢ a = x ∨ a ∈ xs

Tactic:
obtain (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) := h

Premises used: rfl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b : α
xs : List α
ih : ∀ (h : s(a, b) ∈ xs.sym2), a ∈ xs
hc : b ∈ xs
⊢ a = a ∨ a ∈ xs

Tactic:
simp [hc]
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b : α
xs : List α
ih : ∀ (h : s(a, b) ∈ xs.sym2), a ∈ xs
hc : a ∈ xs
⊢ a = b ∨ a ∈ xs

Tactic:
simp [hc]
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b x : α
xs : List α
ih : ∀ (h : s(a, b) ∈ xs.sym2), a ∈ xs
h : s(a, b) ∈ xs.sym2
⊢ a = x ∨ a ∈ xs

Tactic:
.inr <| ih h

Premises used: Or.inr
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b x : α
xs : List α
ih : ∀ (h : s(a, b) ∈ xs.sym2), a ∈ xs
h : s(a, b) ∈ xs.sym2
⊢ a = x ∨ a ∈ xs

Tactic:
exact .inr <| ih h
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
nil : ∀ (h : Membership.mem (γ := List (Sym2 α)) (List.sym2 []) s(a, b)), Membership.mem (γ := List α) [] a
cons : ∀ (x : α) (xs : List α) (ih : ∀ (h : s(a, b) ∈ xs.sym2), a ∈ xs) (h : s(a, b) ∈ (x :: xs).sym2), a ∈ x :: xs
⊢ a ∈ xs

Tactic:
induction xs with
  | nil => exact (not_mem_nil h).elim
  | cons x xs ih =>
    rw [mem_cons]
    rw [mem_sym2_cons_iff] at h
    obtain (h | ⟨c, hc, h⟩ | h) := h
    · rw [Sym2.eq_iff, ← and_or_left] at h
      exact .inl h.1
    · rw [Sym2.eq_iff] at h
      obtain (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) := h <;> simp [hc]
    · exact .inr <| ih h

Premises used: and_or_left, False.elim, List.cons, Sym2.eq_iff, List.mem_cons, List.not_mem_nil, List.mem_sym2_cons_iff, rfl, List.nil
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
⊢ s(b, a) ∈ xs.sym2

Tactic:
rw [Sym2.eq_swap] at h

Premises used: Sym2.eq_swap
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
a b : α
h : s(b, a) ∈ xs.sym2
⊢ b ∈ xs

Tactic:
left_mem_of_mk_mem_sym2 h

Premises used: List.left_mem_of_mk_mem_sym2
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
a b : α
h : s(b, a) ∈ xs.sym2
⊢ b ∈ xs

Tactic:
exact left_mem_of_mk_mem_sym2 h

Premises used: List.left_mem_of_mk_mem_sym2
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b : α
ha : Membership.mem (γ := List α) [] a
hb : Membership.mem (γ := List α) [] b
⊢ Membership.mem (γ := List (Sym2 α)) (List.sym2 []) s(a, b)

Tactic:
simp at ha
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b x : α
xs : List α
ih : ∀ (ha : a ∈ xs) (hb : b ∈ xs), s(a, b) ∈ xs.sym2
ha : a ∈ x :: xs
hb : b ∈ x :: xs
cons : s(a, b) = s(x, x) ∨ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2
⊢ s(a, b) ∈ (x :: xs).sym2

Tactic:
rw [mem_sym2_cons_iff]

Premises used: List.mem_sym2_cons_iff
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
a b x : α
xs : List α
ih : ∀ (ha : a ∈ xs) (hb : b ∈ xs), s(a, b) ∈ xs.sym2
ha : a ∈ x :: xs
hb : b ∈ x :: xs
⊢ s(a, b) = s(x, x) ∨ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2

Tactic:
grind
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
a b : α
ha : a ∈ xs
hb : b ∈ xs
nil :
  ∀ (ha : Membership.mem (γ := List α) [] a) (hb : Membership.mem (γ := List α) [] b),
    Membership.mem (γ := List (Sym2 α)) (List.sym2 []) s(a, b)
cons :
  ∀ (x : α) (xs : List α) (ih : ∀ (ha : a ∈ xs) (hb : b ∈ xs), s(a, b) ∈ xs.sym2) (ha : a ∈ x :: xs) (hb : b ∈ x :: xs),
    s(a, b) ∈ (x :: xs).sym2
⊢ s(a, b) ∈ xs.sym2

Tactic:
induction xs with
  | nil => simp at ha
  | cons x xs ih =>
    rw [mem_sym2_cons_iff]
    grind

Premises used: List.cons, List.mem_sym2_cons_iff, List.nil
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
a b : α
mp : s(a, b) ∈ xs.sym2 → a ∈ xs ∧ b ∈ xs
mpr : a ∈ xs ∧ b ∈ xs → s(a, b) ∈ xs.sym2
⊢ s(a, b) ∈ xs.sym2 ↔ a ∈ xs ∧ b ∈ xs

Tactic:
constructor
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
⊢ a ∈ xs ∧ b ∈ xs

Tactic:
⟨left_mem_of_mk_mem_sym2 h, right_mem_of_mk_mem_sym2 h⟩

Premises used: List.left_mem_of_mk_mem_sym2, And.intro, List.right_mem_of_mk_mem_sym2
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
⊢ a ∈ xs ∧ b ∈ xs

Tactic:
exact ⟨left_mem_of_mk_mem_sym2 h, right_mem_of_mk_mem_sym2 h⟩
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
a b : α
ha : a ∈ xs
hb : b ∈ xs
⊢ s(a, b) ∈ xs.sym2

Tactic:
mk_mem_sym2 ha hb

Premises used: List.mk_mem_sym2
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
a b : α
ha : a ∈ xs
hb : b ∈ xs
⊢ s(a, b) ∈ xs.sym2

Tactic:
exact mk_mem_sym2 ha hb

Premises used: List.mk_mem_sym2
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
z : Sym2 α
⊢ z ∈ xs.sym2 ↔ ∀ y ∈ z, y ∈ xs

Tactic:
z.ind (fun a b => ?_)

Premises used: Sym2.ind
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
z : Sym2 α
refine : ∀ (a b : α), s(a, b) ∈ xs.sym2 ↔ ∀ y ∈ s(a, b), y ∈ xs
⊢ z ∈ xs.sym2 ↔ ∀ y ∈ z, y ∈ xs

Tactic:
refine z.ind (fun a b => ?_)
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
z : Sym2 α
a b : α
⊢ s(a, b) ∈ xs.sym2 ↔ ∀ y ∈ s(a, b), y ∈ xs

Tactic:
simp [mk_mem_sym2_iff]

Premises used: List.mk_mem_sym2_iff
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
z : Sym2 α
a b : α
⊢ Membership.mem (γ := Set (Sym2 α)) {z : Sym2 α | z ∈ xs.sym2} s(a, b) ↔
    Membership.mem (γ := Set (Sym2 α)) (Set.sym2 {x : α | x ∈ xs}) s(a, b)

Tactic:
simp [mk_mem_sym2_iff]

Premises used: List.mk_mem_sym2_iff
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
h : Nodup.{u_1} (α := α) []
⊢ Nodup.{u_1} (α := Sym2 α) (List.sym2 [])

Tactic:
simp only [List.sym2, nodup_nil]

Premises used: List.nodup_nil, List.sym2
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
ih : ∀ (h : xs.Nodup), xs.sym2.Nodup
h : (x :: xs).Nodup
⊢ xs.sym2.Nodup

Tactic:
specialize ih h.of_cons

Premises used: List.Nodup.of_cons
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : (x :: xs).Nodup
ih : xs.sym2.Nodup
⊢ x ∉ xs ∧ xs.Nodup

Tactic:
rw [nodup_cons] at h

Premises used: List.nodup_cons
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : (x :: xs).Nodup
ih : xs.sym2.Nodup
h₁ : x ∉ xs ∧ xs.Nodup
⊢ xs.sym2.Nodup

Tactic:
rw [nodup_cons] at h

Premises used: List.nodup_cons
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ (map (fun (y : α) ↦ s(x, y)) (x :: xs) ++ xs.sym2).Nodup

Tactic:
Nodup.append (Nodup.cons ?notmem (h.2.map ?inj)) ih ?disj

Premises used: List.Nodup.append, List.Nodup.map, And.right, List.Nodup.cons
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
refine : (fun (y : α) ↦ s(x, y)) x ∉ map (fun (y : α) ↦ s(x, y)) xs
refine₁ : Function.Injective (β := Sym2 α) fun (y : α) ↦ s(x, y)
refine₂ : Disjoint (map (fun (y : α) ↦ s(x, y)) (x :: xs)) xs.sym2
⊢ (map (fun (y : α) ↦ s(x, y)) (x :: xs) ++ xs.sym2).Nodup

Tactic:
refine Nodup.append (Nodup.cons ?notmem (h.2.map ?inj)) ih ?disj

Premises used: List.Nodup.append, List.Nodup.map, And.right, List.Nodup.cons
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
z : Sym2 α
hz : Membership.mem (γ := List (Sym2 α)) (map (fun (y : α) ↦ s(x, y)) (x :: xs)) z
hz' : z ∈ xs.sym2
⊢ ∃ (a : α), (a = x ∨ a ∈ xs) ∧ s(x, a) = z

Tactic:
simp only [mem_cons, mem_map] at hz

Premises used: List.mem_cons, List.mem_map
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
z : Sym2 α
hz' : z ∈ xs.sym2
hz : ∃ (a : α), (a = x ∨ a ∈ xs) ∧ s(x, a) = z
inl : ∀ (w : α) (h : w ∉ xs ∧ xs.Nodup) (hz' : s(w, w) ∈ xs.sym2), False
inr : ∀ w ∈ xs, ∀ (hz' : s(x, w) ∈ xs.sym2), False
⊢ False

Tactic:
obtain ⟨_, (rfl | _), rfl⟩ := hz

Premises used: rfl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
ih : xs.sym2.Nodup
w : α
h : w ∉ xs ∧ xs.Nodup
hz' : s(w, w) ∈ xs.sym2
⊢ False

Tactic:
simp [left_mem_of_mk_mem_sym2 hz'] at h

Premises used: List.left_mem_of_mk_mem_sym2
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
w : α
h_1 : w ∈ xs
hz' : s(x, w) ∈ xs.sym2
⊢ False

Tactic:
simp [left_mem_of_mk_mem_sym2 hz'] at h

Premises used: List.left_mem_of_mk_mem_sym2
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ Disjoint (map (fun (y : α) ↦ s(x, y)) (x :: xs)) xs.sym2

Tactic:
case disj =>
      intro z hz hz'
      simp only [mem_cons, mem_map] at hz
      obtain ⟨_, (rfl | _), rfl⟩ := hz
        <;> simp [left_mem_of_mk_mem_sym2 hz'] at h

Premises used: List.mem_cons, List.mem_map, rfl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
h' : Membership.mem (γ := List (Sym2 α)) (map (fun (y : α) ↦ s(x, y)) xs) ((fun (y : α) ↦ s(x, y)) x)
⊢ False

Tactic:
simp only [h.1, mem_map, Sym2.eq_iff, true_and, or_self, exists_eq_right] at h'

Premises used: exists_eq_right, Sym2.eq_iff, And.left, or_self, List.mem_map, true_and
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ (fun (y : α) ↦ s(x, y)) x ∉ map (fun (y : α) ↦ s(x, y)) xs

Tactic:
case notmem =>
      intro h'
      simp only [h.1, mem_map, Sym2.eq_iff, true_and, or_self, exists_eq_right] at h'

Premises used: exists_eq_right, Sym2.eq_iff, And.left, or_self, List.mem_map, true_and
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
a b : α
simp : a = b ∨ x = b ∧ a = x → a = b
⊢ Eq.{u_1 + 1} (α := Sym2 α) ((fun (y : α) ↦ s(x, y)) a) ((fun (y : α) ↦ s(x, y)) b) → a = b

Tactic:
simp only [Sym2.eq_iff, true_and]

Premises used: Sym2.eq_iff, true_and
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
a : α
⊢ a = a

Tactic:
rfl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
ih : xs.sym2.Nodup
a : α
h : a ∉ xs ∧ xs.Nodup
⊢ a = a

Tactic:
rfl
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
case case₁ : ∀ ⦃a b : α⦄, Eq.{u_1 + 1} (α := Sym2 α) ((fun (y : α) ↦ s(x, y)) a) ((fun (y : α) ↦ s(x, y)) b) → a = b
case₂ : ∀ ⦃a b : α⦄, a = b ∨ x = b ∧ a = x → a = b
⊢ Function.Injective (β := Sym2 α) fun (y : α) ↦ s(x, y)

Tactic:
case inj =>
      intro a b
      simp only [Sym2.eq_iff, true_and]
      rintro (rfl | ⟨rfl, rfl⟩) <;> rfl

Premises used: Sym2.eq_iff, rfl, true_and
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
xs : List α
h : xs.Nodup
nil : ∀ (h : Nodup.{u_1} (α := α) []), Nodup.{u_1} (α := Sym2 α) (List.sym2 [])
cons : ∀ (x : α) (xs : List α) (ih : ∀ (h : xs.Nodup), xs.sym2.Nodup) (h : (x :: xs).Nodup), (x :: xs).sym2.Nodup
⊢ xs.sym2.Nodup

Tactic:
induction xs with
  | nil => simp only [List.sym2, nodup_nil]
  | cons x xs ih =>
    rw [List.sym2]
    specialize ih h.of_cons
    rw [nodup_cons] at h
    refine Nodup.append (Nodup.cons ?notmem (h.2.map ?inj)) ih ?disj
    case disj =>
      intro z hz hz'
      simp only [mem_cons, mem_map] at hz
      obtain ⟨_, (rfl | _), rfl⟩ := hz
        <;> simp [left_mem_of_mk_mem_sym2 hz'] at h
    case notmem =>
      intro h'
      simp only [h.1, mem_map, Sym2.eq_iff, true_and, or_self, exists_eq_right] at h'
    case inj =>
      intro a b
      simp only [Sym2.eq_iff, true_and]
      rintro (rfl | ⟨rfl, rfl⟩) <;> rfl

Premises used: exists_eq_right, List.cons, List.nodup_nil, List.nodup_cons, List.sym2, Sym2.eq_iff, or_self, List.mem_cons, List.mem_map, rfl, true_and, List.nil
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
h : Membership.mem (γ := List α) [] x
⊢ Sublist.{u_1} (α := Sym2 α) (map (fun (y : α) ↦ s(x, y)) []) (List.sym2 [])

Tactic:
simp
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
ih : ∀ (h : x ∈ xs), map (fun (y : α) ↦ s(x, y)) xs <+ xs.sym2
⊢ s(x, x) :: map (fun (y : α) ↦ s(x, y)) xs <+ s(x, x) :: (map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)

Tactic:
(sublist_append_left _ _).cons_cons _

Premises used: List.Sublist.cons_cons, List.sublist_append_left
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
ih : ∀ (h : x ∈ xs), map (fun (y : α) ↦ s(x, y)) xs <+ xs.sym2
⊢ s(x, x) :: map (fun (y : α) ↦ s(x, y)) xs <+ s(x, x) :: (map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)

Tactic:
exact (sublist_append_left _ _).cons_cons _

Premises used: List.Sublist.cons_cons, List.sublist_append_left
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x x' : α
xs : List α
ih : ∀ (h : x ∈ xs), map (fun (y : α) ↦ s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ s(x, x') :: map (fun (y : α) ↦ s(x, y)) xs <+ s(x', x') :: (map (fun (y : α) ↦ s(x', y)) xs ++ xs.sym2)

Tactic:
.cons _ ?_

Premises used: List.Sublist.cons
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x x' : α
xs : List α
ih : ∀ (h : x ∈ xs), map (fun (y : α) ↦ s(x, y)) xs <+ xs.sym2
h : Mem x xs
cons : s(x, x') :: map (fun (y : α) ↦ s(x, y)) xs <+ map (fun (y : α) ↦ s(x', y)) xs ++ xs.sym2
⊢ s(x, x') :: map (fun (y : α) ↦ s(x, y)) xs <+ s(x', x') :: (map (fun (y : α) ↦ s(x', y)) xs ++ xs.sym2)

Tactic:
refine .cons _ ?_
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x x' : α
xs : List α
ih : ∀ (h : x ∈ xs), map (fun (y : α) ↦ s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ [s(x, x')] ++ map (fun (y : α) ↦ s(x, y)) xs <+ map (fun (y : α) ↦ s(x', y)) xs ++ xs.sym2

Tactic:
.append ?_ (ih h)

Premises used: List.Sublist.append
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x x' : α
xs : List α
ih : ∀ (h : x ∈ xs), map (fun (y : α) ↦ s(x, y)) xs <+ xs.sym2
h : Mem x xs
cons : [s(x, x')] <+ map (fun (y : α) ↦ s(x', y)) xs
⊢ [s(x, x')] ++ map (fun (y : α) ↦ s(x, y)) xs <+ map (fun (y : α) ↦ s(x', y)) xs ++ xs.sym2

Tactic:
refine .append ?_ (ih h)
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x x' : α
xs : List α
ih : ∀ (h : x ∈ xs), map (fun (y : α) ↦ s(x, y)) xs <+ xs.sym2
h : Mem x xs
cons : ∃ a ∈ xs, s(x', a) = s(x, x')
⊢ [s(x, x')] <+ map (fun (y : α) ↦ s(x', y)) xs

Tactic:
rw [singleton_sublist, mem_map]

Premises used: List.mem_map, List.singleton_sublist
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x x' : α
xs : List α
ih : ∀ (h : x ∈ xs), map (fun (y : α) ↦ s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ ∃ a ∈ xs, s(x', a) = s(x, x')

Tactic:
⟨_, h, Sym2.eq_swap⟩

Premises used: Sym2.eq_swap, And.intro, Exists.intro
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x x' : α
xs : List α
ih : ∀ (h : x ∈ xs), map (fun (y : α) ↦ s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ ∃ a ∈ xs, s(x', a) = s(x, x')

Tactic:
exact ⟨_, h, Sym2.eq_swap⟩
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x x' : α
xs : List α
ih : ∀ (h : x ∈ xs), map (fun (y : α) ↦ s(x, y)) xs <+ xs.sym2
h : x ∈ x' :: xs
cons : s(x, x) :: map (fun (y : α) ↦ s(x, y)) xs <+ s(x, x) :: (map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)
cons₁ :
  ∀ (h : Mem x xs),
    s(x, x') :: map (fun (y : α) ↦ s(x, y)) xs <+ s(x', x') :: (map (fun (y : α) ↦ s(x', y)) xs ++ xs.sym2)
⊢ s(x, x') :: map (fun (y : α) ↦ s(x, y)) xs <+ s(x', x') :: (map (fun (y : α) ↦ s(x', y)) xs ++ xs.sym2)

Tactic:
cases h with
    | head =>
      exact (sublist_append_left _ _).cons_cons _
    | tail _ h =>
      refine .cons _ ?_
      rw [← singleton_append]
      refine .append ?_ (ih h)
      rw [singleton_sublist, mem_map]
      exact ⟨_, h, Sym2.eq_swap⟩

Premises used: List.head, List.Sublist.cons_cons, List.tail, List.singleton_append, List.sublist_append_left, List.mem_map, List.singleton_sublist
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : x ∈ xs
nil :
  ∀ (h : Membership.mem (γ := List α) [] x), Sublist.{u_1} (α := Sym2 α) (map (fun (y : α) ↦ s(x, y)) []) (List.sym2 [])
cons :
  ∀ (x' : α) (xs : List α) (ih : ∀ (h : x ∈ xs), map (fun (y : α) ↦ s(x, y)) xs <+ xs.sym2) (h : x ∈ x' :: xs),
    map (fun (y : α) ↦ s(x, y)) (x' :: xs) <+ (x' :: xs).sym2
⊢ map (fun (y : α) ↦ s(x, y)) xs <+ xs.sym2

Tactic:
induction xs with
  | nil => simp
  | cons x' xs ih =>
    simp only [map_cons, List.sym2, cons_append]
    cases h with
    | head =>
      exact (sublist_append_left _ _).cons_cons _
    | tail _ h =>
      refine .cons _ ?_
      rw [← singleton_append]
      refine .append ?_ (ih h)
      rw [singleton_sublist, mem_map]
      exact ⟨_, h, Sym2.eq_swap⟩

Premises used: List.head, List.map_cons, List.Sublist.cons_cons, List.tail, List.cons, List.sym2, List.singleton_append, List.sublist_append_left, List.mem_map, List.cons_append, List.singleton_sublist, List.nil
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
h : x ∉ []
⊢ Disjoint.{u_1} (α := Sym2 α) (map (fun (y : α) ↦ s(x, y)) []) (List.sym2 [])

Tactic:
simp
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x x' : α
xs : List α
ih : ∀ (h : x ∉ xs), Disjoint (map (fun (y : α) ↦ s(x, y)) xs) xs.sym2
h : x ∉ x' :: xs
⊢ Disjoint (map (fun (y : α) ↦ s(x, y)) (x' :: xs)) (x' :: xs).sym2

Tactic:
aesop (add simp mk_mem_sym2_iff, unfold safe List.Disjoint)

Premises used: List.Disjoint, List.mk_mem_sym2_iff
-- Module: Mathlib.Data.List.Sym
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs
nil : ∀ (h : x ∉ []), Disjoint.{u_1} (α := Sym2 α) (map (fun (y : α) ↦ s(x, y)) []) (List.sym2 [])
cons :
  ∀ (x' : α) (xs : List α) (ih : ∀ (h : x ∉ xs), Disjoint (map (fun (y : α) ↦ s(x, y)) xs) xs.sym2) (h : x ∉ x' :: xs),
    Disjoint (map (fun (y : α) ↦ s(x, y)) (x' :: xs)) (x' :: xs).sym2
⊢ Disjoint (map (fun (y : α) ↦ s(x, y)) xs) xs.sym2

Tactic:
induction xs with
  | nil => simp
  | cons x' xs ih => aesop (add simp mk_mem_sym2_iff, unfold safe List.Disjoint)

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

Tactic:
simp only [List.sym2, dedup_nil]

Premises used: List.dedup_nil, List.sym2