/lean4

Domain-Specific Patterns for Lean 4

TLDR

Purpose: Quick reference for common proof patterns and tactics across mathematical domains.

When to use: When working in a specific domain (measure theory, analysis, algebra, etc.) and need proven patterns for common tasks.

Coverage: Measure theory (12 patterns), analysis & topology (3 patterns), geometry (8 patterns), algebra (3 patterns), number theory (3 patterns), plus cross-domain tactics.

For deep measure theory patterns (sub-σ-algebras, conditional expectation, type class errors): See references/measure-theory.md

Quick Reference by Domain

Measure Theory & Probability (12 Patterns)

Common tactics: measurability, positivity, ae_of_all, filter_upwards

Analysis & Topology (3 Patterns)

Common tactics: continuity, fun_prop

Geometry (8 Patterns)

Common tactics: norm_num (for angle comparisons), linarith (for angle algebra)

Algebra (3 Patterns)

Common tactics: ring, field_simp, group

Number Theory & Combinatorics (3 Patterns)

Common tactics: linarith, norm_num, omega

Cross-Domain

Essential tactics: simp only, by_cases, rcases, rw, ext, apply, exact, refine, grind (for mixed-constraint cleanup)

Equality via uniqueness: Works across all domains (measures, functions, homs)

Measure Theory & Probability

Pattern 1: Proving Integrability

Golden rule: bounded + measurable + finite measure = integrable

lemma integrable_of_bounded_measurable
    [IsFiniteMeasure μ] {f : X → ℝ}
    (h_meas : Measurable f)
    (h_bound : ∃ C, ∀ x, ‖f x‖ ≤ C) :
    Integrable f μ := by
  obtain ⟨C, hC⟩ := h_bound
  exact Integrable.of_bound h_meas.aestronglyMeasurable C (ae_of_all _ hC)

Key variations:

• AE bound: Use AEMeasurable and ∀ᵐ x ∂μ, ‖f x‖ ≤ C
• Indicator: hf.indicator hA when hf : Integrable f μ

Pattern 2: Conditional Expectation Equality

Uniqueness theorem: To show μ[f | m] = g, prove all three:

1. g is m-measurable
2. g is integrable
3. ∀ B (m-measurable set): ∫ x in B, g x ∂μ = ∫ x in B, f x ∂μ

lemma condExp_eq_of_integral_eq
    {f g : Ω → ℝ} (hf : Integrable f μ)
    (hg_meas : Measurable[m] g)
    (hg_int : Integrable g μ)
    (h_eq : ∀ s, MeasurableSet[m] s → ∫ x in s, g x ∂μ = ∫ x in s, f x ∂μ) :
    μ[f | m] =ᵐ[μ] g := by
  symm
  exact ae_eq_condExp_of_forall_setIntegral_eq (μ := μ) (m := m) hm
    hf hg_meas hg_int h_eq

Pattern 3: Sub-σ-Algebras and Type Class Management

Critical issues:

• Binder order: instance parameters before plain parameters
• Never use ‹_› for ambient space (resolves incorrectly)
• Check whether trimmed-measure instances already synthesize before adding any; freeze with plain have if needed (haveI only inlines — irrelevant in a proof)

-- ✅ Correct pattern
lemma my_condExp_lemma {Ω : Type*} {m₀ : MeasurableSpace Ω}
    {μ : Measure Ω} [IsFiniteMeasure μ]
    {m : MeasurableSpace Ω} (hm : m ≤ m₀) : Result := by
  -- `IsFiniteMeasure (μ.trim hm)` is a Mathlib instance; σ-finiteness follows.
  -- Optional freeze (plain `have` registers the instance):
  have : SigmaFinite (μ.trim hm) := inferInstance
  -- Now call mathlib lemmas

For complete coverage: See references/measure-theory.md for sub-σ-algebra patterns, condExpWith, debugging type class errors, and binder order requirements.

Pattern 4: Almost Everywhere Properties

From universal to ae:

have h : ∀ x, P x := ...
have h_ae : ∀ᵐ x ∂μ, P x := ae_of_all _ h

Combining ae properties:

filter_upwards [h1, h2] with x hP hQ
-- Now have: ∀ᵐ x ∂μ, P x ∧ Q x

ae equality reasoning:

-- Transitivity
h1.trans h2  -- f =ᵐ[μ] g → g =ᵐ[μ] h → f =ᵐ[μ] h

-- Substitution
hf.congr h  -- Integrable f μ → f =ᵐ[μ] g → Integrable g μ

Pattern 5: Filtrations and Martingales

def Filtration (f : ℕ → MeasurableSpace Ω) : Prop :=
  Monotone f ∧ ∀ n, f n ≤ m₀

def Adapted (X : ℕ → Ω → ℝ) (f : ℕ → MeasurableSpace Ω) : Prop :=
  ∀ n, Measurable[f n] (X n)

def IsMartingale (X : ℕ → Ω → ℝ) (f : ℕ → MeasurableSpace Ω) : Prop :=
  Adapted X f ∧ (∀ n, Integrable (X n) μ) ∧
  ∀ m n, m ≤ n → μ[X n | f m] =ᵐ[μ] X m

Pattern 6: Product Measures and Independence

-- Infinite product via Ionescu-Tulcea
noncomputable def productMeasure (ν : Measure α) : Measure (ℕ → α) :=
  Measure.pi (fun _ ↦ ν)

lemma independent_of_product :
    ∀ n m, n ≠ m →
    IndepFun (fun ω ↦ ω n) (fun ω ↦ ω m) (productMeasure ν) := by
  sorry

Pattern 7: Managing Section Variables with omit

Exclude section variables from specific lemmas:

section IntegrationHelpers
variable [MeasurableSpace Ω] {μ : Measure Ω}

-- This lemma doesn't need MeasurableSpace Ω
omit [MeasurableSpace Ω] in
lemma abs_integral_mul_le_L2 [IsFiniteMeasure μ] {f g : Ω → ℝ}
    (hf : MemLp f 2 μ) (hg : MemLp g 2 μ) :
    |∫ x, f x * g x ∂μ| ≤ ... := by sorry

end IntegrationHelpers

Critical: omit [...] in must appear before the docstring. The rule for everything that can precede a declaration, and the unexpected token 'omit' error you get when the order is wrong, live in compilation-errors.md § 21.

When to use: Lemma doesn't use section variable, or variable causes unwanted instance requirements.

Pattern 8: Automating Measurability Proofs

Manual vs automated:

-- ❌ Manual: verbose
lemma measurable_projection {n : ℕ} :
    Measurable (fun (x : ℕ → α) ↦ fun (i : Fin n) ↦ x i.val) := by
  refine measurable_pi_lambda _ (fun i ↦ ?_)
  exact measurable_pi_apply i.val

-- ✅ Automated: clean
lemma measurable_projection {n : ℕ} :
    Measurable (fun (x : ℕ → α) ↦ fun (i : Fin n) ↦ x i.val) := by
  measurability

Make lemmas discoverable:

@[measurability]
lemma measurable_shiftSeq {d : ℕ} : Measurable (shiftSeq (β:=β) d) := by
  measurability

For function compositions:

-- Use fun_prop with measurability discharger
have h : Measurable (fun ω ↦ fun i ↦ X (k i) ω) := by
  fun_prop (disch := measurability)

Combine attributes for maximum automation:

@[measurability, fun_prop]
lemma measurable_myFunc : Measurable myFunc := by measurability

When automation works well:

• ✅ Product types and compositions
• ✅ Pi-type projections
• ✅ Coordinate permutations
• ✅ After adding @[measurability] attributes

When automation doesn't work:

• ⚠️ Complex set operations (can timeout)
• ⚠️ Custom definitions unknown to fun_prop
• Solution: Break into smaller steps or use direct proof

Real-world results: Simplified 33 proofs, eliminated ~90 lines of boilerplate.

Pattern 9: Implicit vs Explicit Parameters

Core principle: {param} when inferrable, (param) when primary data or not inferrable.

Use implicit {param} when:

-- ✅ n inferrable from S
def prefixCylinder {n : ℕ} (S : Set (Fin n → α)) : Set (ℕ → α)

-- ✅ n inferrable from c
lemma l2_bound {n : ℕ} {c : Fin n → ℝ} (σSq ρ : ℝ) : ...

Keep explicit (param) when:

-- ✅ Primary data
theorem deFinetti (μ : Measure Ω) (X : ℕ → Ω → α) : ...

-- ✅ Used in body, not types
def shiftedCylinder (n : ℕ) (F : Ω[α] → ℝ) : Ω[α] → ℝ :=
  fun ω ↦ F ((shift^[n]) ω)

-- ✅ In return type
lemma foo (n : ℕ) : Fin n → α := ...

When in doubt, keep explicit. See mathlib-style.md for conventions.

Pattern 10: Measurable Structure Must Match Goal

When using Measurable.const_mul with sums, structure must match goal's parenthesization.

-- ❌ WRONG: constant inside each term
have h : Measurable (fun ω ↦ (1/(m:ℝ)) * ∑ k, f k ω) :=
  Finset.measurable_sum _ (fun k _ ↦ Measurable.const_mul ...)
-- Applies const_mul to EACH TERM - wrong variable binding!

-- ✅ CORRECT: constant wraps entire sum
have h : Measurable (fun ω ↦ (1/(m:ℝ)) * ∑ k, f k ω) :=
  Measurable.const_mul (Finset.measurable_sum _ (fun k _ ↦ ...)) _
-- const_mul wraps whole sum, matching goal structure

Key: Match goal parenthesization: c * (∑ ...) not ∑ (c * ...)

Pattern 11: Integrable.of_bound Type Matching

Bound expression in measurability hypothesis must match canonical form after simp.

-- ❌ WRONG: Definition uses 1/(m:ℝ) but goal has (m:ℝ)⁻¹ after simp
have h_meas : Measurable (fun ω ↦ 1/(m:ℝ) * ∑ i, f i ω) := ...
apply Integrable.of_bound h_meas.aestronglyMeasurable 1
filter_upwards with ω; simp [Real.norm_eq_abs]
-- Type mismatch: goal has (m:ℝ)⁻¹ but h_meas has 1/(m:ℝ)

-- ✅ CORRECT: Use canonical form (m:ℝ)⁻¹ from start
have h_meas : Measurable (fun ω ↦ (m:ℝ)⁻¹ * ∑ i, f i ω) := ...
apply Integrable.of_bound h_meas.aestronglyMeasurable 1
filter_upwards with ω; simp [Real.norm_eq_abs]
-- Matches exactly after simp!

Rule: Use canonical forms: (m:ℝ)⁻¹ not 1/(m:ℝ). See calc-patterns.md.

Pattern 12: Pointwise Inequalities

Use intro ω for simple pointwise proofs:

-- ❌ WRONG: filter_upwards doesn't unfold for simple inequalities
filter_upwards with ω
exact abs_sub_le _ _ _
-- Error: type mismatch in implicit EventuallyEq form

-- ✅ CORRECT: intro for simple pointwise
intro ω
exact abs_sub_le _ _ _
-- Works: explicit inequality with ω

When to use:

• intro ω: Simple pointwise inequalities, just applying lemmas
• filter_upwards: Combining multiple ae conditions, measure theory structure

Common Measure Theory Tactics

measurability    -- Prove measurability automatically
positivity       -- Prove positivity of measures/integrals
ae_of_all        -- Universal → ae
filter_upwards   -- Combine ae properties

Automation philosophy:

• ✅ Use for: boilerplate (measurability), trivial arithmetic (omega/linarith)
• ❌ Don't hide: key mathematical insights, proof architecture, non-obvious lemma applications

Analysis & Topology

Pattern 1: Continuity Proofs

-- From preimage of open sets
lemma continuous_of_isOpen_preimage
    {f : X → Y} (h : ∀ U, IsOpen U → IsOpen (f ⁻¹' U)) :
    Continuous f := by
  rw [continuous_def]; exact h

-- Using automation
lemma continuous_comp_add :
    Continuous (fun (p : ℝ × ℝ) ↦ p.1 + p.2) := by
  continuity

Pattern 2: Compactness Arguments

-- Min/max on compact sets
example {K : Set ℝ} (hK : IsCompact K) (hne : K.Nonempty) :
    ∃ x ∈ K, ∀ y ∈ K, f x ≤ f y :=
  IsCompact.exists_isMinOn hK hne (continuous_id.comp continuous_f)

Pattern 3: Limits via Filters

-- ε-δ criterion
lemma tendsto_of_forall_eventually
    (h : ∀ ε > 0, ∀ᶠ n in atTop, ‖x n - L‖ < ε) :
    Tendsto x atTop (𝓝 L) := by
  rw [Metric.tendsto_atTop]; exact h

Common tactics: continuity, fun_prop

Geometry

Pattern 1: Betweenness via Line Parameters

Key lemma: Sbtw.sbtw_lineMap_iff characterizes strict betweenness: Sbtw ℝ A (lineMap A B s) B ↔ A ≠ B ∧ s ∈ Set.Ioo 0 1. Eliminates manual field-by-field Sbtw proofs - parameter in (0,1) gives betweenness, then Sbtw.angle₁₂₃_eq_pi yields straight angle.

-- Two-liner instead of 50+ lines
have h_sbtw : Sbtw ℝ A H B := Sbtw.sbtw_lineMap_iff.mpr ⟨h_ne_AB, hs_in_Ioo⟩
have : ∠ A H B = π := h_sbtw.angle₁₂₃_eq_pi

Pattern 2: Triangle Angle Sum

angle_add_angle_add_angle_eq_pi gives sum at specified vertex. Order adapts to input - no canonical form fighting. Use directly without rearrangement.

have angle_sum : ∠ B H C + ∠ H C B + ∠ C B H = π := angle_add_angle_add_angle_eq_pi C ⟨h_ne_BC, h_ne_CH, h_ne_HB⟩

Pattern 3: Segment Membership to Betweenness

Replace parametric obtains with direct mathlib conversion. mem_segment_iff_wbtw converts x ∈ segment ℝ A B to Wbtw ℝ A x B in one step.

-- ❌ BAD: 70 lines extracting parameters, proving strict bounds
obtain ⟨s, hs_ge, hs_le, hH_eq⟩ := h_H_on_AB
-- ... 50+ lines proving 0 < s < 1 from H ≠ A, H ≠ B ...
have : Sbtw ℝ A H B := ...

-- ✅ GOOD: 1 line
have : Sbtw ℝ A H B := ⟨mem_segment_iff_wbtw.mp h_H_on_AB, h_H_ne_A, h_H_ne_B⟩

Pattern 4: Collinearity from Betweenness

Direct collinearity proof. Wbtw.mem_affineSpan proves G ∈ affineSpan ℝ {A, C} from Wbtw ℝ A G C without parametric machinery.

-- ❌ BAD: Manual lineMap construction (10+ lines)
obtain ⟨t, ht_ge, ht_le, hG_eq⟩ := h_G_on_AC
have : G ∈ affineSpan ℝ {A, C} := by
  rw [hG_eq]
  -- Convert to lineMap, prove membership...

-- ✅ GOOD: Direct
have : G ∈ affineSpan ℝ {A, C} := (mem_segment_iff_wbtw.mp h_G_on_AC).mem_affineSpan

Pattern 5: Angle Proofs from Betweenness

Combine with Pattern 3 for instant angle proofs. Chain mem_segment_iff_wbtw → Sbtw → Sbtw.angle₁₂₃_eq_pi.

have angle_AHB_eq_pi : ∠ A H B = π :=
  Sbtw.angle₁₂₃_eq_pi ⟨mem_segment_iff_wbtw.mp h_H_on_AB, h_H_ne_A, h_H_ne_B⟩

Pattern 6: Infrastructure Wrappers for Missing Lemmas

Create thin wrappers with documented sorries. When mathlib lacks domain-specific lemmas, isolate missing pieces with clear documentation and alternatives.

namespace AngleTools
/-- Right subtraction: from `∠XTY = π`, get `∠TZY = ∠XZY − ∠XZT`.
    Missing mathlib lemma for angle splitting at external vertex.
    Alternative: Use Module.Oriented with oangle_add (complex). -/
lemma sub_right (X T Y Z : P) (hπ : ∠ X T Y = Real.pi) :
    ∠ T Z Y = ∠ X Z Y - ∠ X Z T := by
  sorry
end AngleTools

-- Usage: Clean structure throughout proof
have angle_ABD : ∠ A B D = π / 3 := by
  calc ∠ A B D = ∠ A B C - ∠ D B C := AngleTools.sub_right A D C B angle_ADC_eq_pi
    _ = 4 * π / 9 - π / 9 := by rw [angle_ABC, h_DBC]
    _ = π / 3 := by ring

Benefits: Sorry is isolated, strategy documented, proof structure maintainable.

Pattern 7: Deep Context Timeouts

After ~1000 lines, standard lemmas can timeout. Use cheaper alternatives or document strategy.

Technique A: Non-Degeneracy via angle_self_right

Problem: In deep contexts, angle_self_of_ne times out in contradiction proofs.

Key insight: The unoriented angle ∠ P X X = π/2 (not 0). This comes from angle_self_right, a cheap [simp] lemma that avoids the expensive angle_self_of_ne.

-- General pattern: Given h_angle : ∠ P X Y = α where α ≠ π/2
-- Goal: Prove Y ≠ X

-- Example: h_angle_CBD : ∠ C B D = π/9, prove D ≠ B
have h_DB_ne : D ≠ B := by
  intro h_eq
  rw [h_eq] at h_angle_CBD
  -- Now have: ∠ C B B = π/9

  -- Key step: Get the actual value of degenerate angle
  have angle_CBB : ∠ C B B = ((π / 2 : ℝ) : Real.Angle) := by
    simp [EuclideanGeometry.angle_self_right]  -- Fast! [simp] lemma

  -- Derive the impossible equation: π/9 = π/2
  have : ((π / 9 : ℝ) : Real.Angle) = ((π / 2 : ℝ) : Real.Angle) := by
    rw [← h_angle_CBD, angle_CBB]

  exact pi_div_nine_ne_pi_div_two this  -- Use helper lemma

Helper lemma pattern (prove once using toReal_injective):

lemma pi_div_nine_ne_pi_div_two :
    ((π / 9 : ℝ) : Real.Angle) ≠ ((π / 2 : ℝ) : Real.Angle) := by
  rw [← Real.Angle.toReal_injective.ne_iff]
  -- Convert to -π < x ≤ π range
  have h_range1 : -π < π/9 ∧ π/9 ≤ π := by constructor <;> linarith [Real.pi_pos]
  have h_range2 : -π < π/2 ∧ π/2 ≤ π := by constructor <;> linarith [Real.pi_pos]
  rw [Real.Angle.toReal_coe_eq_self_iff.mpr h_range1]
  rw [Real.Angle.toReal_coe_eq_self_iff.mpr h_range2]
  linarith [Real.pi_pos]

Why this works:

• angle_self_right is marked [simp], so simp resolves it instantly (no timeout)
• Avoids expensive angle_self_of_ne which requires non-degeneracy proof
• Works entirely in Real.Angle (quotient group), no toReal unwrapping
• Helper lemmas (like pi_div_nine_ne_pi_div_two) proved once, reused everywhere

Applicability: Works when α ≠ π/2. For most angle values this is true (π/9, π/3, π/4, 2π/3, etc.).

General pattern: To prove Y ≠ X when you know ∠ P X Y = α:

1. Assume Y = X for contradiction
2. Substitute: get ∠ P X X = α
3. Apply angle_self_right: get ∠ P X X = π/2
4. Derive impossible equation: α = π/2 in Real.Angle
5. Apply contradiction helper lemma that proves α ≠ π/2

Technique B: Document and Continue

When no cheap alternative exists, document the strategy:

have h_DB_ne : D ≠ B := by
  -- If D = B, then ∠CBD = ∠CBB = π/2 by angle_self_right,
  -- contradicting h_angle_CBD : ∠CBD = π/9.
  -- Elaboration times out in deep context (>1000 lines)
  sorry

When to use: Proof >1000 lines, simple logic times out. Try cheap lemmas first (Technique A), then document strategy.

Pattern 8: Angle Arithmetic at Quotient Level

Work with Real.Angle's group structure directly. Don't unwrap to ℝ via toReal for arithmetic—the quotient handles algebra automatically.

Key insight: Real.Angle ≃ ℝ / (2π) is a group. Addition, subtraction, and linear algebra work directly at the quotient level. Only use toReal when you need real number properties (like < π), not for algebra.

-- ❌ BAD: Unwrap to ℝ, prove bounds, wrap back up
have E : ∠ABD + π/9 = 4*π/9 := split
have toReal_E : (∠ABD).toReal + (π/9).toReal = (4*π/9).toReal := ... -- need bound proofs!
have result : ∠ABD = π/3 := add_right_cancel ... -- manual group operation

-- ✅ GOOD: Use group operations directly
calc ∠ABD = (4*π/9 : Real.Angle) - (π/9 : Real.Angle) := by linarith [split]
  _ = π/3 := by ring

Why linarith works: It operates on ANY additive group, not just ℝ. Given a + b = c in any group, linarith derives a = c - b, b = c - a, etc.

Type coercion spam = code smell: If you need ((π/3 : ℝ) : Real.Angle) everywhere, you're fighting the type system. Let Lean's coercion work—write 4*π/9 - π/9 and Lean infers Real.Angle from context.

Separation of concerns:

• Group level (Real.Angle): +, -, equality via linarith
• Arithmetic level (ℝ component): 4*π/9 - π/9 = π/3 via ring

-- Clean pattern
calc (x : Real.Angle)
    = y - z := by linarith [group_fact]  -- group algebra
  _ = a - b := by rw [substitutions]     -- still in quotient
  _ = c := by ring                        -- arithmetic on ℝ component

Infrastructure lemma strategy: One infrastructure admit (e.g., angle_split_external) with clean pattern everywhere beats many scattered admits at call sites. Infrastructure admits are well-isolated, documented, and can be proven later without touching call sites.

Common tactics: norm_num (for angle comparisons), linarith (for angle algebra)

Algebra

Pattern 1: Building Algebraic Instances

-- Compositional
instance : CommRing (Polynomial R) := inferInstance

-- Manual for custom types
instance : Ring MyType := {
  add := my_add,
  add_assoc := my_add_assoc,
  -- ... all required fields
}

Pattern 2: Quotient Constructions

-- Ring homomorphism from quotient
lemma quotient_ring_hom (I : Ideal R) : RingHom R (R ⧸ I) := by
  refine { toFun := Ideal.Quotient.mk I,
           map_one' := rfl,
           map_mul' := fun x y ↦ rfl,
           map_zero' := rfl,
           map_add' := fun x y ↦ rfl }

Pattern 3: Universal Properties

-- Unique morphism via universal property
lemma exists_unique_hom (h : ...) : ∃! φ : A →+* B, ... := by
  use my_homomorphism
  constructor
  · -- Prove it satisfies property
  · -- Prove uniqueness
    intro ψ hψ; ext x; sorry

Common tactics: ring, field_simp, group

Number Theory & Combinatorics

Pattern 1: Induction

lemma property_of_list (l : List α) : P l := by
  induction l with
  | nil => sorry  -- Base case
  | cons head tail ih => sorry  -- Inductive case with ih : P tail

Pattern 2: Divisibility

lemma dvd_example (n : ℕ) : 2 ∣ n * (n + 1) := by
  rcases Nat.even_or_odd n with h | h
  · -- n even
    obtain ⟨k, rfl⟩ := h
    use k * (2 * k + 1); ring
  · -- n odd
    obtain ⟨k, rfl⟩ := h
    use (2 * k + 1) * (k + 1); ring

Pattern 3: Complex List Counting

Key techniques:

Positional splitting: Use first/second position to decompose counting problems.

-- Example: Count pairs in list where first witness is at position i
-- Split into: (1) second witness before i, (2) second witness after i
have h := countElem_union l.take i l.drop (i+1)
-- Then count each part separately

Complementary counting: Count what's NOT in a set when direct counting is hard.

-- Total pairs - pairs_with_property = pairs_without_property
calc l.countPairs P
    = l.length.choose 2 - l.countPairs (¬P ∘₂ ·) := by ...

When to use: Proofs requiring counting list elements with complex predicates, especially when witnesses appear at multiple positions.

Common tactics: linarith, norm_num, omega

Cross-Domain Tactics

Essential for all domains:

-- Simplification
simp only [lem1, lem2]  -- Explicit lemmas (preferred)
simpa using h           -- simp then exact h

-- Case analysis
by_cases h : p          -- Split on decidable
rcases h with ⟨x, hx⟩   -- Destructure exists/and/or

-- Rewriting
rw [lemma]              -- Left-to-right
rw [← lemma]            -- Right-to-left

-- Extensionality
ext x                   -- Function equality pointwise
funext x                -- Alternative

-- Application
apply lemma             -- Apply, leaving subgoals
exact expr              -- Close goal exactly
refine template ?_ ?_   -- Apply with placeholders

Pattern: Equality via Uniqueness

Works across all domains:

To show f = g, prove both satisfy unique criterion:

lemma my_eq : f = g := by
  have hf : satisfies_property f := ...
  have hg : satisfies_property g := ...
  exact unique_satisfier hf hg

Examples:

• Measures: Equal if agree on π-system
• Conditional expectations: Equal if same integrals on all measurable sets
• Functions: Equal if continuous and agree on dense subset
• Group homomorphisms: Equal if agree on generators

Related References

• measure-theory.md - Deep dive on sub-σ-algebras, conditional expectation, type class errors
• tactics-reference.md - Comprehensive tactic catalog
• mathlib-style.md - Mathlib conventions
• calc-patterns.md - Calculation chains and canonical forms