feat: Add first EvalT and ProdT Interaction Lemma - #1344

Merged

jstoobysmith merged 16 commits into

leanprover-community:masterfrom

NicolaBernini:feat/add-first-EvalT-ProdT-Interaction-Lemma-1July2026

Jul 4, 2026

Commits on Jul 1, 2026

feat: Add first EvalT and ProdT Interaction Lemma
NicolaBernini
committed
8ef68cb
fix: Fix
NicolaBernini
committed
9dae214
Fix evalT product right index transport

NicolaBernini
and
Claude Opus 4.8
committed
ef4896b
Fix evalT product proof indices

NicolaBernini
and
Claude Opus 4.8
committed
6e44f5d
Stabilize evalT product proof branches

NicolaBernini
and
Claude Opus 4.8
committed
9ab5193

Commits on Jul 2, 2026

Fix evalT product dependent rewrites

NicolaBernini
and
Claude Opus 4.8
committed
1344132
Merge origin master into evalT product PR

NicolaBernini
and
Claude Opus 4.8
committed
52e870f
Fix evalT product basis transport

NicolaBernini
and
Claude Opus 4.8
committed
c27b654
Fix evalT product transport proof

NicolaBernini
and
Claude Opus 4.8
committed
69773ed

Commits on Jul 3, 2026

Simplify evalT product transport casts

NicolaBernini
and
Claude Opus 4.8
committed
5076ba6
Address evalT product review comments

NicolaBernini
and
Claude Opus 4.8
committed
e41bd2e
Fix evalT product cast simplification

NicolaBernini
and
Claude Opus 4.8
committed
f96e8b4
Normalize evalT product basis casts

NicolaBernini
and
Claude Opus 4.8
committed
16457ad

Commits on Jul 4, 2026

Collapse evalT product cast transports

NicolaBernini
and
Claude Opus 4.8
committed
7442d50
Use HEq for evalT product basis casts

NicolaBernini
and
Claude Opus 4.8
committed
e4b9b9f
Compose HEq casts in evalT product proof

NicolaBernini
and
Claude Opus 4.8
committed
0e6ef53