From aa01e2673ecd8befe44771613b52d019d5c7eb33 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Wed, 13 Mar 2024 18:58:31 +0000 Subject: [PATCH] Strong.smul Signed-off-by: zeramorphic --- ConNF/Counting/CodingFunction.lean | 11 ++- ConNF/Counting/Spec.lean | 152 +---------------------------- ConNF/Counting/SpecSMul.lean | 140 -------------------------- ConNF/Counting/StrongSupport.lean | 77 ++++++++++++++- 4 files changed, 89 insertions(+), 291 deletions(-) diff --git a/ConNF/Counting/CodingFunction.lean b/ConNF/Counting/CodingFunction.lean index cb57355424..93a34a5bb9 100644 --- a/ConNF/Counting/CodingFunction.lean +++ b/ConNF/Counting/CodingFunction.lean @@ -1,4 +1,4 @@ -import ConNF.FOA.Basic.Hypotheses +import ConNF.Counting.StrongSupport /-! # Coding functions @@ -161,6 +161,15 @@ theorem code_smul (S : Support β) (t : Tangle β) (ρ : Allowable β) rw [this] simp only [code_decode, Part.get_some, inv_smul_smul] +def Strong (χ : CodingFunction β) : Prop := + ∀ S ∈ χ.decode.Dom, S.Strong + +theorem strong_of_strong_mem (χ : CodingFunction β) (S : Support β) + (hS : S.Strong) (hSχ : S ∈ χ.decode.Dom) : χ.Strong := by + intro T hTχ + obtain ⟨ρ, rfl⟩ := (χ.dom_iff S T hSχ).mp hTχ + exact hS.smul ρ + end CodingFunction end ConNF diff --git a/ConNF/Counting/Spec.lean b/ConNF/Counting/Spec.lean index 1eda3d6804..4e60b2c88b 100644 --- a/ConNF/Counting/Spec.lean +++ b/ConNF/Counting/Spec.lean @@ -16,153 +16,11 @@ namespace ConNF variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} -inductive SpecComponent (β : Λ) : Type u - | atom (A : ExtendedIndex β) (others : Set κ) (nearLitters : Set κ) : - SpecComponent β - | flexible (A : ExtendedIndex β) (others : Set κ) : - SpecComponent β - | inflexibleCoe (A : ExtendedIndex β) (h : InflexibleCoePath A) - (χ : CodingFunction h.δ) (r : κ → κ) : - SpecComponent β - | inflexibleBot (A : ExtendedIndex β) (h : InflexibleBotPath A) (atoms : Set κ) : - SpecComponent β - -inductive Spec : Λ → Type u - | mk {β : Λ} (cond : Enumeration (SpecComponent β)) - (lower : ∀ {γ : Λ}, (γ : TypeIndex) < β → Path (β : TypeIndex) γ → Spec γ) - (r : ∀ {γ : Λ}, (γ : TypeIndex) < β → Path (β : TypeIndex) γ → κ → κ) : Spec β - -def Spec.cond : Spec β → Enumeration (SpecComponent β) - | mk cond _ _ => cond - -def Spec.lower : Spec β → ∀ {γ : Λ}, (γ : TypeIndex) < β → Path (β : TypeIndex) γ → Spec γ - | mk _ lower _ => lower - -def Spec.r : Spec β → ∀ {γ : Λ}, (γ : TypeIndex) < β → Path (β : TypeIndex) γ → κ → κ - | mk _ _ r => r - -inductive SpecifiesC (σ : Spec β) (S : Support β) - (lS : ∀ {γ : Λ}, (hγ : (γ : TypeIndex) < β) → (A : Path (β : TypeIndex) γ) → Support γ) : - SpecComponent β → Address β → Prop - | atom (A : ExtendedIndex β) (a : Atom) : - SpecifiesC σ S lS - (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⟩}) - ⟨A, inl a⟩ +inductive SpecCondition (β : Λ) + | atom (A : ExtendedIndex β) (i : κ) | flexible (A : ExtendedIndex β) - (N : NearLitter) (h : Flexible A N.1) : - SpecifiesC σ S lS - (SpecComponent.flexible A - {i | ∃ hi : i < S.max, ∃ N', S.f i hi = ⟨A, inr N'⟩ ∧ N'.1 = N.1}) - ⟨A, inr N⟩ - | inflexibleCoe (A : ExtendedIndex β) - (N : NearLitter) (h : InflexibleCoe A N.1) (r : κ → κ) - (hr : ∀ i < h.t.support.max, r i < (lS (h.path.δ_lt_β) (h.path.B.cons h.path.hδ)).max) - (hS : ∀ (i : κ) (hit : i < h.t.support.max), - h.t.support.f i hit = (lS (h.path.δ_lt_β) (h.path.B.cons h.path.hδ)).f (r i) (hr i hit)) : - SpecifiesC σ S lS - (SpecComponent.inflexibleCoe A h.path - (CodingFunction.code h.t.support h.t (support_supports _)) r) - ⟨A, inr N⟩ - | inflexibleBot (A : ExtendedIndex β) - (N : NearLitter) (h : InflexibleBot A N.1) : - SpecifiesC σ S lS - (SpecComponent.inflexibleBot A h.path - {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 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) γ), - ∀ i < (lS hγ A).max, σ.r hγ A i < S.max) - (hlS₂ : ∀ {γ : Λ} (hγ : (γ : TypeIndex) < β) (A : Path (β : TypeIndex) γ) - (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) γ), - (σ.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 - -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 + | inflexibleCoe (A : ExtendedIndex β) (h : InflexibleCoePath A) + (χ : CodingFunction h.δ) (hχ : χ.Strong) + | inflexibleBot (A : ExtendedIndex β) (h : InflexibleBotPath A) (i : κ) end ConNF diff --git a/ConNF/Counting/SpecSMul.lean b/ConNF/Counting/SpecSMul.lean index 2bbbe0a672..79852d6942 100644 --- a/ConNF/Counting/SpecSMul.lean +++ b/ConNF/Counting/SpecSMul.lean @@ -13,144 +13,4 @@ namespace ConNF variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [i : LeLevel β] {σ : Spec β} {S : Support β} {lS : ∀ {γ : Λ}, (hγ : (γ : TypeIndex) < β) → (A : Path (β : TypeIndex) γ) → Support γ} -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 - constructor - · rintro ⟨hi₁, hi₂⟩ - refine ⟨hi₁, ?_⟩ - rw [hi₂] - rfl - · rintro ⟨hi₁, hi₂⟩ - 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] - · ext i - constructor - · rintro ⟨N, ha, hi₁, hi₂⟩ - refine ⟨Allowable.toStructPerm ρ A • N, ?_, hi₁, ?_⟩ - · rw [← SetLike.mem_coe, NearLitterPerm.smul_nearLitter_coe, smul_mem_smul_set_iff] - exact ha - · rw [hi₂] - rfl - · rintro ⟨N, ha, hi₁, hi₂⟩ - 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] - -theorem specifiesCondition_flexible_smul {S : Support β} - {σ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 : 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, Allowable.smul_support_max, Enumeration.smul_f] at hi ⊢ - rw [← hS i hi] - simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleCoe_smul_path, - Allowable.toStructPerm_smul, Allowable.toStructPerm_comp, Enumeration.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 : 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, - 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, - Tree.inv_apply, smul_inl, inv_smul_smul] - -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 ρ - · exact specifiesCondition_inflexibleCoe_smul h' h ρ - -theorem Spec.Specifies.smul {σ : Spec β} {S : Support β} (h : σ.Specifies S) (ρ : Allowable β) : - σ.Specifies (ρ • S) := by - 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 [Enumeration.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 (cond i hiσ hiS).smul ρ - end ConNF diff --git a/ConNF/Counting/StrongSupport.lean b/ConNF/Counting/StrongSupport.lean index 04714966fd..555221fa8e 100644 --- a/ConNF/Counting/StrongSupport.lean +++ b/ConNF/Counting/StrongSupport.lean @@ -2,7 +2,6 @@ import Mathlib.Order.Extension.Well import ConNF.Mathlib.Support import ConNF.FOA.Basic.Reduction import ConNF.FOA.Basic.Flexible -import ConNF.Counting.CodingFunction /-! # Strong supports @@ -34,7 +33,7 @@ inductive Precedes : Address β → Address β → Prop ⟨(h.path.B.cons h.path.hε).cons (bot_lt_coe _), inr N⟩ @[mk_iff] -structure Strong (S : Support β) : Prop where +structure Support.Strong (S : Support β) : Prop where 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₂⟩) @@ -245,7 +244,7 @@ theorem subset_strongSupport {s : Set (Address β)} (hs : Small s) : s ⊆ stron obtain ⟨j, hj, hc⟩ := exists_of_mem_strongClosure hs c (subset_strongClosure s hc) exact ⟨j, hj, hc.symm⟩ -theorem strongSupport_strong {s : Set (Address β)} (hs : Small s) : Strong (strongSupport hs) := by +theorem strongSupport_strong {s : Set (Address β)} (hs : Small s) : (strongSupport hs).Strong := by constructor · intro i₁ i₂ hi₁ hi₂ A N₁ N₂ hN₁ hN₂ a ha have hi₁' := mem_of_strongSupport_f_eq hs hi₁ @@ -270,4 +269,76 @@ theorem strongSupport_strong {s : Set (Address β)} (hs : Small s) : Strong (str rw [hc'] exact StrongSupportRel.precedes _ _ hc +theorem Interferes.smul {a : Atom} {N₁ N₂ : NearLitter} (h : Interferes a N₁ N₂) + (π : NearLitterPerm) : Interferes (π • a) (π • N₁) (π • N₂) := by + cases h + case symmDiff h₁ h₂ => + refine Interferes.symmDiff ?_ ?_ + · simp only [NearLitterPerm.smul_nearLitter_fst, smul_left_cancel_iff] + exact h₁ + · obtain (h₂ | h₂) := h₂ + · refine Or.inl ?_ + rw [NearLitterPerm.smul_nearLitter_coe, NearLitterPerm.smul_nearLitter_coe, + mem_diff, smul_mem_smul_set_iff, smul_mem_smul_set_iff] + exact h₂ + · refine Or.inr ?_ + rw [NearLitterPerm.smul_nearLitter_coe, NearLitterPerm.smul_nearLitter_coe, + mem_diff, smul_mem_smul_set_iff, smul_mem_smul_set_iff] + exact h₂ + case inter h₁ h₂ => + refine Interferes.inter ?_ ?_ + · simp only [NearLitterPerm.smul_nearLitter_fst, ne_eq, smul_left_cancel_iff] + exact h₁ + · rw [mem_inter_iff, NearLitterPerm.smul_nearLitter_coe, NearLitterPerm.smul_nearLitter_coe, + smul_mem_smul_set_iff, smul_mem_smul_set_iff] + exact h₂ + +theorem Precedes.smul [LeLevel β] {c d : Address β} (h : Precedes c d) (ρ : Allowable β) : + Precedes (ρ • c) (ρ • d) := by + cases h + case fuzz A N h c hc => + have := Precedes.fuzz A (Allowable.toStructPerm ρ A • N) (h.smul ρ) + (Allowable.comp (h.path.B.cons h.path.hδ) ρ • c) ?_ + · simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleCoe_smul_path, + Allowable.smul_address, Allowable.toStructPerm_comp, Tree.comp_apply] at this + simp only [Allowable.smul_address, smul_inr] + rw [← h.path.hA] at this ⊢ + exact this + · simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleCoe_smul_path, inflexibleCoe_smul_t, + smul_support] + change _ ∈ (_ : Set (Address h.path.δ)) + rw [Enumeration.smul_coe, smul_mem_smul_set_iff] + exact hc + case fuzzBot A N h => + have := Precedes.fuzzBot A (Allowable.toStructPerm ρ A • N) (h.smul ρ) + simp only [Allowable.smul_address, smul_inl, smul_inr] + simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleBot_smul_path, inflexibleBot_smul_a, + ofBot_smul, Allowable.toStructPerm_apply] at this + simp_rw [h.path.hA] at this ⊢ + exact this + +theorem Support.Strong.smul [LeLevel β] {S : Support β} (hS : S.Strong) (ρ : Allowable β) : + (ρ • S).Strong := by + constructor + · intro i₁ i₂ hi₁ hi₂ A N₁ N₂ hN₁ hN₂ a ha + have := ha.smul (Allowable.toStructPerm ρ A)⁻¹ + 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₂, ?_⟩ + 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] + · rw [Enumeration.smul_f, smul_eq_iff_eq_inv_smul] at hN₂ + rw [hN₂, Allowable.smul_address, map_inv, Tree.inv_apply, smul_inr] + · intro i hi c hc + have := hS.precedes hi (ρ⁻¹ • c) ?_ + · obtain ⟨j, hj, hj', hc⟩ := this + refine ⟨j, hj, hj', ?_⟩ + rw [Enumeration.smul_f, smul_eq_iff_eq_inv_smul, hc] + · have := hc.smul ρ⁻¹ + simp only [Enumeration.smul_f, inv_smul_smul] at this + exact this + end ConNF