awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r₁ r₂ : α → α → Prop
sym₁ : Symmetric r₁
sym₂ : Symmetric r₂
⊢ fromRel (r := r₁) sym₁ = fromRel (r := r₂) sym₂ ↔
    Eq (α := Set (Sym2 α))
      ((fromRelOrderIso α : (a : { r : α → α → Prop // Symmetric r }) → Set (Sym2 α))
          (Subtype.mk (p := Symmetric) r₁ sym₁) :
        Set (Sym2 α))
      ((fromRelOrderIso α : (a : { r : α → α → Prop // Symmetric r }) → Set (Sym2 α))
          (Subtype.mk (p := Symmetric) r₂ sym₂) :
        Set (Sym2 α))

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
z_1 : Sym2 α_1
f : α_1 → β
α : Type u_4
z : Sym2 α
refine : { f : α → α → Multiset α // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
⊢ Multiset α

Tactic:
refine Sym2.lift ?_ z

Premises used: Sym2.lift, DFunLike.coe
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
z_1 : Sym2 α_1
f : α_1 → β
α : Type u_4
z : Sym2 α
property :
  ∀ (a₁ a₂ : α),
    Eq.{u_4 + 1} (α := Multiset α) ((fun (x1 x2 : α) ↦ (↑[x1, x2] : Multiset α)) a₁ a₂)
      ((fun (x1 x2 : α) ↦ (↑[x1, x2] : Multiset α)) a₂ a₁)
⊢ { f : α → α → Multiset α // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }

Tactic:
use (Multiset.ofList [·, ·])

Premises used: List.cons, Multiset.ofList, List.nil
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
z_1 : Sym2 α_1
f : α_1 → β
α : Type u_4
z : Sym2 α
⊢ ∀ (a₁ a₂ : α),
    Eq.{u_4 + 1} (α := Multiset α) ((fun (x1 x2 : α) ↦ (↑[x1, x2] : Multiset α)) a₁ a₂)
      ((fun (x1 x2 : α) ↦ (↑[x1, x2] : Multiset α)) a₂ a₁)

Tactic:
simp [List.Perm.swap]

Premises used: List.Perm.swap
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_4
z : Sym2 α
h : ∀ (x y : α), s(x, y).toMultiset.card = 2
⊢ z.toMultiset.card = 2

Tactic:
induction z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_4
x y : α
⊢ s(x, y).toMultiset.card = 2

Tactic:
simp [Sym2.toMultiset]

Premises used: Sym2.toMultiset
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_4
x : α
z : Sym2 α
h : ∀ (x_1 y : α), x ∈ s(x_1, y).toMultiset ↔ x ∈ s(x_1, y)
⊢ x ∈ z.toMultiset ↔ x ∈ z

Tactic:
induction z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_4
x x_1 y : α
⊢ x ∈ s(x_1, y).toMultiset ↔ x ∈ s(x_1, y)

Tactic:
simp [Sym2.toMultiset]

Premises used: Sym2.toMultiset
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
x : α
z : Sym2 α
rw : x ∈ z.toFinset ↔ x ∈ z.toMultiset
rw₁ : x ∈ z.toMultiset.toFinset ↔ x ∈ z.toMultiset
rw₂ rw₃ : x ∈ z.toMultiset ↔ x ∈ z.toMultiset
⊢ x ∈ z.toFinset ↔ x ∈ z

Tactic:
rw [← Sym2.mem_toMultiset, Sym2.toFinset, Multiset.mem_toFinset]

Premises used: Sym2.toFinset, Sym2.mem_toMultiset, Multiset.mem_toFinset
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
z : Sym2 α
⊢ z.toFinset ≠ ∅

Tactic:
Finset.ne_empty_of_mem (Sym2.mem_toFinset.mpr (Sym2.out_fst_mem _))

Premises used: Iff.mpr, Finset.ne_empty_of_mem, Sym2.out_fst_mem, Sym2.mem_toFinset
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
z : Sym2 α
⊢ z.toFinset ≠ ∅

Tactic:
exact Finset.ne_empty_of_mem (Sym2.mem_toFinset.mpr (Sym2.out_fst_mem _))

Premises used: Iff.mpr, Finset.ne_empty_of_mem, Sym2.out_fst_mem, Sym2.mem_toFinset
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
h : ∀ (a : α), a ∈ s(x, y).toFinset ↔ Membership.mem (γ := Finset α) {x, y} a
⊢ s(x, y).toFinset = {x, y}

Tactic:
ext
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
x y a : α
⊢ a ∈ s(x, y).toFinset ↔ Membership.mem (γ := Finset α) {x, y} a

Tactic:
simp [← Sym2.mem_toFinset, ← Sym2.mem_iff]

Premises used: Sym2.mem_toFinset, Sym2.mem_iff
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
z : Sym2 α
h : z.IsDiag
h₁ : ∀ (x y : α) (h : s(x, y).IsDiag), #s(x, y).toFinset = 1
⊢ #z.toFinset = 1

Tactic:
induction z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
h : s(x, y).IsDiag
⊢ x = y

Tactic:
rw [Sym2.mk_isDiag_iff] at h

Premises used: Sym2.mk_isDiag_iff
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
h : x = y
⊢ #s(x, y).toFinset = 1

Tactic:
simp [Sym2.toFinset_mk_eq, h]

Premises used: Sym2.toFinset_mk_eq
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
z : Sym2 α
h : ¬z.IsDiag
h₁ : ∀ (x y : α) (h : ¬s(x, y).IsDiag), #s(x, y).toFinset = 2
⊢ #z.toFinset = 2

Tactic:
induction z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
h : ¬s(x, y).IsDiag
⊢ ¬x = y

Tactic:
rw [Sym2.mk_isDiag_iff] at h

Premises used: Sym2.mk_isDiag_iff
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
h : ¬x = y
⊢ #s(x, y).toFinset = 2

Tactic:
simp [Sym2.toFinset_mk_eq, h]

Premises used: Sym2.toFinset_mk_eq
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
z : Sym2 α
pos : ∀ (h : z.IsDiag), #z.toFinset = if z.IsDiag then 1 else 2
neg : ∀ (h : ¬z.IsDiag), #z.toFinset = if z.IsDiag then 1 else 2
⊢ #z.toFinset = if z.IsDiag then 1 else 2

Tactic:
by_cases h : z.IsDiag

Premises used: Sym2.IsDiag
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
z : Sym2 α
h : z.IsDiag
⊢ #z.toFinset = if z.IsDiag then 1 else 2

Tactic:
simp [card_toFinset_of_isDiag z h, h]

Premises used: Sym2.card_toFinset_of_isDiag
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
z : Sym2 α
h : ¬z.IsDiag
⊢ #z.toFinset = if z.IsDiag then 1 else 2

Tactic:
simp [card_toFinset_of_not_isDiag z h, h]

Premises used: Sym2.card_toFinset_of_not_isDiag
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
simp : a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
⊢ [a₁, b₁].Perm [a₂, b₂] → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂

Tactic:
simp only [← Multiset.coe_eq_coe, ← Multiset.cons_coe, Multiset.coe_nil, Multiset.cons_zero,
        Multiset.cons_eq_cons, Multiset.singleton_inj, ne_eq, Multiset.singleton_eq_cons_iff,
        exists_eq_right_right, and_true]

Premises used: exists_eq_right_right, and_true, Multiset.singleton_inj, Multiset.coe_eq_coe, Multiset.cons_eq_cons, ne_eq, Multiset.singleton_eq_cons_iff, Multiset.cons_coe, Multiset.cons_zero, Multiset.coe_nil
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
inl : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₁ : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inr₁ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
inl₂ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inl₃ : a₁ = a₂ → b₁ = b₂ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
inr₂ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → a₁ = b₂
inr₃ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬(a₁ = a₂ ∧ b₁ = b₂) → b₁ = a₂
inl₄ : a₁ = a₂ → b₁ = b₂ → ¬a₁ = a₂ → a₁ = b₂
inl₅ : a₁ = a₂ → b₁ = b₂ → ¬b₁ = b₂ → a₁ = b₂
inl₆ : a₁ = a₂ → b₁ = b₂ → ¬a₁ = a₂ → b₁ = a₂
inl₇ : a₁ = a₂ → b₁ = b₂ → ¬b₁ = b₂ → b₁ = a₂
inr₄ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬a₁ = a₂ → a₁ = b₂
inr₅ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬b₁ = b₂ → a₁ = b₂
inr₆ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬a₁ = a₂ → a₁ = b₂
inr₇ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬b₁ = b₂ → a₁ = b₂
inr₈ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬a₁ = a₂ → a₁ = b₂
inr₉ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬b₁ = b₂ → a₁ = b₂
inr₁₀ inr₁₁ inr₁₂ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬a₁ = a₂ → a₁ = b₂
inr₁₃ inr₁₄ inr₁₅ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬b₁ = b₂ → a₁ = b₂
inr₁₆ inr₁₇ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬a₁ = a₂ → a₁ = b₂
inr₁₈ inr₁₉ : ¬a₁ = a₂ → b₁ = a₂ → b₂ = a₁ → ¬b₁ = b₂ → a₁ = b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂

Tactic:
tauto
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = a₂
h₂ : b₁ = b₂
rw : [a₂, b₁].Perm [a₂, b₂]
rw₁ rw₂ : [a₂, b₂].Perm [a₂, b₂]
⊢ [a₁, b₁].Perm [a₂, b₂]

Tactic:
rw [h₁, h₂]
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
rw : [b₂, a₂].Perm [a₂, b₂]
⊢ [a₁, b₁].Perm [a₂, b₂]

Tactic:
rw [h₁, h₂]
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂].Perm [a₂, b₂]

Tactic:
done
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂].Perm [a₂, b₂]

Tactic:
constructor
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂].Perm [a₂, b₂]

Tactic:
first | done | constructor
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x y : α
refl : [(x, y).2].Perm [(x, y).2]
⊢ (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    ((fun (x : α × α) ↦
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [x.1, x.2] ⋯ : { l : List α // l.length = 2 }))
      (x, y))
    ((fun (x : α × α) ↦
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [x.1, x.2] ⋯ : { l : List α // l.length = 2 }))
      (x, y))

Tactic:
constructor
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x y : α
⊢ [(x, y).2].Perm [(x, y).2]

Tactic:
apply List.Perm.refl

Premises used: List.Perm.refl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x y : α
swap : List.Perm.{u_1} (α := α) [] []
⊢ (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    ((fun (x : α × α) ↦
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [x.1, x.2] ⋯ : { l : List α // l.length = 2 }))
      (x, y))
    ((fun (x : α × α) ↦
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [x.1, x.2] ⋯ : { l : List α // l.length = 2 }))
      (y, x))

Tactic:
apply List.Perm.swap'

Premises used: List.Perm.swap'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x y : α
⊢ List.Perm.{u_1} (α := α) [] []

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : List α
hx : x.length = 2
y : List α
hy : y.length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) x hx) (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
nil :
  ∀ (hx : List.length.{u_1} (α := α) [] = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
cons :
  ∀ (head : α) (x : List α) (hx : (head :: x).length = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) x hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))

Tactic:
rcases x with - | ⟨_, x⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
hx : List.length.{u_1} (α := α) [] = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hx) (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))

Tactic:
simp at hx
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head : α
x : List α
hx : (head :: x).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
cons :
  ∀ (hx : [head].length = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head] hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head] hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
cons₁ :
  ∀ (head_1 : α) (x : List α) (hx : (head :: head_1 :: x).length = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))

Tactic:
rcases x with - | ⟨_, x⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head : α
hx : [head].length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head] hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))

Tactic:
simp at hx
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head head_1 : α
x : List α
hx : (head :: head_1 :: x).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
cons :
  ∀ (hx : [head, head_1].length = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
cons₁ :
  ∀ (head_2 : α) (x : List α) (hx : (head :: head_1 :: head_2 :: x).length = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: head_2 :: x) hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: head_2 :: x) hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))

Tactic:
rcases x with - | ⟨_, x⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head head_1 head_2 : α
x : List α
hx : (head :: head_1 :: head_2 :: x).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: head_2 :: x) hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
cons : False
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: head_2 :: x) hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))

Tactic:
exfalso
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head head_1 head_2 : α
x : List α
hx : (head :: head_1 :: head_2 :: x).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: head_2 :: x) hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
⊢ False

Tactic:
simp at hx
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head head_1 : α
hx : [head, head_1].length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy)
cons :
  ∀ (hy : List.length.{u_1} (α := α) [] = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hy))
cons₁ :
  ∀ (head_2 : α) (y : List α) (hy : (head_2 :: y).length = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: y) hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: y) hy))
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) y hy))

Tactic:
rcases y with - | ⟨_, y⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head head_1 : α
hx : [head, head_1].length = 2
hy : List.length.{u_1} (α := α) [] = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hy)
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hy))

Tactic:
simp at hy
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head head_1 : α
hx : [head, head_1].length = 2
head_2 : α
y : List α
hy : (head_2 :: y).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: y) hy)
cons :
  ∀ (hy : [head_2].length = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head_2] hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head_2] hy))
cons₁ :
  ∀ (head_3 : α) (y : List α) (hy : (head_2 :: head_3 :: y).length = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: head_3 :: y) hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: head_3 :: y) hy))
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: y) hy))

Tactic:
rcases y with - | ⟨_, y⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head head_1 : α
hx : [head, head_1].length = 2
head_2 : α
hy : [head_2].length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head_2] hy)
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head_2] hy))

Tactic:
simp at hy
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head head_1 : α
hx : [head, head_1].length = 2
head_2 head_3 : α
y : List α
hy : (head_2 :: head_3 :: y).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: head_3 :: y) hy)
cons :
  ∀ (hy : [head_2, head_3].length = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head_2, head_3] hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head_2, head_3] hy))
cons₁ :
  ∀ (head_4 : α) (y : List α) (hy : (head_2 :: head_3 :: head_4 :: y).length = 2)
    (h :
      (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
        (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: head_3 :: head_4 :: y) hy)),
    Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
      (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: head_3 :: head_4 :: y) hy))
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: head_3 :: y) hy))

Tactic:
rcases y with - | ⟨_, y⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head head_1 : α
hx : [head, head_1].length = 2
head_2 head_3 head_4 : α
y : List α
hy : (head_2 :: head_3 :: head_4 :: y).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: head_3 :: head_4 :: y) hy)
cons : False
⊢ Rel α (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx))
    (fromVector (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: head_3 :: head_4 :: y) hy))

Tactic:
exfalso
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head head_1 : α
hx : [head, head_1].length = 2
head_2 head_3 head_4 : α
y : List α
hy : (head_2 :: head_3 :: head_4 :: y).length = 2
h :
  (Vector.Perm.isSetoid α 2 : List.Vector α 2 → List.Vector α 2 → Prop)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx)
    (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head_2 :: head_3 :: head_4 :: y) hy)
⊢ False

Tactic:
simp at hy