awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
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))
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))
⊢ 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 perm_card_two_iff.mp h with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)

Premises used: _private.0.Sym2.perm_card_two_iff, Iff.mp, rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head head_1 : α
hx 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:
constructor
-- 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 : [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:
apply Sym2.Rel.swap

Premises used: Sym2.Rel.swap
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
h :
  ∀ (x y : α),
    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] ⋯) ⋯ s(x, y)) =
      s(x, y)
⊢ 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] ⋯) ⋯)

Tactic:
apply Sym2.ind
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
⊢ ∀ (x y : α),
    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] ⋯) ⋯ s(x, y)) =
      s(x, y)

Tactic:
aesop (add norm unfold [Sym2.fromVector])

Premises used: _private.0.Sym2.fromVector
-- Module: Mathlib.Data.Sym.Sym2
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

Tactic:
x.recOnSubsingleton fun x => ?_

Premises used: Quotient.recOnSubsingleton
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
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] ⋯) ⋯
        (Quot.map (ra := (⇑(Vector.Perm.isSetoid α 2) : List.Vector α 2 → List.Vector α 2 → Prop)) (rb := Rel α)
          fromVector ⋯ ⟦x⟧) =
      ⟦x⟧
⊢ 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

Tactic:
refine x.recOnSubsingleton fun x => ?_
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x_1 : Sym' α 2
x : List.Vector α 2
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] ⋯) ⋯
        (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⟧
⊢ 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⟧

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.Data.Sym.Sym2
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⟧
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] ⋯) ⋯
        (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⟧
⊢ 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⟧

Tactic:
obtain - | ⟨-, x⟩ := x
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
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⟧

Tactic:
simp at hx
-- Module: Mathlib.Data.Sym.Sym2
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⟧
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] ⋯) ⋯
        (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⟧
⊢ 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⟧

Tactic:
rcases x with - | ⟨_, x⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
head : α
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⟧

Tactic:
simp at hx
-- Module: Mathlib.Data.Sym.Sym2
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⟧
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] ⋯) ⋯
        (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⟧
⊢ 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⟧

Tactic:
rcases x with - | ⟨_, x⟩
-- Module: Mathlib.Data.Sym.Sym2
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
cons : False
⊢ 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⟧

Tactic:
exfalso
-- Module: Mathlib.Data.Sym.Sym2
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
⊢ False

Tactic:
simp at hx
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
head head_1 : α
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⟧

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Sym2
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)
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) ⋯ hy =
      if a = d then e else d
⊢ 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

Tactic:
ext hy
-- Module: Mathlib.Data.Sym.Sym2
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
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) ⋯ h =
      if a = b then c else b
⊢ 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:
subst g
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst : DecidableEq α
a b c d e : α
h_1 : Rel α (b, c) (d, e)
hy : a ∈ s(d, e)
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) ⋯ h =
    if a = b then c else b

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Sym2
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)
⊢ ∀ {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
-- Module: Mathlib.Data.Sym.Sym2
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)
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
⊢ 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

Tactic:
aesop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
h₁ : ∀ (x y : α) (h : a ∈ s(x, y)), s(a, Mem.other' h) = s(x, y)
⊢ s(a, Mem.other' h) = z

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

Tactic:
aesop (add norm unfold [Sym2.rec, Quot.rec]) (rule_sets := [Sym2])

Premises used: Sym2
-- Module: Mathlib.Data.Sym.Sym2
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
rw₃ rw₄ : z = z
⊢ Mem.other h = Mem.other' h

Tactic:
rw [← congr_right, other_spec' h, other_spec]

Premises used: Sym2.other_spec, Sym2.other_spec', Sym2.congr_right
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
rw : Mem.other h ∈ z
⊢ Mem.other' h ∈ z

Tactic:
rw [← other_eq_other']

Premises used: Sym2.other_eq_other'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z

Tactic:
other_mem h

Premises used: Sym2.other_mem
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z

Tactic:
exact other_mem h

Premises used: Sym2.other_mem
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other' ha ∈ z
h : ∀ (x y : α) (ha : a ∈ s(x, y)) (hb : Mem.other' ha ∈ s(x, y)), Mem.other' hb = a
⊢ Mem.other' hb = a

Tactic:
induction z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
a x y : α
ha : a ∈ s(x, y)
hb : Mem.other' ha ∈ s(x, y)
⊢ Mem.other' hb = a

Tactic:
aesop (rule_sets := [Sym2]) (add norm unfold [Sym2.rec, Quot.rec])

Premises used: Sym2
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
rw : ∀ (hb_1 : Mem.other' ha ∈ z), Mem.other' hb = a
⊢ Mem.other hb = a

Tactic:
rw [other_eq_other'] at hb ⊢

Premises used: Sym2.other_eq_other'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb_1 : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb = a

Tactic:
other_invol' ha hb

Premises used: Sym2.other_invol'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb_1 : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
h : Mem.other ha = Mem.other' ha
⊢ Mem.other' hb_1 = a

Tactic:
convert! other_invol' ha hb using 2

Premises used: Sym2.other_invol'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb_1 : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other ha = Mem.other' ha

Tactic:
apply other_eq_other'

Premises used: Sym2.other_eq_other'
-- Module: Mathlib.Data.Sym.Sym2
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
h : ∀ (hb : Mem.other' ha ∈ z), Mem.other ha = Mem.other' ha
⊢ Mem.other hb = a

Tactic:
classical
    rw [other_eq_other'] at hb ⊢
    convert! other_invol' ha hb using 2
    apply other_eq_other'

Premises used: Sym2.other_eq_other'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ {x ∈ image (uncurry Sym2.mk) (s ×ˢ s) | x.IsDiag} = image (uncurry Sym2.mk) s.diag

Tactic:
aesop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ {x ∈ image (uncurry Sym2.mk) (s ×ˢ s) | ¬x.IsDiag} = image (uncurry Sym2.mk) s.offDiag

Tactic:
aesop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst : Subsingleton α
⊢ Subsingleton.{u_1 + 1} (Sym2 α)

Tactic:
(equivSym α).injective.subsingleton

Premises used: Function.Injective.subsingleton, Equiv.injective, Sym2.equivSym
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst : IsEmpty α
⊢ IsEmpty.{u_1 + 1} (Sym2 α)

Tactic:
(equivSym α).isEmpty

Premises used: Equiv.isEmpty, Sym2.equivSym
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst : Nontrivial α
⊢ Nontrivial.{u_1} (Sym2 α)

Tactic:
diag_injective.nontrivial

Premises used: Function.Injective.nontrivial, Sym2.diag_injective
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α_1
f_1 : α_1 → β
α : Type u_4
R : Type u_5
N : Type u_6
inst : SMul R N
f : { f : α → α → R // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g : α → α → N // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x x_1 : α
rw : ((↑f : α → α → R) x • (↑g : α → α → N) x) x_1 = ((↑f : α → α → R) • (↑g : α → α → N)) x_1 x
rw₁ : (↑f : α → α → R) x x_1 • (↑g : α → α → N) x x_1 = ((↑f : α → α → R) • (↑g : α → α → N)) x_1 x
rw₂ : (↑f : α → α → R) x x_1 • (↑g : α → α → N) x x_1 = ((↑f : α → α → R) x_1 • (↑g : α → α → N) x_1) x
rw₃ : (↑f : α → α → R) x x_1 • (↑g : α → α → N) x x_1 = (↑f : α → α → R) x_1 x • (↑g : α → α → N) x_1 x
rw₄ : (↑f : α → α → R) x_1 x • (↑g : α → α → N) x x_1 = (↑f : α → α → R) x_1 x • (↑g : α → α → N) x_1 x
rw₅ rw₆ : (↑f : α → α → R) x_1 x • (↑g : α → α → N) x_1 x = (↑f : α → α → R) x_1 x • (↑g : α → α → N) x_1 x
⊢ ((↑f : α → α → R) • (↑g : α → α → N)) x x_1 = ((↑f : α → α → R) • (↑g : α → α → N)) x_1 x

Tactic:
rw [Pi.smul_apply', Pi.smul_apply', Pi.smul_apply', Pi.smul_apply', f.prop, g.prop]

Premises used: Pi.smul_apply', Subtype.prop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_4
R : Type u_5
N : Type u_6
inst : SMul R N
f : { f : α → α → R // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g : α → α → N // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
h :
  ∀ (x : Sym2 α) (i j : α),
    HSMul.hSMul (α := Sym2 α → R) (β := Sym2 α → N)
        ((lift : (a : { f : α → α → R // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → R) f : Sym2 α → R)
        ((lift : (a : { f : α → α → N // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → N) g : Sym2 α → N)
        (Quot.mk (Rel α) (i, j)) =
      (lift : (a : { f : α → α → N // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → N)
        (Subtype.mk (p := fun (f : α → α → N) ↦ ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁) ((↑f : α → α → R) • (↑g : α → α → N))
          ⋯)
        (Quot.mk (Rel α) (i, j))
⊢ HSMul.hSMul (α := Sym2 α → R) (β := Sym2 α → N)
      ((lift : (a : { f : α → α → R // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → R) f : Sym2 α → R)
      ((lift : (a : { f : α → α → N // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → N) g : Sym2 α → N) =
    (lift : (a : { f : α → α → N // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → N)
      (Subtype.mk (p := fun (f : α → α → N) ↦ ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁) ((↑f : α → α → R) • (↑g : α → α → N)) ⋯)

Tactic:
ext ⟨i, j⟩