awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
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)
⊢ 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))
have 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))
Tactic: rcases y with - | ⟨_, y⟩
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
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))
⊢ 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))
have 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))
Tactic: rcases y with - | ⟨_, y⟩
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
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)
⊢ 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))
have cons : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
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 : α
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))
have cons : ∀ (hy : [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) [head, head_1] 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, head_1] hy))
Tactic: rcases perm_card_two_iff.mp h with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
Cleared hypotheses: head_2, head_3, hy, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
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 : α
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)
cons :
  ∀ (hy : [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) [head, head_1] 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, head_1] 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))
have cons₁ : ∀ (hy : [head_1, 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, head_1] hx)
      (Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head_1, head] 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_1, head] hy))
Tactic: rcases perm_card_two_iff.mp h with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
Cleared hypotheses: head_2, head_3, hy, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
⊢ LeftInverse.{u_1 + 1, u_1 + 1} (α := Sym2 α)
    (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α) fromVector
      ⋯)
    (Quot.map (ra := Rel α) (rb := (⇑(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] ⋯) ⋯)
have h : ∀ (x y : α),
  Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α) fromVector sorry
      (Quot.map (ra := Rel α) (rb := (⇑(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] sorry) sorry s(x, y)) =
    s(x, y)
Tactic: apply Sym2.ind
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
⊢ Quot.map (ra := Rel α) (rb := (⇑(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] ⋯) ⋯
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector ⋯ x) =
    x
have refine : ∀ (x : List.Vector α 2),
  Quot.map (ra := Rel α) (rb := (⇑(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] sorry) sorry
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector sorry ⟦x⟧) =
    ⟦x⟧
Tactic: refine x.recOnSubsingleton fun x => ?_
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x_1 : Sym' α 2
x : List.Vector α 2
⊢ Quot.map (ra := Rel α) (rb := (⇑(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] ⋯) ⋯
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector ⋯ ⟦x⟧) =
    ⟦x⟧
have obtain : ∀ (x : List α) (hx : x.length = 2),
  Quot.map (ra := Rel α) (rb := (⇑(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] sorry) sorry
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector sorry ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) x hx⟧) =
    ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) x hx⟧
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x_1 : Sym' α 2
x : List α
hx : x.length = 2
⊢ Quot.map (ra := Rel α) (rb := (⇑(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] ⋯) ⋯
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector ⋯ ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) x hx⟧) =
    ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) x hx⟧
have nil : ∀ (hx : List.length.{u_1} (α := α) [] = 2),
  Quot.map (ra := Rel α) (rb := (⇑(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] sorry) sorry
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector sorry ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hx⟧) =
    ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hx⟧
Tactic: obtain - | ⟨-, x⟩ := x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x_1 : Sym' α 2
x : List α
hx : x.length = 2
nil :
  ∀ (hx : List.length.{u_1} (α := α) [] = 2),
    Quot.map (ra := Rel α) (rb := (⇑(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] ⋯) ⋯
        (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
          fromVector ⋯ ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hx⟧) =
      ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [] hx⟧
⊢ Quot.map (ra := Rel α) (rb := (⇑(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] ⋯) ⋯
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector ⋯ ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) x hx⟧) =
    ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) x hx⟧
have cons : ∀ (head : α) (x : List α) (hx : (head :: x).length = 2),
  Quot.map (ra := Rel α) (rb := (⇑(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] sorry) sorry
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector sorry ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx⟧) =
    ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx⟧
Tactic: obtain - | ⟨-, x⟩ := x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x_1 : Sym' α 2
head : α
x : List α
hx : (head :: x).length = 2
⊢ Quot.map (ra := Rel α) (rb := (⇑(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] ⋯) ⋯
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector ⋯ ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx⟧) =
    ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx⟧
have cons : ∀ (hx : [head].length = 2),
  Quot.map (ra := Rel α) (rb := (⇑(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] sorry) sorry
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector sorry ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head] hx⟧) =
    ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head] hx⟧
Tactic: rcases x with - | ⟨_, x⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x_1 : Sym' α 2
head : α
x : List α
hx : (head :: x).length = 2
cons :
  ∀ (hx : [head].length = 2),
    Quot.map (ra := Rel α) (rb := (⇑(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] ⋯) ⋯
        (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
          fromVector ⋯ ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head] hx⟧) =
      ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head] hx⟧
⊢ Quot.map (ra := Rel α) (rb := (⇑(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] ⋯) ⋯
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector ⋯ ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx⟧) =
    ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: x) hx⟧
have cons₁ : ∀ (head_1 : α) (x : List α) (hx : (head :: head_1 :: x).length = 2),
  Quot.map (ra := Rel α) (rb := (⇑(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] sorry) sorry
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector sorry ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx⟧) =
    ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx⟧
Tactic: rcases x with - | ⟨_, x⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x_1 : Sym' α 2
head head_1 : α
x : List α
hx : (head :: head_1 :: x).length = 2
⊢ Quot.map (ra := Rel α) (rb := (⇑(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] ⋯) ⋯
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector ⋯ ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx⟧) =
    ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx⟧
have cons : ∀ (hx : [head, head_1].length = 2),
  Quot.map (ra := Rel α) (rb := (⇑(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] sorry) sorry
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector sorry ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx⟧) =
    ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx⟧
Tactic: rcases x with - | ⟨_, x⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x_1 : Sym' α 2
head head_1 : α
x : List α
hx : (head :: head_1 :: x).length = 2
cons :
  ∀ (hx : [head, head_1].length = 2),
    Quot.map (ra := Rel α) (rb := (⇑(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] ⋯) ⋯
        (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
          fromVector ⋯ ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx⟧) =
      ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) [head, head_1] hx⟧
⊢ Quot.map (ra := Rel α) (rb := (⇑(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] ⋯) ⋯
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector ⋯ ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx⟧) =
    ⟦Subtype.mk (p := fun (l : List α) ↦ l.length = 2) (head :: head_1 :: x) hx⟧
have cons₁ : ∀ (head_2 : α) (x : List α) (hx : (head :: head_1 :: head_2 :: x).length = 2),
  Quot.map (ra := Rel α) (rb := (⇑(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] sorry) sorry
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector sorry ⟦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) (head :: head_1 :: head_2 :: x) hx⟧
Tactic: rcases x with - | ⟨_, x⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x_1 : Sym' α 2
head head_1 head_2 : α
x : List α
hx : (head :: head_1 :: head_2 :: x).length = 2
⊢ Quot.map (ra := Rel α) (rb := (⇑(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] ⋯) ⋯
      (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
        fromVector ⋯ ⟦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) (head :: head_1 :: head_2 :: x) hx⟧
have cons : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst : DecidableEq α
a b c d e : α
h : Rel α (b, c) (d, e)
⊢ Eq (α := a ∈ s(d, e) → α)
    (Eq.ndrec (motive := fun (x : Sym2 α) ↦ a ∈ x → α) (fun (x : a ∈ s(b, c)) ↦ if a = b then c else b) ⋯ :
      a ∈ s(d, e) → α)
    fun (x : a ∈ s(d, e)) ↦ if a = d then e else d
have h₁ : ∀ (hy : a ∈ s(d, e)),
  Eq.ndrec (motive := fun (x : Sym2 α) ↦ a ∈ x → α) (fun (x : a ∈ s(b, c)) ↦ if a = b then c else b) sorry hy =
    if a = d then e else d
Tactic: ext hy
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f_1 : α → β
inst : DecidableEq α
a b c d e : α
h_1 : Rel α (b, c) (d, e)
hy : a ∈ s(d, e)
f : Sym2 α
g : s(b, c) = f
h : a ∈ f
⊢ Eq.ndrec (motive := fun (x : Sym2 α) ↦ a ∈ x → α) (fun (x : a ∈ s(b, c)) ↦ if a = b then c else b) g h =
    if a = b then c else b
have subst : ∀ {h : a ∈ s(b, c)},
  Eq.ndrec (motive := fun (x : Sym2 α) ↦ a ∈ x → α) (fun (x : a ∈ s(b, c)) ↦ if a = b then c else b) sorry h =
    if a = b then c else b
Tactic: subst g
Cleared hypotheses: f, g, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst : DecidableEq α
a b c d e : α
h : Rel α (b, c) (d, e)
hy : a ∈ s(d, e)
⊢ Eq.ndrec (motive := fun (x : Sym2 α) ↦ a ∈ x → α) (fun (x : a ∈ s(b, c)) ↦ if a = b then c else b) ⋯ hy =
    if a = d then e else d
have this : ∀ {f : Sym2 α} {g : s(b, c) = f} {h : a ∈ f},
  Eq.ndrec (motive := fun (x : Sym2 α) ↦ a ∈ x → α) (fun (x : a ∈ s(b, c)) ↦ if a = b then c else b) g h =
    if a = b then c else b
Tactic: have {f g h} : @Eq.ndrec (Sym2 α) s(b, c)
      (fun x => a ∈ x → α) (fun _ => if a = b then c else b) f g h =
        if a = b then c else b := by subst g; rfl
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ s(a, Mem.other' h) = z
have h₁ : ∀ (x y : α) (h : a ∈ s(x, y)), s(a, Mem.other' h) = s(x, y)
Tactic: induction z
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h = Mem.other' h
have rw : s(a, Mem.other h) = s(a, Mem.other' h)
Tactic: rw [← congr_right, other_spec' h, other_spec]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
rw : s(a, Mem.other h) = s(a, Mem.other' h)
rw₁ : α
⊢ Mem.other h = Mem.other' h
have rw₂ : s(a, Mem.other h) = z
Tactic: rw [← congr_right, other_spec' h, other_spec]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
rw : s(a, Mem.other h) = s(a, Mem.other' h)
rw₁ : α
rw₂ : s(a, Mem.other h) = z
⊢ Mem.other h = Mem.other' h
have rw₃ : z = z
Tactic: rw [← congr_right, other_spec' h, other_spec]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other' h ∈ z
have rw : Mem.other h ∈ z
Tactic: rw [← other_eq_other']
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb = a
have h : ∀ (x y : α) (ha : a ∈ s(x, y)) (hb : Mem.other' ha ∈ s(x, y)), Mem.other' hb = a
Tactic: induction z
Cleared hypotheses: z, ha, hb
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
⊢ Mem.other hb = a
have rw : ∀ (hb_1 : Mem.other' ha ∈ z), Mem.other' hb = a
Tactic: rw [other_eq_other'] at hb ⊢
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb_1 : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb_1 = a
have h : Mem.other ha = Mem.other' ha
Tactic: convert! other_invol' ha hb using 2
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
⊢ Mem.other hb = a
have rw : ∀ (hb_1 : Mem.other' ha ∈ z), Mem.other' hb = a
Tactic: classical
    rw [other_eq_other'] at hb ⊢
    convert! other_invol' ha hb using 2
    apply other_eq_other'
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
rw rw₁ rw₂ : ∀ (hb_1 : Mem.other' ha ∈ z), Mem.other' hb = a
⊢ Mem.other hb = a
have h : ∀ (hb : Mem.other' ha ∈ z), Mem.other ha = Mem.other' ha
Tactic: classical
    rw [other_eq_other'] at hb ⊢
    convert! other_invol' ha hb using 2
    apply other_eq_other'