Left case of distributivity shunt

DeBruijnSSA/BinSyntax/Rewrite/Region/Uniform.lean

@@ -452,7 +452,7 @@ theorem Uniform.lsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ
       funext i
       cases i using Fin.elim1
       simp only [Subst.liftn_one, ← Subst.vlift_lift_comm, Fin.isValue, Fin.elim1_zero, vwk1_lsubst]
-      simp [Subst.vlift, <-Function.comp.assoc, vwk2_comp_vwk1]
+      simp [Subst.vlift, <-Function.comp_assoc, vwk2_comp_vwk1]
     · simp only [BinSyntax.Region.lsubst, Subst.liftn_one, cfg.injEq, heq_eq_eq, true_and]
       funext i
       cases i using Fin.elim1
@@ -511,7 +511,7 @@ theorem Uniform.lsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ
         split
         · simp only [BinSyntax.Region.lsubst, wk, Nat.liftWk_zero, Function.comp_apply,
           Subst.extend, ↓reduceIte, vsubst0_var0_vwk1, *]
-          simp [vwk1_lsubst, <-Function.comp.assoc, vwk2_comp_vwk1]
+          simp [vwk1_lsubst, <-Function.comp_assoc, vwk2_comp_vwk1]
         · simp only [BinSyntax.Region.lsubst, wk, Nat.liftWk_zero, Function.comp_apply,
           Subst.liftn, add_lt_iff_neg_right, not_lt_zero', ↓reduceIte, add_tsub_cancel_right,
           vsubst0_var0_vwk1]
@@ -526,7 +526,7 @@ theorem Uniform.lsubst {P Q : Ctx α ε → LCtx α → Region φ → Region φ
       split
       · simp only [BinSyntax.Region.lsubst, wk, Nat.liftWk_zero, Function.comp_apply,
         Subst.fromFCFG, ↓reduceDIte, vsubst0_var0_vwk1, *]
-        simp [vwk1_lsubst, <-Function.comp.assoc, vwk2_comp_vwk1]
+        simp [vwk1_lsubst, <-Function.comp_assoc, vwk2_comp_vwk1]
       · simp only [BinSyntax.Region.lsubst, wk, Nat.liftWk_zero, Function.comp_apply, Subst.liftn,
         add_lt_iff_neg_right, not_lt_zero', ↓reduceIte, add_tsub_cancel_right, vsubst0_var0_vwk1]
         simp only [vwk1_lwk]

DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Distrib.lean

@@ -124,8 +124,23 @@ theorem Eqv.split_rtimes_pi_r_distl_pure {X A B C : Ty α} {Γ : Ctx α ε}
     (_ ⋊' (split ;;' inj_r ⋉' _) ;;' assoc_inv) := by
   apply distl_seq_injective
   conv => rhs; rw [seq_assoc, distl_distl_inv, nil_seq]
-  rw [distl, coprod_seq]
-  sorry
+  rw [distl, coprod_seq, sum]
+  congr 1
+  · rw [seq_assoc, seq_assoc, dup_pure, split, pair_tensor_pure, pair_rtimes, seq_distl_inv]
+    conv =>
+      lhs
+      simp only [← seq_assoc, rtimes_pi_r, let2_pair, nil_seq]
+      simp only [seq, inj_l, wk1_inl, wk1_nil]
+    simp [let1_beta_pure, subst0_var0_wk1, wk1_inj_l, coprod, case_inl, seq_inj_l]
+    apply congrArg
+    simp [
+      split, pair_ltimes_pure, nil_seq, rtimes, tensor, wk1_pair, seq_assoc_inv, reassoc_inv_let2,
+      reassoc_inv_beta, nil, pi_r, pr
+    ]
+    rw [<-Pure.let2_dist_pair (ha := by simp)]
+    simp [seq, let1_beta_pure, inj_l]
+  · sorry
+
 --   rw [seq_distl_inv]
 --   simp [
 --     seq_rtimes, split, distl_inv, seq_let2, coprod_seq, sum, wk1_seq, wk1_coprod,

DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean

@@ -326,6 +326,15 @@ theorem Eqv.seq_reassoc_inv {X Y A B C : Ty α} {Γ : Ctx α ε}
   : a ;;' reassoc_inv b = reassoc_inv (a ;;' b)
   := by rw [seq, wk1_reassoc_inv, let1_reassoc_inv]; rfl
 
+theorem Eqv.subst_reassoc_inv {A B C : Ty α} {Γ Δ : Ctx α ε} {σ : Subst.Eqv φ Γ Δ}
+  {a : Eqv φ Δ ⟨A.prod (B.prod C), e⟩}
+  : (reassoc_inv a).subst σ = reassoc_inv (a.subst σ) := by
+  induction a using Quotient.inductionOn; induction σ using Quotient.inductionOn; rfl
+
+theorem Eqv.reassoc_inv_subst {A B C : Ty α} {Γ Δ : Ctx α ε} {σ : Subst.Eqv φ Γ Δ}
+  {a : Eqv φ Δ ⟨A.prod (B.prod C), e⟩}
+  : reassoc_inv (a.subst σ) = (reassoc_inv a).subst σ := subst_reassoc_inv.symm
+
 def Eqv.pi_l {A B : Ty α} {Γ : Ctx α ε} : Eqv φ (⟨A.prod B, ⊥⟩::Γ) ⟨A, e⟩
   := nil.pl
 
@@ -900,14 +909,26 @@ theorem Eqv.Pure.tensor_seq_right {A₀ A₁ A₂ B₀ B₁ B₂ : Ty α} {Γ :
   (hr : r.Pure) : tensor l r ;;' tensor l' r' = tensor (l ;;' l') (r ;;' r')
   := tensor_seq_of_comm (hr.right_central _)
 
-theorem Eqv.tensor_seq_pure {A B B' C C' : Ty α} {Γ : Ctx α ε}
-  {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩} {r : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B', ⊥⟩}
+theorem Eqv.tensor_seq_pure {A A' B B' C C' : Ty α} {Γ : Ctx α ε}
+  {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩} {r : Eqv φ (⟨A', ⊥⟩::Γ) ⟨B', ⊥⟩}
   {l' : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, ⊥⟩} {r' : Eqv φ (⟨B', ⊥⟩::Γ) ⟨C', ⊥⟩}
   : tensor l r ;;' tensor l' r' = tensor (l ;;' l') (r ;;' r')
   := Eqv.Pure.tensor_seq_left (by simp)
 
+theorem Eqv.tensor_ltimes_pure {A A' B B' C : Ty α} {Γ : Ctx α ε}
+  {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩} {l' : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, ⊥⟩}
+  {r : Eqv φ (⟨A', ⊥⟩::Γ) ⟨B', ⊥⟩}
+  : tensor l r ;;' ltimes l' B' = tensor (l ;;' l') r := by
+  rw [ltimes, tensor_seq_pure, seq_nil]
+
+theorem Eqv.tensor_rtimes {A A' B B' C : Ty α} {Γ : Ctx α ε}
+  {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, e⟩}
+  {r : Eqv φ (⟨A', ⊥⟩::Γ) ⟨B', e⟩} {r' : Eqv φ (⟨B', ⊥⟩::Γ) ⟨C, e⟩}
+  : tensor l r ;;' rtimes B r' = tensor l (r ;;' r') := by
+  rw [<-ltimes_rtimes, <-seq_assoc, rtimes_rtimes, ltimes_rtimes]
+
 theorem Eqv.Pure.dup {A B : Ty α} {Γ : Ctx α ε}
-  (l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, e⟩) : l.Pure → l ;;' split = split ;;' l.tensor l
+  {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, e⟩} : l.Pure → l ;;' split = split ;;' l.tensor l
   | ⟨l, hl⟩ => by
     cases hl
     rw [seq_tensor]
@@ -920,6 +941,10 @@ theorem Eqv.Pure.dup {A B : Ty α} {Γ : Ctx α ε}
     ext k
     cases k using Fin.cases <;> rfl
 
+theorem Eqv.dup_pure {A B : Ty α} {Γ : Ctx α ε}
+  {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩} : l ;;' split = split ;;' l.tensor l
+  := Eqv.Pure.dup (by simp)
+
 @[simp]
 theorem Eqv.wk_eff_split {A : Ty α} {Γ : Ctx α ε} {h : lo ≤ hi}
   : (split (φ := φ) (Γ := Γ) (A := A) (e := lo)).wk_eff h = split := rfl
@@ -1284,3 +1309,13 @@ theorem Eqv.Pure.pair_eta {A B : Ty α} {Γ : Ctx α ε} {p : Eqv φ Γ ⟨A.pro
 theorem Eqv.pair_eta_pure {A B : Ty α} {Γ : Ctx α ε} {p : Eqv φ Γ ⟨A.prod B, ⊥⟩}
   : pair p.pl p.pr = p
   := Eqv.Pure.pair_eta (by simp)
+
+theorem Eqv.ltimes_pi_l {A B : Ty α} {Γ : Ctx α ε} {l : Eqv φ ((A, ⊥)::Γ) ⟨B, e⟩}
+  : ltimes l C ;;' pi_l = pi_l ;;' l := by
+  simp [ltimes, tensor, seq_let2, pair_pi_l, pi_l_seq]
+
+theorem Eqv.rtimes_pi_r {A B : Ty α} {Γ : Ctx α ε} {r : Eqv φ ((A, ⊥)::Γ) ⟨B, e⟩}
+  : rtimes C r ;;' pi_r = pi_r ;;' r := by
+  simp only [rtimes, tensor, wk1_nil, seq_let2, wk1_pi_r, pi_r_seq]
+  rw [pair_pi_r]
+  exact ⟨(var 1 Ctx.Var.shead.step), rfl⟩

DeBruijnSSA/BinSyntax/Syntax.lean

@@ -208,8 +208,8 @@ theorem TRegion.coe_toRegion_vsubst (σ : Term.Subst φ) (t : TRegion φ)
 def BBCFG.toTCFG : BBCFG φ ≃ TCFG φ where
   toFun := λG => ⟨G.length, TRegion.ofBBRegion ∘ G.targets⟩
   invFun := λG => ⟨G.length, TRegion.ofBBRegion.symm ∘ G.targets⟩
-  left_inv := λ⟨_, _⟩ => by simp [<-Function.comp.assoc]
-  right_inv := λ⟨_, _⟩ => by simp [<-Function.comp.assoc]
+  left_inv := λ⟨_, _⟩ => by simp [<-Function.comp_assoc]
+  right_inv := λ⟨_, _⟩ => by simp [<-Function.comp_assoc]
 
 /-- Convert a terminator CFG to a basic block CFG -/
 def TCFG.toBBCFG : TCFG φ ≃ BBCFG φ := BBCFG.toTCFG.symm

DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean

@@ -228,7 +228,7 @@ theorem lsubst_vlift_lift_append {r₀ r₁ : Region φ} {σ : Region.Subst φ}
       vwk1_lsubst, vsubst_lsubst, Term.wk, Nat.liftWk
     ]
     congr
-    · simp only [<-Function.comp.assoc, vwk1, vwk2, <-vwk_comp]
+    · simp only [<-Function.comp_assoc, vwk1, vwk2, <-vwk_comp]
       apply congrFun
       apply congrArg
       funext r

DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Cong.lean

@@ -326,7 +326,7 @@ theorem Cong.fv_eq {P : Region φ → Region φ → Sort _} {r r' : Region φ}
     funext k
     simp only [<-Function.comp_apply (f := Multiset.liftnFv 1)]
     simp only [<-Function.comp_apply (g := G)]
-    rw [Function.comp.assoc]
+    rw [Function.comp_assoc]
     rw [Function.update_eq_self]
   | _ => simp [*]
 

DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Directed.lean

@@ -205,7 +205,7 @@ def RWD.cast {P} {Γ : ℕ → ε} {r₀ r₀' r₁ r₁' : Region φ} (hr₀ :
 --     (by
 --       rw [
 --         <-Fin.comp_addCases,
---         <-Function.comp.assoc,
+--         <-Function.comp_assoc,
 --         lwk_lwk, comp_lwk,
 --         Fin.swapAdd
 --       ]
@@ -347,7 +347,7 @@ def RWD.cfg_blocks {P} {Γ : ℕ → ε} (β n) (G G' : Fin n → Region φ)
 --     (cfg β n G) :=
 --     (cast_trg (swap_cfg (β.lwk (n.liftnWk (· + m))) n (lwk (n.liftnWk (· + m)) ∘ G) m G')
 --       (by rw [
---         Fin.comp_addCases, lwk_lwk, <-Function.comp.assoc, comp_lwk,
+--         Fin.comp_addCases, lwk_lwk, <-Function.comp_assoc, comp_lwk,
 --         Fin.toNatWk_swapAdd_comp_liftnWk_add]
 --       )).comp
 --     (dead_cfg_left β m _ n G)

DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean

@@ -272,13 +272,13 @@ theorem Reduce.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (p : Reduce r r') : Red
 --     rw [sup_assoc, sup_comm (r.effect _), <-sup_assoc]
 --     simp
 --   | wk_cfg _ _ _ _ _ =>
---     simp only [effect_cfg, effect_lwk, <-Function.comp.assoc, effect_comp_lwk]
+--     simp only [effect_cfg, effect_lwk, <-Function.comp_assoc, effect_comp_lwk]
 --     apply sup_le_sup_left
 --     apply Fin.sup_comp_le
 --   | dead_cfg_left _ _ _ _ =>
 --     simp only [effect_cfg, effect_lwk, Fin.comp_addCases, Fin.sup_addCases]
 --     apply sup_le_sup_left
 --     apply le_sup_of_le_right
---     rw [<-Function.comp.assoc, effect_comp_lwk]
+--     rw [<-Function.comp_assoc, effect_comp_lwk]
 --   | ucfg β n G =>
 --     simp only [effect_cfg, Region.ucfg, effect_lsubst, Fin.sup_ucfg]

DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean

@@ -130,7 +130,7 @@ def RewriteD.cast {r₀ r₀' r₁ r₁' : Region φ} (h₀ : r₀ = r₀') (h
 --     funext i
 --     simp [Region.effect_lwk]
 --   -- | cfg_fuse β n G k ρ hρ =>
---   --   simp only [effect_cfg, effect_lwk, <-Function.comp.assoc, effect_comp_lwk]
+--   --   simp only [effect_cfg, effect_lwk, <-Function.comp_assoc, effect_comp_lwk]
 --   --   apply congrArg
 --   --   rw [Fin.sup_comp_surj _ hρ]
 --   | let1_eta => sorry

DeBruijnSSA/BinSyntax/Syntax/Subst/Region.lean

@@ -308,7 +308,7 @@ theorem Subst.id_comp (σ : Subst φ) : Subst.id.comp σ = σ
 
 theorem Subst.vlift_comp_liftWk_stepn (σ : Subst φ) (n)
     : vlift (vwk (Nat.liftWk (· + n)) ∘ σ) = vwk (Nat.liftWk (· + n)) ∘ σ.vlift := by
-  simp only [vlift, vwk1, <-Function.comp.assoc]
+  simp only [vlift, vwk1, <-Function.comp_assoc]
   apply congrArg₂
   funext i
   simp only [Function.comp_apply, vwk_vwk]
@@ -378,11 +378,11 @@ theorem Subst.vwk_liftWk_comp_liftn (σ : Subst φ) (ρ)
 
 theorem Subst.vwk_liftWk_liftWk_comp_vlift (σ : Subst φ) (ρ)
     : vwk (Nat.liftWk (Nat.liftWk ρ)) ∘ σ.vlift = vlift (vwk (Nat.liftWk ρ) ∘ σ) := by
-  simp only [vlift, vwk1, ← Function.comp.assoc, ← vwk_comp, ← Nat.liftWk_comp, Nat.liftWk_comp_succ]
+  simp only [vlift, vwk1, ← Function.comp_assoc, ← vwk_comp, ← Nat.liftWk_comp, Nat.liftWk_comp_succ]
 
 theorem Subst.vwk_liftWk_liftnWk_comp_vliftn (n : ℕ) (σ : Subst φ) (ρ)
     : vwk (Nat.liftWk (Nat.liftnWk n ρ)) ∘ σ.vliftn n = vliftn n (vwk (Nat.liftWk ρ) ∘ σ) := by
-  simp only [vliftn, ← Function.comp.assoc, ← vwk_comp, ← Nat.liftWk_comp, Nat.liftnWk_comp_add]
+  simp only [vliftn, ← Function.comp_assoc, ← vwk_comp, ← Nat.liftWk_comp, Nat.liftnWk_comp_add]
 
 theorem vwk_lsubst (σ ρ) (t : Region φ)
   : (t.lsubst σ).vwk ρ = (t.vwk ρ).lsubst (vwk (Nat.liftWk ρ) ∘ σ)
@@ -400,12 +400,12 @@ theorem vwk1_lsubst (σ) (t : Region φ)
 
 theorem vwk1_lsubst_vlift (σ : Subst φ) (t : Region φ)
   : (t.lsubst σ.vlift).vwk1 = t.vwk1.lsubst σ.vlift.vlift
-  := by simp only [Subst.vlift, vwk1_lsubst, ←Function.comp.assoc, vwk2_comp_vwk1]
+  := by simp only [Subst.vlift, vwk1_lsubst, ←Function.comp_assoc, vwk2_comp_vwk1]
 
 theorem vwk2_lsubst_vlift₂ (σ : Subst φ) (t : Region φ)
   : (t.lsubst σ.vlift.vlift).vwk2 = t.vwk2.lsubst σ.vlift.vlift.vlift
   := by
-  simp only [Subst.vlift, vwk2, vwk_lsubst, vwk1, <-vwk_comp, <-Function.comp.assoc]
+  simp only [Subst.vlift, vwk2, vwk_lsubst, vwk1, <-vwk_comp, <-Function.comp_assoc]
   congr
   apply congrFun
   apply congrArg
@@ -419,16 +419,16 @@ theorem Subst.vliftn_comp (n : ℕ) (σ τ : Subst φ)
   simp only [Function.comp_apply, comp, vlift, vliftn, vwk1, Function.comp_apply]
   generalize τ m = t
   rw [vwk_lsubst]
-  simp only [<-Function.comp.assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ]
+  simp only [<-Function.comp_assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ]
 
 theorem Subst.vlift_comp (σ τ : Subst φ) : (σ.comp τ).vlift = σ.vlift.comp τ.vlift
   := σ.vliftn_comp 1 τ
 
 theorem Subst.lwk_comp_vlift (ρ) (σ : Subst φ) : lwk ρ ∘ σ.vlift = vlift (lwk ρ ∘ σ)
-  := by simp only [vlift, vwk1, <-Function.comp.assoc, vwk_comp_lwk]
+  := by simp only [vlift, vwk1, <-Function.comp_assoc, vwk_comp_lwk]
 
 theorem Subst.lwk_comp_vliftn (ρ) (σ : Subst φ) (n) : lwk ρ ∘ σ.vliftn n = vliftn n (lwk ρ ∘ σ)
-  := by simp only [vliftn, <-Function.comp.assoc, vwk_comp_lwk]
+  := by simp only [vliftn, <-Function.comp_assoc, vwk_comp_lwk]
 
 theorem Subst.vlift_comp_lwk (σ : Subst φ) (ρ) : vlift (σ ∘ ρ) = σ.vlift ∘ ρ := rfl
 
@@ -469,7 +469,7 @@ theorem Subst.liftn_comp (n : ℕ) (σ τ : Subst φ) : (σ.comp τ).liftn n = (
   case isFalse h =>
     rw [lwk_lsubst, lsubst_lwk]
     congr
-    rw [lwk_comp_vlift, vlift, vlift, Function.comp.assoc, liftn_comp_add]
+    rw [lwk_comp_vlift, vlift, vlift, Function.comp_assoc, liftn_comp_add]
 
 theorem Subst.lift_comp (σ τ : Subst φ) : (σ.comp τ).lift = σ.lift.comp τ.lift := by
   have h := Subst.liftn_comp 1 σ τ
@@ -516,8 +516,8 @@ theorem llsubst_lcomp (σ τ : Subst φ) : llsubst (σ.lcomp τ) = llsubst σ 
   funext k
   simp only [Function.comp_apply, vwk, Term.wk, Nat.liftWk_zero, let1.injEq, true_and, vwk_vwk]
   congr
-  simp only [<-Nat.liftWk_comp, Nat.liftWk_comp_succ, <-Function.comp.assoc]
-  rw [Function.comp.assoc, Nat.liftWk_comp_succ, Function.comp.assoc]
+  simp only [<-Nat.liftWk_comp, Nat.liftWk_comp_succ, <-Function.comp_assoc]
+  rw [Function.comp_assoc, Nat.liftWk_comp_succ, Function.comp_assoc]
 
 theorem llsubst_llsubst (σ τ : Subst φ) (t : Region φ)
   : (t.llsubst τ).llsubst σ = t.llsubst (σ.lcomp τ)
@@ -603,7 +603,7 @@ theorem vsubst_lift₃_vwk2 {ρ : Term.Subst φ} {r : Region φ}
 
 theorem vsubst_lift_lift_comp_vlift {ρ : Term.Subst φ} {σ : Subst φ}
   : (vsubst ρ.lift.lift ∘ σ.vlift) = Subst.vlift (vsubst ρ.lift ∘ σ) := by
-  rw [Subst.vlift, <-Function.comp.assoc, vsubst_lift_lift_comp_vwk1]; rfl
+  rw [Subst.vlift, <-Function.comp_assoc, vsubst_lift_lift_comp_vwk1]; rfl
 
 theorem Subst.vsubst_lift_comp_liftn (σ : Subst φ) (ρ : Term.Subst φ)
     : vsubst ρ.lift ∘ σ.liftn n = liftn n (vsubst ρ.lift ∘ σ) := by

DeBruijnSSA/BinSyntax/Syntax/Subst/Terminator.lean

@@ -287,7 +287,7 @@ theorem Subst.id_comp (σ : Subst φ) : Subst.id.comp σ = σ
 
 theorem Subst.vlift_comp_liftWk_stepn (σ : Subst φ) (n)
   : vlift (vwk (Nat.liftWk (· + n)) ∘ σ) = vwk (Nat.liftWk (· + n)) ∘ σ.vlift := by
-  simp only [vlift, vwk1, <-Function.comp.assoc]
+  simp only [vlift, vwk1, <-Function.comp_assoc]
   apply congrArg₂
   funext i
   simp only [Function.comp_apply, vwk_vwk]
@@ -350,7 +350,7 @@ theorem vwk_lsubst (σ ρ) (t : Terminator φ)
   | _ =>
     simp only [vwk, lsubst, *]
     congr <;> simp only [
-      Subst.vlift, vwk1, <-Function.comp.assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ
+      Subst.vlift, vwk1, <-Function.comp_assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ
     ]
 
 theorem Subst.vliftn_comp (n : ℕ) (σ τ : Subst φ)
@@ -360,7 +360,7 @@ theorem Subst.vliftn_comp (n : ℕ) (σ τ : Subst φ)
   simp only [Function.comp_apply, comp, vlift, vliftn, vwk1, Function.comp_apply]
   generalize τ m = t
   rw [vwk_lsubst]
-  simp only [<-Function.comp.assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ]
+  simp only [<-Function.comp_assoc, <-vwk_comp, <-Nat.liftWk_comp, Nat.liftWk_comp_succ]
 
 theorem Subst.vlift_comp (σ τ : Subst φ) : (σ.comp τ).vlift = σ.vlift.comp τ.vlift
   := σ.vliftn_comp 1 τ

DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean

@@ -672,7 +672,7 @@ theorem Region.InS.vwk1_lsubst_vlift {Γ : Ctx α ε} {L K : LCtx α}
   simp only [Set.mem_setOf_eq, vwk1, coe_vwk, Ctx.InS.coe_wk1, coe_lsubst, Subst.InS.coe_vlift,
     Subst.vlift, Region.vwk_lsubst]
   congr
-  simp only [<-Function.comp.assoc, Region.vwk1, <-Region.vwk_comp]
+  simp only [<-Function.comp_assoc, Region.vwk1, <-Region.vwk_comp]
   apply congrFun
   apply congrArg
   apply congrArg

lake-manifest.json

@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "418c53780957030e8fd99d2007872a87ad82d9e6",
+   "rev": "7da2960d5ff6656028a8d2bece5370ad5859b270",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "64879d94466c15f3832a5eb1e85efbdc7956d2da",
+   "rev": "632e2ca5a9a34f2f541ebfaa91795816fd679370",
    "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",