awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
xs : List α
⊢ (map f xs).sym2 = map (Sym2.map f) xs.sym2
have nil : (map f []).sym2 = map (Sym2.map f) (List.sym2 [])
Tactic: induction xs with
  | nil => simp [List.sym2]
  | cons x xs ih => simp [List.sym2, ih, Function.comp]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
xs : List α
nil : (map f []).sym2 = map (Sym2.map f) (List.sym2 [])
⊢ (map f xs).sym2 = map (Sym2.map f) xs.sym2
have 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
Tactic: induction xs with
  | nil => simp [List.sym2]
  | cons x xs ih => simp [List.sym2, ih, Function.comp]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
x : α
xs : List α
z : Sym2 α
⊢ z ∈ (x :: xs).sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2
have 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
Tactic: simp only [List.sym2, map_cons, cons_append, mem_cons, mem_append, mem_map]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
⊢ xs.sym2 = [] ↔ xs = []
have nil : Eq.{u_1 + 1} (α := List (Sym2 α)) (List.sym2 []) [] ↔ Eq.{u_1 + 1} (α := List α) [] []
Tactic: cases xs
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
nil : Eq.{u_1 + 1} (α := List (Sym2 α)) (List.sym2 []) [] ↔ Eq.{u_1 + 1} (α := List α) [] []
⊢ xs.sym2 = [] ↔ xs = []
have cons : ∀ (head : α) (tail : List α), (head :: tail).sym2 = [] ↔ head :: tail = []
Tactic: cases xs
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ a ∈ x :: xs
have cons : a = x ∨ a ∈ xs
Tactic: rw [mem_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sym (hypothesis)
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
⊢ a = x ∨ a ∈ xs
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ a = x ∨ a ∈ xs
have cons : ∀ (h : s(a, b) = s(x, x)), a = x ∨ a ∈ xs
Tactic: obtain (h | ⟨c, hc, h⟩ | h) := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ a = x ∨ a ∈ xs
have cons₁ : ∀ (c : α) (hc : c ∈ xs) (h : s(a, b) = s(x, c)), a = x ∨ a ∈ xs
Tactic: obtain (h | ⟨c, hc, h⟩ | h) := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ a = x ∨ a ∈ xs
have cons₂ : ∀ (h : s(a, b) ∈ xs.sym2), a = x ∨ a ∈ xs
Tactic: obtain (h | ⟨c, hc, h⟩ | h) := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (hypothesis)
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 ∨ a ∈ xs
have h₁ : a = x ∧ (b = x ∨ b = x)
Tactic: rw [Sym2.eq_iff, ← and_or_left] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (hypothesis)
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 ∨ a ∈ xs
have h₁ : a = x ∧ b = c ∨ a = c ∧ b = x
Tactic: rw [Sym2.eq_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ a = x ∨ a ∈ xs
have cons : ∀ (hc : b ∈ xs), a = a ∨ a ∈ xs
Tactic: obtain (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) := h
Cleared hypotheses: x, c, hc, h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ a = x ∨ a ∈ xs
have cons₁ : ∀ (hc : a ∈ xs), a = b ∨ a ∈ xs
Tactic: obtain (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) := h
Cleared hypotheses: x, c, hc, h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
⊢ a ∈ xs
have nil : ∀ (h : Membership.mem (γ := List (Sym2 α)) (List.sym2 []) s(a, b)), Membership.mem (γ := List α) [] a
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
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ a ∈ xs
have cons : ∀ (x : α) (xs : List α) (ih : ∀ (h : s(a, b) ∈ xs.sym2), a ∈ xs) (h : s(a, b) ∈ (x :: xs).sym2), a ∈ x :: 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
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Sym (hypothesis)
Goal:
α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
⊢ b ∈ xs
have h₁ : s(b, a) ∈ xs.sym2
Tactic: rw [Sym2.eq_swap] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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) ∈ (x :: xs).sym2
have cons : 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]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
a b : α
ha : a ∈ xs
hb : b ∈ xs
⊢ s(a, b) ∈ xs.sym2
have nil : ∀ (ha : Membership.mem (γ := List α) [] a) (hb : Membership.mem (γ := List α) [] b),
  Membership.mem (γ := List (Sym2 α)) (List.sym2 []) s(a, b)
Tactic: induction xs with
  | nil => simp at ha
  | cons x xs ih =>
    rw [mem_sym2_cons_iff]
    grind
Cleared hypotheses: xs, ha, hb
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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)
⊢ s(a, b) ∈ xs.sym2
have 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
Tactic: induction xs with
  | nil => simp at ha
  | cons x xs ih =>
    rw [mem_sym2_cons_iff]
    grind
Cleared hypotheses: xs, ha, hb
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
a b : α
⊢ s(a, b) ∈ xs.sym2 ↔ a ∈ xs ∧ b ∈ xs
have mp : s(a, b) ∈ xs.sym2 → a ∈ xs ∧ b ∈ xs
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
a b : α
mp : s(a, b) ∈ xs.sym2 → a ∈ xs ∧ b ∈ xs
⊢ s(a, b) ∈ xs.sym2 ↔ a ∈ xs ∧ b ∈ xs
have mpr : a ∈ xs ∧ b ∈ xs → s(a, b) ∈ xs.sym2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
z : Sym2 α
⊢ z ∈ xs.sym2 ↔ ∀ y ∈ z, y ∈ xs
have refine : ∀ (a b : α), s(a, b) ∈ xs.sym2 ↔ ∀ y ∈ s(a, b), y ∈ xs
Tactic: refine z.ind (fun a b => ?_)
-- Lean 4 proof step from Mathlib.Data.List.Sym (hypothesis)
Goal:
α : Type u_1
x : α
xs : List α
ih : ∀ (h : xs.Nodup), xs.sym2.Nodup
h : (x :: xs).Nodup
⊢ (map (fun (y : α) ↦ s(x, y)) (x :: xs) ++ xs.sym2).Nodup
have ih₁ : xs.sym2.Nodup
Tactic: specialize ih h.of_cons
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.List.Sym (hypothesis)
Goal:
α : Type u_1
x : α
xs : List α
h : (x :: xs).Nodup
ih : xs.sym2.Nodup
⊢ (map (fun (y : α) ↦ s(x, y)) (x :: xs) ++ xs.sym2).Nodup
have h₁ : x ∉ xs ∧ xs.Nodup
Tactic: rw [nodup_cons] at h
Cleared hypotheses: h, ih
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
have refine : (fun (y : α) ↦ s(x, y)) x ∉ map (fun (y : α) ↦ s(x, y)) xs
Tactic: refine Nodup.append (Nodup.cons ?notmem (h.2.map ?inj)) ih ?disj
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ (map (fun (y : α) ↦ s(x, y)) (x :: xs) ++ xs.sym2).Nodup
have refine₁ : Function.Injective (β := Sym2 α) fun (y : α) ↦ s(x, y)
Tactic: refine Nodup.append (Nodup.cons ?notmem (h.2.map ?inj)) ih ?disj
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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)
⊢ (map (fun (y : α) ↦ s(x, y)) (x :: xs) ++ xs.sym2).Nodup
have refine₂ : Disjoint (map (fun (y : α) ↦ s(x, y)) (x :: xs)) xs.sym2
Tactic: refine Nodup.append (Nodup.cons ?notmem (h.2.map ?inj)) ih ?disj
-- Lean 4 proof step from Mathlib.Data.List.Sym (hypothesis)
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
⊢ False
have hz₁ : ∃ (a : α), (a = x ∨ a ∈ xs) ∧ s(x, a) = z
Tactic: simp only [mem_cons, mem_map] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ False
have inl : ∀ (w : α) (h : w ∉ xs ∧ xs.Nodup) (hz' : s(w, w) ∈ xs.sym2), False
Tactic: obtain ⟨_, (rfl | _), rfl⟩ := hz
Cleared hypotheses: x, h, z, hz', hz
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ False
have inr : ∀ w ∈ xs, ∀ (hz' : s(x, w) ∈ xs.sym2), False
Tactic: obtain ⟨_, (rfl | _), rfl⟩ := hz
Cleared hypotheses: z, hz', hz
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
a b : α
⊢ Eq.{u_1 + 1} (α := Sym2 α) ((fun (y : α) ↦ s(x, y)) a) ((fun (y : α) ↦ s(x, y)) b) → a = b
have simp : a = b ∨ x = b ∧ a = x → a = b
Tactic: simp only [Sym2.eq_iff, true_and]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ Function.Injective (β := Sym2 α) fun (y : α) ↦ s(x, y)
have case : ∀ ⦃a a₂ : α⦄, Eq.{u_1 + 1} (α := Sym2 α) ((fun (y : α) ↦ s(x, y)) a) ((fun (y : α) ↦ s(x, y)) a₂) → a = a₂
Tactic: case inj =>
      intro a b
      simp only [Sym2.eq_iff, true_and]
      rintro (rfl | ⟨rfl, rfl⟩) <;> rfl
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ Function.Injective (β := Sym2 α) fun (y : α) ↦ s(x, y)
have case₂ : ∀ ⦃a b : α⦄, a = b ∨ x = b ∧ a = x → a = b
Tactic: case inj =>
      intro a b
      simp only [Sym2.eq_iff, true_and]
      rintro (rfl | ⟨rfl, rfl⟩) <;> rfl
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
h : xs.Nodup
⊢ xs.sym2.Nodup
have nil : ∀ (h : Nodup.{u_1} (α := α) []), Nodup.{u_1} (α := Sym2 α) (List.sym2 [])
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
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
h : xs.Nodup
nil : ∀ (h : Nodup.{u_1} (α := α) []), Nodup.{u_1} (α := Sym2 α) (List.sym2 [])
⊢ xs.sym2.Nodup
have cons : ∀ (x : α) (xs : List α) (ih : ∀ (h : xs.Nodup), xs.sym2.Nodup) (h : (x :: xs).Nodup), (x :: 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
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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)
have cons : s(x, x') :: map (fun (y : α) ↦ s(x, y)) xs <+ map (fun (y : α) ↦ s(x', y)) xs ++ xs.sym2
Tactic: refine .cons _ ?_
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
have cons : [s(x, x')] <+ map (fun (y : α) ↦ s(x', y)) xs
Tactic: refine .append ?_ (ih h)
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
have cons : ∃ a ∈ xs, s(x', a) = s(x, x')
Tactic: rw [singleton_sublist, mem_map]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ s(x, x') :: map (fun (y : α) ↦ s(x, y)) xs <+ s(x', x') :: (map (fun (y : α) ↦ s(x', y)) xs ++ xs.sym2)
have cons : 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⟩
Cleared hypotheses: x', h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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)
⊢ s(x, x') :: map (fun (y : α) ↦ s(x, y)) xs <+ s(x', x') :: (map (fun (y : α) ↦ s(x', y)) xs ++ xs.sym2)
have 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)
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⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
x : α
xs : List α
h : x ∈ xs
⊢ map (fun (y : α) ↦ s(x, y)) xs <+ xs.sym2
have nil : ∀ (h : Membership.mem (γ := List α) [] x), Sublist.{u_1} (α := Sym2 α) (map (fun (y : α) ↦ s(x, y)) []) (List.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⟩
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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 [])
⊢ map (fun (y : α) ↦ s(x, y)) xs <+ xs.sym2
have 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
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⟩
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
x : α
xs : List α
h : x ∉ xs
⊢ Disjoint (map (fun (y : α) ↦ s(x, y)) xs) xs.sym2
have nil : ∀ (h : x ∉ []), Disjoint.{u_1} (α := Sym2 α) (map (fun (y : α) ↦ s(x, y)) []) (List.sym2 [])
Tactic: induction xs with
  | nil => simp
  | cons x' xs ih => aesop (add simp mk_mem_sym2_iff, unfold safe List.Disjoint)
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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 [])
⊢ Disjoint (map (fun (y : α) ↦ s(x, y)) xs) xs.sym2
have 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
Tactic: induction xs with
  | nil => simp
  | cons x' xs ih => aesop (add simp mk_mem_sym2_iff, unfold safe List.Disjoint)
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
⊢ (s(x, x) :: (map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2
have cons : ∀ (hm : x ∈ xs), (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)
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ (s(x, x) :: (map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2
have cons₁ : ∀ (hm : x ∉ xs), (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)
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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)).dedup = (x :: xs).dedup.sym2
have cons : s(x, x) ∈ map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2
Tactic: rw [dedup_cons_of_mem hm, ← ih, dedup_cons_of_mem,
        List.Subset.dedup_append_right (map_mk_sublist_sym2 _ _ hm).subset]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
have cons : Membership.mem (γ := List (Sym2 α)) (map (fun (y : α) ↦ s(x, y)) xs) s(x, x)
Tactic: refine mem_append_left _ ?_
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∈ xs
⊢ Membership.mem (γ := List (Sym2 α)) (map (fun (y : α) ↦ s(x, y)) xs) s(x, x)
have cons : ∃ a ∈ xs, s(x, a) = s(x, x)
Tactic: rw [mem_map]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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)).dedup = (x :: xs).dedup.sym2
have cons : Function.Injective (β := Sym2 α) fun (y : α) ↦ s(x, y)
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]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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)
⊢ (s(x, x) :: (map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2
have cons₁ : Disjoint (map (fun (y : α) ↦ s(x, y)) xs) xs.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]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
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
⊢ (s(x, x) :: (map (fun (y : α) ↦ s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2
have cons₂ : s(x, x) ∉ map (fun (y : α) ↦ s(x, y)) xs ++ xs.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]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
⊢ xs.sym2.dedup = xs.dedup.sym2
have nil : Eq.{u_1 + 1} (α := List (Sym2 α)) (dedup (List.sym2 [])) (List.sym2 (dedup []))
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