Prove Specifies.smul

Signed-off-by: zeramorphic <[email protected]>

ConNF/Counting/Spec.lean

@@ -72,11 +72,12 @@ inductive SpecifiesC (σ : Spec β) (S : Support β)
         {i | ∃ hi : i < S.max, S.f i hi = ⟨h.path.B.cons (bot_lt_coe _), inl h.a⟩})
       ⟨A, inr N⟩
 
+/-- TODO: We really should make this definition much earlier. -/
 def Address.comp {β γ : TypeIndex} (A : Quiver.Path β γ) (c : Address γ) : Address β :=
   ⟨A.comp c.1, c.2⟩
 
-inductive Specifies : ∀ {β : Λ}, Spec β → Support β → Prop
-  | mk (σ : Spec β) (S : Support β)
+inductive Spec.Specifies : ∀ {β : Λ}, Spec β → Support β → Prop
+  | mk {β : Λ} (σ : Spec β) (S : Support β)
     (max_eq_max : σ.cond.max = S.max)
     (lS : ∀ {γ : Λ}, (γ : TypeIndex) < β → Path (β : TypeIndex) γ → Support γ)
     (hlS₁ : ∀ {γ : Λ} (hγ : (γ : TypeIndex) < β) (A : Path (β : TypeIndex) γ),
@@ -85,9 +86,83 @@ inductive Specifies : ∀ {β : Λ}, Spec β → Support β → Prop
       (i : κ) (hi : i < (lS hγ A).max),
       ((lS hγ A).f i hi).comp A = S.f (σ.r hγ A i) (hlS₁ hγ A i hi))
     (hlS₃ : ∀ {γ : Λ} (hγ : (γ : TypeIndex) < β) (A : Path (β : TypeIndex) γ),
-      Specifies (σ.lower hγ A) (lS hγ A))
+      (σ.lower hγ A).Specifies (lS hγ A))
     (cond : ∀ (i : κ) (hiσ : i < σ.cond.max) (hiS : i < S.max),
       SpecifiesC σ S lS (σ.cond.f i hiσ) (S.f i hiS)) :
-    Specifies σ S
+    σ.Specifies S
+
+variable {σ : Spec β} {S : Support β}
+  {lS : ∀ {γ : Λ}, (hγ : (γ : TypeIndex) < β) → (A : Path (β : TypeIndex) γ) → Support γ}
+
+theorem specifiesC_atom_right_iff (σc : SpecComponent β) (A : ExtendedIndex β) (a : Atom) :
+    SpecifiesC σ S lS σc ⟨A, inl a⟩ ↔
+      σc = SpecComponent.atom A
+        {i | ∃ hi : i < S.max, S.f i hi = ⟨A, inl a⟩}
+        {i | ∃ N : NearLitter, a ∈ N ∧ ∃ hi : i < S.max, S.f i hi = ⟨A, inr N⟩} := by
+  constructor
+  · rintro ⟨⟩
+    rfl
+  · rintro rfl
+    exact SpecifiesC.atom A a
+
+theorem specifiesC_flexible_right_iff (σc : SpecComponent β)
+    (A : ExtendedIndex β) (N : NearLitter) (hN : Flexible A N.1) :
+    SpecifiesC σ S lS σc ⟨A, inr N⟩ ↔
+      σc = SpecComponent.flexible A
+        {i | ∃ hi : i < S.max, ∃ N', S.f i hi = ⟨A, inr N'⟩ ∧ N'.1 = N.1} := by
+  constructor
+  · intro h
+    cases h
+    case flexible => rfl
+    case inflexibleCoe r h hr hS =>
+      rw [flexible_iff_not_inflexibleBot_inflexibleCoe] at hN
+      exact hN.2.elim h
+    case inflexibleBot h =>
+      rw [flexible_iff_not_inflexibleBot_inflexibleCoe] at hN
+      exact hN.1.elim h
+  · rintro rfl
+    exact SpecifiesC.flexible A N hN
+
+theorem specifiesC_inflexibleCoe_right_iff (σc : SpecComponent β)
+    (A : ExtendedIndex β) (N : NearLitter) (hN : InflexibleCoe A N.1) :
+    SpecifiesC σ S lS σc ⟨A, inr N⟩ ↔
+      ∃ (r : κ → κ)
+      (hr : ∀ i < hN.t.support.max, r i < (lS (hN.path.δ_lt_β) (hN.path.B.cons hN.path.hδ)).max),
+      (∀ (i : κ) (hit : i < hN.t.support.max), hN.t.support.f i hit =
+        (lS (hN.path.δ_lt_β) (hN.path.B.cons hN.path.hδ)).f (r i) (hr i hit)) ∧
+      σc = SpecComponent.inflexibleCoe A hN.path
+        (CodingFunction.code hN.t.support hN.t (support_supports _)) r := by
+  constructor
+  · intro h
+    cases h
+    case flexible h' =>
+      rw [flexible_iff_not_inflexibleBot_inflexibleCoe] at h'
+      exact h'.2.elim hN
+    case inflexibleCoe r h hr hS =>
+      cases Subsingleton.elim hN h
+      exact ⟨r, hr, hS, rfl⟩
+    case inflexibleBot h =>
+      cases inflexibleBot_inflexibleCoe h hN
+  · rintro ⟨r, hr, hS, rfl⟩
+    exact SpecifiesC.inflexibleCoe A N hN r hr hS
+
+theorem specifiesC_inflexibleBot_right_iff (σc : SpecComponent β)
+    (A : ExtendedIndex β) (N : NearLitter) (hN : InflexibleBot A N.1) :
+    SpecifiesC σ S lS σc ⟨A, inr N⟩ ↔
+      σc = SpecComponent.inflexibleBot A hN.path
+        {i | ∃ hi : i < S.max, S.f i hi = ⟨hN.path.B.cons (bot_lt_coe _), inl hN.a⟩} := by
+  constructor
+  · intro h
+    cases h
+    case flexible h' =>
+      rw [flexible_iff_not_inflexibleBot_inflexibleCoe] at h'
+      exact h'.1.elim hN
+    case inflexibleCoe _ h _ _ =>
+      cases inflexibleBot_inflexibleCoe hN h
+    case inflexibleBot h =>
+      cases Subsingleton.elim hN h
+      rfl
+  · rintro ⟨r, hr, hS, rfl⟩
+    exact SpecifiesC.inflexibleBot A N hN
 
 end ConNF

ConNF/Counting/SpecSMul.lean

@@ -10,14 +10,16 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [i : LeLevel β]
+variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [i : LeLevel β] {σ : Spec β} {S : Support β}
+    {lS : ∀ {γ : Λ}, (hγ : (γ : TypeIndex) < β) → (A : Path (β : TypeIndex) γ) → Support γ}
 
-theorem specifiesCondition_atom_smul {S : Support β}
-    {σc : SpecCondition β} {A : ExtendedIndex β} {a : Atom}
-    (h : Spec.SpecifiesCondition S σc ⟨A, inl a⟩) (ρ : Allowable β) :
-    Spec.SpecifiesCondition (ρ • S) σc ⟨A, inl (Allowable.toStructPerm ρ A • a)⟩ := by
-  rw [Spec.specifiesCondition_atom_right_iff] at h
-  rw [Spec.specifiesCondition_atom_right_iff, h, SpecCondition.atom.injEq]
+theorem specifiesCondition_atom_smul
+    {σc : SpecComponent β} {A : ExtendedIndex β} {a : Atom}
+    (h : SpecifiesC σ S lS σc ⟨A, inl a⟩) (ρ : Allowable β) :
+    SpecifiesC σ (ρ • S) (fun hγ A => (Allowable.toStructPerm ρ).comp A • lS hγ A)
+      σc ⟨A, inl (Allowable.toStructPerm ρ A • a)⟩ := by
+  rw [specifiesC_atom_right_iff] at h
+  rw [specifiesC_atom_right_iff, h, SpecComponent.atom.injEq]
   simp only [Allowable.smul_support_f, Allowable.smul_support_max, true_and]
   constructor
   · ext i
@@ -30,7 +32,7 @@ theorem specifiesCondition_atom_smul {S : Support β}
       refine ⟨hi₁, ?_⟩
       rw [smul_eq_iff_eq_inv_smul] at hi₂
       rw [hi₂]
-      simp only [Allowable.smul_Address, map_inv, Tree.inv_apply, smul_inl, inv_smul_smul]
+      simp only [Allowable.smul_address, map_inv, Tree.inv_apply, smul_inl, inv_smul_smul]
   · ext i
     constructor
     · rintro ⟨N, ha, hi₁, hi₂⟩
@@ -43,89 +45,112 @@ theorem specifiesCondition_atom_smul {S : Support β}
       refine ⟨(Allowable.toStructPerm ρ A)⁻¹ • N, ha, hi₁, ?_⟩
       rw [smul_eq_iff_eq_inv_smul] at hi₂
       rw [hi₂]
-      simp only [Allowable.smul_Address, map_inv, Tree.inv_apply, smul_inr]
+      simp only [Allowable.smul_address, map_inv, Tree.inv_apply, smul_inr]
 
 theorem specifiesCondition_flexible_smul {S : Support β}
-    {σc : SpecCondition β} {A : ExtendedIndex β} {N : NearLitter} (hN : Flexible A N.1)
-    (h : Spec.SpecifiesCondition S σc ⟨A, inr N⟩) (ρ : Allowable β) :
-    Spec.SpecifiesCondition (ρ • S) σc ⟨A, inr (Allowable.toStructPerm ρ A • N)⟩ := by
-  rw [Spec.specifiesCondition_flexible_right_iff _ _ _ hN] at h
-  rw [Spec.specifiesCondition_flexible_right_iff _ _ _ (by exact hN.smul ρ)]
-  exact h
+    {σc : SpecComponent β} {A : ExtendedIndex β} {N : NearLitter} (hN : Flexible A N.1)
+    (h : SpecifiesC σ S lS σc ⟨A, inr N⟩) (ρ : Allowable β) :
+    SpecifiesC σ (ρ • S) (fun hγ A => (Allowable.toStructPerm ρ).comp A • lS hγ A) σc
+      ⟨A, inr (Allowable.toStructPerm ρ A • N)⟩ := by
+  rw [specifiesC_flexible_right_iff _ _ _ hN] at h
+  rw [specifiesC_flexible_right_iff _ _ _ (by exact hN.smul ρ), h]
+  refine congr_arg _ ?_
+  ext i
+  constructor
+  · rintro ⟨hi, N', hS, hN'⟩
+    refine ⟨hi, Allowable.toStructPerm ρ A • N', ?_, ?_⟩
+    · rw [Allowable.smul_support_f, hS]
+      rfl
+    · rw [NearLitterPerm.smul_nearLitter_fst, hN']
+      rfl
+  · rintro ⟨hi, N', hS, hN'⟩
+    refine ⟨hi, (Allowable.toStructPerm ρ A)⁻¹ • N', ?_, ?_⟩
+    · rw [Allowable.smul_support_f, smul_eq_iff_eq_inv_smul] at hS
+      rw [hS, Allowable.smul_address]
+      simp only [map_inv, Tree.inv_apply, smul_inr]
+    · rw [NearLitterPerm.smul_nearLitter_fst, hN',
+        NearLitterPerm.smul_nearLitter_fst, inv_smul_smul]
 
 theorem specifiesCondition_inflexibleCoe_smul {S : Support β}
-    {σc : SpecCondition β} {A : ExtendedIndex β} {N : NearLitter} (hN : InflexibleCoe A N.1)
-    (h : Spec.SpecifiesCondition S σc ⟨A, inr N⟩) (ρ : Allowable β)
-    (ih : ∀ {σ : Spec hN.path.δ} {S : Support hN.path.δ} (_ : σ.Specifies S)
-      (ρ : Allowable hN.path.δ), σ.Specifies (ρ • S)) :
-    Spec.SpecifiesCondition (ρ • S) σc ⟨A, inr (Allowable.toStructPerm ρ A • N)⟩ := by
-  rw [Spec.specifiesCondition_inflexibleCoe_right_iff _ _ _ hN] at h
-  rw [Spec.specifiesCondition_inflexibleCoe_right_iff _ _ _ (by exact hN.smul ρ)]
-  obtain ⟨S', hS', σ, hσ, h⟩ := h
-  refine ⟨Allowable.comp (hN.path.B.cons hN.path.hδ) ρ • S', ?_, σ, ih hσ _, ?_⟩
-  · have := Allowable.support_isSum_smul hS' (Allowable.comp (hN.path.B.cons hN.path.hδ) ρ)
-    rw [inflexibleCoe_smul_t, smul_support]
-    rw [Allowable.comp_smul_support_comp] at this
-    exact this
-  · rw [h]
+    {σc : SpecComponent β} {A : ExtendedIndex β} {N : NearLitter} (hN : InflexibleCoe A N.1)
+    (h : SpecifiesC σ S lS σc ⟨A, inr N⟩) (ρ : Allowable β) :
+    SpecifiesC σ (ρ • S) (fun hγ A => (Allowable.toStructPerm ρ).comp A • lS hγ A) σc
+      ⟨A, inr (Allowable.toStructPerm ρ A • N)⟩ := by
+  rw [specifiesC_inflexibleCoe_right_iff _ _ _ hN] at h
+  rw [specifiesC_inflexibleCoe_right_iff _ _ _ (by exact hN.smul ρ)]
+  obtain ⟨r, hr, hS, rfl⟩ := h
+  refine ⟨r, ?_, ?_, ?_⟩
+  · intro i hi
+    simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleCoe_smul_path, inflexibleCoe_smul_t,
+      smul_support, Allowable.smul_support_max] at hi
+    exact hr i hi
+  · intro i hi
     simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleCoe_smul_path, inflexibleCoe_smul_t,
-      smul_support, SpecCondition.inflexibleCoe.injEq, heq_eq_eq, and_true, true_and]
-    rw [CodingFunction.code_smul]
+      smul_support, Allowable.smul_support_max, Support.smul_f] at hi ⊢
+    rw [← hS i hi]
+    simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleCoe_smul_path,
+      Allowable.toStructPerm_smul, Allowable.toStructPerm_comp, Support.smul_f]
+  · refine congr_arg₂ _ ?_ rfl
+    simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleCoe_smul_path, inflexibleCoe_smul_t,
+      smul_support]
+    exact (CodingFunction.code_smul _ _ _ _ _).symm
 
 theorem specifiesCondition_inflexibleBot_smul {S : Support β}
-    {σc : SpecCondition β} {A : ExtendedIndex β} {N : NearLitter} (hN : InflexibleBot A N.1)
-    (h : Spec.SpecifiesCondition S σc ⟨A, inr N⟩) (ρ : Allowable β) :
-    Spec.SpecifiesCondition (ρ • S) σc ⟨A, inr (Allowable.toStructPerm ρ A • N)⟩ := by
-  rw [Spec.specifiesCondition_inflexibleBot_right_iff _ _ _ hN] at h
-  rw [Spec.specifiesCondition_inflexibleBot_right_iff _ _ _ (by exact hN.smul ρ),
-    h, SpecCondition.inflexibleBot.injEq]
+    {σc : SpecComponent β} {A : ExtendedIndex β} {N : NearLitter} (hN : InflexibleBot A N.1)
+    (h : SpecifiesC σ S lS σc ⟨A, inr N⟩) (ρ : Allowable β) :
+    SpecifiesC σ (ρ • S) (fun hγ A => (Allowable.toStructPerm ρ).comp A • lS hγ A) σc
+      ⟨A, inr (Allowable.toStructPerm ρ A • N)⟩ := by
+  rw [specifiesC_inflexibleBot_right_iff _ _ _ hN] at h
+  rw [specifiesC_inflexibleBot_right_iff _ _ _ (by exact hN.smul ρ),
+    h, SpecComponent.inflexibleBot.injEq]
   refine ⟨rfl, HEq.rfl, ?_⟩
   ext i
   constructor
   · rintro ⟨hi₁, hi₂⟩
     refine ⟨hi₁, ?_⟩
     rw [Allowable.smul_support_f, hi₂]
-    simp only [Allowable.smul_Address, smul_inl, NearLitterPerm.smul_nearLitter_fst,
+    simp only [Allowable.smul_address, smul_inl, NearLitterPerm.smul_nearLitter_fst,
       inflexibleBot_smul_path, inflexibleBot_smul_a, ofBot_smul, Allowable.toStructPerm_apply]
   · rintro ⟨hi₁, hi₂⟩
     refine ⟨hi₁, ?_⟩
     rw [Allowable.smul_support_f, smul_eq_iff_eq_inv_smul] at hi₂
     rw [hi₂]
     simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleBot_smul_path, inflexibleBot_smul_a,
-      ofBot_smul, Allowable.toStructPerm_apply, Allowable.smul_Address, map_inv,
+      ofBot_smul, Allowable.toStructPerm_apply, Allowable.smul_address, map_inv,
       Tree.inv_apply, smul_inl, inv_smul_smul]
 
-theorem Spec.SpecifiesCondition.smul {S : Support β}
-    {σc : SpecCondition β} {c : Address β}
-    (h : Spec.SpecifiesCondition S σc c) (ρ : Allowable β) :
-    Spec.SpecifiesCondition (ρ • S) σc (ρ • c) := by
-  have : WellFoundedLT Λ := inferInstance
-  revert i S σc c
-  have := this.induction
-    (C := fun β => (i : LeLevel β) → ∀ S : Support β, ∀ σc : SpecCondition β,
-      ∀ c : Address β, ∀ _ : Spec.SpecifiesCondition S σc c, ∀ ρ : Allowable β,
-      Spec.SpecifiesCondition (ρ • S) σc (ρ • c))
-  refine this β ?_
-  intro β ih _ S σc c h ρ
+theorem SpecifiesC.smul {σc : SpecComponent β} {c : Address β}
+    (h : SpecifiesC σ S lS σc c) (ρ : Allowable β) :
+    SpecifiesC σ (ρ • S) (fun hγ A => (Allowable.toStructPerm ρ).comp A • lS hγ A) σc (ρ • c) := by
   obtain ⟨B, a | N⟩ := c
   · exact specifiesCondition_atom_smul h ρ
   · obtain (h' | ⟨⟨h'⟩⟩ | ⟨⟨h'⟩⟩) := flexible_cases' B N.1
     · exact specifiesCondition_flexible_smul h' h ρ
     · exact specifiesCondition_inflexibleBot_smul h' h ρ
-    · refine specifiesCondition_inflexibleCoe_smul h' h ρ ?_
-      intro σ S hS ρ
-      rw [specifies_iff] at hS ⊢
-      constructor
-      · exact hS.1
-      · intro i hiσ hiS
-        exact ih h'.path.δ (coe_lt_coe.mp h'.δ_lt_β) inferInstance S _ _ (hS.2 i hiσ hiS) ρ
+    · exact specifiesCondition_inflexibleCoe_smul h' h ρ
 
 theorem Spec.Specifies.smul {σ : Spec β} {S : Support β} (h : σ.Specifies S) (ρ : Allowable β) :
     σ.Specifies (ρ • S) := by
-  rw [specifies_iff] at h ⊢
-  constructor
-  · exact h.1
+  have : WellFoundedLT Λ := inferInstance
+  revert i σ S
+  have := this.induction
+    (C := fun β => ∀ (i : LeLevel ↑β) {σ : Spec β} {S : Support ↑β},
+      Specifies σ S → ∀ (ρ : Allowable ↑β), Specifies σ (ρ • S))
+  refine this β ?_
+  intro β ih i σ S h ρ
+  obtain ⟨_, _, max_eq_max, lS, hlS₁, hlS₂, hlS₃, cond⟩ := h
+  refine ⟨_, _, max_eq_max, fun hγ A => (Allowable.toStructPerm ρ).comp A • lS hγ A,
+      hlS₁, ?_, ?_, ?_⟩
+  · intro γ hγ A i hi
+    simp only [Support.smul_f, Allowable.smul_support_f]
+    rw [← hlS₂ hγ A i hi]
+    rfl
+  · intro γ hγ A
+    have : LeLevel γ := ⟨hγ.le.trans i.elim⟩
+    have := ih γ (coe_lt_coe.mp hγ) _ (hlS₃ hγ A) (Allowable.comp A ρ)
+    rw [Allowable.toStructPerm_smul, Allowable.toStructPerm_comp] at this
+    exact this
   · intro i hiσ hiS
-    exact (h.2 i hiσ hiS).smul ρ
+    exact (cond i hiσ hiS).smul ρ
 
 end ConNF

ConNF/FOA/Basic/Reduction.lean

@@ -160,7 +160,7 @@ theorem reduction_supports (S : Set (Address β)) (c : Address β) (hc : c ∈ S
   by_cases h : N.IsLitter
   · obtain ⟨L, rfl⟩ := h.exists_litter_eq
     exact hc' (mem_reduction_of_reduced _ _ (Reduced.mkLitter L) hc)
-  simp only [StructPerm.smul_Address_eq_iff, smul_inr, inr.injEq] at hc' ⊢
+  simp only [StructPerm.smul_address_eq_iff, smul_inr, inr.injEq] at hc' ⊢
   have h₃ := hc' (mem_reduction_of_reduced_constrains _ ⟨B, inr N.fst.toNearLitter⟩ _
     (Reduced.mkLitter N.fst) (Constrains.nearLitter B N h) hc)
   have h₄ := fun a ha => hc' (mem_reduction_of_reduced_constrains _ ⟨B, inl a⟩ _

ConNF/FOA/Properties/Injective.lean

@@ -91,7 +91,7 @@ theorem Biexact.smul_eq_smul {β : Λ} [LeLevel β] {π π' : Allowable β} {c :
     (constrains_wf β) c _
   clear c
   intro c ih h
-  simp only [Allowable.smul_Address_eq_smul_iff] at ih ⊢
+  simp only [Allowable.smul_address_eq_smul_iff] at ih ⊢
   obtain ⟨A, a | N⟩ := c
   · simp only [smul_inl, inl.injEq]
     exact h.smul_eq_smul_atom A a Relation.ReflTransGen.refl
@@ -138,7 +138,7 @@ theorem Biexact.smul_eq_smul {β : Λ} [LeLevel β] {π π' : Allowable β} {c :
     rw [mul_smul, inv_smul_eq_iff]
     simp only [Allowable.toStructPerm_smul, Allowable.toStructPerm_comp, Tree.comp_comp]
     have := ih ⟨(B.cons hδ).comp c.path, c.value⟩ ?_ ?_
-    · simp only [Path.comp_cons, Path.comp_nil, StructPerm.smul_Address_eq_smul_iff,
+    · simp only [Path.comp_cons, Path.comp_nil, StructPerm.smul_address_eq_smul_iff,
         Tree.comp_apply]
       exact this.symm
     · exact Constrains.fuzz hδ hε hδε _ _ _ hc
@@ -166,7 +166,7 @@ theorem Biexact.smul_eq_smul_nearLitter {β : Λ} [LeLevel β]
     Allowable.toStructPerm π A • N =
     Allowable.toStructPerm π' A • N := by
   have := h.smul_eq_smul
-  simp only [Allowable.toStructPerm_smul, StructPerm.smul_Address_eq_smul_iff, smul_inr,
+  simp only [Allowable.toStructPerm_smul, StructPerm.smul_address_eq_smul_iff, smul_inr,
     inr.injEq] at this
   exact this
 
@@ -341,7 +341,7 @@ theorem supports {β : Λ} [LeLevel β] {π π' : Allowable β} {t : Tangle β}
   refine' support_supports t _ _
   intro c hc
   rw [mul_smul, inv_smul_eq_iff]
-  simp only [Allowable.smul_Address_eq_smul_iff]
+  simp only [Allowable.smul_address_eq_smul_iff]
   obtain ⟨A, a | N⟩ := c
   · simp only [smul_inl, inl.injEq]
     exact ha A a hc
@@ -719,7 +719,7 @@ theorem ihAction_smul_tangle' (hπf : π.Free) (c d : Address β) (A : ExtendedI
   refine' support_supports t _ _
   intro e he
   rw [mul_smul, inv_smul_eq_iff]
-  simp only [ne_eq, Allowable.smul_Address_eq_smul_iff]
+  simp only [ne_eq, Allowable.smul_address_eq_smul_iff]
   obtain ⟨C, a | N⟩ := e
   · simp only [smul_inl, inl.injEq]
     refine'

ConNF/Fuzz/Hypotheses.lean

@@ -106,20 +106,20 @@ theorem support_isSum_smul {S S₁ S₂ : Support α} (h : S.IsSum S₁ S₂) (
 
 variable {ρ ρ' : Allowable α} {c : Address α}
 
-theorem smul_Address :
+theorem smul_address :
     ρ • c = ⟨c.path, Allowable.toStructPerm ρ c.path • c.value⟩ :=
   rfl
 
 @[simp]
-theorem smul_Address_eq_iff :
+theorem smul_address_eq_iff :
     ρ • c = c ↔ Allowable.toStructPerm ρ c.path • c.value = c.value :=
-  StructPerm.smul_Address_eq_iff
+  StructPerm.smul_address_eq_iff
 
 @[simp]
-theorem smul_Address_eq_smul_iff :
+theorem smul_address_eq_smul_iff :
     ρ • c = ρ' • c ↔
     Allowable.toStructPerm ρ c.path • c.value = Allowable.toStructPerm ρ' c.path • c.value :=
-  StructPerm.smul_Address_eq_smul_iff
+  StructPerm.smul_address_eq_smul_iff
 
 end Allowable
 
@@ -185,7 +185,7 @@ instance Bot.tangleData : TangleData ⊥
   support a := Support.singleton ⟨Quiver.Path.nil, Sum.inl a⟩
   support_supports a π h := by
     simp only [Support.singleton_enum, Enumeration.mem_carrier_iff, κ_lt_one_iff, exists_prop,
-      exists_eq_left, NearLitterPerm.smul_Address_eq_iff, forall_eq, Sum.smul_inl,
+      exists_eq_left, NearLitterPerm.smul_address_eq_iff, forall_eq, Sum.smul_inl,
       Sum.inl.injEq] at h
     exact h