Smul near Litter of smul litter

theorem smul_nearLitter_of_smul_litter [Level] [CoherentData] {β : TypeIndex} [LeLevel β]    {ξ : BaseAction} {ψ : BaseApprox} {A : β ↝ ⊥} {π : BasePerm} {N₁ N₂ : NearLitter}    (hξ : ξ.FlexApprox A ψ) (hψ : ψ.ExactlyApproximates π) (hNξ : ξᴺ N₁ N₂) (hNπ : π • N₁ᴸ = N₂ᴸ) :    π • N₁ = N₂ := by  apply NearLitter.ext  calc (π • N₁)ᴬ    _ = π • N₁ᴬ := rfl    _ = π • (N₁ᴸᴬ ∆ (N₁ᴸᴬ ∆ N₁ᴬ)) := by rw [symmDiff_symmDiff_cancel_left]    _ = (π • N₁ᴸᴬ) ∆ (π • N₁ᴬ ∆ N₁ᴸᴬ) := by rw [Set.smul_set_symmDiff, symmDiff_comm N₁ᴬ]    _ = (π • (N₁ᴸᴬ ∩ ψ.exceptions.dom ∪ N₁ᴸᴬ \ ψ.exceptions.dom)) ∆ (π • N₁ᴬ ∆ N₁ᴸᴬ) :=        by rw [Set.inter_union_diff]    _ = (π • (N₁ᴸᴬ ∩ ψ.exceptions.dom) ∪ π • (N₁ᴸᴬ \ ψ.exceptions.dom)) ∆ (π • N₁ᴬ ∆ N₁ᴸᴬ) :=        by rw [Set.smul_set_union]    _ = (π • (N₁ᴸᴬ ∩ ψ.exceptions.dom) ∪ N₂ᴸᴬ \ ψ.exceptions.dom) ∆ (π • N₁ᴬ ∆ N₁ᴸᴬ) :=        by rw [hψ.smulSet_nearLitter hNπ]    _ = ((ψ.exceptions.image (N₁ᴸᴬ ∩ ψ.exceptions.dom)) ∪ N₂ᴸᴬ \ ψ.exceptions.dom) ∆          (ψ.exceptions.image (N₁ᴬ ∆ N₁ᴸᴬ)) := by        rw [hψ.smulSet_eq_exceptions_image, hψ.smulSet_eq_exceptions_image]        · exact hξ.symmDiff_subset_dom ⟨N₂, hNξ⟩        · exact Set.inter_subset_right    _ = ((ψ.exceptions.image (N₁ᴸᴬ ∩ ψ.exceptions.dom)) ∆ (ψ.exceptions.image (N₁ᴬ ∆ N₁ᴸᴬ))) ∪          N₂ᴸᴬ \ ψ.exceptions.dom := by        apply Set.union_symmDiff_of_disjoint        rw [Set.disjoint_iff_inter_eq_empty, Set.eq_empty_iff_forall_notMem]        rintro a ⟨ha, b, hb⟩        exact ha.2 (ψ.exceptions_permutative.mem_dom hb.2)    _ = ψ.exceptions.image ((N₁ᴸᴬ ∩ ψ.exceptions.dom) ∆ (N₁ᴬ ∆ N₁ᴸᴬ)) ∪          N₂ᴸᴬ \ ψ.exceptions.dom := by rw [← ψ.exceptions_permutative.image_symmDiff]    _ = ψ.exceptions.image (((N₁ᴸᴬ ∩ ψ.exceptions.dom) ∆ N₁ᴸᴬ) ∆ N₁ᴬ) ∪          N₂ᴸᴬ \ ψ.exceptions.dom := by rw [symmDiff_assoc, symmDiff_comm N₁ᴬ]    _ = ψ.exceptions.image ((N₁ᴸᴬ \ ψ.exceptions.dom) ∆ N₁ᴬ) ∪ N₂ᴸᴬ \ ψ.exceptions.dom :=        by rw [Set.inter_symmDiff_left]    _ = ψ.exceptions.image (N₁ᴬ \ (N₁ᴸᴬ \ ψ.exceptions.dom)) ∪ N₂ᴸᴬ \ ψ.exceptions.dom := by        rw [Set.symmDiff_def, Rel.image_union, Set.diff_diff, Rel.image_empty_of_disjoint_dom,          Set.empty_union]        rw [Set.disjoint_iff_inter_eq_empty, Set.eq_empty_iff_forall_notMem]        intro a ha        exact ha.2.2 (Or.inl ha.1)    _ = ψ.exceptions.image (N₁ᴬ ∩ ψ.exceptions.dom) ∪ N₂ᴸᴬ \ ψ.exceptions.dom := by        congr 1        apply Rel.image_eq_of_inter_eq        ext a        simp only [Set.mem_inter_iff, Set.mem_diff]        tauto    _ = N₂ᴬ := by        ext a        rw [hξ.mem_iff_mem hNξ a]        constructor        · rintro (⟨b, hb, hba⟩ | ha)          · exact Or.inl ⟨b, hb.1, hba⟩          · exact Or.inr ⟨ha.2, ha.1⟩        · rintro (⟨b, hb, hba⟩ | ha)          · exact Or.inl ⟨b, ⟨hb, a, hba⟩, hba⟩          · exact Or.inr ⟨ha.2, ha.1⟩