theorem ConNF.inflexible_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} : ∀ (a : ConNF.ExtendedIndex β) (a_1 : ConNF.Litter), ConNF.Inflexible a a_1 ↔ (∃ (γ : ConNF.Λ), ConNF.LeLevel ↑γ ∧ ∃ (δ : ConNF.Λ) (inst : ConNF.LtLevel ↑δ) (ε : ConNF.Λ), ConNF.LtLevel ↑ε ∧ ↑δ < ↑γ ∧ ∃ (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) (A : Quiver.Path β ↑γ) (t : ConNF.Tangle ↑δ), a = (A.cons hε).cons ⋯ ∧ a_1 = ConNF.fuzz hδε t) ∨ ∃ (γ : ConNF.Λ), ConNF.LeLevel ↑γ ∧ ∃ (ε : ConNF.Λ), ConNF.LtLevel ↑ε ∧ ∃ (hε : ↑ε < ↑γ) (A : Quiver.Path β ↑γ) (a_2 : ConNF.Atom), a = (A.cons hε).cons ⋯ ∧ a_1 = ConNF.fuzz ⋯ a_2

inductive ConNF.Inflexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} : ConNF.ExtendedIndex β → ConNF.Litter → Prop

A litter is inflexible if it is the image of some f-map.

• mk_coe: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.TypeIndex} ⦃γ : ConNF.Λ⦄ [inst_4 : ConNF.LeLevel ↑γ] ⦃δ : ConNF.Λ⦄ [inst_5 : ConNF.LtLevel ↑δ] ⦃ε : ConNF.Λ⦄ [inst_6 : ConNF.LtLevel ↑ε], ↑δ < ↑γ → ∀ (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) (A : Quiver.Path β ↑γ) (t : ConNF.Tangle ↑δ), ConNF.Inflexible ((A.cons hε).cons ⋯) (ConNF.fuzz hδε t)
• mk_bot: ∀ [inst : ConNF.Params] [inst_1 : ConNF.Level] [inst_2 : ConNF.BasePositions] [inst_3 : ConNF.FOAAssumptions] {β : ConNF.TypeIndex} ⦃γ : ConNF.Λ⦄ [inst_4 : ConNF.LeLevel ↑γ] ⦃ε : ConNF.Λ⦄ [inst_5 : ConNF.LtLevel ↑ε] (hε : ↑ε < ↑γ) (A : Quiver.Path β ↑γ) (a : ConNF.Atom), ConNF.Inflexible ((A.cons hε).cons ⋯) (ConNF.fuzz ⋯ a)

def ConNF.Flexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (A : ConNF.ExtendedIndex β) (L : ConNF.Litter) : Prop

A litter is flexible if it is not the image of any f-map.

Equations

• ConNF.Flexible A L = ¬ConNF.Inflexible A L

theorem ConNF.flexible_cases [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (A : ConNF.ExtendedIndex β) (L : ConNF.Litter) : ConNF.Inflexible A L ∨ ConNF.Flexible A L

theorem ConNF.mk_flexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} (A : ConNF.ExtendedIndex β) : Cardinal.mk ↑{L : ConNF.Litter | ConNF.Flexible A L} = Cardinal.mk ConNF.μ

theorem ConNF.Inflexible.comp [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} {L : ConNF.Litter} {A : ConNF.ExtendedIndex γ} (h : ConNF.Inflexible A L) (B : Quiver.Path β γ) : ConNF.Inflexible (B.comp A) L

@[simp]

theorem ConNF.not_flexible_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} {L : ConNF.Litter} {A : ConNF.ExtendedIndex β} : ¬ConNF.Flexible A L ↔ ConNF.Inflexible A L

theorem ConNF.flexible_of_comp_flexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.TypeIndex} {γ : ConNF.TypeIndex} {L : ConNF.Litter} {A : ConNF.ExtendedIndex γ} {B : Quiver.Path β γ} (h : ConNF.Flexible (B.comp A) L) : ConNF.Flexible A L

structure ConNF.InflexibleCoePath [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) : Type u

• γ : ConNF.Λ
• δ : ConNF.Λ
• ε : ConNF.Λ
• inst_γ : ConNF.LeLevel ↑self.γ
• inst_δ : ConNF.LtLevel ↑self.δ
• inst_ε : ConNF.LtLevel ↑self.ε
• hδ : ↑self.δ < ↑self.γ
• hε : ↑self.ε < ↑self.γ
• hδε : ↑self.δ ≠ ↑self.ε
• B : Quiver.Path ↑β ↑self.γ
• hA : A = (self.B.cons ⋯).cons ⋯

theorem ConNF.InflexibleCoePath.inst_γ [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (self : ConNF.InflexibleCoePath A) : ConNF.LeLevel ↑self.γ

theorem ConNF.InflexibleCoePath.inst_δ [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (self : ConNF.InflexibleCoePath A) : ConNF.LtLevel ↑self.δ

theorem ConNF.InflexibleCoePath.inst_ε [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (self : ConNF.InflexibleCoePath A) : ConNF.LtLevel ↑self.ε

theorem ConNF.InflexibleCoePath.hδ [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (self : ConNF.InflexibleCoePath A) : ↑self.δ < ↑self.γ

theorem ConNF.InflexibleCoePath.hε [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (self : ConNF.InflexibleCoePath A) : ↑self.ε < ↑self.γ

theorem ConNF.InflexibleCoePath.hδε [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (self : ConNF.InflexibleCoePath A) : ↑self.δ ≠ ↑self.ε

theorem ConNF.InflexibleCoePath.hA [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (self : ConNF.InflexibleCoePath A) : A = (self.B.cons ⋯).cons ⋯

instance ConNF.instLeLevelSomeΛγ [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (path : ConNF.InflexibleCoePath A) : ConNF.LeLevel ↑path.γ

Equations

• ⋯ = ⋯

instance ConNF.instLtLevelSomeΛδ [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (path : ConNF.InflexibleCoePath A) : ConNF.LtLevel ↑path.δ

Equations

• ⋯ = ⋯

instance ConNF.instLtLevelSomeΛε [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (path : ConNF.InflexibleCoePath A) : ConNF.LtLevel ↑path.ε

Equations

• ⋯ = ⋯

structure ConNF.InflexibleCoe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) : Type u

A proof-relevant statement that L is A-inflexible (excluding ε = ⊥).

• path : ConNF.InflexibleCoePath A
• t : ConNF.Tangle ↑self.path.δ
• hL : L = ConNF.fuzz ⋯ self.t

theorem ConNF.InflexibleCoe.hL [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (self : ConNF.InflexibleCoe A L) : L = ConNF.fuzz ⋯ self.t

structure ConNF.InflexibleBotPath [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) : Type u

• γ : ConNF.Λ
• ε : ConNF.Λ
• inst_γ : ConNF.LeLevel ↑self.γ
• inst_ε : ConNF.LtLevel ↑self.ε
• hε : ↑self.ε < ↑self.γ
• B : Quiver.Path ↑β ↑self.γ
• hA : A = (self.B.cons ⋯).cons ⋯

theorem ConNF.InflexibleBotPath.inst_γ [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (self : ConNF.InflexibleBotPath A) : ConNF.LeLevel ↑self.γ

theorem ConNF.InflexibleBotPath.inst_ε [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (self : ConNF.InflexibleBotPath A) : ConNF.LtLevel ↑self.ε

theorem ConNF.InflexibleBotPath.hε [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (self : ConNF.InflexibleBotPath A) : ↑self.ε < ↑self.γ

theorem ConNF.InflexibleBotPath.hA [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (self : ConNF.InflexibleBotPath A) : A = (self.B.cons ⋯).cons ⋯

instance ConNF.instLeLevelSomeΛγ_1 [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (path : ConNF.InflexibleBotPath A) : ConNF.LeLevel ↑path.γ

Equations

• ⋯ = ⋯

instance ConNF.instLtLevelSomeΛε_1 [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (path : ConNF.InflexibleBotPath A) : ConNF.LtLevel ↑path.ε

Equations

• ⋯ = ⋯

structure ConNF.InflexibleBot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) : Type u

A proof-relevant statement that L is A-inflexible, where δ = ⊥.

• path : ConNF.InflexibleBotPath A
• a : ConNF.Atom
• hL : L = ConNF.fuzz ⋯ self.a

theorem ConNF.InflexibleBot.hL [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (self : ConNF.InflexibleBot A L) : L = ConNF.fuzz ⋯ self.a

instance ConNF.instSubsingletonInflexibleCoe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) : Subsingleton (ConNF.InflexibleCoe A L)

Equations

• ⋯ = ⋯

instance ConNF.instSubsingletonInflexibleBot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) : Subsingleton (ConNF.InflexibleBot A L)

Equations

• ⋯ = ⋯

theorem ConNF.inflexibleBot_inflexibleCoe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} : ConNF.InflexibleBot A L → ConNF.InflexibleCoe A L → False

theorem ConNF.InflexibleCoePath.δ_lt_β [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (h : ConNF.InflexibleCoePath A) : ↑h.δ < ↑β

theorem ConNF.InflexibleCoe.δ_lt_β [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (h : ConNF.InflexibleCoe A L) : ↑h.path.δ < ↑β

def ConNF.InflexibleCoePath.comp [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} (h : ConNF.InflexibleCoePath B) (A : Quiver.Path ↑β ↑γ) : ConNF.InflexibleCoePath (A.comp B)

Equations

• h.comp A = ConNF.InflexibleCoePath.mk h.γ h.δ h.ε ⋯ ⋯ ⋯ (A.comp h.B) ⋯

def ConNF.InflexibleBotPath.comp [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} (h : ConNF.InflexibleBotPath B) (A : Quiver.Path ↑β ↑γ) : ConNF.InflexibleBotPath (A.comp B)

Equations

• h.comp A = ConNF.InflexibleBotPath.mk h.γ h.ε ⋯ (A.comp h.B) ⋯

def ConNF.InflexibleCoe.comp [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} {L : ConNF.Litter} (h : ConNF.InflexibleCoe B L) (A : Quiver.Path ↑β ↑γ) : ConNF.InflexibleCoe (A.comp B) L

Equations

• h.comp A = { path := h.path.comp A, t := h.t, hL := ⋯ }

def ConNF.InflexibleBot.comp [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} {L : ConNF.Litter} (h : ConNF.InflexibleBot B L) (A : Quiver.Path ↑β ↑γ) : ConNF.InflexibleBot (A.comp B) L

Equations

• h.comp A = { path := h.path.comp A, a := h.a, hL := ⋯ }

@[simp]

theorem ConNF.InflexibleCoe.comp_path [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} {L : ConNF.Litter} (h : ConNF.InflexibleCoe B L) (A : Quiver.Path ↑β ↑γ) : (h.comp A).path = h.path.comp A

@[simp]

theorem ConNF.InflexibleCoePath.comp_γ [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} (h : ConNF.InflexibleCoePath B) (A : Quiver.Path ↑β ↑γ) : (h.comp A).γ = h.γ

@[simp]

theorem ConNF.InflexibleCoePath.comp_δ [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} (h : ConNF.InflexibleCoePath B) (A : Quiver.Path ↑β ↑γ) : (h.comp A).δ = h.δ

@[simp]

theorem ConNF.InflexibleCoePath.comp_ε [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} (h : ConNF.InflexibleCoePath B) (A : Quiver.Path ↑β ↑γ) : (h.comp A).ε = h.ε

@[simp]

theorem ConNF.InflexibleCoe.comp_t [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} {L : ConNF.Litter} (h : ConNF.InflexibleCoe B L) (A : Quiver.Path ↑β ↑γ) : (h.comp A).t = h.t

@[simp]

theorem ConNF.InflexibleCoePath.comp_B [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} (h : ConNF.InflexibleCoePath B) (A : Quiver.Path ↑β ↑γ) : (h.comp A).B = A.comp h.B

@[simp]

theorem ConNF.InflexibleBot.comp_path [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} {L : ConNF.Litter} (h : ConNF.InflexibleBot B L) (A : Quiver.Path ↑β ↑γ) : (h.comp A).path = h.path.comp A

@[simp]

theorem ConNF.InflexibleBotPath.comp_γ [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} (h : ConNF.InflexibleBotPath B) (A : Quiver.Path ↑β ↑γ) : (h.comp A).γ = h.γ

@[simp]

theorem ConNF.InflexibleBotPath.comp_ε [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} (h : ConNF.InflexibleBotPath B) (A : Quiver.Path ↑β ↑γ) : (h.comp A).ε = h.ε

@[simp]

theorem ConNF.InflexibleBot.comp_a [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} {L : ConNF.Litter} (h : ConNF.InflexibleBot B L) (A : Quiver.Path ↑β ↑γ) : (h.comp A).a = h.a

@[simp]

theorem ConNF.InflexibleBotPath.comp_B [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {γ : ConNF.Λ} {B : ConNF.ExtendedIndex ↑γ} (h : ConNF.InflexibleBotPath B) (A : Quiver.Path ↑β ↑γ) : (h.comp A).B = A.comp h.B

theorem ConNF.inflexible_of_inflexibleBot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (h : ConNF.InflexibleBot A L) : ConNF.Inflexible A L

theorem ConNF.inflexible_of_inflexibleCoe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (h : ConNF.InflexibleCoe A L) : ConNF.Inflexible A L

theorem ConNF.inflexibleBot_or_inflexibleCoe_of_inflexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (h : ConNF.Inflexible A L) : Nonempty (ConNF.InflexibleBot A L) ∨ Nonempty (ConNF.InflexibleCoe A L)

theorem ConNF.inflexible_iff_inflexibleBot_or_inflexibleCoe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} : ConNF.Inflexible A L ↔ Nonempty (ConNF.InflexibleBot A L) ∨ Nonempty (ConNF.InflexibleCoe A L)

theorem ConNF.flexible_iff_not_inflexibleBot_inflexibleCoe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} : ConNF.Flexible A L ↔ IsEmpty (ConNF.InflexibleBot A L) ∧ IsEmpty (ConNF.InflexibleCoe A L)

theorem ConNF.flexible_cases' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) : ConNF.Flexible A L ∨ Nonempty (ConNF.InflexibleBot A L) ∨ Nonempty (ConNF.InflexibleCoe A L)

def ConNF.InflexibleCoe.smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (h : ConNF.InflexibleCoe A L) (ρ : ConNF.Allowable ↑β) : ConNF.InflexibleCoe A (ConNF.Allowable.toStructPerm ρ A • L)

Equations

• h.smul ρ = { path := h.path, t := (ConNF.Allowable.comp (h.path.B.cons ⋯)) ρ • h.t, hL := ⋯ }

@[simp]

theorem ConNF.inflexibleCoe_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} {ρ : ConNF.Allowable ↑β} : Nonempty (ConNF.InflexibleCoe A (ConNF.Allowable.toStructPerm ρ A • L)) ↔ Nonempty (ConNF.InflexibleCoe A L)

def ConNF.InflexibleBot.smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (h : ConNF.InflexibleBot A L) (ρ : ConNF.Allowable ↑β) : ConNF.InflexibleBot A (ConNF.Allowable.toStructPerm ρ A • L)

Equations

• h.smul ρ = { path := h.path, a := (ConNF.Allowable.comp (h.path.B.cons ⋯)) ρ • h.a, hL := ⋯ }

@[simp]

theorem ConNF.inflexibleBot_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} {ρ : ConNF.Allowable ↑β} : Nonempty (ConNF.InflexibleBot A (ConNF.Allowable.toStructPerm ρ A • L)) ↔ Nonempty (ConNF.InflexibleBot A L)

theorem ConNF.Flexible.smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (h : ConNF.Flexible A L) (ρ : ConNF.Allowable ↑β) : ConNF.Flexible A (ConNF.Allowable.toStructPerm ρ A • L)

@[simp]

theorem ConNF.flexible_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} {ρ : ConNF.Allowable ↑β} : ConNF.Flexible A (ConNF.Allowable.toStructPerm ρ A • L) ↔ ConNF.Flexible A L

@[simp]

theorem ConNF.inflexibleCoe_smul_path [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} {ρ : ConNF.Allowable ↑β} (h : ConNF.InflexibleCoe A L) : (h.smul ρ).path = h.path

@[simp]

theorem ConNF.inflexibleCoe_smul_t [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} {ρ : ConNF.Allowable ↑β} (h : ConNF.InflexibleCoe A L) : (h.smul ρ).t = (ConNF.Allowable.comp (h.path.B.cons ⋯)) ρ • h.t

@[simp]

theorem ConNF.inflexibleBot_smul_path [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} {ρ : ConNF.Allowable ↑β} (h : ConNF.InflexibleBot A L) : (h.smul ρ).path = h.path

@[simp]

theorem ConNF.inflexibleBot_smul_a [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} {ρ : ConNF.Allowable ↑β} (h : ConNF.InflexibleBot A L) : (h.smul ρ).a = (ConNF.Allowable.comp (h.path.B.cons ⋯)) ρ • h.a