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

State before:
n : ℕ
i : PFin2 n
⊢ inv (weaken i) = fs (inv i)
Tactic:
induction i
<;> simp[inv, weaken, last]
State after:
case fs
n n✝ : ℕ
a✝ : PFin2 n✝
a_ih✝ : inv (weaken a✝) = fs (inv a✝)
⊢ weaken (inv (weaken a✝)) = fs (inv (fs a✝))

State before:
n✝ n : ℕ
i : PFin2 n
ih : inv (weaken i) = fs (inv i)
⊢ weaken (inv (weaken i)) = fs (inv (fs i))
Tactic:
case fs n i ih =>
  simp[ih]
  cases n
  . contradiction
  . simp[inv, weaken]
State after:
no goals

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

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

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

State before:
case zero
n : ℕ
i : PFin2 zero
ih : inv (weaken i) = fs (inv i)
⊢ weaken (fs (inv i)) = fs (inv (fs i))

case succ
n n✝ : ℕ
i : PFin2 (succ n✝)
ih : inv (weaken i) = fs (inv i)
⊢ weaken (fs (inv i)) = fs (inv (fs i))
Tactic:
. contradiction
State after:
case succ
n n✝ : ℕ
i : PFin2 (succ n✝)
ih : inv (weaken i) = fs (inv i)
⊢ weaken (fs (inv i)) = fs (inv (fs i))

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

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

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