More minor fixes

Signed-off-by: zeramorphic <[email protected]>
leanprover-community · Oct 22, 2023 · 669c2bf · 669c2bf
1 parent 2197b7d
commit 669c2bf
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 7 deletions.
diff --git a/ConNF/Counting/OrdSupportOrbitEquiv.lean b/ConNF/Counting/OrdSupportOrbitEquiv.lean
@@ -46,14 +46,16 @@ noncomputable def InflexibleBot.smul {A : ExtendedIndex β} {L : Litter}
   path := h.path
   a := Allowable.toStructPerm ρ (h.path.B.cons (WithBot.bot_lt_coe _)) • h.a
   hL := by
-    have := toStructPerm_smul_fuzz (β : IicBot α) h.path.γ ⊥ h.path.ε ?_ ?_ ?_
-      h.path.B ρ h.a
-    rw [Allowable.comp_bot (β := (β : IicBot α))] at this
-    rw [← this, ← h.path.hA, ← h.hL]
+    refine Eq.trans ?_ (congr_arg _
+      (comp_bot_smul_atom (β := (β : IicBot α)) ρ (Quiver.Path.cons h.path.B ?_) h.a))
+    refine Eq.trans ?_ (toStructPerm_smul_fuzz (β : IicBot α) h.path.γ ⊥ h.path.ε ?_ ?_ ?_
+      h.path.B ρ h.a)
+    rw [← h.path.hA, ← h.hL]
     · intro hδε
       simp only [IioBot.bot_ne_mk_coe] at hδε
     · exact WithBot.coe_lt_coe.mpr h.path.hε
     · exact WithBot.bot_lt_coe _
+    · exact WithBot.bot_lt_coe _
 
 @[simp]
 theorem InflexibleBot.smul_path {A : ExtendedIndex β} {L : Litter}

diff --git a/ConNF/Counting/SpecSame.lean b/ConNF/Counting/SpecSame.lean
@@ -735,8 +735,9 @@ theorem smul_litter_eq_of_lawfulBefore' (A : ExtendedIndex β) (L : Litter)
     have := ih.smul_eq ⟨_, ha⟩ ?_
     · rw [convertCondition_eq_convertAtom hσS hσT hS hT, Allowable.smul_supportCondition] at this
       simp only [smul_inl, SupportCondition.mk.injEq, inl.injEq, true_and] at this
-      rw [← this, Allowable.comp_bot (show Path ((β : IicBot α) : TypeIndex) (⊥ : IicBot α) from
+      rw [← this, ← Allowable.comp_bot (show Path ((β : IicBot α) : TypeIndex) (⊥ : IicBot α) from
           hL.path.B.cons (bot_lt_coe _))]
+      rfl
     · simp only [OrdSupport.coe_sort_coe, mem_setOf_eq, typein_lt_typein, hL.hL, hL.path.hA]
       exact hS.lt_of_transConstrains _ _
         (Relation.TransGen.single (Constrains.fuzz_bot hL.path.hε hL.path.B hL.a))
@@ -793,8 +794,9 @@ theorem inv_smul_litter_eq_of_lawfulBefore' (A : ExtendedIndex β) (L : Litter)
         convertCondition_eq_convertAtom hσT hσS hT hS, Allowable.smul_supportCondition] at this
       simp only [smul_inl, SupportCondition.mk.injEq, inl.injEq, true_and] at this
       rw [← inv_smul_eq_iff] at this
-      rw [← this, Allowable.comp_bot (show Path ((β : IicBot α) : TypeIndex) (⊥ : IicBot α) from
-          hL.path.B.cons (bot_lt_coe _)), map_inv, Tree.inv_apply]
+      rw [← this, ← Allowable.comp_bot (show Path ((β : IicBot α) : TypeIndex) (⊥ : IicBot α) from
+          hL.path.B.cons (bot_lt_coe _)), map_inv]
+      rfl
     · simp only [OrdSupport.coe_sort_coe, mem_setOf_eq, typein_lt_typein, hL.hL, hL.path.hA]
       exact hT.lt_of_transConstrains _ _
         (Relation.TransGen.single <| Constrains.fuzz_bot hL.path.hε hL.path.B hL.a)