Merge branch 'main' of https://github.com/leanprover-community/con-nf

ConNF/Counting/Spec.lean

@@ -122,8 +122,8 @@ structure Specifies (σ : Spec β) (S : Support β) (hS : S.Strong) : Prop where
       σ.f i (hi.trans_eq max_eq_max) = SpecCondition.inflexibleBot A h.path
         {j | ∃ hj, S.f j hj = ⟨h.path.B.cons (bot_lt_coe _), inl h.a⟩}
         (fun j => {k | ∃ hj hk, ∃ (a : Atom) (N' : NearLitter),
-            N'.1 = N.1 ∧ a ∈ (N : Set Atom) ∆ N' ∧
-            S.f j hj = ⟨A, inr N'⟩ ∧ S.f k hk = ⟨A, inl a⟩})
+          N'.1 = N.1 ∧ a ∈ (N : Set Atom) ∆ N' ∧
+          S.f j hj = ⟨A, inr N'⟩ ∧ S.f k hk = ⟨A, inl a⟩})
 
 theorem Specifies.of_eq_atom {σ : Spec β} {S : Support β} {hS : S.Strong} (h : σ.Specifies S hS)
     {i : κ} {hi : i < σ.max} {A : ExtendedIndex β} {s t : Set κ}

ConNF/Counting/SpecSame.lean

@@ -74,7 +74,7 @@ theorem convertNearLitter_subsingleton_flexible (A : ExtendedIndex β) (NS NT NT
   refine NearLitter.ext ?_
   rw [← symmDiff_eq_bot, bot_eq_empty, eq_empty_iff_forall_not_mem]
   intro a ha
-  obtain ⟨j, hj, -, -, hja⟩ :=
+  obtain ⟨j, hj, hja⟩ :=
     hT.interferes hiT₁ hiT₁' hiT₂ hiT₂' (Support.Interferes.symmDiff h₂ ha)
   simp only [Function.funext_iff, Set.ext_iff] at h₅'
   obtain ⟨_, _, a', NS', _, ha', hS', -⟩ :=
@@ -230,7 +230,7 @@ theorem convertNearLitter_subsingleton_inflexibleCoe (A : ExtendedIndex β) (NS
   refine NearLitter.ext ?_
   rw [← symmDiff_eq_bot, bot_eq_empty, eq_empty_iff_forall_not_mem]
   intro a ha
-  obtain ⟨j, hj, -, -, hja⟩ :=
+  obtain ⟨j, hj, hja⟩ :=
     hT.interferes hiT₁ hiT₁' hiT₂ hiT₂' (Support.Interferes.symmDiff hNTT' ha)
   simp only [Function.funext_iff, Set.ext_iff] at h₇
   obtain ⟨_, _, a', NS', _, ha', hS', -⟩ :=
@@ -279,7 +279,7 @@ theorem convertNearLitter_subsingleton_inflexibleBot (A : ExtendedIndex β) (NS
   refine NearLitter.ext ?_
   rw [← symmDiff_eq_bot, bot_eq_empty, eq_empty_iff_forall_not_mem]
   intro a ha
-  obtain ⟨j, hj, -, -, hja⟩ :=
+  obtain ⟨j, hj, hja⟩ :=
     hT.interferes hiT₁ hiT₁' hiT₂ hiT₂' (Support.Interferes.symmDiff hNTT' ha)
   simp only [Function.funext_iff, Set.ext_iff] at h₅'
   obtain ⟨_, _, a', NS', _, ha', hS', -⟩ :=
@@ -638,19 +638,19 @@ theorem convert_lawful : (convert hσS hσT).Lawful := by
     exact convertAtom_mem_convertLitter_iff hσS hσT ha hN
   case dom_of_mem_symmDiff =>
     rintro a N₁ N₂ hN ⟨N₁', i, hiS, hiT, hiS', -⟩ ⟨N₂', j, hjS, hjT, hjS', -⟩ ha
-    obtain ⟨k, hkS, -, -, hk⟩ :=
+    obtain ⟨k, hkS, hk⟩ :=
       hS.interferes hiS hjS hiS' hjS' (Support.Interferes.symmDiff hN ha)
     exact convertAtom_dom hσS hσT ⟨k, hkS, hk.symm⟩
   case dom_of_mem_inter =>
     rintro a N₁ N₂ hN ⟨N₁', i, hiS, hiT, hiS', -⟩ ⟨N₂', j, hjS, hjT, hjS', -⟩ ha
-    obtain ⟨k, hkS, -, -, hk⟩ :=
+    obtain ⟨k, hkS, hk⟩ :=
       hS.interferes hiS hjS hiS' hjS' (Support.Interferes.inter hN ha)
     exact convertAtom_dom hσS hσT ⟨k, hkS, hk.symm⟩
   case ran_of_mem_symmDiff =>
     rintro a N₁ N₂ hN ⟨N₁', i, hiS, hiT, hiS', hiT'⟩ ⟨N₂', j, hjS, hjT, hjS', hjT'⟩ ha
     rw [convert_nearLitterMap_eq hσS hσT ⟨i, hiS, hiT, hiS', hiT'⟩,
       convert_nearLitterMap_eq hσS hσT ⟨j, hjS, hjT, hjS', hjT'⟩] at ha
-    obtain ⟨k, hkT, -, -, hk⟩ := hT.interferes hiT hjT hiT' hjT'
+    obtain ⟨k, hkT, hk⟩ := hT.interferes hiT hjT hiT' hjT'
       (Support.Interferes.symmDiff
         (convertNearLitter_fst hσS hσT ⟨i, hiS, hiT, hiS', hiT'⟩ ⟨j, hjS, hjT, hjS', hjT'⟩ hN) ha)
     have := hσT.atom_spec k hkT A a hk
@@ -661,7 +661,7 @@ theorem convert_lawful : (convert hσS hσT).Lawful := by
     rintro a N₁ N₂ hN ⟨N₁', i, hiS, hiT, hiS', hiT'⟩ ⟨N₂', j, hjS, hjT, hjS', hjT'⟩ ha
     rw [convert_nearLitterMap_eq hσS hσT ⟨i, hiS, hiT, hiS', hiT'⟩,
       convert_nearLitterMap_eq hσS hσT ⟨j, hjS, hjT, hjS', hjT'⟩] at ha
-    obtain ⟨k, hkT, -, -, hk⟩ := hT.interferes hiT hjT hiT' hjT'
+    obtain ⟨k, hkT, hk⟩ := hT.interferes hiT hjT hiT' hjT'
       (Support.Interferes.inter
         (hN ∘ convertNearLitter_fst' hσS hσT
           ⟨i, hiS, hiT, hiS', hiT'⟩ ⟨j, hjS, hjT, hjS', hjT'⟩) ha)

ConNF/Counting/StrongSupport.lean

@@ -36,11 +36,12 @@ inductive Precedes : Address β → Address β → Prop
 
 @[mk_iff]
 structure Strong (S : Support β) : Prop where
+  /-- TODO: We can simplify this statement now that we've removed the extra inequalities. -/
   interferes {i₁ i₂ : κ} (hi₁ : i₁ < S.max) (hi₂ : i₂ < S.max)
     {A : ExtendedIndex β} {N₁ N₂ : NearLitter}
     (h₁ : S.f i₁ hi₁ = ⟨A, inr N₁⟩) (h₂ : S.f i₂ hi₂ = ⟨A, inr N₂⟩)
     {a : Atom} (ha : Interferes a N₁ N₂) :
-    ∃ (j : κ) (hj : j < S.max), j < i₁ ∧ j < i₂ ∧ S.f j hj = ⟨A, inl a⟩
+    ∃ (j : κ) (hj : j < S.max), S.f j hj = ⟨A, inl a⟩
   precedes {i : κ} (hi : i < S.max) (c : Address β) (hc : Precedes c (S.f i hi)) :
     ∃ (j : κ) (hj : j < S.max), j < i ∧ S.f j hj = c
 
@@ -260,14 +261,7 @@ theorem strongSupport_strong {s : Set (Address β)} (hs : Small s) : (strongSupp
     rw [hN₁] at hi₁'
     rw [hN₂] at hi₂'
     have := interferes_mem_strongClosure s A a N₁ N₂ ha hi₁' hi₂'
-    obtain ⟨j, hj, hc⟩ := exists_of_mem_strongClosure _ _ this
-    refine ⟨j, hj, ?_, ?_, hc⟩
-    · refine lt_of_strongSupportRel hs hj hi₁ ?_
-      rw [hc, hN₁]
-      exact StrongSupportRel.atom _ _ _ _
-    · refine lt_of_strongSupportRel hs hj hi₂ ?_
-      rw [hc, hN₂]
-      exact StrongSupportRel.atom _ _ _ _
+    exact exists_of_mem_strongClosure _ _ this
   · intro i hi c hc
     have hi' := mem_of_strongSupport_f_eq hs hi
     have := precedes_mem_strongClosure s hc hi'
@@ -345,8 +339,8 @@ theorem Strong.smul [LeLevel β] {S : Support β} (hS : S.Strong) (ρ : Allowabl
     have := hS.interferes hi₁ hi₂
         (N₁ := (Allowable.toStructPerm ρ A)⁻¹ • N₁) (N₂ := (Allowable.toStructPerm ρ A)⁻¹ • N₂)
         ?_ ?_ (A := A) (a := (Allowable.toStructPerm ρ A)⁻¹ • a) this
-    · obtain ⟨j, hj, hj₁, hj₂, h⟩ := this
-      refine ⟨j, hj, hj₁, hj₂, ?_⟩
+    · obtain ⟨j, hj, h⟩ := this
+      refine ⟨j, hj, ?_⟩
       rw [Enumeration.smul_f, h, Allowable.smul_address, smul_inl, smul_inv_smul]
     · rw [Enumeration.smul_f, smul_eq_iff_eq_inv_smul] at hN₁
       rw [hN₁, Allowable.smul_address, map_inv, Tree.inv_apply, smul_inr]
@@ -380,16 +374,6 @@ theorem before_carrier (S : Support β) (i : κ) (hi : i < S.max) :
   · rintro ⟨j, hj₁, hj₂, rfl⟩
     exact ⟨j, hj₂, rfl⟩
 
-theorem before_strong (S : Support β) (i : κ) (hi : i < S.max) (hS : S.Strong) :
-    (S.before i hi).Strong := by
-  constructor
-  · intro i₁ i₂ hi₁ hi₂ A N₁ N₂ hN₁ hN₂ a ha
-    obtain ⟨j, hj, hj₁, hj₂, h⟩ := hS.interferes (hi₁.trans hi) (hi₂.trans hi) hN₁ hN₂ ha
-    exact ⟨j, hj₁.trans hi₁, hj₁, hj₂, h⟩
-  · intro j hj c hc
-    obtain ⟨k, hk₁, hk₂, h⟩ := hS.precedes (hj.trans hi) c hc
-    exact ⟨k, hk₂.trans hj, hk₂, h⟩
-
 @[simp]
 theorem before_smul [LeLevel β] (S : Support β) (i : κ) (hi : i < S.max) (ρ : Allowable β) :
     (ρ • S).before i hi = ρ • S.before i hi := rfl
@@ -551,6 +535,13 @@ theorem comp_carrier {γ : Λ} (S : Support β) (A : Path (β : TypeIndex) γ) :
     rw [comp_eq_of_canComp hS]
     exact ⟨i, hi, (comp_decomp_eq hS hi hc.symm).symm⟩
 
+theorem comp_f_eq' {γ : Λ} {S : Support β} {A : Path (β : TypeIndex) γ}
+    {i : κ} {hi : i < (S.comp A).max} {c : Address γ}
+    (hiS : (S.comp A).f i hi = c) :
+    ∃ j hj, S.f j hj = ⟨A.comp c.1, c.2⟩ := by
+  obtain ⟨j, hj, hc⟩ := (Set.ext_iff.mp (comp_carrier S A) c).mp ⟨i, hi, hiS.symm⟩
+  exact ⟨j, hj, hc.symm⟩
+
 theorem Precedes.comp {γ : Λ} {c d : Address γ} (h : Precedes c d) (A : Path (β : TypeIndex) γ) :
     Precedes ⟨A.comp c.1, c.2⟩ ⟨A.comp d.1, d.2⟩ := by
   cases h
@@ -575,18 +566,10 @@ theorem comp_strong {γ : Λ} (S : Support β) (A : Path (β : TypeIndex) γ) (h
     have h₂ := decomp_spec hS' hi₂
     rw [hN₁] at h₁
     rw [hN₂] at h₂
-    obtain ⟨j, hj, hj₁, hj₂, h⟩ := hS.interferes _ _ h₁ h₂ ha
-    refine ⟨j, ?_, ?_, ?_, ?_⟩
+    obtain ⟨j, hj, h⟩ := hS.interferes _ _ h₁ h₂ ha
+    refine ⟨j, ?_, ?_⟩
     · rw [comp_max_eq_of_canComp hS']
       exact hj
-    · rw [compIndex] at hj₁
-      split_ifs at hj₁ with hj'
-      · exact hj₁
-      · exact (not_lt_leastCompIndex hS' j ⟨hj, ⟨B, inl a⟩, h⟩ hj₁).elim
-    · rw [compIndex] at hj₂
-      split_ifs at hj₂ with hj'
-      · exact hj₂
-      · exact (not_lt_leastCompIndex hS' j ⟨hj, ⟨B, inl a⟩, h⟩ hj₂).elim
     · rw [comp_f_eq]
       exact comp_decomp_eq hS' hj h
   · intro i hi c hc
@@ -682,6 +665,97 @@ theorem comp_smul [LeLevel β] {γ : Λ} [LeLevel γ] (S : Support β) (A : Path
       simp only [hc, Allowable.smul_address, map_inv, Tree.inv_apply, Allowable.toStructPerm_comp,
         Tree.comp_apply]
 
+theorem smul_comp_ext {γ : Λ} [LeLevel γ]
+    {S T : Support β} (A : Path (β : TypeIndex) γ) (ρ : Allowable γ)
+    (h₁ : S.max = T.max)
+    (h₂ : ∀ i hiS hiT, ∀ c : Address γ, S.f i hiS = ⟨A.comp c.1, c.2⟩ →
+      T.f i hiT = ⟨A.comp c.1, Allowable.toStructPerm ρ c.1 • c.2⟩)
+    (h₃ : ∀ i hiT hiS, ∀ c : Address γ, T.f i hiT = ⟨A.comp c.1, c.2⟩ →
+      S.f i hiS = ⟨A.comp c.1, Allowable.toStructPerm ρ⁻¹ c.1 • c.2⟩) :
+    ρ • S.comp A = T.comp A := by
+  refine Enumeration.ext' ?_ ?_
+  · by_cases h : S.CanComp A
+    · rw [Enumeration.smul_max, comp_max_eq_of_canComp h, comp_max_eq_of_canComp, h₁]
+      obtain ⟨i, hi, c, hc⟩ := h
+      exact ⟨i, h₁ ▸ hi, ρ • c, h₂ i hi (h₁ ▸ hi) c hc⟩
+    · rw [Enumeration.smul_max, comp_max_eq_of_not_canComp h, comp_max_eq_of_not_canComp]
+      contrapose! h
+      obtain ⟨i, hi, c, hc⟩ := h
+      exact ⟨i, h₁ ▸ hi, ρ⁻¹ • c, h₃ i hi (h₁ ▸ hi) c hc⟩
+  · intro i hS hT
+    have hS' : i < S.max
+    · rw [Enumeration.smul_max] at hS
+      exact lt_max_of_lt_comp_max hS
+    have hT' := hS'.trans_eq h₁
+    rw [Enumeration.smul_f, comp_f_eq, comp_f_eq]
+    by_cases h : ∃ c : Address γ, S.f i hS' = ⟨A.comp c.1, c.2⟩
+    · obtain ⟨c, hc⟩ := h
+      rw [comp_decomp_eq _ _ hc, comp_decomp_eq _ _ (c := ρ • c) (h₂ i hS' hT' c hc)]
+    · rw [comp_decomp_eq' _ _ h, comp_decomp_eq']
+      · have hSA : S.CanComp A := canComp_of_lt_comp_max hS
+        have hTA : T.CanComp A := canComp_of_lt_comp_max hT
+        obtain ⟨hlS, c, hc⟩ := leastCompIndex_mem hSA
+        obtain ⟨hlT, d, hd⟩ := leastCompIndex_mem hTA
+        have hlTS := not_lt_leastCompIndex hSA _ ⟨hlT.trans_eq h₁.symm, ρ⁻¹ • d, h₃ _ _ _ _ hd⟩
+        have hlST := not_lt_leastCompIndex hTA _ ⟨hlS.trans_eq h₁, ρ • c, h₂ _ _ _ _ hc⟩
+        have hST := le_antisymm (le_of_not_lt hlTS) (le_of_not_lt hlST)
+        have hSA' := leastComp_spec hSA
+        have hTA' := leastComp_spec hTA
+        have hTA'' := h₂ _ hlS (hlS.trans_eq h₁) _ hSA'
+        simp_rw [hST] at hTA''
+        simp only [hTA', Address.mk.injEq] at hTA''
+        refine Address.ext _ _ ?_ ?_
+        · exact Path.comp_injective_right _ hTA''.1.symm
+        · exact hTA''.2.symm
+      · rintro ⟨c, hc⟩
+        exact h ⟨ρ⁻¹ • c, h₃ i hT' hS' c hc⟩
+
+/- theorem canComp_comp {γ δ : Λ} {S : Support β}
+    {A : Path (β : TypeIndex) γ} {B : Path (γ : TypeIndex) δ}
+    (h : S.CanComp (A.comp B)) : S.CanComp A := by
+  obtain ⟨i, hi, c, hc⟩ := h
+  rw [Path.comp_assoc] at hc
+  exact ⟨i, hi, ⟨B.comp c.1, c.2⟩, hc⟩
+
+theorem canComp_comp' {γ δ : Λ} {S : Support β}
+    {A : Path (β : TypeIndex) γ} {B : Path (γ : TypeIndex) δ} :
+    (S.comp A).CanComp B ↔ S.CanComp (A.comp B) := by
+  constructor
+  · rintro ⟨i, hi, c, hc⟩
+    obtain ⟨j, hj, hjc⟩ := comp_f_eq' hc
+    rw [← Path.comp_assoc] at hjc
+    exact ⟨j, hj, c, hjc⟩
+  · rintro ⟨i, hi, c, hc⟩
+    refine ⟨i, ?_, c, ?_⟩
+    · rw [comp_max_eq_of_canComp (canComp_comp ⟨i, hi, c, hc⟩)]
+      exact hi
+    · rw [Path.comp_assoc] at hc
+      rw [comp_f_eq, comp_decomp_eq _ _ (c := ⟨B.comp c.1, c.2⟩) hc]
+
+theorem comp_comp [LeLevel β] {γ δ : Λ} [LeLevel γ] [LeLevel δ] (S : Support β)
+    (A : Path (β : TypeIndex) γ) (B : Path (γ : TypeIndex) δ) :
+    S.comp (A.comp B) = (S.comp A).comp B := by
+  refine Enumeration.ext' ?_ ?_
+  · by_cases h : S.CanComp (A.comp B)
+    · rw [comp_max_eq_of_canComp h,
+        comp_max_eq_of_canComp (canComp_comp'.mpr h),
+        comp_max_eq_of_canComp (canComp_comp h)]
+    · rw [comp_max_eq_of_not_canComp h, comp_max_eq_of_not_canComp]
+      rw [canComp_comp']
+      exact h
+  · intro i hE hF
+    have hcomp : S.CanComp (A.comp B) := canComp_of_lt_comp_max hE
+    have hS' := lt_max_of_lt_comp_max hF
+    have hS := lt_max_of_lt_comp_max (lt_max_of_lt_comp_max hF)
+    by_cases h : ∃ c : Address δ, S.f i hS = ⟨(A.comp B).comp c.1, c.2⟩
+    · obtain ⟨c, hc⟩ := h
+      rw [comp_f_eq, comp_decomp_eq hcomp hS hc]
+      rw [comp_f_eq, comp_decomp_eq]
+      rw [comp_f_eq, comp_decomp_eq]
+      rw [hc, Path.comp_assoc]
+    · rw [comp_f_eq, comp_decomp_eq' hcomp hS h]
+      sorry -/
+
 end Support
 
 end ConNF

ConNF/Model.lean

@@ -6,3 +6,5 @@ import ConNF.Model.Basic
 import ConNF.Model.Predicative
 import ConNF.Model.FOA
 import ConNF.Model.RaiseStrong
+import ConNF.Model.Union
+import ConNF.Model.Result

ConNF/Model/Predicative.lean

@@ -87,6 +87,13 @@ theorem smul_singleton (t : TSet β) (ρ : Allowable α) :
   intro s
   simp only [mem_smul_iff, mem_singleton_iff, inv_smul_eq_iff]
 
+theorem singleton_injective' (t₁ t₂ : TSet β) (h : TSet.singleton hβ t₁ = TSet.singleton hβ t₂) :
+    t₁ = t₂ := by
+  have : t₁ ∈[hβ] TSet.singleton hβ t₁
+  · rw [mem_singleton_iff]
+  rw [h, mem_singleton_iff] at this
+  exact this
+
 @[simp]
 theorem TangleData.TSet.mem_up_iff (t₁ t₂ : TSet β) (s : TSet β) :
     s ∈[hβ] up hβ t₁ t₂ ↔ s = t₁ ∨ s = t₂ := by
@@ -99,6 +106,53 @@ theorem smul_up (t₁ t₂ : TSet β) (ρ : Allowable α) :
   intro s
   simp only [mem_smul_iff, mem_up_iff, inv_smul_eq_iff]
 
+theorem up_self (t : TSet β) : up hβ t t = .singleton hβ t := by
+  refine ext hβ _ _ ?_
+  simp only [mem_up_iff, or_self, mem_singleton_iff, implies_true]
+
+theorem up_injective (t₁ t₂ t₁' t₂' : TSet β) (h : up hβ t₁ t₂ = up hβ t₁' t₂') :
+    (t₁ = t₁' ∧ t₂ = t₂') ∨ (t₁ = t₂' ∧ t₂ = t₁') := by
+  have h₁ : t₁ ∈[hβ] up hβ t₁ t₂
+  · rw [mem_up_iff]
+    exact Or.inl rfl
+  have h₂ : t₂ ∈[hβ] up hβ t₁ t₂
+  · rw [mem_up_iff]
+    exact Or.inr rfl
+  rw [h] at h₁ h₂
+  rw [mem_up_iff] at h₁ h₂
+  obtain (h₁ | h₁) := h₁ <;> obtain (h₂ | h₂) := h₂
+  · refine Or.inl ⟨h₁, ?_⟩
+    cases h₁.trans h₂.symm
+    have : t₂' ∈[hβ] up hβ t₁' t₂'
+    · rw [mem_up_iff]
+      exact Or.inr rfl
+    rw [← h, up_self, mem_singleton_iff] at this
+    exact this.symm
+  · refine Or.inl ⟨h₁, h₂⟩
+  · refine Or.inr ⟨h₁, h₂⟩
+  · refine Or.inr ⟨h₁, ?_⟩
+    cases h₁.trans h₂.symm
+    have : t₁' ∈[hβ] up hβ t₁' t₂'
+    · rw [mem_up_iff]
+      exact Or.inl rfl
+    rw [← h, up_self, mem_singleton_iff] at this
+    exact this.symm
+
+theorem up_eq_singleton_iff (t t₁ t₂ : TSet β) :
+    up hβ t₁ t₂ = .singleton hβ t ↔ t₁ = t ∧ t₂ = t := by
+  constructor
+  · intro h
+    have h₁ : t₁ ∈[hβ] up hβ t₁ t₂
+    · rw [mem_up_iff]
+      exact Or.inl rfl
+    have h₂ : t₂ ∈[hβ] up hβ t₁ t₂
+    · rw [mem_up_iff]
+      exact Or.inr rfl
+    rw [h, mem_singleton_iff] at h₁ h₂
+    exact ⟨h₁, h₂⟩
+  · rintro ⟨rfl, rfl⟩
+    rw [up_self]
+
 @[simp]
 theorem TangleData.TSet.mem_op_iff (t₁ t₂ : TSet γ) (s : TSet β) :
     s ∈[hβ] op hβ hγ t₁ t₂ ↔ s = singleton hγ t₁ ∨ s = up hγ t₁ t₂ :=
@@ -112,6 +166,44 @@ theorem smul_op (t₁ t₂ : TSet γ) (ρ : Allowable α) :
   intro s
   simp only [mem_smul_iff, mem_op_iff, inv_smul_eq_iff, smul_singleton, smul_up]
 
+theorem op_injective (t₁ t₂ t₁' t₂' : TSet γ) (h : op hβ hγ t₁ t₂ = op hβ hγ t₁' t₂') :
+    t₁ = t₁' ∧ t₂ = t₂' := by
+  have h₁ : .singleton hγ t₁ ∈[hβ] op hβ hγ t₁ t₂
+  · rw [mem_op_iff]
+    exact Or.inl rfl
+  have h₂ : up hγ t₁ t₂ ∈[hβ] op hβ hγ t₁ t₂
+  · rw [mem_op_iff]
+    exact Or.inr rfl
+  rw [h] at h₁ h₂
+  rw [mem_op_iff] at h₁ h₂
+  obtain (h₁ | h₁) := h₁ <;> obtain (h₂ | h₂) := h₂
+  · cases singleton_injective' _ _ _ h₁
+    rw [up_eq_singleton_iff] at h₂
+    have h' : up hγ t₁ t₂' ∈[hβ] op hβ hγ t₁ t₂'
+    · rw [mem_op_iff]
+      exact Or.inr rfl
+    rw [← h, mem_op_iff] at h'
+    obtain (h' | h') := h'
+    · rw [up_eq_singleton_iff] at h'
+      exact ⟨rfl, h₂.2.trans h'.2.symm⟩
+    · obtain (h' | ⟨rfl, rfl⟩) := up_injective _ _ _ _ _ h'
+      · exact ⟨rfl, h'.2.symm⟩
+      · exact ⟨rfl, rfl⟩
+  · cases singleton_injective' _ _ _ h₁
+    obtain (h' | ⟨rfl, rfl⟩) := up_injective _ _ _ _ _ h₂
+    · exact h'
+    · exact ⟨rfl, rfl⟩
+  · symm at h₁
+    rw [up_eq_singleton_iff] at h₁ h₂
+    obtain ⟨rfl, rfl⟩ := h₁
+    obtain ⟨_, rfl⟩ := h₂
+    exact ⟨rfl, rfl⟩
+  · symm at h₁
+    rw [up_eq_singleton_iff] at h₁
+    obtain ⟨rfl, rfl⟩ := h₁
+    rw [up_self, up_eq_singleton_iff] at h₂
+    exact h₂
+
 theorem Symmetric.singletonImage {s : Set (TSet γ)} (h : Symmetric hγ s) :
     Symmetric hβ {p | ∃ a b : TSet ε, op hδ hε a b ∈ s ∧
       p = op hγ hδ (.singleton hε a) (.singleton hε b)} := by