Theorem: PFin2.inv_involution (Qpf/MathlibPort/Fin2.lean)

State before:
n : ℕ
i : PFin2 n
⊢ inv (inv i) = i
Tactic:
induction i
State after:
case fz
n n✝ : ℕ
⊢ inv (inv fz) = fz

case fs
n n✝ : ℕ
a✝ : PFin2 n✝
a_ih✝ : inv (inv a✝) = a✝
⊢ inv (inv (fs a✝)) = fs a✝

State before:
case fz
n n✝ : ℕ
⊢ inv (inv fz) = fz

case fs
n n✝ : ℕ
a✝ : PFin2 n✝
a_ih✝ : inv (inv a✝) = a✝
⊢ inv (inv (fs a✝)) = fs a✝
Tactic:
simp [inv]
State after:
case fz
n n✝ : ℕ
⊢ inv last = fz

case fs
n n✝ : ℕ
a✝ : PFin2 n✝
a_ih✝ : inv (inv a✝) = a✝
⊢ inv (inv (fs a✝)) = fs a✝

State before:
n n✝ : ℕ
⊢ inv last = fz
Tactic:
case fz => apply inv_last_eq_fz
State after:
no goals

State before:
n✝ n : ℕ
i : PFin2 n
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i
Tactic:
case fs n i ih => {
  cases n;
  case zero => contradiction
  case succ n =>
    simp[inv]
    rw[inv_weaken_eq_fs_inv i.inv]
    apply congrArg
    apply ih
}
State after:
no goals

State before:
n n✝ : ℕ
⊢ inv last = fz
Tactic:
apply inv_last_eq_fz
State after:
no goals

State before:
n✝ n : ℕ
i : PFin2 n
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i
Tactic:
cases n
State after:
case zero
n : ℕ
i : PFin2 zero
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i

case succ
n n✝ : ℕ
i : PFin2 (succ n✝)
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i

State before:
n : ℕ
i : PFin2 zero
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i
Tactic:
case zero => contradiction
State after:
no goals

State before:
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i
Tactic:
case succ n =>
  simp[inv]
  rw[inv_weaken_eq_fs_inv i.inv]
  apply congrArg
  apply ih
State after:
no goals

State before:
n : ℕ
i : PFin2 zero
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i
Tactic:
contradiction
State after:
no goals

State before:
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ inv (inv (fs i)) = fs i
Tactic:
simp[inv]
State after:
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ inv (weaken (inv i)) = fs i

State before:
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ inv (weaken (inv i)) = fs i
Tactic:
rw[inv_weaken_eq_fs_inv i.inv]
State after:
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ fs (inv (inv i)) = fs i

State before:
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ fs (inv (inv i)) = fs i
Tactic:
apply congrArg
State after:
case h
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ inv (inv i) = i

State before:
case h
n✝ n : ℕ
i : PFin2 (succ n)
ih : inv (inv i) = i
⊢ inv (inv i) = i
Tactic:
apply ih
State after:
no goals