Plain-language statement
Two CoPsetRaw trees are equal if they have the same membership function and both are well-formed.
Exact Lean statement
theorem coPsetRaw_eq {t1 t2 : CoPsetRaw} (Ht : ∀ p, ElemOf p t1 = ElemOf p t2)
(Hwf1 : coPsetWf t1 = true) (Hwf2 : coPsetWf t2 = true) : t1 = t2Formal artifact
Lean source
theorem coPsetRaw_eq {t1 t2 : CoPsetRaw} (Ht : ∀ p, ElemOf p t1 = ElemOf p t2) (Hwf1 : coPsetWf t1 = true) (Hwf2 : coPsetWf t2 = true) : t1 = t2 := by match t1, t2 with | .leaf b1, .leaf b2 => congr 1; exact Ht .xH | .leaf b1, .node b2 l2 r2 => simp only [ElemOf] at Ht exact coPsetLeaf_wf Hwf2 (fun p => .symm (Ht p)) |>.symm | .node b1 l1 r1, .leaf b2 => simp only [ElemOf] at Ht exact (coPsetLeaf_wf Hwf1 Ht) | .node b1 l1 r1, .node b2 l2 r2 => congr · exact Ht .xH · exact coPsetRaw_eq (Ht <| .xO ·) (node_wf_l Hwf1) (node_wf_l Hwf2) · exact coPsetRaw_eq (Ht <| .xI ·) (node_wf_r Hwf1) (node_wf_r Hwf2)- Project
- Iris-Lean
- License
- Apache-2.0
- Commit
- 37f53e0ac065
- Source
- Iris/Iris/Std/CoPset.lean:190-204
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Inj on of nodup map
FromMathlib.inj_on_of_nodup_map
Plain-language statement
NB. Copied from Mathlib
Source project: Iris-Lean
Person-level attribution pending.
Big Op L hom weak
Iris.Algebra.BigOpL.bigOpL_hom_weak
Plain-language statement
Weak monoid homomorphisms distribute over non-empty big ops.
Source project: Iris-Lean
Person-level attribution pending.
Embed internal inj
Iris.BI.embed_internal_inj
Plain-language statement
⎡·⎤ reflects internal equality.
Source project: Iris-Lean
Person-level attribution pending.