diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean
index 20857243cc814b..bdc7c7c8981c4e 100644
--- a/Mathlib/Tactic/Common.lean
+++ b/Mathlib/Tactic/Common.lean
@@ -8,6 +8,7 @@ Authors: Kim Morrison
 import Aesop
 import Qq
 import Plausible
+-- import Canonical
 
 -- Tools for analysing imports, like `#find_home`, `#minimize_imports`, ...
 import ImportGraph.Imports
@@ -147,3 +148,5 @@ register_hint (priority := 200) omega
 register_hint (priority := 200) fun_prop
 
 end Hint
+
+-- example : True := by canonical +suggestions
diff --git a/Mathlib/Tactic/Linter/DirectoryDependency.lean b/Mathlib/Tactic/Linter/DirectoryDependency.lean
index 557a6640d6dda6..7ba00f5c69836d 100644
--- a/Mathlib/Tactic/Linter/DirectoryDependency.lean
+++ b/Mathlib/Tactic/Linter/DirectoryDependency.lean
@@ -176,6 +176,7 @@ def allowedImportDirs : NamePrefixRel := .ofArray #[
   (`MathlibTest.Header, `Plausible),
   (`MathlibTest.Header, `ProofWidgets),
   (`MathlibTest.Header, `Qq),
+  (`MathlibTest.Header, `Canonical),
   -- (`MathlibTest.Header, `Mathlib.Tactic),
   -- (`MathlibTest.Header, `Mathlib.Deprecated),
   (`MathlibTest.Header, `Batteries),
@@ -649,13 +650,14 @@ def directoryDependencyCheck (mainModule : Name) : CommandElabM (Array MessageDa
   else
     -- We always allow imports in the same directory (for each matching prefix),
     -- from `Init`, `Lean` and `Std`, as well as imports in `Aesop`, `Qq`, `Plausible`,
-    -- `ImportGraph`, `ProofWidgets` or `LeanSearchClient` (as these are imported in Tactic.Common).
+    -- `ImportGraph`, `ProofWidgets`, `LeanSearchClient` and `Canonical`
+    -- (as these are imported in Tactic.Common).
     -- We also allow transitive imports of Mathlib.Init, as well as Mathlib.Init itself.
     let initImports := (← findImports ("Mathlib" / "Init.lean")).append
       #[`Mathlib.Init, `Mathlib.Tactic.DeclarationNames]
     let exclude := [
       `Init, `Std, `Lean,
-      `Aesop, `Qq, `Plausible, `ImportGraph, `ProofWidgets, `LeanSearchClient
+      `Aesop, `Qq, `Plausible, `ImportGraph, `ProofWidgets, `LeanSearchClient, `Canonical
     ]
     let importsToCheck := imports.filter (fun imp ↦ !exclude.any (·.isPrefixOf imp))
       |>.filter (fun imp ↦ !matchingPrefixes.any (·.isPrefixOf imp))
diff --git a/Mathlib/Tactic/TacticAnalysis/Declarations.lean b/Mathlib/Tactic/TacticAnalysis/Declarations.lean
index 64f0152cc57a5a..b7b74b005bf595 100644
--- a/Mathlib/Tactic/TacticAnalysis/Declarations.lean
+++ b/Mathlib/Tactic/TacticAnalysis/Declarations.lean
@@ -8,6 +8,7 @@ import Mathlib.Tactic.ExtractGoal
 import Mathlib.Tactic.MinImports
 import Lean.Elab.Tactic.Meta
 import Lean.Elab.Command
+import Aesop
 
 /-!
 # Tactic linters
@@ -322,6 +323,18 @@ def tryAtEachStepAesop := tryAtEachStep
   fun _ _ => return ⟨TSyntax.raw <|
     mkNode `Aesop.Frontend.Parser.aesopTactic #[mkAtom "aesop", mkNullNode]⟩
 
+-- /-- Run `canonical` at every step in proofs, reporting where it succeeds. -/
+-- register_option linter.tacticAnalysis.tryAtEachStepCanonical : Bool := {
+--   defValue := false
+-- }
+
+-- @[tacticAnalysis linter.tacticAnalysis.tryAtEachStepCanonical,
+--    inherit_doc linter.tacticAnalysis.tryAtEachStepCanonical]
+-- def tryAtEachStepCanonical := tryAtEachStep
+--   -- As `canonical` isn't imported here, we construct the tactic syntax manually.
+--   fun _ _ => return ⟨TSyntax.raw <|
+--     mkNode `Mathlib.Tactic.Canonical.canonical #[mkAtom "canonical", mkNullNode]⟩
+
 /-- Run `grind +suggestions` at every step in proofs, reporting where it succeeds. -/
 register_option linter.tacticAnalysis.tryAtEachStepGrindSuggestions : Bool := {
   defValue := false
@@ -338,7 +351,19 @@ register_option linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions : Bool :=
 
 @[tacticAnalysis linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions,
    inherit_doc linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions]
-def tryAtEachStepSimpAllSuggestions := tryAtEachStep fun _ _ => `(tactic| simp_all? +suggestions)
+def tryAtEachStepSimpAllSuggestions := tryAtEachStep fun _ _ => `(tactic| try simp_all? +suggestions)
+
+-- /-- Run `canonical +suggestions` at every step in proofs, reporting where it succeeds. -/
+-- register_option linter.tacticAnalysis.tryAtEachStepCanonicalSuggestions : Bool := {
+--   defValue := false
+-- }
+
+-- @[tacticAnalysis linter.tacticAnalysis.tryAtEachStepCanonicalSuggestions,
+--    inherit_doc linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions]
+-- def tryAtEachStepCanonicalSuggestions := tryAtEachStep
+--   -- As `canonical` isn't imported here, we construct the tactic syntax manually.
+--   fun _ _ => return ⟨TSyntax.raw <|
+--     mkNode `Mathlib.Tactic.Canonical.canonical #[mkAtom "canonical", mkNullNode]⟩
 
 -- TODO: add compatibility with `rintro` and `intros`
 /-- Suggest merging two adjacent `intro` tactics which don't pattern match. -/
diff --git a/MathlibTest/canonical.lean b/MathlibTest/canonical.lean
new file mode 100644
index 00000000000000..b7cfd7f020bb16
--- /dev/null
+++ b/MathlibTest/canonical.lean
@@ -0,0 +1,46 @@
+import Mathlib.Data.Real.Basic
+
+-- From https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Canonical/near/538098556
+
+/--
+info: Try this:
+  [apply] exact
+    Exists.intro 2
+      (by simp only [Nat.zero_add, Nat.zero_mul, Nat.succ_mul, Nat.succ.injEq, Nat.succ_add] <;> exact Eq.refl Nat.zero)
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : ∃ n : Nat, n * n = 4 := by
+  canonical
+
+-- From https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Canonical/near/538228811
+
+def continuous_function_at (f : ℝ → ℝ) (x₀ : ℝ) :=
+∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε
+
+def sequence_tendsto (u : ℕ → ℝ) (l : ℝ) :=
+∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε
+
+/--
+info: Try this:
+  [apply] exact fun ε a ↦
+    Exists.intro (hu (hf ε a).choose (Exists.choose_spec (hf ε a)).1).choose fun n a_1 ↦
+      (Exists.choose_spec (hf ε a)).2 (u n)
+        (Exists.choose_spec (hu (hf ε a).choose (Exists.choose_spec (hf ε a)).1) n a_1)
+---
+warning: declaration uses 'sorry'
+---
+warning: unused variable `hf`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
+---
+warning: unused variable `hu`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
+-/
+#guard_msgs in
+example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
+    (hf : continuous_function_at f x₀) (hu : sequence_tendsto u x₀) :
+    sequence_tendsto (f ∘ u) (f x₀) := by
+  canonical
diff --git a/lakefile.lean b/lakefile.lean
index e1b9b1b484e037..b89b580ab545c5 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -17,6 +17,7 @@ require "leanprover-community" / "proofwidgets" @ git "v0.0.77" -- ProofWidgets
 require "leanprover-community" / "importGraph" @ git "main"
 require "leanprover-community" / "LeanSearchClient" @ git "main"
 require "leanprover-community" / "plausible" @ git "nightly-testing"
+-- require "chasenorman" / "Canonical" @ git "nightly-2025-11-03"
 
 
 /-!
@@ -31,6 +32,11 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
   ⟨`linter.allScriptsDocumented, true⟩,
   ⟨`linter.pythonStyle, true⟩,
   ⟨`linter.style.longFile, .ofNat 1500⟩,
+  -- ⟨`linter.tacticAnalysis.tryAtEachStepAesop, true⟩,
+  ⟨`linter.tacticAnalysis.tryAtEachStepSimpAll, true⟩,
+  ⟨`linter.tacticAnalysis.tryAtEachStepGrind, true⟩,
+  ⟨`linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions, true⟩,
+  ⟨`linter.tacticAnalysis.tryAtEachStepGrindSuggestions, true⟩,
   -- ⟨`linter.nightlyRegressionSet, true⟩,
   -- `latest_import.yml` uses this comment: if you edit it, make sure that the workflow still works
 ]
diff --git a/lean-toolchain b/lean-toolchain
index 3189ca3eb77681..097d521897fbdc 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2025-11-03
+leanprover/lean4-pr-releases:pr-release-11064
diff --git a/scripts/README.md b/scripts/README.md
index f1d277a8dc4770..04e1b0ead19528 100644
--- a/scripts/README.md
+++ b/scripts/README.md
@@ -79,6 +79,9 @@ to learn about it as well!
   Generates `unused.md` containing a markdown table showing the unused imports,
   and suggests `lake exe graph` commands to visualize the largest "rectangles" of unused imports.
 
+**Analyzing hammer tactic suggestions**
+- `analyze_hammer_suggestions.py` analyzes which tactics can replace existing tactics at each location, with and without +suggestions. By default analyzes simp_all and grind on all of Mathlib. Use `--aesop` and `--canonical` to enable additional tactics, or `--no-<tactic>` to disable defaults. Use `--raw` for location:tactic pairs instead of summary tables.
+
 **CI workflow**
 - `lake-build-with-retry.sh`
   Runs `lake build` on a target until `lake build --no-build` succeeds. Used in the main build workflows.
diff --git a/scripts/analyze_hammer_suggestions.py b/scripts/analyze_hammer_suggestions.py
new file mode 100755
index 00000000000000..c390ca0a0e7c91
--- /dev/null
+++ b/scripts/analyze_hammer_suggestions.py
@@ -0,0 +1,281 @@
+#!/usr/bin/env python3
+"""
+Analyze hammer suggestions from Lean build output.
+
+This script processes the output of `lake build --no-build` to extract and analyze
+tactic replacement suggestions generated by Lean's hammer tactics.
+
+Usage:
+    # Analyze all of Mathlib with default tactics (simp_all and grind)
+    ./scripts/analyze_hammer_suggestions.py
+
+    # Analyze a specific module
+    ./scripts/analyze_hammer_suggestions.py Mathlib.Data.List.Basic
+
+    # Enable specific tactics (use --no-<tactic> to disable)
+    ./scripts/analyze_hammer_suggestions.py --aesop --canonical
+
+    # Disable default tactics
+    ./scripts/analyze_hammer_suggestions.py --no-simp-all --no-grind
+
+    # Output raw location:tactic pairs for further processing
+    ./scripts/analyze_hammer_suggestions.py --raw
+
+By default, only simp_all and grind are enabled. Use --aesop and --canonical to
+enable additional tactics. The script analyzes which tactics can replace existing
+tactics at each location, both with and without the +suggestions flag.
+
+Output includes:
+  - Count of locations solvable by each subset of enabled tactics
+  - Grid format showing binary patterns (1=tactic works, 0=doesn't)
+  - Separate tables for base tactics and +suggestions variants
+
+Normalization:
+  - Removes 'try ' prefix from tactics
+  - Removes '?' modifier (e.g., 'simp_all?' -> 'simp_all')
+  - Removes dagger symbol '✝' from tactic names
+"""
+
+import argparse
+import re
+import subprocess
+from collections import defaultdict
+from itertools import product
+
+
+def normalize_tactic(tactic):
+    """Normalize tactic name, handling +suggestions variants and try prefix."""
+    # Remove dagger symbol
+    tactic = tactic.replace('✝', '')
+    tactic = tactic.strip()
+
+    # Remove 'try ' prefix if present
+    if tactic.startswith('try '):
+        tactic = tactic[4:].strip()
+
+    # Remove '?' modifier (but keep it before +suggestions)
+    # e.g., "simp_all? +suggestions" -> "simp_all +suggestions"
+    tactic = tactic.replace('? +', ' +')
+    # Remove trailing '?' if present
+    if tactic.endswith('?'):
+        tactic = tactic[:-1].strip()
+
+    return tactic
+
+
+def extract_suggestions(target):
+    """Run lake build and extract hammer suggestions."""
+    result = subprocess.run(
+        ['lake', 'build', '--no-build', target],
+        capture_output=True,
+        text=True
+    )
+
+    output = result.stdout + result.stderr
+
+    # Pattern to match info messages with "can be replaced with"
+    pattern = r'info: ([^:]+):(\d+):(\d+):.*? can be replaced with `([^`]+)`'
+    matches = re.findall(pattern, output, re.DOTALL)
+
+    # Group suggestions by location
+    locations = defaultdict(set)
+    for filepath, row, col, replacement in matches:
+        location = f"{filepath}:{row}:{col}"
+        normalized = normalize_tactic(replacement)
+        locations[location].add(normalized)
+
+    return locations
+
+
+def output_raw(locations):
+    """Output raw location:tactic pairs."""
+    for location, tactics in sorted(locations.items()):
+        for tactic in sorted(tactics):
+            print(f"{location}:{tactic}")
+
+
+def check_tactic_support(locations, tactics):
+    """
+    For each location, determine which tactics from the given set are suggested.
+    Returns a dict mapping location -> set of supported tactics.
+    """
+    result = {}
+    for location, suggestions in locations.items():
+        supported = set()
+        for tactic in tactics:
+            if tactic in suggestions:
+                supported.add(tactic)
+        result[location] = frozenset(supported)
+
+    return result
+
+
+def count_subsets(tactic_support):
+    """
+    Count how many locations support each subset of tactics.
+    Returns a dict mapping frozenset -> count.
+    """
+    counts = defaultdict(int)
+    for supported in tactic_support.values():
+        counts[supported] += 1
+
+    return counts
+
+
+def format_subset(subset, tactics):
+    """Format a subset as a binary string for display."""
+    return ''.join('1' if t in subset else '0' for t in tactics)
+
+
+def print_table(counts, tactics, title):
+    """Print a formatted table of counts."""
+    print(f"\n{title}")
+    print("=" * len(title))
+
+    # Generate all possible subsets
+    all_subsets = []
+    for bits in product([0, 1], repeat=len(tactics)):
+        subset = frozenset(t for t, b in zip(tactics, bits) if b)
+        all_subsets.append(subset)
+
+    # Sort subsets by binary representation for consistent display
+    all_subsets.sort(key=lambda s: format_subset(s, tactics), reverse=True)
+
+    # Print header
+    print(f"\n{'Subset':<40} {'Count':>8}")
+    print("-" * 50)
+
+    total = 0
+    for subset in all_subsets:
+        count = counts.get(subset, 0)
+        total += count
+        if count > 0 or subset == frozenset():  # Show zero count for empty set
+            subset_str = '{' + ', '.join(sorted(subset)) + '}' if subset else '{}'
+            print(f"{subset_str:<40} {count:>8}")
+
+    print("-" * 50)
+    print(f"{'Total locations':<40} {total:>8}")
+
+    # Print grid format
+    print(f"\n{title} - Grid Format")
+    print("=" * len(title))
+
+    # Create a mapping from binary pattern to count
+    pattern_counts = {}
+    for subset in all_subsets:
+        pattern = format_subset(subset, tactics)
+        pattern_counts[pattern] = counts.get(subset, 0)
+
+    # Print all combinations
+    num_tactics = len(tactics)
+    num_combinations = 2 ** num_tactics
+    print(f"\nTactics: {', '.join(tactics)}")
+    print("Binary pattern: " + "".join(f"{t[0]}" for t in tactics))
+    print()
+
+    # Group into rows of 4 for readability
+    for i in range(0, num_combinations, 4):
+        for j in range(min(4, num_combinations - i)):
+            combo_idx = num_combinations - 1 - (i + j)  # Count down from all 1s
+            bits = format(combo_idx, f'0{num_tactics}b')
+            count = pattern_counts.get(bits, 0)
+            subset_names = [tactics[k] for k in range(num_tactics) if bits[k] == '1']
+            subset_str = '{' + ','.join(subset_names) + '}' if subset_names else '{}'
+            print(f"{bits} {count:>6}  {subset_str}")
+        if i + 4 < num_combinations:
+            print()
+
+
+def output_analysis(locations, enabled_tactics):
+    """Output analysis tables."""
+    print(f"Found {len(locations)} unique locations with suggestions")
+
+    # Filter to only enabled tactics
+    base_tactics = [t for t in ['simp_all', 'aesop', 'canonical', 'grind'] if enabled_tactics[t]]
+
+    if not base_tactics:
+        print("\nNo tactics enabled. Use --simp-all, --aesop, --canonical, or --grind to enable tactics.")
+        return
+
+    print(f"\nAnalyzing tactics: {', '.join(base_tactics)}")
+
+    # Tactics with +suggestions
+    suggestions_tactics = [f'{t} +suggestions' for t in base_tactics]
+
+    # Analyze base tactics
+    base_support = check_tactic_support(locations, base_tactics)
+    base_counts = count_subsets(base_support)
+    print_table(base_counts, base_tactics, "Counts without +suggestions")
+
+    # Analyze +suggestions tactics
+    sugg_support = check_tactic_support(locations, suggestions_tactics)
+    sugg_counts = count_subsets(sugg_support)
+    print_table(sugg_counts, suggestions_tactics, "Counts with +suggestions")
+
+
+def main():
+    parser = argparse.ArgumentParser(
+        description='Analyze hammer suggestions from Lean build output'
+    )
+    parser.add_argument(
+        'target',
+        nargs='?',
+        default='Mathlib',
+        help='Build target to analyze (default: Mathlib)'
+    )
+    parser.add_argument(
+        '--raw',
+        action='store_true',
+        help='Output raw location:tactic pairs instead of analysis tables'
+    )
+
+    # Tactic enable/disable flags (simp_all and grind enabled by default)
+    parser.add_argument(
+        '--simp-all',
+        action=argparse.BooleanOptionalAction,
+        default=True,
+        help='Include simp_all in analysis (default: enabled)'
+    )
+    parser.add_argument(
+        '--aesop',
+        action=argparse.BooleanOptionalAction,
+        default=False,
+        help='Include aesop in analysis (default: disabled)'
+    )
+    parser.add_argument(
+        '--canonical',
+        action=argparse.BooleanOptionalAction,
+        default=False,
+        help='Include canonical in analysis (default: disabled)'
+    )
+    parser.add_argument(
+        '--grind',
+        action=argparse.BooleanOptionalAction,
+        default=True,
+        help='Include grind in analysis (default: enabled)'
+    )
+
+    args = parser.parse_args()
+
+    # Build enabled tactics dict (normalize argument names to tactic names)
+    enabled_tactics = {
+        'simp_all': args.simp_all,
+        'aesop': args.aesop,
+        'canonical': args.canonical,
+        'grind': args.grind
+    }
+
+    # Extract all suggestions
+    locations = extract_suggestions(args.target)
+
+    if args.raw:
+        output_raw(locations)
+    else:
+        print(f"Analyzing hammer suggestions for {args.target}...")
+        print("=" * 70)
+        print()
+        output_analysis(locations, enabled_tactics)
+
+
+if __name__ == '__main__':
+    main()