### Import All Mathlib Tactics for Quick Setup

Source: https://lean4.dev/tactics/mathlib/intro

Import `Mathlib.Tactic` to make all common Mathlib tactics available. This is a convenient way to start using tactics like `ring` and `linarith`.

```lean
-- Quick setup with all Mathlib tactics:
import Mathlib.Tactic

-- Now you can use ring, linarith, and more!
example (a b : ℤ) : (a - b) * (a + b) = a^2 - b^2 := by ring
```

--------------------------------

### Practical Example: Formatting Price

Source: https://lean4.dev/language/foundations/local-scope

A realistic example demonstrating the use of multiple `let` bindings to break down a calculation for formatting a price string from cents.

```lean
def formatPrice (cents : Nat) : String :=
  let dollars := cents / 100
  let remaining := cents % 100
  let dollarStr := toString dollars
  let centStr := if remaining < 10 
                 then "0" ++ toString remaining 
                 else toString remaining
  "$" ++ dollarStr ++ "." ++ centStr

#eval formatPrice 1234   -- "$12.34"
#eval formatPrice 50     -- "$0.50"
#eval formatPrice 1005   -- "$10.05"
```

--------------------------------

### Basic Lean 4 IO Example

Source: https://lean4.dev/

A minimal Lean 4 program that prints 'Hello!' to the console. This is a common starting point for new Lean applications.

```lean
-- Main.lean
def main : IO Unit :=
  IO.println "Hello!"
```

--------------------------------

### Complete CLI Application Example in Lean

Source: https://lean4.dev/language/projects/compiling

A comprehensive example of a Lean CLI application demonstrating argument parsing, version display, help messages, and command handling.

```lean
1def version := "1.0.0"
2
def printHelp : IO Unit :=
do
  IO.println "myapp - A command line tool"
  IO.println ""
  IO.println "Usage: myapp [options] <command>"
  IO.println ""
  IO.println "Options:"
  IO.println "  --help, -h     Show this help"
  IO.println "  --version, -v  Show version"
  IO.println ""
  IO.println "Commands:"
  IO.println "  init           Initialize a new project"
  IO.println "  build          Build the project"
  IO.println "  run            Run the project"

def doInit : IO UInt32 :=
do
  IO.println "Initializing..."
  IO.FS.writeFile "config.json" "{}"
  IO.println "Created config.json"
  return 0

def doBuild : IO UInt32 :=
do
  IO.println "Building..."
  -- Build logic here
  IO.println "Done!"
  return 0

def main (args : List String) : IO UInt32 :=
do
  match args with
  | [] | ["--help"] | ["-h"] => 
    printHelp
    return 0
  | ["--version"] | ["-v"] =>
    IO.println s!"myapp version {version}"
    return 0
  | ["init"] => doInit
  | ["build"] => doBuild
  | ["run"] => 
    IO.println "Running..."
    return 0
  | cmd :: _ =>
    IO.println s!"Error: Unknown command '{cmd}'"
    IO.println "Run 'myapp --help' for usage"
    return 1
```

--------------------------------

### Verify Lean Setup with #eval

Source: https://lean4.dev/course/level-1/installation

This Lean code snippet evaluates a string to verify that the Lean environment and Infoview are working correctly.

```lean
#eval "Lean is ready"
```

--------------------------------

### Install Lean Toolchain Manager

Source: https://lean4.dev/

Installs the elan toolchain manager, which is the first step to getting started with Lean 4.

```bash
curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh
```

--------------------------------

### Real-World Example: Vieta's Formulas

Source: https://lean4.dev/tactics/mathlib/polyrith

Demonstrates using polyrith to prove Vieta's formulas, relating the roots of a polynomial to its coefficients.

```lean
import Mathlib.Tactic.Polyrith

-- If r, s are roots of x^2 - px + q = 0
-- Then r + s = p and rs = q
theorem vieta (r s p q : ℚ)
    (h1 : r^2 - p*r + q = 0)
    (h2 : s^2 - p*s + q = 0)
    (h3 : r + s = p) :
    r * s = q := by
  polyrith
```

--------------------------------

### Interactive Proof State Exploration

Source: https://lean4.dev/tactics/intro/proof-state

An interactive example demonstrating how to step through a proof in an editor to observe the proof state evolution after each tactic.

```lean
-- Try stepping through this proof in your editor
theorem symmetry (a b : Nat) (h : a = b) : b = a := by
  -- Cursor here:
  -- a b : Nat
  -- h : a = b
  -- ⊢ b = a
  
  rw [h]
  -- Cursor here:
  -- a b : Nat
  -- h : a = b
  -- ⊢ a = a
  
  rfl
  -- No goals
```

--------------------------------

### Finish Proofs After Setup with Aesop

Source: https://lean4.dev/tactics/automation/aesop

Use aesop as a finishing tactic after setting up the proof context with explicit steps.

```lean
import Mathlib.Tactic

example (P Q R : Prop) : (P -> Q) -> (Q -> R) -> P -> R := by
  intro hPQ hQR hP
  aesop

```

--------------------------------

### Install Lean via elan

Source: https://lean4.dev/course/level-1/installation

Use `elan` to manage Lean toolchains. This command installs `elan` on Windows using winget. For macOS and Linux, it downloads and executes an installation script.

```bash
winget install Lean4.elan
```

```bash
curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh
```

--------------------------------

### Verified Proof Example

Source: https://lean4.dev/tactics/intro/what-is-proof

An example of a proof verified by Lean's kernel. Lean catches attempts to prove false statements.

```lean
-- This proof is VERIFIED by Lean's kernel
theorem example_proof : ∀ n : Nat, n + 0 = n := by
  intro n
  rfl  -- Lean checks that this step is valid

-- If you try to cheat, Lean catches it:
-- theorem bad_proof : 1 = 2 := by rfl  -- ERROR: rfl cannot prove this
```

--------------------------------

### Basic linarith Examples

Source: https://lean4.dev/tactics/mathlib/linarith

Demonstrates simple transitivity and more complex chains of inequalities solvable by linarith.

```lean
import Mathlib.Tactic.Linarith

-- Simple transitivity
example (x y z : Int) (h1 : x < y) (h2 : y < z) : x < z := by linarith

-- More complex chains
example (a b c d e : Int) 
    (h1 : a ≤ b) (h2 : b < c) (h3 : c ≤ d) (h4 : d < e) 
    : a < e := by linarith

-- Combining many constraints
example (x y z : Int) 
    (h1 : x + y ≤ 10) (h2 : y + z ≤ 10) (h3 : z + x ≤ 10) 
    : x + y + z ≤ 15 := by linarith
```

--------------------------------

### Real-World Example: Proving List Associativity

Source: https://lean4.dev/tactics/core/rw

Demonstrates a step-by-step proof of list append associativity using `rw` and induction.

```lean
-- A step-by-step proof using rw
theorem list_append_assoc (xs ys zs : List α) : 
    (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by
  induction xs with
  | nil => 
    rw [List.nil_append, List.nil_append]
    -- ([] ++ ys) ++ zs = [] ++ (ys ++ zs)
    -- After rewrites: ys ++ zs = ys ++ zs
  | cons h t ih =>
    rw [List.cons_append, List.cons_append, List.cons_append]
    rw [ih]
    -- Use induction hypothesis
```

--------------------------------

### Interactive Proof Workflow Example in Lean

Source: https://lean4.dev/tactics/intro/what-is-proof

Demonstrates the interactive nature of proving in Lean. The `omega` tactic solves the goal, showing the proof state changing from a goal to 'No goals'.

```lean
1-- Watch the proof state change with each tactic
2theorem add_example (a b c : Nat) : a + b + c = c + b + a := by
3  -- Proof state: ⊢ a + b + c = c + b + a
4  omega
5  -- Proof state: No goals (proof complete!)

```

--------------------------------

### Discovering Lemmas with simp?

Source: https://lean4.dev/tactics/core/simp

Run `simp?` to get suggestions for `simp only` lemmas that would achieve the same simplification. This is helpful for converting exploratory `simp` calls into reproducible ones.

```lean
example (n : Nat) : 0 + n + 0 = n :=
  simp?
  -- Output: Try this: simp only [Nat.zero_add, Nat.add_zero]
```

```lean
example (n : Nat) : n + 0 = n :=
by
  simp?
  -- Output: Try this: simp only [Nat.add_zero]
  -- Click the suggestion or copy it!
```

```lean
example (a : Nat) (h : a = 5) : a + 0 = 5 :=
  simp? [h]
  -- Output: Try this: simp only [Nat.add_zero, h]
```

--------------------------------

### Start a New Lean Project with Lake

Source: https://lean4.dev/language/projects/lake

Use `lake new` to create a new project structure, `cd` into it, and then `lake build` to compile. If your project is an executable, you can run it with `lake exe myproject`.

```bash
1lake new myproject
2cd myproject
3lake build
4lake exe myproject  # If it's an executable

```

--------------------------------

### Read Input and Compute Double in Lean

Source: https://lean4.dev/language/effects/io

A practical example demonstrating how to read user input, parse it as a number, and then perform a computation (doubling the value) and print the result.

```lean
def readDouble : IO Unit :=
  do
  IO.print "Enter a number: "
  let input ← IO.getLine
  let n := input.trim.toNat!
  IO.println s!"Double is {n * 2}"
```

--------------------------------

### Basic Lean 4 Syntax and Examples

Source: https://lean4.dev/

Demonstrates basic Lean 4 syntax including string definitions, theorem statements with tactics, and functional programming with pattern matching for a Fibonacci function.

```lean
1-- Welcome to Lean 4
2def hello : String := "Hello, Lean!"
3
4-- A simple theorem
5theorem add_comm (a b : Nat) : a + b = b + a := by
6  omega
7
8-- Functional programming with pattern matching
9def fibonacci : Nat → Nat
10  | 0 => 0
11  | 1 => 1
12  | n + 2 => fibonacci n + fibonacci (n + 1)
```

--------------------------------

### The main Function in Lean4 Executables

Source: https://lean4.dev/language/effects/io

Provides examples of the `main` function, the entry point for Lean executables. It shows the simplest form, handling command-line arguments, and returning an exit code.

```lean
1-- Simplest form
2def main : IO Unit := do
3  IO.println "Hello, World!"
4
5-- With command line arguments
6def main (args : List String) : IO Unit := do
7  match args with
8  | [] => IO.println "No arguments"
9  | _ => IO.println s!"Arguments: {args}"
10
11-- With exit code
12def main : IO UInt32 := do
13  IO.println "Running..."
14  return 0  -- 0 = success
```

--------------------------------

### Exercise: Add a simp Lemma

Source: https://lean4.dev/tactics/automation/simp-attrs

Marks a 'double_zero' lemma with @[simp] and uses it in an example proof, demonstrating the automatic application of simp lemmas.

```lean
def double (n : Nat) : Nat := n + n

@[simp] theorem double_zero : double 0 = 0 := rfl

example : double 0 + 1 = 1 := by simp
```

--------------------------------

### Product Bounds Proof with nlinarith

Source: https://lean4.dev/tactics/mathlib/nlinarith

Demonstrates proving bounds on the product of two variables using `nlinarith`. This example requires `Mathlib.Tactic.Linarith` and multiple `sq_nonneg` hints for both lower and upper bounds.

```Lean
import Mathlib.Tactic.Linarith

-- Bounded inputs give bounded outputs
theorem product_bound (x y : Int) 
    (hx1 : 1 ≤ x) (hx2 : x ≤ 10)
    (hy1 : 1 ≤ y) (hy2 : y ≤ 10) : 
    1 ≤ x * y ∧ x * y ≤ 100 := by
  constructor
  · nlinarith [sq_nonneg x, sq_nonneg y, sq_nonneg (x-1), sq_nonneg (y-1)]
  · nlinarith [sq_nonneg (10-x), sq_nonneg (10-y)]
```

--------------------------------

### Quadratic Bounds Proof with nlinarith

Source: https://lean4.dev/tactics/mathlib/nlinarith

Example of proving bounds on quadratic expressions using `nlinarith`. Requires `Mathlib.Tactic.Linarith` and relevant `sq_nonneg` hints.

```Lean
import Mathlib.Tactic.Linarith

-- Prove bounds on quadratic expressions
theorem quadratic_lower_bound (x : Int) (h : x ≥ 1) : 
    x^2 + x ≥ 2 := by
  nlinarith [sq_nonneg x, sq_nonneg (x - 1)]
```

--------------------------------

### Complete Commutative Addition Proof in Lean

Source: https://lean4.dev/tactics/intro/what-is-proof

A full example proving `a + b = b + a` using induction and tactics like `simp` and `exact`. It also shows how to check the theorem with specific values.

```lean
1-- Statement: addition is commutative
2theorem add_comm_example : ∀ a b : Nat, a + b = b + a := by
3  intro a b           -- Let a and b be any Nats
4  -- Goal: a + b = b + a
5  induction a with    -- Prove by induction on a
6  | zero => 
7    -- Base case: 0 + b = b + 0
8    simp              -- simp knows 0 + b = b and b + 0 = b
9  | succ n ih =>
10    -- Inductive case: (n + 1) + b = b + (n + 1)
11    -- ih: n + b = b + n (induction hypothesis)
12    simp [Nat.succ_add, Nat.add_succ]  -- Use known lemmas
13    exact ih          -- Apply induction hypothesis
14
15-- Now we can use this theorem
16#check add_comm_example 3 5  -- : 3 + 5 = 5 + 3

```

--------------------------------

### Exercise: Solve Both Goals with a Single Combinator

Source: https://lean4.dev/tactics/advanced/combinators

This example requires solving two goals generated by `constructor` using a single combinator, demonstrating the application of combinators to multiple subgoals.

```lean
example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  constructor <;> assumption
```

--------------------------------

### Get Current Time in Lean

Source: https://lean4.dev/language/effects/io

Retrieves the current time in milliseconds since the start of the program's execution.

```lean
def showTime : IO Unit :=
  do
  let now ← IO.monoMsNow
  IO.println s!"Milliseconds since start: {now}"
```

--------------------------------

### Creating and Using Ranges in Lean4

Source: https://lean4.dev/language/data-modeling/collections

Shows how to create number ranges using '[start:stop]' syntax, including ranges with steps, converting ranges to Lists, and using ranges with `map` for generating sequences.

```lean
1-- Ranges (exclusive end)
2#eval [0:5]           -- [0, 1, 2, 3, 4]
3#eval [1:10:2]        -- [1, 3, 5, 7, 9] (step of 2)
4
5-- Convert range to List
6#eval (List.range 5)  -- [0, 1, 2, 3, 4]
7
8-- Useful for generating test data
9def squares := (List.range 10).map (fun n => n * n)
10#eval squares  -- [0, 1, 4, 9, 16, 25, 36, 49, 64, 81]
```

--------------------------------

### Aesop for a Simple Implication Proof

Source: https://lean4.dev/tactics/automation/aesop

An example demonstrating aesop's ability to close a simple implication goal after setup.

```lean
import Mathlib.Tactic

example (P Q R : Prop) (hP : P) (hPQ : P → Q) (hQR : Q → R) : R := by
  aesop

```

--------------------------------

### Exercise 1: Introduce and Use

Source: https://lean4.dev/tactics/core/intro

A simple exercise to practice using 'intro' to bring assumptions into context and complete a proof.

```lean
example (P Q : Prop) : P → Q → Q := by
  intro hp hq
  exact hq
```

--------------------------------

### Create a First Lean Project

Source: https://lean4.dev/course/level-1/installation

Initialize a new Lean project named 'hello' using `lake`, create a directory for it, navigate into it, and open the project in VS Code.

```bash
mkdir lean-playground
cd lean-playground
lake init hello
code .
```

--------------------------------

### Basic Instance Syntax for ToString and BEq

Source: https://lean4.dev/language/type-classes/instances

Demonstrates the basic syntax for declaring instances using `instance`. Anonymous instances are common, while named instances can be useful for debugging.

```lean
structure Point where
  x : Float
  y : Float

-- Anonymous instance (most common)
instance : ToString Point where
  toString p := s!"({p.x}, {p.y})"

-- Named instance (useful for debugging)
instance instBEqPoint : BEq Point where
  beq p1 p2 := p1.x == p2.x && p1.y == p2.y

#eval toString (Point.mk 3.0 4.0)  -- "(3.0, 4.0)"
#eval Point.mk 1.0 2.0 == Point.mk 1.0 2.0  -- true
```

--------------------------------

### Simplify Hypothesis and Goal with simp only at h ⊢

Source: https://lean4.dev/tactics/core/simp

This example demonstrates simplifying a specific hypothesis `h` and the goal `⊢` using `simp only` with explicit lemmas. It ensures only specified rules are applied.

```lean
example (n : Nat) (h : n + 0 = n + 0) : n + 0 = n :=
by
  simp only [Nat.add_zero] at h ⊢
```

--------------------------------

### Guiding Aesop Search with Simplification

Source: https://lean4.dev/tactics/automation/aesop

Simplify the goal using `simp` with relevant hypotheses before calling `aesop` to guide the search.

```lean
import Mathlib.Tactic

example (n : Nat) (h : n = 3) : n + 1 = 4 := by
  simp [h]
  aesop

```

--------------------------------

### Basic Function Proof with `intro` and `exact`

Source: https://lean4.dev/tactics/intro/workflow

Demonstrates introducing an input to a function type goal and then using `exact` to provide the final term. The Infoview updates after each tactic, showing the goal's progression.

```Lean
1example : Nat → Nat := by
2  -- Goal: Nat → Nat
3  -- This is a function type, so we introduce the input
4  intro n
5  -- Goal: Nat
6  -- Now we just need to produce a Nat
7  exact n + 1

```

--------------------------------

### Divisibility Example with Contraposition

Source: https://lean4.dev/tactics/mathlib/contrapose

An example illustrating the potential use of contraposition in divisibility theorems, noting that direct proofs can sometimes still be simpler.

```lean
import Mathlib.Tactic.Contrapose

-- If a divides bc and gcd(a,b) = 1, then a divides c
-- Contrapositive: If a doesn't divide c, then...
-- (Sometimes the direct proof is still easier)
```

--------------------------------

### Introduce All with 'intros'

Source: https://lean4.dev/tactics/core/intro

The 'intros' tactic introduces all available hypotheses or universal variables at once, often with auto-generated names. Prefer explicit 'intro' for clarity.

```lean
-- intros introduces everything it can
example : ∀ a b : Nat, a = b → b = a := by
  intros
  -- Introduces a, b, and the equality proof with auto-generated names
  assumption

-- Better to name them explicitly:
example : ∀ a b : Nat, a = b → b = a := by
  intro a b hab
  exact hab.symm
```

--------------------------------

### Structural Recursion Examples in Lean4

Source: https://lean4.dev/language/control-flow/recursion

Demonstrates structural recursion on Nat, List, and a custom Tree type. These examples are automatically proven terminating due to their adherence to data structure.

```Lean
def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

def length : List α → Nat
  | [] => 0
  | _ :: xs => 1 + length xs

inductive Tree where
  | leaf
  | node (left : Tree) (value : Nat) (right : Tree)

def Tree.size : Tree → Nat
  | leaf => 0
  | node left _ right => 1 + left.size + right.size

#eval factorial 5  -- 120
#eval length [1, 2, 3, 4]  -- 4
```

--------------------------------

### Using Automation Tactics with calc

Source: https://lean4.dev/tactics/advanced/calc

Shows how to use automation tactics like `ring` and `omega` within `calc` steps for polynomial identities and integer arithmetic. It also includes an example of a single step proof using `by ring`.

```lean
-- calc with ring, omega, simp
example (a b : Int) : (a + b)^2 = a^2 + 2*a*b + b^2 := calc
  (a + b)^2 = (a + b) * (a + b) := by ring
  _ = a*a + a*b + b*a + b*b := by ring
  _ = a^2 + 2*a*b + b^2 := by ring

-- Or just one step with ring
example (a b : Int) : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring

-- calc is for when you want to show the reasoning
example (n : Nat) (h : n > 5) : n + 10 > 15 := calc
  n + 10 > 5 + 10 := by omega
  _ = 15 := by rfl
  _ ≥ 15 := by omega
```

--------------------------------

### When rfl Fails: Examples

Source: https://lean4.dev/tactics/core/rfl

Illustrates scenarios where `rfl` fails because the equality requires reasoning beyond simple computation. These examples typically involve unknown variables or properties that need lemmas or induction.

```Lean
-- example : a + b = b + a := rfl  
-- ❌ Fails! Lean doesn't know what a and b are, can't compute
-- example : n + 0 = n := rfl
-- ❌ Fails for arbitrary n (works for specific n like 5)
-- example : n * 1 = n := rfl
-- ❌ Fails! Requires induction to prove for all n
-- example : List.reverse (List.reverse xs) = xs := rfl
-- ❌ Fails! Can't compute without knowing xs
```

--------------------------------

### Boolean Negation Property

Source: https://lean4.dev/tactics/core/cases-induction

Example demonstrating `cases` for proving a property about boolean negation.

```Lean
example (b : Bool) : !!b = b := by
  cases b with
  | true => rfl
  | false => rfl
```

--------------------------------

### Prove Universals with intro

Source: https://lean4.dev/tactics/core/intro

Use 'intro' to introduce an arbitrary variable x when the goal is a universal quantification (∀ x, P x), making x available in the hypotheses.

```lean
example : ∀ n : Nat, n = n := by
  intro n
  -- Before: ⊢ ∀ n : Nat, n = n
  -- After:  n : Nat ⊢ n = n
  rfl

example : ∀ a b : Nat, a + b = b + a := by
  intro a b
  -- a b : Nat ⊢ a + b = b + a
  exact Nat.add_comm a b
```

--------------------------------

### Get Current Working Directory in Lean

Source: https://lean4.dev/language/effects/io

Retrieves and prints the current working directory of the program.

```lean
def showCwd : IO Unit :=
  do
  let cwd ← IO.currentDir
  IO.println s!"Current directory: {cwd}"
```

--------------------------------

### Linearity Constraints in linarith

Source: https://lean4.dev/tactics/mathlib/linarith

Illustrates what constitutes 'linear' expressions for linarith, showing valid and invalid examples.

```lean
import Mathlib.Tactic.Linarith

-- ✅ Linear: coefficients are constants
example (x y : Int) (h : 3*x + 2*y ≤ 10) (hx : x ≥ 0) (hy : y ≥ 0) : x ≤ 3 := by
  linarith

-- ✅ Subtraction and negation are fine
example (a b : Int) (h : a ≤ b) : -b ≤ -a := by linarith

-- ❌ Non-linear: variable times variable
-- example (x y : Int) : x * y = y * x := by linarith  -- Fails!

-- ❌ Non-linear: squaring
-- example (x : Int) : x^2 ≥ 0 := by linarith  -- Fails!
```

--------------------------------

### Search for Lemmas with exact? and apply?

Source: https://lean4.dev/tactics/core/exact-apply

Use 'exact?' or 'apply?' tactics when unsure which lemma to use. These tactics search Lean's library for applicable lemmas and suggest possible solutions.

```lean
example (n : Nat) : n + 0 = n :=
  exact?
```

```lean
example (a b : Nat) : a + b = b + a :=
  apply?
```

--------------------------------

### Providing Custom Lemmas to `simp`

Source: https://lean4.dev/tactics/core/simp

Pass additional hypotheses or lemmas in brackets to `simp` to guide its simplification process.

```lean
example (a b : Nat) (h : a = 5) : a + b = 5 + b := by
  simp [h]
```

```lean
example (f : Nat → Nat) (hf : ∀ n, f n = n + 1) : f 5 = 6 := by
  simp [hf]
```

```lean
example (a b : Nat) (h1 : a = 0) (h2 : b = 0) : a + b = 0 := by
  simp [h1, h2]
```

```lean
def triple (n : Nat) := 3 * n
example : triple 4 = 12 := by simp [triple]
```

--------------------------------

### Basic Computation with rfl

Source: https://lean4.dev/tactics/core/rfl

A basic example demonstrating the use of 'rfl' to close a goal that involves a simple computation.

```lean
1example : (3 * 4) + 2 = 14 := by
2  rfl
```

--------------------------------

### Working with Lists and Options in Lean

Source: https://lean4.dev/course/level-2

Demonstrates the usage of `List` for ordered collections and `Option` for values that might be missing. Use `#eval` to test these types.

```lean
1#check List Nat
2#check Option String
3
4#eval ([1, 2, 3] : List Nat)
5#eval (none : Option String)
6#eval (some "Lean" : Option String)
```

--------------------------------

### Get Environment Variable in Lean

Source: https://lean4.dev/language/effects/io

Retrieves the value of a specified environment variable. Handles cases where the variable is not set.

```lean
def getEnv : IO Unit :=
  do
  let path ← IO.getEnv "PATH"
  match path with
  | none => IO.println "PATH not set"
  | some p => IO.println s!"PATH = {p}"
```

--------------------------------

### Deep Dive: intro and Lambda Equivalence

Source: https://lean4.dev/tactics/core/intro

Shows that the 'intro' tactic in Lean4 constructs lambda expressions, demonstrating this equivalence with '#print'.

```lean
-- These produce the same proof term:
theorem t1 : ∀ n : Nat, n = n := by intro n; rfl
theorem t2 : ∀ n : Nat, n = n := fun n => rfl

#print t1  -- fun n => rfl
#print t2  -- fun n => rfl
```

--------------------------------

### Real-World Example: Identity Verification

Source: https://lean4.dev/tactics/mathlib/polyrith

Verifies an identity using polyrith, specifically the Sophie Germain identity with an additional constraint.

```lean
import Mathlib.Tactic.Polyrith

-- Sophie Germain identity with constraint
example (a b : ℚ) (h : a^4 + 4*b^4 = 0) (hb : b = 0) : a = 0 := by
  polyrith
```

--------------------------------

### Correcting 'Introducing when you should apply'

Source: https://lean4.dev/tactics/core/intro

Shows that 'intro' is only valid when the goal is an implication or a universal quantification; it cannot be used for other goal types.

```lean
-- If the goal is not an implication or forall, intro won't work
example (P : Prop) (hp : P) : P := by
  -- intro h  -- ❌ Error: P is not a function type
  exact hp  -- ✓ Correct
```

--------------------------------

### Good simp Lemmas

Source: https://lean4.dev/tactics/automation/simp-attrs

Examples of lemmas that are suitable for the @[simp] attribute. These lemmas simplify to a simpler form or reduce constructors.

```lean
-- Good: simplifies to a simpler form
@[simp] theorem add_zero (n : Nat) : n + 0 = n := rfl
@[simp] theorem mul_one (n : Nat) : n * 1 = n := rfl
@[simp] theorem not_not (b : Bool) : !!b = b := by cases b <;> rfl

-- Good: reduces constructors
@[simp] theorem fst_pair (a : α) (b : β) : (a, b).1 = a := rfl
@[simp] theorem head_cons (x : α) (xs : List α) : (x :: xs).head? = some x := rfl
```

--------------------------------

### Step-by-Step Reduction with #reduce

Source: https://lean4.dev/language/foundations/environment

Use the #reduce command to evaluate an expression step by step using the kernel. This is useful for proof-relevant computation and understanding reduction processes.

```lean
-- Reduce an expression step by step
5#reduce 2 + 2
```

--------------------------------

### Do Notation with Option Type

Source: https://lean4.dev/language/effects/do-notation

A simple example demonstrating the use of do notation with the Option monad to combine two string values.

```lean
def optionExample : Option String := do
  let x ← some "hello"
  let y ← some "world"
  return s!"{x} {y}"
```

--------------------------------

### Create and Build a Lean Project

Source: https://lean4.dev/

Initializes a new Lean project using the Lake build system and then builds it.

```bash
lake init my-project
cd my-project
lake build
```

--------------------------------

### Using aesop? for Proof Script Suggestions

Source: https://lean4.dev/tactics/automation/aesop

Use `aesop?` in the interactive environment to get a suggested tactic script that can be pasted into your proof.

```lean
import Mathlib.Tactic

example (P Q R : Prop) (hP : P) (hPQ : P -> Q) (hQR : Q -> R) : R := by
  aesop?
  -- The messages window shows a suggested tactic script.

```

--------------------------------

### Comparing `exact` and `apply`

Source: https://lean4.dev/tactics/core/exact-apply

Demonstrates when `exact` and `apply` can both be used, and when `apply` offers more flexibility by allowing Lean to infer arguments.

```lean
example (n : Nat) : n + 0 = n :=
  exact Nat.add_zero n
```

```lean
example (n : Nat) : n + 0 = n :=
  apply Nat.add_zero
```

```lean
example (a b c : Nat) (h : a = b) : a + c = b + c :=
  apply congrArg (· + c)
  exact h
```

--------------------------------

### StateM Monad Basics

Source: https://lean4.dev/language/effects/mutable-state

The `StateM` monad manages state explicitly. `get` reads the state, `set` writes it, and `modify` transforms it.

```lean
-- StateM σ α: computation with state of type σ, returning α
-- get: read the state
-- set: write the state
-- modify: transform the state

def counter : StateM Nat Nat := do
  let n ← get        -- Read current state
  set (n + 1)        -- Update state
  return n           -- Return old value

-- Run with initial state
#eval counter.run 0   -- (0, 1) -- returned 0, new state is 1
#eval counter.run 10  -- (10, 11)
```

--------------------------------

### Proving Conjunction (P ∧ Q) in Lean

Source: https://lean4.dev/tactics/intro/propositions-types

Shows how to prove a conjunction (P ∧ Q) in Lean, given individual proofs for P and Q. This uses the `And.intro` constructor.

```lean
example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  exact And.intro hp hq
```

--------------------------------

### Building Collections with let mut

Source: https://lean4.dev/language/effects/mutable-state

Build collections by starting with an empty list and appending elements, particularly useful within `for` loops.

```lean
1def evens (xs : List Nat) : List Nat := Id.run do
2  let mut result : List Nat := []
3  for x in xs do
4    if x % 2 == 0 then
5      result := result ++ [x]
6  return result
7
8#eval evens [1, 2, 3, 4, 5, 6]  -- [2, 4, 6]
```

--------------------------------

### Creating and Manipulating Lists in Lean4

Source: https://lean4.dev/language/data-modeling/collections

Demonstrates list creation using bracket syntax, prepending with '::', concatenation with '++', and common list operations like length, head, tail, reverse, take, and drop.

```lean
1-- Create lists with bracket syntax
2def nums : List Nat := [1, 2, 3, 4, 5]
3def empty : List String := []
4
5-- Prepend with :: (cons)
6def moreNums := 0 :: nums  -- [0, 1, 2, 3, 4, 5]
7
8-- Concatenate with ++
9def combined := [1, 2] ++ [3, 4]  -- [1, 2, 3, 4]
10
11-- Common operations
12#eval nums.length        -- 5
13#eval nums.head?         -- some 1
14#eval nums.tail?         -- some [2, 3, 4, 5]
15#eval nums.reverse       -- [5, 4, 3, 2, 1]
16#eval nums.take 3        -- [1, 2, 3]
17#eval nums.drop 2        -- [3, 4, 5]
```

--------------------------------

### Simp with Hypothesis

Source: https://lean4.dev/tactics/core/simp

Use `simp` with a hypothesis by listing it in square brackets to apply it during simplification. This example uses a hypothesis `h : n = 3`.

```lean
example (n : Nat) (h : n = 3) : n + 0 = 3 := by
  simp [h]
```

--------------------------------

### Create a New Lake Project

Source: https://lean4.dev/language/projects/lake

Use `lake new` to scaffold a new project. Specify `exe` to create an executable project, or omit it for a library project. `lake init` can be used to initialize Lake in an existing directory.

```bash
lake new myproject
lake new myapp exe
lake init myproject
```

--------------------------------

### Nested Universals Tactic in Lean

Source: https://lean4.dev/tactics/core/intro

Illustrates proving statements with nested universal quantifiers. This example uses 'exact' to apply a hypothesis directly.

```lean
1example : ∀ (f : Nat → Nat), (∀ n, f n = n) → f 5 = 5 :=
by
  intro f hf
  -- f : Nat → Nat
  -- hf : ∀ n, f n = n
  -- ⊢ f 5 = 5
  exact hf 5

```

--------------------------------

### Best Practices: Macros and Elab Tactics

Source: https://lean4.dev/tactics/advanced/custom

Illustrates best practices for custom tactics: starting with simple macros and using `elab` for more complex logic involving goal inspection. Includes a documented `close` tactic.

```lean
-- 1. Start with macros for simple patterns
macro "intro_and_split" : tactic => 
  `(tactic| intro h; constructor)

-- 2. Use elab for logic that needs goal inspection
elab "smart_close" : tactic => do
  first
  | evalTactic (← `(tactic| rfl))
  | evalTactic (← `(tactic| assumption))
  | throwError "smart_close failed"

-- 3. Document your tactics
/-- Applies either rfl or assumption to close the goal. -/
elab "close" : tactic => ...
```

--------------------------------

### Graceful Error Handling in Tactics

Source: https://lean4.dev/tactics/advanced/custom

Implement tactics that attempt an operation and fall back to another if it fails. This example tries `rfl` and then `simp`.

```lean
import Lean
open Lean Elab Tactic

elab "try_rfl" : tactic => do
  try
    evalTactic (← `(tactic| rfl))
  catch _ =>
    logInfo "rfl failed, trying simp"
    evalTactic (← `(tactic| simp))
```

--------------------------------

### Fetch and Build Dependencies

Source: https://lean4.dev/language/projects/lake

After adding new dependencies to your `lakefile.lean`, run `lake update` to fetch them, followed by `lake build` to compile your project with the new dependencies.

```bash
lake update
lake build
```

--------------------------------

### Do Notation with IO Type (Side Effects)

Source: https://lean4.dev/language/effects/do-notation

An example of using do notation for sequencing IO actions, such as printing to the console and reading user input.

```lean
def greet : IO Unit := do
  IO.println "What's your name?"
  let name ← IO.getLine
  IO.println s!"Hello, {name}!"
```

--------------------------------

### Instance Priority with High and Low Priority

Source: https://lean4.dev/language/type-classes/instances

Demonstrates how instance priority can be controlled using `priority := high` and `priority := low`. Higher priority instances are tried first.

```lean
-- Lower number = higher priority (tried first)
instance (priority := high) : ToString Bool where
  toString b := if b then "yes" else "no"

instance (priority := low) : ToString Bool where
  toString b := if b then "1" else "0"

-- The high priority instance wins
#eval toString true  -- "yes"
```

--------------------------------

### Basic Simp Usage

Source: https://lean4.dev/tactics/core/simp

Use the `simp` tactic to automatically simplify goals. This example demonstrates closing a goal involving list concatenation and identity.

```lean
example (xs : List Nat) : [] ++ xs ++ [] = xs := by
  simp
```

--------------------------------

### Prove Implications with intro

Source: https://lean4.dev/tactics/core/intro

Use 'intro' to assume the premise P when the goal is P → Q, allowing you to then prove Q.

```lean
example : True → True := by
  intro h
  -- Before: ⊢ True → True
  -- After:  h : True ⊢ True
  trivial

example (P : Prop) : P → P := by
  intro hp
  -- hp : P ⊢ P
  exact hp
```

--------------------------------

### Existential Proposition Examples in Lean

Source: https://lean4.dev/tactics/intro/propositions-types

Demonstrates how to define and construct existential propositions (∃) in Lean, which require a witness and a proof that the witness satisfies the predicate.

```lean
example : ∃ n : Nat, n > 5 := ⟨10, by decide⟩
```

```lean
example : ∃ n : Nat, n + n = 10 := ⟨5, rfl⟩
```

```lean
example : ∃ s : String, s.length = 5 := ⟨"hello", rfl⟩
```

--------------------------------

### Basic linarith Usage with Inequalities and Equalities

Source: https://lean4.dev/tactics/mathlib/linarith

Shows how linarith proves basic inequalities, equalities, and works with different integer constraints.

```lean
import Mathlib.Tactic.Linarith

-- Basic inequalities
example (x y : Int) (h1 : x < y) (h2 : y < x + 2) : y = x + 1 := by
  linarith

example (a b c : Int) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by
  linarith

example (x : Int) (h : x > 0) : x ≥ 1 := by
  linarith

-- Works with equalities too
example (a b : Int) (h1 : a ≤ b) (h2 : b ≤ a) : a = b := by
  linarith
```

--------------------------------

### Termination Proof for Countdown

Source: https://lean4.dev/tactics/automation/termination

This example provides a termination measure for a simple recursive function `countdown`. The `termination_by` clause specifies that `n` is the measure that decreases.

```lean
def countdown : Nat → Nat
  | 0 => 0
  | n + 1 => countdown n
termination_by n
```

--------------------------------

### ext with Patterns

Source: https://lean4.dev/tactics/mathlib/ext

Introduce and pattern-match variables using `ext` with patterns, or use wildcards for components that are not relevant to the proof.

```lean
import Mathlib.Tactic.Ext

-- You can name and pattern-match the introduced variable
example : (fun p : Nat × Nat => p.1 + p.2) = (fun p => p.2 + p.1) := by
  ext ⟨a, b⟩
  ring
```

```lean
-- Or use wildcards
example : (fun _ : Nat => 0) = (fun _ => 0) := by
  ext _
  rfl
```

--------------------------------

### Nested Binds Without Do Notation

Source: https://lean4.dev/language/effects/do-notation

This example demonstrates the complexity of chaining Option-returning functions without do notation, leading to deeply nested match expressions.

```lean
1def lookup (key : String) (env : List (String × Nat)) : Option Nat :=
  env.lookup key

-- Without do notation: deeply nested
def compute (env : List (String × Nat)) : Option Nat :=
  match lookup "x" env with
  | none => none
  | some x => match lookup "y" env with
    | none => none
    | some y => match lookup "z" env with
      | none => none
      | some z => some (x + y + z)
```

--------------------------------

### Exercise: Import and Use `ring` Tactic

Source: https://lean4.dev/tactics/mathlib/intro

This exercise demonstrates importing `Mathlib.Tactic` and applying the `ring` tactic to prove a simple algebraic identity.

```lean
import Mathlib.Tactic

example (x : Int) : (x + 1)^2 = x^2 + 2*x + 1 := by
  ring
```

--------------------------------

### Common Patterns with Linarith

Source: https://lean4.dev/tactics/mathlib/linarith

Presents common usage patterns for `linarith`, including absolute value bounds, sandwich theorem setup, and interval arithmetic.

```lean
import Mathlib.Tactic.Linarith

-- Absolute value bounds (given expanded form)
example (x : Int) (h1 : -5 ≤ x) (h2 : x ≤ 5) : -5 ≤ x ∧ x ≤ 5 := by
  constructor <;> linarith

-- Sandwich theorem setup
example (a b c : Int) (h1 : a ≤ b) (h2 : b ≤ c) (h3 : a = c) : b = a := by
  linarith

-- Interval arithmetic
example (x y : Int) (hx : 1 ≤ x) (hx' : x ≤ 3) (hy : 2 ≤ y) (hy' : y ≤ 4) 
    : 3 ≤ x + y := by linarith
```

--------------------------------

### Manage Lean Toolchains with Elan

Source: https://lean4.dev/language/projects/lake

Elan is Lean's version manager. Use it to install, list, and set different Lean toolchain versions for your projects.

```bash
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
elan show
elan install leanprover/lean4:v4.3.0
elan default leanprover/lean4:stable
```

--------------------------------

### Deep Dive: Unification with apply

Source: https://lean4.dev/tactics/core/exact-apply

Illustrates how the 'apply' tactic works by unifying a lemma's conclusion with the current goal. It shows how Lean determines the necessary arguments for the lemma.

```lean
-- Goal: 5 + 0 = 5
-- Lemma: Nat.add_zero : ∀ n, n + 0 = n

-- apply Nat.add_zero unifies:
-- n + 0 = n  with  5 + 0 = 5
-- Solution: n = 5
```

--------------------------------

### Exercise: Script to Show Lean Version

Source: https://lean4.dev/language/projects/lake

Create a custom script that reads the `lean-toolchain` file and prints the project's Lean version.

```lean
script showVersion do
  IO.println s!"Lean toolchain: "{(← IO.FS.readFile "lean-toolchain").trim}
```

--------------------------------

### Using simp with Additional Lemmas

Source: https://lean4.dev/tactics/core/simp

You can provide additional lemmas to `simp` in brackets, like `simp [h]`, to guide the simplification process beyond the default lemmas.

```lean
example (a : Nat) (h : a = 5) : a + 0 = 5 := by simp [h]
```

--------------------------------

### Recursion vs. Iteration with `for` loop sugar

Source: https://lean4.dev/language/control-flow/recursion

Shows how Lean's `for` loops in `do` notation are syntactic sugar for explicit recursion. This example sums elements of an array.

```Lean
-- Imperative-looking but actually recursive
def sumArray (arr : Array Nat) : Nat := Id.run do
  let mut total := 0
  for x in arr do
    total := total + x
  return total

-- Equivalent explicit recursion
def sumArray' (arr : Array Nat) : Nat :=
  arr.foldl (· + ·) 0

#eval sumArray #[1, 2, 3, 4, 5]  -- 15
```

--------------------------------

### Exercise 1: Chain Rewrites

Source: https://lean4.dev/tactics/core/rw

Simplifies a goal by applying two `Nat.add_zero` rewrites sequentially.

```lean
example (n : Nat) : n + 0 + 0 = n := by
  rw [Nat.add_zero, Nat.add_zero]
```