Lean Study Group — Tactics & Proof Style

In this session of our Lean study group, we move beyond basic definitions and start actually proving things interactively in Lean.
This is where Lean begins to feel powerful.
We’ll focus on:

• Writing proofs in tactic mode
• Understanding and navigating proof states
• Using core tactics like `intro`, `apply`, `exact`, `cases`, `constructor`, `rw`, and `simp`
• Translating between tactic-style proofs and term-style proofs
• Learning how to read and respond to Lean’s error messages

Instead of passively watching proofs, we’ll work directly in the editor, stepping through proofs together and predicting what Lean will do next.
By the end of this session, you’ll be able to:

• Break complex logical goals into manageable subgoals
• Rewrite equalities confidently
• Structure proofs cleanly and intentionally
• Understand what Lean is actually asking you to prove

We’ll prove small but meaningful results involving logical connectives (`∧`, `∨`, `→`) and simple inductive types.
Prerequisites:
You should be comfortable with Lean basics (definitions, `#check`, simple proofs with `rfl`). No deep math background required.
Format:

• 20 min concept intro
• 40 min guided live proofs
• 30 min group exercises & discussion