awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
xs : List α
nil :
  Eq (α := List (Sym α 2)) (map (α := Sym2 α) (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) (List.sym2 []))
    (List.sym 2 [])
⊢ Eq (α := List (Sym α 2)) (map (⇑(Sym2.equivSym α) : (a : Sym2 α) → Sym α 2) xs.sym2) (List.sym 2 xs)
have 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))
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
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β
n : ℕ
xs x : List α
⊢ Eq (α := List (Sym β 0)) (List.sym 0 (map f x)) (map (Sym.map f) (List.sym 0 x))
have simp : [Sym.nil] = map (Sym.map f) [Sym.nil]
Tactic: simp only [List.sym]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
⊢ Eq (α := List (Sym β (n + 1))) (List.sym (n + 1) (map f (x :: xs))) (map (Sym.map f) (List.sym (n + 1) (x :: xs)))
have rw : HAppend.hAppend (α := List (Sym β n.succ))
    (map (fun (p : Sym β n) ↦ f x ::ₛ p) (map (Sym.map f) (List.sym n (x :: xs))))
    (map (Sym.map f) (List.sym (n + 1) xs)) =
  map (Sym.map f) (List.sym (n + 1) (x :: xs))
Tactic: rw [map_cons, List.sym, ← map_cons, sym_map f n (x :: xs), sym_map f (n + 1) xs]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
⊢ HAppend.hAppend (α := List (Sym β n.succ))
      (map (fun (p : Sym β n) ↦ f x ::ₛ p) (map (Sym.map f) (List.sym n (x :: xs))))
      (map (Sym.map f) (List.sym (n + 1) xs)) =
    map (Sym.map f) (List.sym (n + 1) (x :: xs))
have simp : Eq (α := List (Sym β n.succ)) (map ((fun (p : Sym β n) ↦ f x ::ₛ p) ∘ Sym.map f) (List.sym n (x :: xs)))
  (map (Sym.map f ∘ fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs)))
Tactic: simp only [map_map, List.sym, map_append, append_cancel_right_eq]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
⊢ Eq (α := List (Sym β n.succ)) (map ((fun (p : Sym β n) ↦ f x ::ₛ p) ∘ Sym.map f) (List.sym n (x :: xs)))
    (map (Sym.map f ∘ fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs)))
have e_f : Eq (α := Sym α n → Sym β n.succ) ((fun (p : Sym β n) ↦ f x ::ₛ p) ∘ Sym.map f) (Sym.map f ∘ fun (p : Sym α n) ↦ x ::ₛ p)
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
⊢ Eq (α := Sym α n → Sym β n.succ) ((fun (p : Sym β n) ↦ f x ::ₛ p) ∘ Sym.map f)
    (Sym.map f ∘ fun (p : Sym α n) ↦ x ::ₛ p)
have e_f : ∀ (s : Sym α n),
  (↑(((fun (p : Sym β n) ↦ f x ::ₛ p) ∘ Sym.map f) s) : Multiset β) =
    (↑((Sym.map f ∘ fun (p : Sym α n) ↦ x ::ₛ p) s) : Multiset β)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 ys : List α
h_1 : xs_1 <+ ys
xs : List α
n : ℕ
l₂ : List α
a : α
h : xs <+ l₂
⊢ Sublist (α := Sym α (n + 1)) (List.sym (n + 1) xs) (List.sym (n + 1) (a :: l₂))
have rw : HAppend.hAppend (α := List (Sym α (n + 1))) [] (List.sym (n + 1) xs) <+
  HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₂)))
    (List.sym (n + 1) l₂)
Tactic: rw [List.sym, ← nil_append (List.sym (n + 1) xs)]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 ys : List α
h_1 : xs_1 <+ ys
xs : List α
n : ℕ
l₂ : List α
a : α
h : xs <+ l₂
⊢ HAppend.hAppend (α := List (Sym α (n + 1))) [] (List.sym (n + 1) xs) <+
    HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₂)))
      (List.sym (n + 1) l₂)
have apply : Sublist (α := Sym α (n + 1)) (List.sym (n + 1) xs) (List.sym (n + 1) l₂)
Tactic: apply Sublist.append (nil_sublist _)
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs ys : List α
h_1 : xs <+ ys
n : ℕ
l₁ l₂ : List α
a : α
h : l₁ <+ l₂
⊢ Sublist (α := Sym α (n + 1)) (List.sym (n + 1) (a :: l₁)) (List.sym (n + 1) (a :: l₂))
have rw : HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₁)))
    (List.sym (n + 1) l₁) <+
  HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₂)))
    (List.sym (n + 1) l₂)
Tactic: rw [List.sym, List.sym]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs ys : List α
h_1 : xs <+ ys
n : ℕ
l₁ l₂ : List α
a : α
h : l₁ <+ l₂
⊢ HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₁)))
      (List.sym (n + 1) l₁) <+
    HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₂)))
      (List.sym (n + 1) l₂)
have hl : Sublist (α := Sym α (n + 1)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₁)))
  (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₂)))
Tactic: apply Sublist.append
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs ys : List α
h_1 : xs <+ ys
n : ℕ
l₁ l₂ : List α
a : α
h : l₁ <+ l₂
hl :
  Sublist (α := Sym α (n + 1)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₁)))
    (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₂)))
⊢ HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₁)))
      (List.sym (n + 1) l₁) <+
    HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ a ::ₛ p) (List.sym n (a :: l₂)))
      (List.sym (n + 1) l₂)
have hr : Sublist (α := Sym α (n + 1)) (List.sym (n + 1) l₁) (List.sym (n + 1) l₂)
Tactic: apply Sublist.append
-- Lean 4 proof step from Mathlib.Data.List.Sym (hypothesis)
Goal:
α : Type u_1
n : ℕ
xs_1 : List α
a : α
xs : List α
z : Sym α 0
ha : a ∈ z
hz : Membership.mem (γ := List (Sym α 0)) (List.sym 0 xs) z
⊢ a ∈ xs
have ha₁ : Membership.mem (γ := Sym α 0) Sym.nil a
Tactic: cases Sym.eq_nil_of_card_zero z
Cleared hypotheses: z, ha, hz
-- Lean 4 proof step from Mathlib.Data.List.Sym (hypothesis)
Goal:
α : Type u_1
n : ℕ
xs_1 : List α
a : α
xs : List α
z : Sym α 0
ha : a ∈ z
hz : Membership.mem (γ := List (Sym α 0)) (List.sym 0 xs) z
ha₁ : Membership.mem (γ := Sym α 0) Sym.nil a
⊢ a ∈ xs
have hz₁ : Membership.mem (γ := List (Sym α 0)) (List.sym 0 xs) Sym.nil
Tactic: cases Sym.eq_nil_of_card_zero z
Cleared hypotheses: z, ha, hz
-- Lean 4 proof step from Mathlib.Data.List.Sym (hypothesis)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) (x :: xs)) z
⊢ a ∈ x :: xs
have hz₁ : (∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z) ∨ Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
Tactic: rw [List.sym, mem_append, mem_map] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : (∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z) ∨ Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
⊢ a ∈ x :: xs
have inl : ∀ (z : Sym α n) (hz : z ∈ List.sym n (x :: xs)) (ha : a ∈ x ::ₛ z), a ∈ x :: xs
Tactic: obtain ⟨z, hz, rfl⟩ | hz := hz
Cleared hypotheses: z, ha, hz
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : (∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z) ∨ Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
inl : ∀ (z : Sym α n) (hz : z ∈ List.sym n (x :: xs)) (ha : a ∈ x ::ₛ z), a ∈ x :: xs
⊢ a ∈ x :: xs
have inr : ∀ (hz : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z), a ∈ x :: xs
Tactic: obtain ⟨z, hz, rfl⟩ | hz := hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Data.List.Sym (hypothesis)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a ∈ x ::ₛ z
⊢ a ∈ x :: xs
have ha₁ : a = x ∨ a ∈ z
Tactic: rw [Sym.mem_cons] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a = x ∨ a ∈ z
⊢ a ∈ x :: xs
have inl : ∀ (hz : z ∈ List.sym n (a :: xs)), a ∈ a :: xs
Tactic: obtain rfl | ha := ha
Cleared hypotheses: x, hz, ha
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a = x ∨ a ∈ z
inl : ∀ (hz : z ∈ List.sym n (a :: xs)), a ∈ a :: xs
⊢ a ∈ x :: xs
have inl₁ : ∀ (ha : a ∈ z), a ∈ x :: xs
Tactic: obtain rfl | ha := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
⊢ a ∈ x :: xs
have inr : a = x ∨ a ∈ xs
Tactic: rw [mem_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
⊢ a = x ∨ a ∈ xs
have inr : a ∈ xs
Tactic: right
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ Nodup (α := Sym α (n + 1)) (List.sym (n + 1) (x :: xs))
have rw : (HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs)))
    (List.sym (n + 1) xs)).Nodup
Tactic: rw [List.sym]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs)))
      (List.sym (n + 1) xs)).Nodup
have refine : Function.Injective (β := Sym α (n + 1)) fun (p : Sym α n) ↦ x ::ₛ p
Tactic: refine Nodup.append (Nodup.map ?inj (Nodup.sym n h)) (Nodup.sym (n + 1) h.of_cons) ?disj
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
refine : Function.Injective (β := Sym α (n + 1)) fun (p : Sym α n) ↦ x ::ₛ p
⊢ (HAppend.hAppend (α := List (Sym α n.succ)) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs)))
      (List.sym (n + 1) xs)).Nodup
have refine₁ : Disjoint (α := Sym α (n + 1)) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) (List.sym (n + 1) xs)
Tactic: refine Nodup.append (Nodup.map ?inj (Nodup.sym n h)) (Nodup.sym (n + 1) h.of_cons) ?disj
-- Lean 4 proof step from Mathlib.Data.List.Sym (hypothesis)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : Membership.mem (γ := List (Sym α (n + 1))) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) z
hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
⊢ False
have hz₁ : ∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z
Tactic: rw [mem_map] at hz
Cleared hypotheses: hz, hz'
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : ∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z
hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z
⊢ False
have obtain : ∀ (z : Sym α n) (_hz : z ∈ List.sym n (x :: xs))
  (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) (x ::ₛ z)), False
Tactic: obtain ⟨z, _hz, rfl⟩ := hz
Cleared hypotheses: z, hz, hz'
-- Lean 4 proof step from Mathlib.Data.List.Sym (hypothesis)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α n
_hz : z ∈ List.sym n (x :: xs)
hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) (x ::ₛ z)
⊢ False
have this : x ∈ xs
Tactic: have := first_mem_of_cons_mem_sym hz'
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ Disjoint (α := Sym α (n + 1)) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) (List.sym (n + 1) xs)
have case : ∀ ⦃z : Sym α (n + 1)⦄,
  Membership.mem (γ := List (Sym α (n + 1))) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) z →
    Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z → False
Tactic: case disj =>
      intro z hz hz'
      rw [mem_map] at hz
      obtain ⟨z, _hz, rfl⟩ := hz
      have := first_mem_of_cons_mem_sym hz'
      simp only [nodup_cons, this, not_true_eq_false, false_and] at h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
case case₁ case₂ :
  ∀ ⦃z : Sym α (n + 1)⦄
    (hz : Membership.mem (γ := List (Sym α (n + 1))) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) z)
    (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z), False
⊢ Disjoint (α := Sym α (n + 1)) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) (List.sym (n + 1) xs)
have case₃ : ∀ ⦃z : Sym α (n + 1)⦄ (hz : ∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z)
  (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z), False
Tactic: case disj =>
      intro z hz hz'
      rw [mem_map] at hz
      obtain ⟨z, _hz, rfl⟩ := hz
      have := first_mem_of_cons_mem_sym hz'
      simp only [nodup_cons, this, not_true_eq_false, false_and] at h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
case case₁ case₂ :
  ∀ ⦃z : Sym α (n + 1)⦄
    (hz : Membership.mem (γ := List (Sym α (n + 1))) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) z)
    (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z), False
case₃ :
  ∀ ⦃z : Sym α (n + 1)⦄ (hz : ∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z)
    (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z), False
⊢ Disjoint (α := Sym α (n + 1)) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) (List.sym (n + 1) xs)
have case₄ : ∀ (z : Sym α n) (_hz : z ∈ List.sym n (x :: xs))
  (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) (x ::ₛ z)), False
Tactic: case disj =>
      intro z hz hz'
      rw [mem_map] at hz
      obtain ⟨z, _hz, rfl⟩ := hz
      have := first_mem_of_cons_mem_sym hz'
      simp only [nodup_cons, this, not_true_eq_false, false_and] at h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
case case₁ case₂ :
  ∀ ⦃z : Sym α (n + 1)⦄
    (hz : Membership.mem (γ := List (Sym α (n + 1))) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) z)
    (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z), False
case₃ :
  ∀ ⦃z : Sym α (n + 1)⦄ (hz : ∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z)
    (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) z), False
case₄ :
  ∀ (z : Sym α n) (_hz : z ∈ List.sym n (x :: xs))
    (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) (x ::ₛ z)), False
⊢ Disjoint (α := Sym α (n + 1)) (map (fun (p : Sym α n) ↦ x ::ₛ p) (List.sym n (x :: xs))) (List.sym (n + 1) xs)
have case₅ : ∀ (z : Sym α n) (_hz : z ∈ List.sym n (x :: xs))
  (hz' : Membership.mem (γ := List (Sym α (n + 1))) (List.sym (n + 1) xs) (x ::ₛ z)) (this : x ∈ xs), False
Tactic: case disj =>
      intro z hz hz'
      rw [mem_map] at hz
      obtain ⟨z, _hz, rfl⟩ := hz
      have := first_mem_of_cons_mem_sym hz'
      simp only [nodup_cons, this, not_true_eq_false, false_and] at h
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n : ℕ
xs x : List α
⊢ length (α := Sym α 0) (List.sym 0 x) = x.length.multichoose 0
have rw : length.{u_1} (α := Sym α 0) [Sym.nil] = 1
Tactic: rw [List.sym, Nat.multichoose]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
⊢ length (α := Sym α (n + 1)) (List.sym (n + 1) (x :: xs)) = (x :: xs).length.multichoose (n + 1)
have rw : (List.sym n (x :: xs)).length + length (α := Sym α (n + 1)) (List.sym (n + 1) xs) = (xs.length + 1).multichoose (n + 1)
Tactic: rw [List.sym, length_append, length_map, length_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
⊢ (List.sym n (x :: xs)).length + length (α := Sym α (n + 1)) (List.sym (n + 1) xs) =
    (xs.length + 1).multichoose (n + 1)
have rw : (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) = (xs.length + 1).multichoose (n + 1)
Tactic: rw [@length_sym n (x :: xs), @length_sym (n + 1) xs]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
⊢ (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) = (xs.length + 1).multichoose (n + 1)
have rw : (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) =
  xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n
Tactic: rw [Nat.multichoose_succ_succ, length_cons, add_comm]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
rw :
  (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) =
    xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n
⊢ (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) = (xs.length + 1).multichoose (n + 1)
have rw₁ : (xs.length + 1).multichoose n + xs.length.multichoose (n + 1) =
  xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n
Tactic: rw [Nat.multichoose_succ_succ, length_cons, add_comm]
-- Lean 4 proof step from Mathlib.Data.List.Sym (goal)
Goal:
α : Type u_1
n_1 : ℕ
xs_1 : List α
n : ℕ
x : α
xs : List α
rw :
  (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) =
    xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n
rw₁ :
  (xs.length + 1).multichoose n + xs.length.multichoose (n + 1) =
    xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n
⊢ (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) = (xs.length + 1).multichoose (n + 1)
have rw₂ : xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n =
  xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n
Tactic: rw [Nat.multichoose_succ_succ, length_cons, add_comm]
-- Lean 4 proof step from Mathlib.Data.List.TFAE (goal)
Goal:
c : Prop
l : List Prop
IH :
  ∀ {a b : Prop} (h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (a :: b :: l)) (h_last : l.getLastD b → a),
    (a :: b :: l).TFAE
a b : Prop
h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (a :: b :: c :: l)
h_last : (c :: l).getLastD b → a
⊢ (a :: b :: c :: l).TFAE
have cons : ∀
  (IH :
    ∀ {a b : Prop} (h_chain : (a → b) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (b :: l)) (h_last : l.getLastD b → a),
      (a ↔ b) ∧ (b :: l).TFAE)
  (h_chain : (a → b) ∧ (b → c) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (c :: l)) (h_last : l.getLastD c → a),
  (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE
Tactic: simp only [tfae_cons_cons, getLastD_cons, isChain_cons_cons] at *
Cleared hypotheses: IH, h_chain, h_last
-- Lean 4 proof step from Mathlib.Data.List.TFAE (hypothesis)
Goal:
c : Prop
l : List Prop
a b : Prop
IH :
  ∀ {a b : Prop} (h_chain : (a → b) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (b :: l)) (h_last : l.getLastD b → a),
    (a ↔ b) ∧ (b :: l).TFAE
h_chain : (a → b) ∧ (b → c) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (c :: l)
h_last : l.getLastD c → a
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE
have ab : a → b
Tactic: rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩
Cleared hypotheses: h_chain
-- Lean 4 proof step from Mathlib.Data.List.TFAE (hypothesis)
Goal:
c : Prop
l : List Prop
a b : Prop
IH :
  ∀ {a b : Prop} (h_chain : (a → b) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (b :: l)) (h_last : l.getLastD b → a),
    (a ↔ b) ∧ (b :: l).TFAE
h_chain : (a → b) ∧ (b → c) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (c :: l)
h_last : l.getLastD c → a
ab : a → b
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE
have bc : b → c
Tactic: rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩
Cleared hypotheses: h_chain
-- Lean 4 proof step from Mathlib.Data.List.TFAE (hypothesis)
Goal:
c : Prop
l : List Prop
a b : Prop
IH :
  ∀ {a b : Prop} (h_chain : (a → b) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (b :: l)) (h_last : l.getLastD b → a),
    (a ↔ b) ∧ (b :: l).TFAE
h_chain : (a → b) ∧ (b → c) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (c :: l)
h_last : l.getLastD c → a
ab : a → b
bc : b → c
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE
have ch : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (c :: l)
Tactic: rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩
Cleared hypotheses: h_chain
-- Lean 4 proof step from Mathlib.Data.List.TFAE (hypothesis)
Goal:
c : Prop
l : List Prop
a b : Prop
IH :
  ∀ {a b : Prop} (h_chain : (a → b) ∧ IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (b :: l)) (h_last : l.getLastD b → a),
    (a ↔ b) ∧ (b :: l).TFAE
h_last : l.getLastD c → a
ab : a → b
bc : b → c
ch : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (c :: l)
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE
have this : (b ↔ c) ∧ (c :: l).TFAE
Tactic: have := IH ⟨bc, ch⟩ (ab ∘ h_last)
-- Lean 4 proof step from Mathlib.Data.List.TFAE (goal)
Goal:
a b : Prop
l : List Prop
h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (a :: b :: l)
h_last : l.getLastD b → a
⊢ (a :: b :: l).TFAE
have nil : ∀ {a b : Prop} (h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) [a, b]) (h_last : getLastD [] b → a), [a, b].TFAE
Tactic: induction l generalizing a b with
  | nil => simp_all [tfae_cons_cons, iff_def]
  | cons c l IH =>
    simp only [tfae_cons_cons, getLastD_cons, isChain_cons_cons] at *
    rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩
    have := IH ⟨bc, ch⟩ (ab ∘ h_last)
    exact ⟨⟨ab, h_last ∘ (this.2 c (.head _) _ getLastD_mem_cons).1 ∘ bc⟩, this⟩
Cleared hypotheses: a, b, l, h_chain, h_last
-- Lean 4 proof step from Mathlib.Data.List.TFAE (goal)
Goal:
a b : Prop
l : List Prop
h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (a :: b :: l)
h_last : l.getLastD b → a
nil : ∀ {a b : Prop} (h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) [a, b]) (h_last : getLastD [] b → a), [a, b].TFAE
⊢ (a :: b :: l).TFAE
have cons : ∀ (c : Prop) (l : List Prop)
  (IH :
    ∀ {a b : Prop} (h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (a :: b :: l)) (h_last : l.getLastD b → a),
      (a :: b :: l).TFAE)
  {a b : Prop} (h_chain : IsChain (fun (x1 x2 : Prop) ↦ x1 → x2) (a :: b :: c :: l)) (h_last : (c :: l).getLastD b → a),
  (a :: b :: c :: l).TFAE
Tactic: induction l generalizing a b with
  | nil => simp_all [tfae_cons_cons, iff_def]
  | cons c l IH =>
    simp only [tfae_cons_cons, getLastD_cons, isChain_cons_cons] at *
    rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩
    have := IH ⟨bc, ch⟩ (ab ∘ h_last)
    exact ⟨⟨ab, h_last ∘ (this.2 c (.head _) _ getLastD_mem_cons).1 ∘ bc⟩, this⟩
Cleared hypotheses: a, b, l, h_chain, h_last
-- Lean 4 proof step from Mathlib.Data.List.TFAE (goal)
Goal:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun (p : α → Prop) ↦ p a) l)
⊢ TFAE (map (fun (p : α → Prop) ↦ ∀ (a : α), p a) l)
have simp : ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∀ (a : α), j a) ↔ ∀ (a : α), j_1 a)
Tactic: simp only [TFAE, List.forall_mem_map]
-- Lean 4 proof step from Mathlib.Data.List.TFAE (goal)
Goal:
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun (p : α → Prop) ↦ p a) l)
⊢ TFAE (map (fun (p : α → Prop) ↦ ∃ (a : α), p a) l)
have simp : ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∃ (a : α), j a) ↔ ∃ (a : α), j_1 a)
Tactic: simp only [TFAE, List.forall_mem_map]