awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
⊢ Eq.{u_3 + 1} (α := γ) ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₁ a₂ b₁ b₂)
    ((fun (a₁ a₂ : α) (b₁ b₂ : β) ↦ F s(a₁, a₂) s(b₁, b₂)) a₂ a₁ b₁ b₂)

Tactic:
exacts [congr_arg₂ F eq_swap rfl, congr_arg₂ F rfl eq_swap]

Premises used: Sym2.eq_swap, rfl, congr_arg₂
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f :
  { f : α → α → β → β → γ // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }
a₁ a₂ : α
b₁ b₂ : β
⊢ (lift₂ :
        (a :
            { f : α → α → β → β → γ //
              ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 β → γ)
      f s(a₁, a₂) s(b₁, b₂) =
    (↑f : α → α → β → β → γ) a₁ a₂ b₁ b₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : Sym2 α → Sym2 β → γ
a₁ a₂ : α
b₁ b₂ : β
⊢ (↑((Equiv.symm lift₂ :
              (a : Sym2 α → Sym2 β → γ) →
                { f : α → α → β → β → γ //
                  ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ })
            F) :
        α → α → β → β → γ)
      a₁ a₂ b₁ b₂ =
    F s(a₁, a₂) s(b₁, b₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a : α × α
_ : ∀ ⦃b : α × α⦄, Rel α a b → Rel β (Prod.map f f a) (Prod.map f f b)
⊢ ∀ ⦃b : α × α⦄, Rel α a b → Rel β (Prod.map f f a) (Prod.map f f b)

Tactic:
_
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a b : α × α
h : Rel α a b
refl : ∀ (x y : α), Rel β (Prod.map f f (x, y)) (Prod.map f f (x, y))
swap : ∀ (x y : α), Rel β (Prod.map f f (x, y)) (Prod.map f f (y, x))
⊢ Rel β (Prod.map f f a) (Prod.map f f b)

Tactic:
cases h
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x y : α
⊢ Rel β (Prod.map f f (x, y)) (Prod.map f f (x, y))

Tactic:
constructor
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x y : α
⊢ Rel β (Prod.map f f (x, y)) (Prod.map f f (y, x))

Tactic:
constructor
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
h : ∀ (x : Sym2 α) (x y : α), map id (Quot.mk (Rel α) (x, y)) = id (Quot.mk (Rel α) (x, y))
⊢ Eq.{u_1 + 1} (α := Sym2 α → Sym2 α) (map id) id

Tactic:
ext ⟨⟨x, y⟩⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x_1 : Sym2 α
x y : α
⊢ map id (Quot.mk (Rel α) (x, y)) = id (Quot.mk (Rel α) (x, y))

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
h : ∀ (x : Sym2 α) (x y : α), map (g ∘ f) (Quot.mk (Rel α) (x, y)) = (map g ∘ map f) (Quot.mk (Rel α) (x, y))
⊢ map (g ∘ f) = map g ∘ map f

Tactic:
ext ⟨⟨x, y⟩⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x_1 : Sym2 α
x y : α
⊢ map (g ∘ f) (Quot.mk (Rel α) (x, y)) = (map g ∘ map f) (Quot.mk (Rel α) (x, y))

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x : Sym2 α
h : ∀ (x y : α), map g (map f s(x, y)) = map (g ∘ f) s(x, y)
⊢ map g (map f x) = map (g ∘ f) x

Tactic:
induction x
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x y : α
⊢ map g (map f s(x, y)) = map (g ∘ f) s(x, y)

Tactic:
aesop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f : α → β
a b : α
⊢ map f s(a, b) = s(f a, f b)

Tactic:
rfl

Premises used: Sym2.map, Prod.map, Quot.map, rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f : α → β
hinj : Injective f
z z' : Sym2 α
⊢ map f z = map f z' → z = z'

Tactic:
Sym2.inductionOn₂ z z' (fun x y x' y' => ?_)

Premises used: Sym2.inductionOn₂
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f : α → β
hinj : Injective f
z z' : Sym2 α
refine : ∀ (x y x' y' : α), map f s(x, y) = map f s(x', y') → s(x, y) = s(x', y')
⊢ map f z = map f z' → z = z'

Tactic:
refine Sym2.inductionOn₂ z z' (fun x y x' y' => ?_)
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f : α → β
hinj : Injective f
z z' : Sym2 α
x y x' y' : α
⊢ map f s(x, y) = map f s(x', y') → s(x, y) = s(x', y')

Tactic:
simp [hinj.eq_iff]

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a b₁_1 b₁ : α
h : Eq.{u_1 + 1} (α := Sym2 α) ((fun (b : α) ↦ s(a, b)) b₁_1) ((fun (b : α) ↦ s(a, b)) b₁)
⊢ b₁_1 = b₁ ∨ a = b₁ ∧ b₁_1 = a

Tactic:
simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, true_and, Prod.swap_prod_mk] at h

Premises used: Sym2.eq, Prod.swap_prod_mk, Sym2.rel_iff', Prod.mk.injEq, true_and
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a b₁_1 b₁ : α
h : b₁_1 = b₁ ∨ a = b₁ ∧ b₁_1 = a
inl inr : b₁_1 = b₁_1
⊢ b₁_1 = b₁

Tactic:
obtain rfl | ⟨rfl, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a b₁ : α
⊢ b₁ = b₁

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
b₁ : α
⊢ b₁ = b₁

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ → α
f : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
⊢ Eq (α := Sym2 γ → β) ((lift : (a : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → β) f ∘ map g)
    ((lift : (a : { f : γ → γ → β // ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁ }) → Sym2 γ → β)
      (Subtype.mk (p := fun (f : γ → γ → β) ↦ ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁)
        (fun (c₁ c₂ : γ) ↦ (↑f : α → α → β) (g c₁) (g c₂)) ⋯))

Tactic:
lift.symm_apply_eq.mp rfl

Premises used: Sym2.lift, Equiv.symm_apply_eq, Iff.mp, rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ → α
f : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
p : Sym2 γ
rw : ((lift : (a : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → β) f (map g p) : β)
| ((lift : (a : { f : γ → γ → β // ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁ }) → Sym2 γ → β)
      (Subtype.mk (p := fun (f : γ → γ → β) ↦ ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁)
        (fun (c₁ c₂ : γ) ↦ (↑f : α → α → β) (g c₁) (g c₂)) ⋯)
      p :
    β)

Tactic:
rw [← lift_comp_map, comp_apply]

Premises used: Sym2.lift_comp_map, Function.comp_apply
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ → α
f : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
p : Sym2 γ
conv_rhs :
  Eq.{u_2 + 1} (α := β)
    ((lift : (a : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → β) f (map g p) : β)
    ((lift : (a : { f : γ → γ → β // ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁ }) → Sym2 γ → β)
        (Subtype.mk (p := fun (f : γ → γ → β) ↦ ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁)
          (fun (c₁ c₂ : γ) ↦ (↑f : α → α → β) (g c₁) (g c₂)) ⋯)
        p :
      β)
conv_rhs₁ :
  Eq.{u_2 + 1} (α := β)
    ((lift : (a : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → β) f (map g p) : β)
    ((lift : (a : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → β) f (map g p) : β)
⊢ Eq.{u_2 + 1} (α := β)
    ((lift : (a : { f : α → α → β // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) → Sym2 α → β) f (map g p) : β)
    ((lift : (a : { f : γ → γ → β // ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁ }) → Sym2 γ → β)
        (Subtype.mk (p := fun (f : γ → γ → β) ↦ ∀ (a₁ a₂ : γ), f a₁ a₂ = f a₂ a₁)
          (fun (c₁ c₂ : γ) ↦ (↑f : α → α → β) (g c₁) (g c₂)) ⋯)
        p :
      β)

Tactic:
conv_rhs => rw [← lift_comp_map, comp_apply]

Premises used: Sym2.lift_comp_map, Function.comp_apply
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a b c w : α
h : s(b, c) = s(a, w)
⊢ b = a ∧ c = w ∨ b = w ∧ c = a

Tactic:
rw [eq_iff] at h

Premises used: Sym2.eq_iff
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a b c w : α
h : b = a ∧ c = w ∨ b = w ∧ c = a
⊢ a = b ∨ a = c

Tactic:
aesop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a c : α
⊢ Sym2.Mem a s(a, c)

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, Sym2.Mem, rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a c : α
⊢ Sym2.Mem a s(a, c)

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a b : α
inr : Sym2.Mem a s(a, b)
⊢ Sym2.Mem a s(b, a)

Tactic:
rw [eq_swap]

Premises used: Sym2.eq_swap
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a b : α
⊢ Sym2.Mem a s(a, b)

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, Sym2.Mem, rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a b : α
⊢ Sym2.Mem a s(a, b)

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h :
  Eq.{u_1 + 1} (α := Set α) ((fun (z : Sym2 α) ↦ ({x : α | Sym2.Mem x z} : Set α)) z)
    ((fun (z : Sym2 α) ↦ ({x : α | Sym2.Mem x z} : Set α)) z')
⊢ ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'

Tactic:
simp only [Set.ext_iff, Set.mem_setOf_eq] at h

Premises used: Set.mem_setOf_eq, Set.ext_iff
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
mk : ∀ (x y : α) (h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 z'), Quot.mk (Rel α) (x, y) = z'
⊢ z = z'

Tactic:
obtain ⟨x, y⟩ := z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 z'
mk :
  ∀ (x' y' : α) (h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))),
    Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
⊢ Quot.mk (Rel α) (x, y) = z'

Tactic:
obtain ⟨x', y'⟩ := z'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
⊢ Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))

Tactic:
have hx := h x
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
⊢ Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))

Tactic:
have hy := h y
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
⊢ Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))

Tactic:
have hx' := h x'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
⊢ Sym2.Mem y' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y' (Quot.mk (Rel α) (x', y'))

Tactic:
have hy' := h y'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
hy' : Sym2.Mem y' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y' (Quot.mk (Rel α) (x', y'))
⊢ True ∨ x = y ↔ x = x' ∨ x = y'

Tactic:
simp only [mem_iff'] at hx hy hx' hy'

Premises used: Sym2.mem_iff'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
hy' : Sym2.Mem y' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y' (Quot.mk (Rel α) (x', y'))
hx₁ : True ∨ x = y ↔ x = x' ∨ x = y'
⊢ y = x ∨ True ↔ y = x' ∨ y = y'

Tactic:
simp only [mem_iff'] at hx hy hx' hy'

Premises used: Sym2.mem_iff'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
hy' : Sym2.Mem y' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y' (Quot.mk (Rel α) (x', y'))
hx₁ : True ∨ x = y ↔ x = x' ∨ x = y'
hy₁ : y = x ∨ True ↔ y = x' ∨ y = y'
⊢ x' = x ∨ x' = y ↔ True ∨ x' = y'

Tactic:
simp only [mem_iff'] at hx hy hx' hy'

Premises used: Sym2.mem_iff'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
hy' : Sym2.Mem y' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y' (Quot.mk (Rel α) (x', y'))
hx₁ : True ∨ x = y ↔ x = x' ∨ x = y'
hy₁ : y = x ∨ True ↔ y = x' ∨ y = y'
hx'₁ : x' = x ∨ x' = y ↔ True ∨ x' = y'
⊢ y' = x ∨ y' = y ↔ y' = x' ∨ True

Tactic:
simp only [mem_iff'] at hx hy hx' hy'

Premises used: Sym2.mem_iff'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : True ∨ x = y ↔ x = x' ∨ x = y'
hy : y = x ∨ True ↔ y = x' ∨ y = y'
hx' : x' = x ∨ x' = y ↔ True ∨ x' = y'
hy' : y' = x ∨ y' = y ↔ y' = x' ∨ True
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')

Tactic:
aesop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x : α
z : Sym2 α
⊢ Sym2.Mem x z ↔ x ∈ z

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Sym2.Mem
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x : α
z : Sym2 α
⊢ x ∈ z ↔ ∃ (y : α), z = s(x, y)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Sym2.Mem
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
p q : Sym2 α
h : ∀ (x : α), x ∈ p ↔ x ∈ q
⊢ p = q

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y : α
⊢ x ∈ s(x, y)

Tactic:
⟨y, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Sym2.Mem, rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y : α
⊢ y ∈ s(x, y)

Tactic:
eq_swap ▸ mem_mk_left y x

Premises used: Eq.rec, Sym2.mem_mk_left, Sym2.eq_swap
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a b c : α
⊢ a ∈ s(b, c) ↔ a = b ∨ a = c

Tactic:
mem_iff'

Premises used: Set.Mem, setOf, Sym2.Mem, Sym2.mem_iff'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
e : Sym2 α
rw : e = Quot.mk (Rel α) ((Quot.out (r := Rel α) e).1, (Quot.out (r := Rel α) e).2)
rw₁ rw₂ : e = e
⊢ e = s((Quot.out (r := Rel α) e).1, (Quot.out (r := Rel α) e).2)

Tactic:
rw [Sym2.mk, e.out_eq]

Premises used: Sym2.mk, Quot.out_eq
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
e : Sym2 α
rw : e = s((Quot.out (r := Rel α) e).1, (Quot.out (r := Rel α) e).2)
rw₁ : e = Quot.mk (Rel α) ((Quot.out (r := Rel α) e).1, (Quot.out (r := Rel α) e).2)
rw₂ rw₃ : e = e
⊢ e = s((Quot.out (r := Rel α) e).2, (Quot.out (r := Rel α) e).1)

Tactic:
rw [eq_swap, Sym2.mk, e.out_eq]

Premises used: Sym2.mk, Quot.out_eq, Sym2.eq_swap
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
p : α → Prop
a b : α
⊢ (∀ c ∈ s(a, b), p c) ↔ p a ∧ p b

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y : α
h : ∀ (z : α), z ∈ (↑s(x, y) : Set α) ↔ Membership.mem (γ := Set α) {x, y} z
⊢ (↑s(x, y) : Set α) = {x, y}

Tactic:
ext z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y z : α
⊢ z ∈ (↑s(x, y) : Set α) ↔ Membership.mem (γ := Set α) {x, y} z

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f : α → β
z : Sym2 α
h : ∀ (x y : α), (↑(map f s(x, y)) : Set β) = f '' (↑s(x, y) : Set α)
⊢ (↑(map f z) : Set β) = f '' (↑z : Set α)

Tactic:
cases z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f : α → β
x y : α
⊢ (↑(map f s(x, y)) : Set β) = f '' (↑s(x, y) : Set α)

Tactic:
simp [Set.image_pair]

Premises used: Set.image_pair
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
⊢ s(a, Mem.other h) = z

Tactic:
(Classical.choose_spec h).symm

Premises used: Sym2.Mem.other, Classical.choose_spec, Eq.symm
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ s(a, Mem.other h)

Tactic:
mem_mk_right a <| Mem.other h

Premises used: Sym2.mem_mk_right, Sym2.Mem.other
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
h₁ : z = s(a, Mem.other h)
⊢ Mem.other h ∈ z

Tactic:
convert! mem_mk_right a <| Mem.other h

Premises used: Sym2.mem_mk_right, Sym2.Mem.other
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
h₁ h₂ : z = z
⊢ z = s(a, Mem.other h)

Tactic:
rw [other_spec h]

Premises used: Sym2.other_spec
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
mp : x ∈ z ∧ y ∈ z → z = s(x, y)
mpr : z = s(x, y) → x ∈ z ∧ y ∈ z
⊢ x ∈ z ∧ y ∈ z ↔ z = s(x, y)

Tactic:
constructor
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
mp : ∀ (x_1 y_1 : α), x ∈ s(x_1, y_1) ∧ y ∈ s(x_1, y_1) → s(x_1, y_1) = s(x, y)
⊢ x ∈ z ∧ y ∈ z → z = s(x, y)

Tactic:
cases z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y : α
hne : x ≠ y
x_1 y_1 : α
mp : (x = x_1 ∨ x = y_1) ∧ (y = x_1 ∨ y = y_1) → s(x_1, y_1) = s(x, y)
⊢ x ∈ s(x_1, y_1) ∧ y ∈ s(x_1, y_1) → s(x_1, y_1) = s(x, y)

Tactic:
rw [mem_iff, mem_iff]

Premises used: Sym2.mem_iff
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y : α
hne : x ≠ y
x_1 y_1 : α
⊢ (x = x_1 ∨ x = y_1) ∧ (y = x_1 ∨ y = y_1) → s(x_1, y_1) = s(x, y)

Tactic:
aesop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y : α
hne : x ≠ y
⊢ x ∈ s(x, y) ∧ y ∈ s(x, y)

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y : α
z z' : Sym2 α
h : x ≠ y
h1 : x ∈ z
h2 : y ∈ z
h3 : x ∈ z'
h4 : y ∈ z'
⊢ z = z'

Tactic:
((mem_and_mem_iff h).mp ⟨h1, h2⟩).trans ((mem_and_mem_iff h).mp ⟨h3, h4⟩).symm

Premises used: Sym2.mem_and_mem_iff, And.intro, Iff.mp, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
z : Sym2 α
h : ∀ (x y : α), b ∈ map f s(x, y) ↔ ∃ a ∈ s(x, y), f a = b
⊢ b ∈ map f z ↔ ∃ a ∈ z, f a = b

Tactic:
cases z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
x y : α
⊢ b ∈ map f s(x, y) ↔ ∃ a ∈ s(x, y), f a = b

Tactic:
aesop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
h₁ : ∀ (y : β), y ∈ map f s ↔ y ∈ map g s
⊢ map f s = map g s

Tactic:
ext y
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
h₁ : (∃ a ∈ s, f a = y) ↔ ∃ a ∈ s, g a = y
⊢ y ∈ map f s ↔ y ∈ map g s

Tactic:
simp only [mem_map]

Premises used: Sym2.mem_map
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
h₁ : (∃ a ∈ s, f a = y) → ∃ a ∈ s, g a = y
h₂ : (∃ a ∈ s, g a = y) → ∃ a ∈ s, f a = y
⊢ (∃ a ∈ s, f a = y) ↔ ∃ a ∈ s, g a = y

Tactic:
constructor
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
w : α
hw : w ∈ s
⊢ g w = f w

Tactic:
simp [hw, h]
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
w : α
hw : w ∈ s
⊢ ∃ a ∈ s, g a = f w

Tactic:
exact ⟨w, hw, by simp [hw, h]⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
w : α
hw : w ∈ s
⊢ f w = g w

Tactic:
simp [hw, h]
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
w : α
hw : w ∈ s
⊢ ∃ a ∈ s, f a = g w

Tactic:
exact ⟨w, hw, by simp [hw, h]⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Sym2 α → Sym2 α) (map fun (x : α) ↦ x) id

Tactic:
map_id

Premises used: Sym2.map_id
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (H : ∀ a ∈ s(p.1, p.2), P a) → Sym2 β :=
  fun (p : α × α) (H : ∀ a ∈ s(p.1, p.2), P a) ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq : Rel α p q
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
rw :
  ∀ (hpq_1 : p = q ∨ p = q.swap) (Hq : ∀ a ∈ Quot.mk (Rel α) q, P a),
    Eq.ndrec (motive := fun (x : Sym2 α) ↦ (∀ a ∈ x, P a) → Sym2 β) (g p) ⋯ Hq = g q Hq
⊢ Eq.ndrec (motive := fun (x : Sym2 α) ↦ (∀ a ∈ x, P a) → Sym2 β) (g p) ⋯ Hq = g q Hq

Tactic:
rw [rel_iff'] at hpq

Premises used: Sym2.rel_iff'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (H : ∀ a ∈ s(p.1, p.2), P a) → Sym2 β :=
  fun (p : α × α) (H : ∀ a ∈ s(p.1, p.2), P a) ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq_1 : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
⊢ ∀ a ∈ s(p.1, p.2), P a

Tactic:
have Hp : ∀ a ∈ s(p.1, p.2), P a := fun a hmem =>
      Hq a (Sym2.mk_eq_mk_iff.2 hpq ▸ hmem : a ∈ s(q.1, q.2))
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (H : ∀ a ∈ s(p.1, p.2), P a) → Sym2 β :=
  fun (p : α × α) (H : ∀ a ∈ s(p.1, p.2), P a) ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq_1 : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp H : ∀ a ∈ s(p.1, p.2), P a
⊢ Eq.ndrec (motive := fun (s : Sym2 α) ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) ⋯ H = g p Hp

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (H : ∀ a ∈ s(p.1, p.2), P a) → Sym2 β :=
  fun (p : α × α) (H : ∀ a ∈ s(p.1, p.2), P a) ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq_1 : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
⊢ ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun (s : Sym2 α) ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp

Tactic:
have h : ∀ {s₂ e H}, Eq.ndrec (motive := fun s => (∀ a ∈ s, P a) → Sym2 β) (g p) (b := s₂) e H =
      g p Hp := by
      rintro s₂ rfl _
      rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (H : ∀ a ∈ s(p.1, p.2), P a) → Sym2 β :=
  fun (p : α × α) (H : ∀ a ∈ s(p.1, p.2), P a) ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq_1 : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun (s : Sym2 α) ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
⊢ Eq.ndrec (motive := fun (x : Sym2 α) ↦ (∀ a ∈ x, P a) → Sym2 β) (g p) ⋯ Hq = g q Hq

Tactic:
h.trans (Quot.sound ?_)

Premises used: Quot.sound, Eq.trans