awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid.{max 1 u_1} (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), (s₂ : Subtype p₁ → Subtype p₁ → Prop) x y ↔ (s₁ : α → α → Prop) (↑x : α) (↑y : α)
a : { x : Quotient s₁ // p₂ x }
obtain :
  ∀ (a : Quotient s₁) (ha : p₂ a),
    Eq.{max 1 u_1}
      ((fun (a : Quotient.{max 1 u_1} s₂) ↦
          (Quotient.liftOn.{max 1 u_1, max 1 u_1} a
              (fun (a : Subtype p₁) ↦ Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑a : α)⟧ ⋯) ⋯ :
            { x : Quotient s₁ // p₂ x }))
        ((fun (a : { x : Quotient s₁ // p₂ x }) ↦
            (Quotient.hrecOn (motive := fun (x : Quotient s₁) ↦ p₂ x → Quotient.{max 1 u_1} s₂) (↑a : Quotient s₁)
                (fun (a : α) (h : p₂ ⟦a⟧) ↦ ⟦Subtype.mk (p := p₁) a ⋯⟧) ⋯ ⋯ :
              Quotient.{max 1 u_1} s₂))
          (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) a ha)))
      (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) a ha)
⊢ Eq.{max 1 u_1}
    ((fun (a : Quotient.{max 1 u_1} s₂) ↦
        (Quotient.liftOn.{max 1 u_1, max 1 u_1} a
            (fun (a : Subtype p₁) ↦ Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑a : α)⟧ ⋯) ⋯ :
          { x : Quotient s₁ // p₂ x }))
      ((fun (a : { x : Quotient s₁ // p₂ x }) ↦
          (Quotient.hrecOn (motive := fun (x : Quotient s₁) ↦ p₂ x → Quotient.{max 1 u_1} s₂) (↑a : Quotient s₁)
              (fun (a : α) (h : p₂ ⟦a⟧) ↦ ⟦Subtype.mk (p := p₁) a ⋯⟧) ⋯ ⋯ :
            Quotient.{max 1 u_1} s₂))
        a))
    a

Tactic:
obtain ⟨a, ha⟩ := a
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid.{max 1 u_1} (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), (s₂ : Subtype p₁ → Subtype p₁ → Prop) x y ↔ (s₁ : α → α → Prop) (↑x : α) (↑y : α)
a : Quotient s₁
ha : p₂ a
h₁ :
  ∀ (a : α) (ha : p₂ ⟦a⟧),
    Eq.{max 1 u_1}
      ((fun (a : Quotient.{max 1 u_1} s₂) ↦
          (Quotient.liftOn.{max 1 u_1, max 1 u_1} a
              (fun (a : Subtype p₁) ↦ Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑a : α)⟧ ⋯) ⋯ :
            { x : Quotient s₁ // p₂ x }))
        ((fun (a : { x : Quotient s₁ // p₂ x }) ↦
            (Quotient.hrecOn (motive := fun (x : Quotient s₁) ↦ p₂ x → Quotient.{max 1 u_1} s₂) (↑a : Quotient s₁)
                (fun (a : α) (h : p₂ ⟦a⟧) ↦ ⟦Subtype.mk (p := p₁) a ⋯⟧) ⋯ ⋯ :
              Quotient.{max 1 u_1} s₂))
          (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦a⟧ ha)))
      (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦a⟧ ha)
⊢ Eq.{max 1 u_1}
    ((fun (a : Quotient.{max 1 u_1} s₂) ↦
        (Quotient.liftOn.{max 1 u_1, max 1 u_1} a
            (fun (a : Subtype p₁) ↦ Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑a : α)⟧ ⋯) ⋯ :
          { x : Quotient s₁ // p₂ x }))
      ((fun (a : { x : Quotient s₁ // p₂ x }) ↦
          (Quotient.hrecOn (motive := fun (x : Quotient s₁) ↦ p₂ x → Quotient.{max 1 u_1} s₂) (↑a : Quotient s₁)
              (fun (a : α) (h : p₂ ⟦a⟧) ↦ ⟦Subtype.mk (p := p₁) a ⋯⟧) ⋯ ⋯ :
            Quotient.{max 1 u_1} s₂))
        (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) a ha)))
    (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) a ha)

Tactic:
induction a using Quotient.inductionOn
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid.{max 1 u_1} (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), (s₂ : Subtype p₁ → Subtype p₁ → Prop) x y ↔ (s₁ : α → α → Prop) (↑x : α) (↑y : α)
a : α
ha : p₂ ⟦a⟧
⊢ Eq.{max 1 u_1}
    ((fun (a : Quotient.{max 1 u_1} s₂) ↦
        (Quotient.liftOn.{max 1 u_1, max 1 u_1} a
            (fun (a : Subtype p₁) ↦ Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑a : α)⟧ ⋯) ⋯ :
          { x : Quotient s₁ // p₂ x }))
      ((fun (a : { x : Quotient s₁ // p₂ x }) ↦
          (Quotient.hrecOn (motive := fun (x : Quotient s₁) ↦ p₂ x → Quotient.{max 1 u_1} s₂) (↑a : Quotient s₁)
              (fun (a : α) (h : p₂ ⟦a⟧) ↦ ⟦Subtype.mk (p := p₁) a ⋯⟧) ⋯ ⋯ :
            Quotient.{max 1 u_1} s₂))
        (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦a⟧ ha)))
    (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦a⟧ ha)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid.{max 1 u_1} (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), (s₂ : Subtype p₁ → Subtype p₁ → Prop) x y ↔ (s₁ : α → α → Prop) (↑x : α) (↑y : α)
a : Quotient.{max 1 u_1} s₂
h₁ :
  ∀ (a : Subtype p₁),
    Eq.{max 1 u_1}
      ((fun (a : { x : Quotient s₁ // p₂ x }) ↦
          (Quotient.hrecOn (motive := fun (x : Quotient s₁) ↦ p₂ x → Quotient.{max 1 u_1} s₂) (↑a : Quotient s₁)
              (fun (a : α) (h : p₂ ⟦a⟧) ↦ ⟦Subtype.mk (p := p₁) a ⋯⟧) ⋯ ⋯ :
            Quotient.{max 1 u_1} s₂))
        ((fun (a : Quotient.{max 1 u_1} s₂) ↦
            (Quotient.liftOn.{max 1 u_1, max 1 u_1} a
                (fun (a : Subtype p₁) ↦ Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑a : α)⟧ ⋯) ⋯ :
              { x : Quotient s₁ // p₂ x }))
          ⟦a⟧))
      ⟦a⟧
⊢ Eq.{max 1 u_1}
    ((fun (a : { x : Quotient s₁ // p₂ x }) ↦
        (Quotient.hrecOn (motive := fun (x : Quotient s₁) ↦ p₂ x → Quotient.{max 1 u_1} s₂) (↑a : Quotient s₁)
            (fun (a : α) (h : p₂ ⟦a⟧) ↦ ⟦Subtype.mk (p := p₁) a ⋯⟧) ⋯ ⋯ :
          Quotient.{max 1 u_1} s₂))
      ((fun (a : Quotient.{max 1 u_1} s₂) ↦
          (Quotient.liftOn.{max 1 u_1, max 1 u_1} a
              (fun (a : Subtype p₁) ↦ Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑a : α)⟧ ⋯) ⋯ :
            { x : Quotient s₁ // p₂ x }))
        a))
    a

Tactic:
induction a using Quotient.inductionOn
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid.{max 1 u_1} (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), (s₂ : Subtype p₁ → Subtype p₁ → Prop) x y ↔ (s₁ : α → α → Prop) (↑x : α) (↑y : α)
a : Subtype p₁
⊢ Eq.{max 1 u_1}
    ((fun (a : { x : Quotient s₁ // p₂ x }) ↦
        (Quotient.hrecOn (motive := fun (x : Quotient s₁) ↦ p₂ x → Quotient.{max 1 u_1} s₂) (↑a : Quotient s₁)
            (fun (a : α) (h : p₂ ⟦a⟧) ↦ ⟦Subtype.mk (p := p₁) a ⋯⟧) ⋯ ⋯ :
          Quotient.{max 1 u_1} s₂))
      ((fun (a : Quotient.{max 1 u_1} s₂) ↦
          (Quotient.liftOn.{max 1 u_1, max 1 u_1} a
              (fun (a : Subtype p₁) ↦ Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑a : α)⟧ ⋯) ⋯ :
            { x : Quotient s₁ // p₂ x }))
        ⟦a⟧))
    ⟦a⟧

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid.{max 1 u_1} (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), (s₂ : Subtype p₁ → Subtype p₁ → Prop) x y ↔ (↑x : α) ≈ (↑y : α)
x : α
hx : p₂ ⟦x⟧
⊢ Eq.{max 1 u_1}
    ((subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h : (a : { x : Quotient s₁ // p₂ x }) → Quotient s₂)
      (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦x⟧ hx))
    ⟦Subtype.mk (p := p₁) x ⋯⟧

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid.{max 1 u_1} (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), (s₂ : Subtype p₁ → Subtype p₁ → Prop) x y ↔ (↑x : α) ≈ (↑y : α)
x : Subtype p₁
⊢ Eq.{max 1 u_1}
    ((Equiv.symm.{max 1 u_1, max 1 u_1} (subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h) :
        (a : Quotient s₂) → { x : Quotient s₁ // p₂ x })
      ⟦x⟧)
    (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑x : α)⟧ ⋯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a : α
unfold : (if r = a then a else if r = a then a else r) = r
⊢ swapCore a a r = r

Tactic:
unfold swapCore

Premises used: Equiv.swapCore
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a : α
pos : r = a → a = r
neg : ¬r = a → r = r
⊢ (if r = a then a else if r = a then a else r) = r

Tactic:
split_ifs
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a : α
h : r = a
⊢ a = r

Tactic:
simp [*]
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a : α
h : ¬r = a
⊢ r = r

Tactic:
simp [*]
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
unfold :
  (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r
⊢ swapCore a b (swapCore a b r) = r

Tactic:
unfold swapCore

Premises used: Equiv.swapCore
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
pos : r = a → b = a → b = r
pos₁ : r = a → ¬b = a → b = b → a = r
neg : r = a → ¬b = a → ¬b = b → b = r
pos₂ : ¬r = a → r = b → a = a → b = r
pos₃ : ¬r = a → r = b → ¬a = a → a = b → a = r
neg₁ : ¬r = a → r = b → ¬a = a → ¬a = b → a = r
neg₂ : ¬r = a → ¬r = b → r = r
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r

Tactic:
split_ifs
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
h : r = a
h_1 : b = a
⊢ b = r

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
h : r = a
h_1 : ¬b = a
h_2 : b = b
⊢ a = r

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
h : r = a
h_1 : ¬b = a
h_2 : ¬b = b
⊢ b = r

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
h : ¬r = a
h_1 : r = b
h_2 : a = a
⊢ b = r

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
h : ¬r = a
h_1 : r = b
h_2 : ¬a = a
h_3 : a = b
⊢ a = r

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
h : ¬r = a
h_1 : r = b
h_2 : ¬a = a
h_3 : ¬a = b
⊢ a = r

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
h : ¬r = a
h_1 : ¬r = b
⊢ r = r

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
unfold : (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r
⊢ swapCore a b r = swapCore b a r

Tactic:
unfold swapCore

Premises used: Equiv.swapCore
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
pos : r = a → r = b → b = a
neg : r = a → ¬r = b → b = b
pos₁ : ¬r = a → r = b → a = a
neg₁ : ¬r = a → ¬r = b → r = r
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r

Tactic:
split_ifs
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
h : r = a
h_1 : r = b
⊢ b = a

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
h : r = a
h_1 : ¬r = b
⊢ b = b

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
h : ¬r = a
h_1 : r = b
⊢ a = a

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a : α
⊢ Eq.{max 1 u_1} (swap a a) (Equiv.refl α)

Tactic:
ext fun r => swapCore_self r a

Premises used: Equiv.ext, Equiv.swapCore_self
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a b : α
⊢ Eq.{max 1 u_1} (swap a b) (swap b a)

Tactic:
ext fun r => swapCore_comm r _ _

Premises used: Equiv.swapCore_comm, Equiv.ext
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a b x : α
⊢ (swap a b : (a : α) → α) x = if x = a then b else if x = b then a else x

Tactic:
rfl

Premises used: Equiv.swapCore, rfl, ite
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a b : α
⊢ (swap a b : (a : α) → α) a = b

Tactic:
if_pos rfl

Premises used: Equiv.swapCore, if_pos, rfl, ite
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a b : α
⊢ (swap a b : (a : α) → α) b = a

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a b x : α
⊢ x ≠ a → x ≠ b → (swap a b : (a : α) → α) x = x

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a b x : α
h : (swap a b : (a : α) → α) x ≠ x
contrapose! : ∀ (h : x ≠ a ∧ x ≠ b), (swap a b : (a : α) → α) x = x
⊢ x = a ∨ x = b

Tactic:
contrapose! h
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a b x : α
h : x ≠ a ∧ x ≠ b
⊢ (swap a b : (a : α) → α) x = x

Tactic:
swap_apply_of_ne_of_ne h.1 h.2

Premises used: Equiv.swap_apply_of_ne_of_ne, And.right, And.left
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a b x : α
h : x ≠ a ∧ x ≠ b
⊢ (swap a b : (a : α) → α) x = x

Tactic:
exact swap_apply_of_ne_of_ne h.1 h.2

Premises used: Equiv.swap_apply_of_ne_of_ne, And.right, And.left
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a b : α
⊢ Eq.{max 1 u_1} (Equiv.trans (swap a b) (swap a b)) (Equiv.refl α)

Tactic:
ext fun _ => swapCore_swapCore _ _ _

Premises used: Equiv.ext, Equiv.swapCore_swapCore
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a b : α
⊢ Eq.{max 1 u_1} (Equiv.symm (swap a b)) (swap a b)

Tactic:
rfl

Premises used: Equiv.swapCore, Equiv.swap, Equiv.symm, rfl, ite
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
x y : α
h : Eq.{max 1 u_1} (swap x y) (Equiv.refl α)
⊢ Eq (α := α) ((Equiv.refl α : (a : α) → α) x : α) ((Equiv.refl α : (a : α) → α) y : α)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
x y : α
⊢ x = y → Eq.{max 1 u_1} (swap x y) (Equiv.refl α)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a b x : α
π : Perm α
mk :
  ∀ (toFun invFun : α → α) (left_inv : LeftInverse invFun toFun) (right_inv : RightInverse invFun toFun),
    ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ α }.trans (swap a b) :
          (a : α) → α)
        x =
      if
          ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ α } : (a : α) → α) x =
            a then
        b
      else
        if
            ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ α } : (a : α) → α)
                x =
              b then
          a
        else
          ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ α } : (a : α) → α) x
⊢ (Equiv.trans π (swap a b) : (a : α) → α) x =
    if (π : (a : α) → α) x = a then b else if (π : (a : α) → α) x = b then a else (π : (a : α) → α) x

Tactic:
cases π
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a b x : α
toFun invFun : α → α
left_inv : LeftInverse invFun toFun
right_inv : RightInverse invFun toFun
⊢ ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ α }.trans (swap a b) :
        (a : α) → α)
      x =
    if
        ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ α } : (a : α) → α) x =
          a then
      b
    else
      if
          ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ α } : (a : α) → α) x =
            b then
        a
      else ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ α } : (a : α) → α) x

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
i j : α
⊢ (⇑(swap i j) : (a : α) → α) = update (β := fun (a : α) ↦ α) (update (β := fun (a : α) ↦ α) id j i) i j

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
i j : α
f : α → β
⊢ f ∘ (⇑(swap i j) : (a : α) → α) = update (β := fun (a : α) ↦ β) (update (β := fun (a : α) ↦ β) f j (f i)) i (f j)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
inst_1 : DecidableEq β
a b : α
e : α ≃ β
⊢ Eq.{max 1 u_4} ((e.symm.trans (swap a b)).trans e) (swap ((e : (a : α) → β) a) ((e : (a : α) → β) b))

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
inst_1 : DecidableEq β
a b : β
e : α ≃ β
⊢ Eq.{max 1 u_1} ((e.trans (swap a b)).trans e.symm) (swap ((e.symm : (a : β) → α) a) ((e.symm : (a : β) → α) b))

Tactic:
symm_trans_swap_trans a b e.symm

Premises used: Equiv.symm_trans_swap_trans, Equiv.symm
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
i j a : α
⊢ (swap i j : (a : α) → α) ((swap i j : (a : α) → α) a : α) = a

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
v : α → β
i j : α
hv : v i = v j
k : α
⊢ v ((swap i j : (a : α) → α) k) = v k

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
x y z w : α
⊢ (swap x y : (a : α) → α) z = w ↔ z = (swap x y : (a : α) → α) w

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a b x : α
⊢ (swap a b : (a : α) → α) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a c d : α
h : Eq.{max 1 u_1} (swap a c) (swap a d)
rw : (swap a c : (a : α) → α) a = d
rw₁ : (swap a d : (a : α) → α) a = d
rw₂ rw₃ : d = d
⊢ c = d

Tactic:
rw [← Equiv.swap_apply_left a c, h, Equiv.swap_apply_left]

Premises used: Equiv.swap_apply_left
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a : α
simp_rw : Injective (β := Perm α) fun (x : α) ↦ swap a x
⊢ Injective (β := Perm α) fun (x : α) ↦ swap x a

Tactic:
simp_rw [swap_comm _ a]

Premises used: Equiv.swap_comm
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a : α
⊢ Injective (β := Perm α) fun (x : α) ↦ swap a x

Tactic:
swap_injective_of_left a

Premises used: Equiv.swap_injective_of_left
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a : α
⊢ Injective (β := Perm α) fun (x : α) ↦ swap a x

Tactic:
exact swap_injective_of_left a

Premises used: Equiv.swap_injective_of_left
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
inst : DecidableEq α_1
α : Type u_9
inst_1 : Nontrivial α
obtain : ∀ (a : α), Nontrivial.{u_9} (Perm α)
⊢ Nontrivial.{u_9} (Perm α)

Tactic:
obtain ⟨a : α⟩ := Nontrivial.to_nonempty (α := α)

Premises used: Nontrivial.to_nonempty
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
inst : DecidableEq α_1
α : Type u_9
inst_1 : Nontrivial α
a : α
⊢ Nontrivial.{u_9} (Perm α)

Tactic:
Function.Injective.nontrivial (Equiv.swap_injective_of_left a)

Premises used: Function.Injective.nontrivial, Equiv.swap_injective_of_left
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
inst : DecidableEq α_1
α : Type u_9
inst_1 : Nontrivial α
a : α
⊢ Nontrivial.{u_9} (Perm α)

Tactic:
exact Function.Injective.nontrivial (Equiv.swap_injective_of_left a)

Premises used: Function.Injective.nontrivial, Equiv.swap_injective_of_left
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
inst : DecidableEq α_1
α : Type u_9
inst_1 : Nontrivial α
obtain : ∀ (a : α), Nontrivial.{u_9} (Perm α)
⊢ Nontrivial.{u_9} (Perm α)

Tactic:
classical
  obtain ⟨a : α⟩ := Nontrivial.to_nonempty (α := α)
  exact Function.Injective.nontrivial (Equiv.swap_injective_of_left a)

Premises used: Nontrivial.to_nonempty
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
mp : Membership.mem (γ := Set α) (Set.image (⇑(swap i j) : (a : α) → α) s) a → a ∈ insert j s \ {i}
mpr : a ∈ insert j s \ {i} → Membership.mem (γ := Set α) (Set.image (⇑(swap i j) : (a : α) → α) s) a
⊢ Membership.mem (γ := Set α) (Set.image (⇑(swap i j) : (a : α) → α) s) a ↔ a ∈ insert j s \ {i}

Tactic:
constructor
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
mp : ∀ (hi : a ∈ s), Membership.mem (α := α) (insert j s \ {a}) ((swap a j : (a : α) → α) a : α)
mp₁ : ∀ (ne : a ≠ i), Membership.mem (α := α) (insert j s \ {i}) ((swap i j : (a : α) → α) a : α)
⊢ Membership.mem (α := α) (insert j s \ {i}) ((swap i j : (a : α) → α) a : α)

Tactic:
obtain rfl | ne := eq_or_ne a i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
j : α
hj : ¬j ∈ s
a : α
ha hi : a ∈ s
mp : j ∈ insert j s \ {a}
⊢ Membership.mem (α := α) (insert j s \ {a}) ((swap a j : (a : α) → α) a : α)

Tactic:
rw [swap_apply_left]

Premises used: Equiv.swap_apply_left
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
j : α
hj : ¬j ∈ s
a : α
ha hi : a ∈ s
⊢ j ∈ insert j s \ {a}

Tactic:
⟨.inl rfl, (ne_of_mem_of_not_mem hi hj).symm⟩

Premises used: Set.Mem, Set.diff, setOf, Ne.symm, ne_of_mem_of_not_mem, And.intro, Or.inl, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
j : α
hj : ¬j ∈ s
a : α
ha hi : a ∈ s
⊢ j ∈ insert j s \ {a}

Tactic:
exact ⟨.inl rfl, (ne_of_mem_of_not_mem hi hj).symm⟩
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
mp : a ∈ insert j s \ {i}
⊢ Membership.mem (α := α) (insert j s \ {i}) ((swap i j : (a : α) → α) a : α)

Tactic:
rw [swap_apply_of_ne_of_ne ne (ne_of_mem_of_not_mem ha hj)]

Premises used: Equiv.swap_apply_of_ne_of_ne, ne_of_mem_of_not_mem
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
⊢ a ∈ insert j s \ {i}

Tactic:
⟨.inr ha, ne⟩

Premises used: Set.Mem, Set.diff, setOf, And.intro, Or.inr
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
⊢ a ∈ insert j s \ {i}

Tactic:
exact ⟨.inr ha, ne⟩
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
i : α
hi : i ∈ s
a : α
hai : ¬Membership.mem (γ := Set α) {i} a
hj : ¬a ∈ s
⊢ Membership.mem (γ := Set α) (Set.image (⇑(swap i a) : (a : α) → α) s) a

Tactic:
⟨i, hi, swap_apply_left ..⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, Equiv.swap_apply_left
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
i : α
hi : i ∈ s
a : α
hai : ¬Membership.mem (γ := Set α) {i} a
hj : ¬a ∈ s
⊢ Membership.mem (γ := Set α) (Set.image (⇑(swap i a) : (a : α) → α) s) a

Tactic:
exact ⟨i, hi, swap_apply_left ..⟩
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
inst : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
hai : ¬Membership.mem (γ := Set α) {i} a
has : a ∈ s
⊢ Membership.mem (γ := Set α) (Set.image (⇑(swap i j) : (a : α) → α) s) a

Tactic:
⟨a, has, swap_apply_of_ne_of_ne hai (ne_of_mem_of_not_mem has hj)⟩

Premises used: Set.Mem, setOf, Equiv.swap_apply_of_ne_of_ne, ne_of_mem_of_not_mem, And.intro, Exists.intro, Set.image