no goals
α : Type ?u.55329
β : Type ?u.55332
γ : Type ?u.55335
n i j : ℕ
⊢ (fun i => i + 1) i = (fun i => i + 1) j → i = j
simp
no goals
α : Type ?u.55329
β : Type ?u.55332
γ : Type ?u.55335
n : ℕ
⊢ range (n + 1) = insert 0 (map { toFun := fun i => i + 1, inj' := (_ : ∀ (i j : ℕ), i + 1 = j + 1 → i = j) } (range n))
ext (⟨⟩ | ⟨n⟩) <;> simp [Nat.succ_eq_add_one, Nat.zero_lt_succ n]