Theorem: Usa1998P3.lemma2' (Compfiles/Usa1998P3.lean)

State before:
n : ℕ
⊢ (Finset.range (n + 1)).erase n = Finset.range n
Tactic:
rw [←Nat.succ_eq_add_one, Finset.range_succ]
State after:
n : ℕ
⊢ (insert n (Finset.range n)).erase n = Finset.range n

State before:
n : ℕ
⊢ (insert n (Finset.range n)).erase n = Finset.range n
Tactic:
simp
State after:
no goals