smithery/Arthur742Ramos

path-tactics

Use ComputationalPaths path tactics to automate common RwEq goals (path_simp/path_auto/path_normalize), and structure calc-based proofs cleanly.

Installation

$ npx skills add smithery/Arthur742Ramos --skill path-tactics

View on skills.sh ↗ Website ↗

Similar popular skills

Related neighbors and high-traction skills in the same topics — useful to compare before installing.

red-team-tactics Similar name

sickn33/agentic-awesome-skills

Red team tactics principles based on MITRE ATT&CK. Attack phases, detection evasion, reporting.

936 installs

hook-tactics Similar name

motion-team/creative-strategy-skills

Reference library of 35+ hook and headline tactic types.

423 installs

sales-tactics Similar name

louisblythe/sales-skills

When the user needs sales tactics, prospecting ideas, or pipeline generation strategies.

334 installs

red-team-tactics Similar name

davila7/claude-code-templates

Red team tactics principles based on MITRE ATT&CK. Attack phases, detection evasion, reporting.

312 installs

red-team-tactics Similar name

vudovn/ag-kit

Red team tactics principles based on MITRE ATT&CK. Attack phases, detection evasion, reporting.

203 installs

urgency-tactics Similar name

vivy-yi/xiaohongshu-skills

Use when running limited-time offers, launching products, or motivating audiences to take action

142 installs

Also in this package

Other skills from smithery/Arthur742Ramos.

npx skills add smithery/Arthur742Ramos

lean-build 0

Browse all from smithery/Arthur742Ramos

More details

Agent compatibility

Declared targets from SKILL.md / docs. Unmarked agents are not listed — the skill may still install via the CLI.

Claude Code Not declared

Cursor Not declared

Codex Not declared

GitHub Copilot Not declared

Windsurf Not declared

Gemini CLI Not declared

Cline Not declared

OpenCode Not declared

Package contents

Files included with this skill beyond the listing page.

skill md SKILL.md 1,382 B
docs SUMMARY.md 164 B

History

Sep 10, 2026 First recorded snapshot · 0 installs

SKILL.md

Path Tactics

Automated tactics for RwEq proofs.

Import

import ComputationalPaths.Path.Rewrite.PathTactic

Primary Tactics

Tactic	Use Case
`path_auto`	Try first for any RwEq goal
`path_simp`	Unit elimination, inverse cancellation
`path_normalize`	Convert to right-associative form
`path_rfl`	Close reflexive goals `p ≈ p`

Structural Tactics

Tactic	Description
`path_symm`	Apply symmetry to goal
`pathcongrleft h`	`RwEq (trans p q₁) (trans p q₂)` from `h : RwEq q₁ q₂`
`pathcongrright h`	`RwEq (trans p₁ q) (trans p₂ q)` from `h : RwEq p₁ p₂`
`pathcancelleft`	Close `RwEq (trans (symm p) p) refl`
`pathcancelright`	Close `RwEq (trans p (symm p)) refl`

Quick Reference

Goal	Tactic
`RwEq (trans refl p) p`	`path_simp`
`RwEq (trans p refl) p`	`path_simp`
`RwEq (trans (symm p) p) refl`	`pathcancelleft`
`RwEq (symm (symm p)) p`	`path_simp`

Preferred Style

Use calc with ≈ notation:

calc p
  _ ≈ p' := rweq_cmpA_refl_left
  _ ≈ q := rweq_symm rweq_tt

npx skills add smithery/Arthur742Ramos --skill path-tactics