chore: remove unused variables warning showing up in build

Opted to fix the warnings instead of silencing them, except for the
case involving a mutual inductive.

I'm surprised by the behavior of the linter there, disabled warning
for now.

Author: ejgallego

test-projects/tutorial-test/TutorialExample/Data.lean

@@ -341,6 +341,8 @@ mutual
     | succ : Even n → Odd (n + 1)
 end
 
+set_option linter.unusedVariables false
+
 -- Trees with different node types
 mutual
   inductive TreeA (α : Type) where

test-projects/tutorial-test/TutorialExample/RCases.lean

@@ -487,8 +487,8 @@ example (h : ∃ n, P n) : True := by
   trivial
 
 -- Or just:
-example (h : ∃ n, P n) : True := by
-  trivial  -- h not needed at all
+example (_ : ∃ n, P n) : True := by
+  trivial  -- hypothesis not needed at all
 end
 ```
 

test-projects/website/DemoSite/Blog/Conditionals.lean

@@ -153,7 +153,7 @@ Here's an inductive type and a structure:
 ```lean demo
 inductive A where
   | a1 | a2
-  | a3 (n : Nat)
+  | a3 : Nat → A
   | a4 : (n : Nat) → n = 3 → A
 
 structure S where
@@ -190,7 +190,7 @@ def quoted (str : String) : m Syntax := do
   let s ← `(a b c #[x, $(quote str), z])
   pure s
 
-example : ¬(quoted (m := m) = fun x => pure .missing) := by
+example : ¬(quoted (m := m) = fun _ => pure .missing) := by
   unfold quoted
   intro h
   let g : String → m Syntax := fun str => do