Theorem: invertible_id (QuickSortInLean/Permutation.lean)

State before:
α : Sort u_1
⊢ invertible id
Tactic:
have : isInv (id : α → α) id := by
  apply And.intro
  . intro x
    simp
  . intro y
    simp
State after:
α : Sort u_1
this : isInv id id
⊢ invertible id

State before:
α : Sort u_1
this : isInv id id
⊢ invertible id
Tactic:
exact ⟨id, this⟩
State after:
no goals

State before:
α : Sort u_1
⊢ isInv id id
Tactic:
apply And.intro
State after:
case left
α : Sort u_1
⊢ ∀ (x : α), id (id x) = x

case right
α : Sort u_1
⊢ ∀ (y : α), id (id y) = y

State before:
case left
α : Sort u_1
⊢ ∀ (x : α), id (id x) = x

case right
α : Sort u_1
⊢ ∀ (y : α), id (id y) = y
Tactic:
. intro x
  simp
State after:
case right
α : Sort u_1
⊢ ∀ (y : α), id (id y) = y

State before:
case right
α : Sort u_1
⊢ ∀ (y : α), id (id y) = y
Tactic:
. intro y
  simp
State after:
no goals

State before:
case left
α : Sort u_1
⊢ ∀ (x : α), id (id x) = x
Tactic:
intro x
State after:
case left
α : Sort u_1
x : α
⊢ id (id x) = x

State before:
case left
α : Sort u_1
x : α
⊢ id (id x) = x
Tactic:
simp
State after:
no goals

State before:
case right
α : Sort u_1
⊢ ∀ (y : α), id (id y) = y
Tactic:
intro y
State after:
case right
α : Sort u_1
y : α
⊢ id (id y) = y

State before:
case right
α : Sort u_1
y : α
⊢ id (id y) = y
Tactic:
simp
State after:
no goals