From 0e791839777c0cb1c61fbe9e79908f98e5ab6d62 Mon Sep 17 00:00:00 2001
From: Jad Ghalayini <jad.ghalayini@protonmail.com>
Date: Sat, 28 Sep 2024 22:06:57 +0100
Subject: [PATCH] Distlore, now actually

---
 .../BinSyntax/Rewrite/Region/Compose/Distrib.lean  | 14 ++++++++------
 .../BinSyntax/Rewrite/Term/Compose/Distrib.lean    | 12 ++++++------
 2 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Distrib.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Distrib.lean
index 58e6e0c..3017e2b 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Distrib.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Distrib.lean
@@ -94,13 +94,15 @@ theorem Eqv.distl_seq_injective {A B C : Ty α} {Γ : Ctx α ε}
   : r = s := by
   rw [<-nil_seq r, <-nil_seq s, <-distl_inv_distl, seq_assoc, h, seq_assoc]
 
-theorem Eqv.rtimes_inj_l_seq_distl_inv {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+theorem Eqv.rtimes_inj_l_distl_inv {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : A ⋊ inj_l ;; distl_inv (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (L := L) = inj_l := by
-  sorry
+  rw [inj_l_eq_ret, rtimes_eq_ret, distl_inv_eq_ret, <-ret_of_seq, Term.Eqv.rtimes_inj_l_distl_inv]
+  rfl
 
-theorem Eqv.rtimes_inj_r_seq_distl_inv {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
+theorem Eqv.rtimes_inj_r_distl_inv {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : A ⋊ inj_r ;; distl_inv (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (L := L) = inj_r := by
-  sorry
+  rw [inj_r_eq_ret, rtimes_eq_ret, distl_inv_eq_ret, <-ret_of_seq, Term.Eqv.rtimes_inj_r_distl_inv]
+  rfl
 
 theorem Eqv.rtimes_sum_seq_distl_inv {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   {l : Eqv φ ((A, ⊥)::Γ) (A'::L)} {r : Eqv φ ((B, ⊥)::Γ) (B'::L)}
@@ -109,5 +111,5 @@ theorem Eqv.rtimes_sum_seq_distl_inv {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx
   apply distl_seq_injective
   rw [<-seq_assoc, <-seq_assoc, distl_distl_inv, nil_seq, distl, coprod_seq, coprod_seq, sum]
   congr 1
-  · rw [rtimes_rtimes, inj_l_coprod, <-rtimes_rtimes, seq_assoc, rtimes_inj_l_seq_distl_inv]
-  · rw [rtimes_rtimes, inj_r_coprod, <-rtimes_rtimes, seq_assoc, rtimes_inj_r_seq_distl_inv]
+  · rw [rtimes_rtimes, inj_l_coprod, <-rtimes_rtimes, seq_assoc, rtimes_inj_l_distl_inv]
+  · rw [rtimes_rtimes, inj_r_coprod, <-rtimes_rtimes, seq_assoc, rtimes_inj_r_distl_inv]
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Distrib.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Distrib.lean
index 3d1d08c..82e1cbb 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Distrib.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Distrib.lean
@@ -105,23 +105,23 @@ theorem Eqv.distl_seq_injective {A B C : Ty α} {Γ : Ctx α ε}
   : r = s := by
   rw [<-nil_seq r, <-nil_seq s, <-distl_inv_distl, <-seq_assoc, h, seq_assoc]
 
-theorem Eqv.rtimes_inj_l_seq_distl_inv_pure {A B C : Ty α} {Γ : Ctx α ε}
+theorem Eqv.rtimes_inj_l_distl_inv_pure {A B C : Ty α} {Γ : Ctx α ε}
   : A ⋊' inj_l ;;' distl_inv (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (e := ⊥) = inj_l := by
   rw [seq_distl_inv, rtimes, tensor, let2_let2, let2_pair]
   simp [nil, let1_beta_pure, inj_l, coprod, wk2, Nat.liftnWk, case_inl, <-inl_let2, let2_eta]
 
-theorem Eqv.rtimes_inj_r_seq_distl_inv_pure {A B C : Ty α} {Γ : Ctx α ε}
+theorem Eqv.rtimes_inj_r_distl_inv_pure {A B C : Ty α} {Γ : Ctx α ε}
   : A ⋊' inj_r ;;' distl_inv (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (e := ⊥) = inj_r := by
   rw [seq_distl_inv, rtimes, tensor, let2_let2, let2_pair]
   simp [nil, let1_beta_pure, inj_r, coprod, wk2, Nat.liftnWk, case_inr, <-inr_let2, let2_eta]
 
-theorem Eqv.rtimes_inj_l_seq_distl_inv {A B C : Ty α} {Γ : Ctx α ε}
+theorem Eqv.rtimes_inj_l_distl_inv {A B C : Ty α} {Γ : Ctx α ε}
   : A ⋊' inj_l ;;' distl_inv (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (e := e) = inj_l
-  := congrArg (wk_eff (he := bot_le)) rtimes_inj_l_seq_distl_inv_pure
+  := congrArg (wk_eff (he := bot_le)) rtimes_inj_l_distl_inv_pure
 
-theorem Eqv.rtimes_inj_r_seq_distl_inv {A B C : Ty α} {Γ : Ctx α ε}
+theorem Eqv.rtimes_inj_r_distl_inv {A B C : Ty α} {Γ : Ctx α ε}
   : A ⋊' inj_r ;;' distl_inv (φ := φ) (A := A) (B := B) (C := C) (Γ := Γ) (e := e) = inj_r
-  := congrArg (wk_eff (he := bot_le)) rtimes_inj_r_seq_distl_inv_pure
+  := congrArg (wk_eff (he := bot_le)) rtimes_inj_r_distl_inv_pure
 
 def Eqv.distr {A B C : Ty α} {Γ : Ctx α ε}
   : Eqv φ (⟨(A.prod C).coprod (B.prod C), ⊥⟩::Γ) ⟨(A.coprod B).prod C, e⟩