English
If s1 and s2 are disjoint with a common third s3, then (s1 ∪ s3) = (s2 ∪ s3) iff s1 = s2.
Русский
Если s1 и s2 несовместимы с общим s3, то (s1 ∪ s3) = (s2 ∪ s3) тогда и только тогда, когда s1 = s2.
LaTeX
$$$ s_1.Disjoint\ s_3 \to\ s_2.Disjoint\ s_3 \to (s_1 \cup s_3) = (s_2 \cup s_3) \leftrightarrow s_1 = s_2 $$$
Lean4
theorem union_cancel {s₁ s₂ s₃ : Finmap β} (h : Disjoint s₁ s₃) (h' : Disjoint s₂ s₃) : s₁ ∪ s₃ = s₂ ∪ s₃ ↔ s₁ = s₂ :=
⟨fun h'' => by
apply ext_lookup
intro x
have : (s₁ ∪ s₃).lookup x = (s₂ ∪ s₃).lookup x := h'' ▸ rfl
by_cases hs₁ : x ∈ s₁
· rwa [lookup_union_left hs₁, lookup_union_left_of_not_in (h _ hs₁)] at this
· by_cases hs₂ : x ∈ s₂
· rwa [lookup_union_left_of_not_in (h' _ hs₂), lookup_union_left hs₂] at this
· rw [lookup_eq_none.mpr hs₁, lookup_eq_none.mpr hs₂], fun h => h ▸ rfl⟩
