awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
nil : Eq.{u_1 + 1} (α := List (Sym2 α)) (dedup (List.sym2 [])) (List.sym2 (dedup []))
⊢ xs.sym2.dedup = xs.dedup.sym2
have cons : ∀ (x : α) (xs : List α) (ih : xs.sym2.dedup = xs.dedup.sym2), (x :: xs).sym2.dedup = (x :: 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]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs ys : List α
x : α
l₁ l₂ : List α
h : l₁ ~ l₂
ih : l₁.sym2 ~ l₂.sym2
⊢ (x :: l₁).sym2 ~ (x :: l₂).sym2
have cons : List.map (fun (y : α) ↦ s(x, y)) l₁ ++ l₁.sym2 ~ List.map (fun (y : α) ↦ s(x, y)) l₂ ++ l₂.sym2
Tactic: simp only [List.sym2, map_cons, cons_append, perm_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs_1 ys : List α
x y : α
xs : List α
| 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))
have enter : s(y, x)
Tactic: enter [1, 2, 1]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs_1 ys : List α
x y : α
xs : List α
| s(y, x)
have rw : s(x, y)
Tactic: rw [Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs_1 ys : List α
x y : α
xs : List α
| 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))
have enter : s(x, y)
Tactic: enter [1, 2, 1]; rw [Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs_1 ys : List α
x y : α
xs : List α
⊢ 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))
have 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))
Tactic: conv => enter [1, 2, 1]; rw [Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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))
have 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))
Tactic: refine Perm.trans (Perm.swap ..) (Perm.trans (Perm.cons _ ?_) (Perm.swap ..))
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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 ++ 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))
have 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 α)))))
Tactic: simp only [← Multiset.coe_eq_coe, ← Multiset.cons_coe,
      ← Multiset.coe_add, ← Multiset.singleton_add]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs ys : List α
h : xs ~ ys
⊢ xs.sym2 ~ ys.sym2
have nil : Perm.{u_1} (α := Sym2 α) (List.sym2 []) (List.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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs ys : List α
h : xs ~ ys
nil : Perm.{u_1} (α := Sym2 α) (List.sym2 []) (List.sym2 [])
⊢ xs.sym2 ~ ys.sym2
have cons : ∀ (x : α) {l₁ l₂ : List α} (h : l₁ ~ l₂) (ih : l₁.sym2 ~ l₂.sym2), (x :: l₁).sym2 ~ (x :: l₂).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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ xs.sym2 ~ ys.sym2
have swap : ∀ (x y : α) (xs : List α), (y :: x :: xs).sym2 ~ (x :: y :: xs).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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ xs.sym2 ~ ys.sym2
have trans : ∀ {l₁ l₂ l₃ : List α}, l₁ ~ l₂ → l₂ ~ l₃ → ∀ (ih1 : l₁.sym2 ~ l₂.sym2) (ih2 : l₂.sym2 ~ l₃.sym2), l₁.sym2 ~ l₃.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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs ys : List α
h : xs <+ ys
⊢ xs.sym2 <+ ys.sym2
have slnil : Sublist.{u_1} (α := Sym2 α) (List.sym2 []) (List.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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs ys : List α
h : xs <+ ys
slnil : Sublist.{u_1} (α := Sym2 α) (List.sym2 []) (List.sym2 [])
⊢ xs.sym2 <+ ys.sym2
have cons : ∀ {l₁ l₂ : List α} (a : α) (h : l₁ <+ l₂) (ih : l₁.sym2 <+ l₂.sym2), l₁.sym2 <+ (a :: l₂).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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ xs.sym2 <+ ys.sym2
have cons_cons : ∀ {l₁ l₂ : List α} (a : α) (h : l₁ <+ l₂) (ih : l₁.sym2 <+ l₂.sym2), (a :: l₁).sym2 <+ (a :: l₂).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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs ys : List α
h : xs <+~ ys
⊢ xs.sym2 <+~ ys.sym2
have obtain : ∀ (xs' : List α) (hx : xs' ~ xs) (h : xs' <+ ys), xs.sym2 <+~ ys.sym2
Tactic: obtain ⟨xs', hx, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
x : α
xs : List α
ih : xs.sym2.length = (xs.length + 1).choose 2
⊢ (x :: xs).sym2.length = ((x :: xs).length + 1).choose 2
have cons : (map (fun (y : α) ↦ s(x, y)) (x :: xs) ++ 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]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ (x :: xs).sym2.length = ((x :: xs).length + 1).choose 2
have cons₁ : length (α := Sym2 α) (map (fun (y : α) ↦ s(x, y)) (x :: xs)) + 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]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ (x :: xs).sym2.length = ((x :: xs).length + 1).choose 2
have cons₂ : (x :: xs).length + 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]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ (x :: xs).sym2.length = ((x :: xs).length + 1).choose 2
have cons₃ : xs.length + 1 + xs.sym2.length = (xs.length + 1 + 1).choose 2
Tactic: rw [List.sym2, length_append, length_map, length_cons,
        Nat.choose_succ_succ, ← ih, Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ (x :: xs).sym2.length = ((x :: xs).length + 1).choose 2
have cons₄ : xs.length + 1 + xs.sym2.length = (xs.length + 1).choose 1 + (xs.length + 1).choose (Nat.succ 1)
Tactic: rw [List.sym2, length_append, length_map, length_cons,
        Nat.choose_succ_succ, ← ih, Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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)
⊢ (x :: xs).sym2.length = ((x :: xs).length + 1).choose 2
have cons₅ : xs.length + 1 + xs.sym2.length = (xs.length + 1).choose 1 + xs.sym2.length
Tactic: rw [List.sym2, length_append, length_map, length_cons,
        Nat.choose_succ_succ, ← ih, Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ (x :: xs).sym2.length = ((x :: xs).length + 1).choose 2
have cons₆ : xs.length + 1 + xs.sym2.length = xs.length + 1 + xs.sym2.length
Tactic: rw [List.sym2, length_append, length_map, length_cons,
        Nat.choose_succ_succ, ← ih, Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
⊢ xs.sym2.length = (xs.length + 1).choose 2
have nil : length.{u_1} (α := Sym2 α) (List.sym2 []) = (length.{u_1} (α := α) [] + 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]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
nil : length.{u_1} (α := Sym2 α) (List.sym2 []) = (length.{u_1} (α := α) [] + 1).choose 2
⊢ xs.sym2.length = (xs.length + 1).choose 2
have cons : ∀ (x : α) (xs : List α) (ih : xs.sym2.length = (xs.length + 1).choose 2),
  (x :: xs).sym2.length = ((x :: 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]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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)
⊢ Eq (α := List (Sym α 1)) (List.sym 1 (x :: xs)) (map (fun (x : α) ↦ x ::ₛ Sym.nil) (x :: xs))
have cons : List.sym 1 (x :: xs) = (x ::ₛ Sym.nil) :: map (fun (x : α) ↦ x ::ₛ Sym.nil) xs
Tactic: rw [map_cons, ← ih, List.sym, List.sym, map_singleton, singleton_append]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ Eq (α := List (Sym α 1)) (List.sym 1 (x :: xs)) (map (fun (x : α) ↦ x ::ₛ Sym.nil) (x :: xs))
have cons₁ : List.sym 1 (x :: xs) = (x ::ₛ Sym.nil) :: List.sym 1 xs
Tactic: rw [map_cons, ← ih, List.sym, List.sym, map_singleton, singleton_append]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ Eq (α := List (Sym α 1)) (List.sym 1 (x :: xs)) (map (fun (x : α) ↦ x ::ₛ Sym.nil) (x :: xs))
have 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
Tactic: rw [map_cons, ← ih, List.sym, List.sym, map_singleton, singleton_append]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ Eq (α := List (Sym α 1)) (List.sym 1 (x :: xs)) (map (fun (x : α) ↦ x ::ₛ Sym.nil) (x :: xs))
have 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
Tactic: rw [map_cons, ← ih, List.sym, List.sym, map_singleton, singleton_append]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ Eq (α := List (Sym α 1)) (List.sym 1 (x :: xs)) (map (fun (x : α) ↦ x ::ₛ Sym.nil) (x :: xs))
have cons₄ : [x ::ₛ Sym.nil] ++ List.sym (HAdd.hAdd (α := ℕ) 0 1) xs = (x ::ₛ Sym.nil) :: List.sym 1 xs
Tactic: rw [map_cons, ← ih, List.sym, List.sym, map_singleton, singleton_append]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ Eq (α := List (Sym α 1)) (List.sym 1 (x :: xs)) (map (fun (x : α) ↦ x ::ₛ Sym.nil) (x :: xs))
have cons₅ : (x ::ₛ Sym.nil) :: List.sym (HAdd.hAdd (α := ℕ) 0 1) xs = (x ::ₛ Sym.nil) :: List.sym 1 xs
Tactic: rw [map_cons, ← ih, List.sym, List.sym, map_singleton, singleton_append]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
⊢ Eq (α := List (Sym α 1)) (List.sym 1 xs) (map (fun (x : α) ↦ x ::ₛ Sym.nil) xs)
have nil : Eq.{u_1 + 1} (α := List (Sym α 1)) (List.sym 1 []) (map (fun (x : α) ↦ x ::ₛ Sym.nil) [])
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]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
nil : Eq.{u_1 + 1} (α := List (Sym α 1)) (List.sym 1 []) (map (fun (x : α) ↦ x ::ₛ Sym.nil) [])
⊢ Eq (α := List (Sym α 1)) (List.sym 1 xs) (map (fun (x : α) ↦ x ::ₛ Sym.nil) xs)
have 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))
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]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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)
⊢ Eq (α := List (Sym α 2)) (map (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) (x :: xs).sym2) (List.sym 2 (x :: xs))
have 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)
Tactic: rw [List.sym, ← ih, sym_one_eq, map_map, List.sym2, map_append, map_map]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
⊢ Eq (α := List (Sym α 2)) (map (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) xs.sym2) (List.sym 2 xs)
have nil : Eq (α := List (Sym α 2)) (map (α := Sym2 α) (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) (List.sym2 []))
  (List.sym 2 [])
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