diff options
| -rw-r--r-- | Nominal/NameRestriction/Model.lean | 307 |
1 files changed, 247 insertions, 60 deletions
diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean index 7cc0df6..9c6103f 100644 --- a/Nominal/NameRestriction/Model.lean +++ b/Nominal/NameRestriction/Model.lean @@ -214,46 +214,66 @@ def Req1 {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.F lemma Req1.choose_restriction {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) : - Req1 𝔸 f → ∀ (a c d : 𝔸), c # f → d # f → c ≠ a → d ≠ a → - (c \ (⸨a, c⸩ • f).val a) = (d \ (⸨a, d⸩ • f).val a) := by - intro hreq a c d hcfresh hdfresh hca hda - nth_rw 1 [← show ⸨c, d⸩ • f = f from NominalSet.fresh_swap_fix 𝔸 hcfresh hdfresh] - simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap, - Equiv.swap_apply_left] - rw [show ⟪d⟫ ⸨a,d⸩ • f.val d = ⟪⸨a, d⸩ • a⟫ ⸨a,d⸩ • f.val d by simp] - rw [show ⟪⸨a, d⸩ • a⟫ ⸨a,d⸩ • f.val d = ⸨a, d⸩ • ⟪a⟫ f.val d by simp] - rw [show ⟪c⟫ ⸨a,c⸩ • ⸨c, d⸩ • f.val d = ⟪⸨a, c⸩ • a⟫ ⸨a,c⸩ • ⸨c, d⸩ • f.val d by simp] - rw [show ⟪⸨a, c⸩ • a⟫ ⸨a,c⸩ • ⸨c, d⸩ • f.val d = ⸨a, c⸩ • ⟪a⟫ ⸨c, d⸩ • f.val d by simp] - nth_rw 2 [show a = ⸨c, d⸩ • a by - symm; apply FPerm.swap_apply_of_ne_of_ne - · symm; exact hca - · symm; exact hda] - rw [show ⟪⸨c, d⸩ • a⟫ ⸨c,d⸩ • f.val d = ⸨c, d⸩ • ⟪a⟫ f.val d by simp] - suffices ⸨a,c⸩ • ⸨c,d⸩ • ⟪a⟫ f.val d = ⸨a,d⸩ • ⟪a⟫ f.val d by rw [this] - rw [← MulAction.mul_smul] - apply PermSet.support_permutations_eq 𝔸 (NominalSet.supp_is_support 𝔸) - intro b hb - by_cases hba : b = a <;> by_cases hbc : b = c <;> by_cases hbd : b = d - · simp [*] at * - · simp [*] at * - · simp [*] at * - · simp [*] at * - · rw [← hbc, ← hbd]; simp - · rw [hbc] at hb - suffices c ∉ NominalSet.supp 𝔸 (⟪a⟫ f.val d) by contradiction - suffices c ∉ NominalSet.supp 𝔸 (f.val d) by simp [this] - intro hc - have h := NominalSet.support_subset_supp 𝔸 (hreq d) (by simp [NominalSet.supp_finite]) - specialize h hc - simp only [Set.union_singleton, Set.mem_insert_iff] at h - cases h + Req1 𝔸 f → ∀ (a b c d : 𝔸), c # f → d # f → c ≠ a → d ≠ a → c ≠ b → d ≠ b → + (c \ (⸨a, c⸩ • f).val b) = (d \ (⸨a, d⸩ • f).val b) := by + intro hreq a b c d hcfresh hdfresh hca hda hcb hdb + by_cases heq : b = a + · nth_rw 1 [← show ⸨c, d⸩ • f = f from NominalSet.fresh_swap_fix 𝔸 hcfresh hdfresh] + simp only [heq, PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, + PermSet.atom_swap, Equiv.swap_apply_left] + rw [show ⟪d⟫ ⸨a,d⸩ • f.val d = ⸨a, d⸩ • ⟪a⟫ f.val d by simp] + rw [show ⟪c⟫ ⸨a,c⸩ • ⸨c, d⸩ • f.val d = ⸨a, c⸩ • ⟪a⟫ ⸨c, d⸩ • f.val d by simp] + nth_rw 2 [show a = ⸨c, d⸩ • a by + symm; apply FPerm.swap_apply_of_ne_of_ne + · symm; exact hca + · symm; exact hda] + rw [show ⟪⸨c, d⸩ • a⟫ ⸨c,d⸩ • f.val d = ⸨c, d⸩ • ⟪a⟫ f.val d by simp] + suffices ⸨a,c⸩ • ⸨c,d⸩ • ⟪a⟫ f.val d = ⸨a,d⸩ • ⟪a⟫ f.val d by rw [this] + rw [← MulAction.mul_smul] + apply PermSet.support_permutations_eq 𝔸 (NominalSet.supp_is_support 𝔸) + intro b hb + by_cases hba : b = a <;> by_cases hbc : b = c <;> by_cases hbd : b = d + · simp [*] at * + · simp [*] at * + · simp [*] at * + · simp [*] at * + · rw [← hbc, ← hbd]; simp + · rw [hbc] at hb + suffices c ∉ NominalSet.supp 𝔸 (⟪a⟫ f.val d) by contradiction + suffices c ∉ NominalSet.supp 𝔸 (f.val d) by simp [this] + intro hc + have h := NominalSet.support_subset_supp 𝔸 (hreq d) (by simp [NominalSet.supp_finite]) + specialize h hc + simp only [Set.union_singleton, Set.mem_insert_iff] at h + cases h + · simp [*] at * + · contradiction · simp [*] at * - · contradiction - · simp [*] at * - · simp only [Subgroup.coe_mul, Equiv.Perm.coe_mul, Function.comp_apply] - rw [FPerm.swap_apply_of_ne_of_ne hbc hbd] - rw [FPerm.swap_apply_of_ne_of_ne hba hbc] - rw [FPerm.swap_apply_of_ne_of_ne hba hbd] + · simp only [Subgroup.coe_mul, Equiv.Perm.coe_mul, Function.comp_apply] + rw [FPerm.swap_apply_of_ne_of_ne hbc hbd] + rw [FPerm.swap_apply_of_ne_of_ne hba hbc] + rw [FPerm.swap_apply_of_ne_of_ne hba hbd] + · simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap] + rw [Equiv.swap_apply_of_ne_of_ne heq (Ne.symm hcb)] + rw [Equiv.swap_apply_of_ne_of_ne heq (Ne.symm hdb)] + rw [show ⟪c⟫ ⸨a,c⸩ • f.val b = ⸨a,c⸩ • ⟪a⟫ f.val b by simp] + rw [show ⟪d⟫ ⸨a,d⸩ • f.val b = ⸨a,d⸩ • ⟪a⟫ f.val b by simp] + rw [show ⸨a,c⸩ • ⟪a⟫ f.val b = ⟪a⟫ f.val b by + apply NominalSet.fresh_swap_fix + · rw [NameAbstraction.fresh]; right; rfl + · rw [NameAbstraction.fresh]; left + rw [NominalSet.IsFresh]; intro hcontra + have h := NominalSet.support_subset_supp 𝔸 (hreq b) (by simp [NominalSet.supp_finite]) hcontra + simp only [Set.union_singleton, Set.mem_insert_iff] at h + cases h <;> contradiction] + rw [show ⸨a,d⸩ • ⟪a⟫ f.val b = ⟪a⟫ f.val b by + apply NominalSet.fresh_swap_fix + · rw [NameAbstraction.fresh]; right; rfl + · rw [NameAbstraction.fresh]; left + rw [NominalSet.IsFresh]; intro hcontra + have h := NominalSet.support_subset_supp 𝔸 (hreq b) (by simp [NominalSet.supp_finite]) hcontra + simp only [Set.union_singleton, Set.mem_insert_iff] at h + cases h <;> contradiction] def Req2 {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) := -- Traces for all atoms include those from bound traces @@ -404,7 +424,7 @@ private lemma union_req2 {f g : StepModel 𝔸 X} : Req2 𝔸 (union' 𝔸 (f, g have hdg : d # g.val := hd.left.right have hda : d ≠ a := hd.right simp only [PermSet.Finsupp.smul_val] - have h := Req1.choose_restriction 𝔸 (union' 𝔸 (f, g)) (union_req1 𝔸) a c d hcfresh hdfresh hca hda + have h := Req1.choose_restriction 𝔸 (union' 𝔸 (f, g)) (union_req1 𝔸) a a c d hcfresh hdfresh hca hda hca hda simp only [PermSet.Finsupp.smul_val] at h rw [h] simp only [union', union'', PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap, @@ -437,23 +457,23 @@ instance : Function.Equivariant 𝔸 (union 𝔸 : (StepModel 𝔸 X × StepMode rw [show (π • x.fst, π • x.snd) = π • x by ext <;> simp] rw [← Function.equivariant] -private noncomputable def chooseFresh (f : StepModel 𝔸 X) (a : 𝔸) : 𝔸 := - have hinf : (NominalSet.supp 𝔸 f ∪ {a})ᶜ.Infinite := by +private noncomputable def chooseFresh (f : StepModel 𝔸 X) (a b : 𝔸) : 𝔸 := + have hinf : (NominalSet.supp 𝔸 f ∪ {a} ∪ {b})ᶜ.Infinite := by apply Set.Finite.infinite_compl simp only [supp, Set.union_singleton, Set.finite_insert] apply NominalSet.supp_finite Classical.choose hinf.nonempty -private lemma chooseFresh_fresh (f : StepModel 𝔸 X) (a : 𝔸) : - chooseFresh 𝔸 f a # f.val ∧ chooseFresh 𝔸 f a ≠ a := by - have h : chooseFresh 𝔸 f a ∈ (NominalSet.supp 𝔸 f ∪ {a})ᶜ := Classical.choose_spec _ +private lemma chooseFresh_fresh (f : StepModel 𝔸 X) (a b : 𝔸) : + chooseFresh 𝔸 f a b # f.val ∧ chooseFresh 𝔸 f a b ≠ a ∧ chooseFresh 𝔸 f a b ≠ b := by + have h : chooseFresh 𝔸 f a b ∈ (NominalSet.supp 𝔸 f ∪ {a} ∪ {b})ᶜ := Classical.choose_spec _ simp only [supp, Set.union_singleton, Set.mem_compl_iff, Set.mem_insert_iff, not_or] at h - exact ⟨h.right, h.left⟩ + exact ⟨h.right.right, h.right.left, h.left⟩ private noncomputable def restrict'' : NameAbstraction 𝔸 (StepModel 𝔸 X) → 𝔸 → X := Quotient.lift - (fun ⟨a, f⟩ ↦ - let c := chooseFresh 𝔸 f a - fun b ↦ if a = b then (c \ (⸨a, c⸩ • f.val).val a) else f.val.val b) + (fun ⟨a, f⟩ b ↦ + let c := chooseFresh 𝔸 f a b + (c \ (⸨a, c⸩ • f.val).val b)) (by intro ⟨a₁, f₁⟩ ⟨a₂, f₂⟩ haeq ext b @@ -461,17 +481,184 @@ private noncomputable def restrict'' : NameAbstraction 𝔸 (StepModel 𝔸 X) cases haeq with | inl h => rw [h.left, h.right] | inr h => - simp only [PermSet.Finsupp.smul_val] - by_cases h₁ : a₁ = b <;> by_cases h₂ : a₂ = b <;> simp only [h₁, h₂, ↓reduceIte] - · rw [← h₂] at h₁ - have hcontra := h.left + simp only + have hinf : (NominalSet.supp 𝔸 f₁.val ∪ NominalSet.supp 𝔸 f₂.val ∪ {a₁} ∪ {a₂} ∪ {b})ᶜ.Infinite := by + apply Set.Finite.infinite_compl + rw [Set.finite_union, Set.finite_union, Set.finite_union, Set.finite_union] + constructor + · constructor + · constructor + · constructor + · apply NominalSet.supp_finite + · apply NominalSet.supp_finite + · apply Set.finite_singleton + · apply Set.finite_singleton + · apply Set.finite_singleton + obtain ⟨c, hc⟩ := hinf.nonempty + simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hc + have hcf₁ : c # f₁.val := hc.left.left.left.left + have hcf₂ : c # f₂.val := hc.left.left.left.right + have hca₁ : c ≠ a₁ := hc.left.left.right + have hca₂ : c ≠ a₂ := hc.left.right + have hcb : c ≠ b := hc.right + have ⟨hfreshf₁, hfresha₁, hfreshb₁⟩ := chooseFresh_fresh 𝔸 f₁ a₁ b + have ⟨hfreshf₂, hfresha₂, hfreshb₂⟩ := chooseFresh_fresh 𝔸 f₂ a₂ b + rw [Req1.choose_restriction 𝔸 f₁.val f₁.prop.left a₁ b _ c hfreshf₁ hcf₁ hfresha₁ hca₁ hfreshb₁ hcb] + rw [Req1.choose_restriction 𝔸 f₂.val f₂.prop.left a₂ b _ c hfreshf₂ hcf₂ hfresha₂ hca₂ hfreshb₂ hcb] + rw [h.right.right] + suffices ⸨a₂,c⸩ • f₂.val = ⸨a₁,c⸩ • (⸨a₁,a₂⸩ • f₂).val by rw [this] + rw [smul_val, ← MulAction.mul_smul] + apply PermSet.support_permutations_eq 𝔸 (NominalSet.supp_is_support 𝔸) + intro d hd + by_cases hda₁ : d = a₁ <;> by_cases hda₂ : d = a₂ <;> by_cases hdc : d = c + · simp [*] at * + · simp [*] at * + · simp [*] at * + · rw [hda₁] at hd + have hcontra : a₁ ∉ NominalSet.supp 𝔸 f₂ := h.right.left + rw [StepModel.supp] at hcontra contradiction - · - sorry - · rw [h.right.right, ← h₂] - simp only [smul_val, PermSet.Finsupp.smul_val] - have heq := Req1.choose_restriction 𝔸 f₂.val f₂.prop.left - sorry - · sorry) + · simp [*] at * + · simp [*] at * + · simp [*] at * + · simp only [Subgroup.coe_mul, Equiv.Perm.coe_mul, Function.comp_apply] + rw [FPerm.swap_apply_of_ne_of_ne hda₂ hdc] + rw [FPerm.swap_apply_of_ne_of_ne hda₁ hda₂] + rw [FPerm.swap_apply_of_ne_of_ne hda₁ hdc]) + +instance : Function.Equivariant 𝔸 (restrict'' 𝔸 : NameAbstraction 𝔸 (StepModel 𝔸 X) → 𝔸 → X) := by + constructor + apply Quotient.ind + intro ⟨a, f⟩ π + ext b + simp only [restrict'', PermSet.Finsupp.smul_val, NameAbstraction.smul, Quotient.lift_mk, smul_val] + nth_rw 2 [PermSet.smul_function] + have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 (π • f) (π • a) b + have ⟨hdf, hda, hdb⟩ := chooseFresh_fresh 𝔸 f a (π⁻¹ • b) + have hcf' : π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b # f.val := by + nth_rw 2 [show f = π⁻¹ • π • f by simp] + rw [← StepModel.fresh, ← Rel.equivariant 𝔸 NominalSet.IsFresh, StepModel.fresh] + exact hcf + have hca' : π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b ≠ a := by + intro hcontra + have h : π • π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b = π • a := by rw [hcontra] + rw [smul_inv_smul] at h + contradiction + have hcb' : π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b ≠ π⁻¹ • b := by + intro hcontra + have h : π • π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b = π • π⁻¹ • b := by rw [hcontra] + rw [smul_inv_smul, smul_inv_smul] at h + contradiction + have h := Req1.choose_restriction 𝔸 f.val f.prop.left a (π⁻¹ • b) _ _ hdf hcf' hda hca' hdb hcb' + rw [PermSet.Finsupp.smul_val] at h + rw [h, AlgebraStructure.res_equivariant, smul_inv_smul] + rw [← MulAction.mul_smul] + rw [show ⸨π • a,chooseFresh 𝔸 (π • f) (π • a) b⸩ * π = π * ⸨a, π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b⸩ by + rw [FPerm.mul_swap_eq_swap_mul] + rw [show π⁻¹ • chooseFresh 𝔸 (π • f) (π • a) b = π⁻¹ (chooseFresh 𝔸 (π • f) (π • a) b) from rfl] + rw [show π • a = π a from rfl] + simp] + rw [MulAction.mul_smul] + simp + +private noncomputable def restrict' : NameAbstraction 𝔸 (StepModel 𝔸 X) → PermSet.FinsuppFunction 𝔸 𝔸 X := + fun p ↦ ⟨restrict'' 𝔸 p, by + use NominalSet.supp 𝔸 p; constructor + · apply Function.Equivariant.preserve_support + apply NominalSet.supp_is_support + · apply NominalSet.supp_finite⟩ + +private lemma restrict_req1 {a : 𝔸} {f : StepModel 𝔸 X} : Req1 𝔸 (restrict' 𝔸 (⟪a⟫ f)) := by + intro b π hπ + have hπ₁ : π ∈ PermSet.fix 𝔸 (NominalSet.supp 𝔸 (restrict' 𝔸 (⟪a⟫ f))) := by + apply PermSet.fix_antitone_mem 𝔸 hπ; exact Set.subset_union_left + have hπ₂ : π • b = b := by + apply hπ; apply Set.mem_union_right; rfl + show π • (chooseFresh 𝔸 f a b \ (⸨a,chooseFresh 𝔸 f a b⸩ • f.val).val b) = (restrict' 𝔸 (⟪a⟫ f)).val b + rw [AlgebraStructure.res_equivariant] + rw [PermSet.Finsupp.smul_val] + rw [show π • (⸨a,chooseFresh 𝔸 f a b⸩ • f.val.val) b = (π • ⸨a,chooseFresh 𝔸 f a b⸩ • f.val.val) (π • b) by simp] + rw [← MulAction.mul_smul] + rw [FPerm.mul_swap_eq_swap_mul] + rw [show ⸨π a,π (chooseFresh 𝔸 f a b)⸩ = ⸨π • a,π • (chooseFresh 𝔸 f a b)⸩ from rfl] + rw [MulAction.mul_smul] + let d := chooseFresh 𝔸 (π • f) (π • a) (π • b) + have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b + have ⟨hdf, hda, hdb⟩ := chooseFresh_fresh 𝔸 (π • f) (π • a) (π • b) + have hcf' : π • chooseFresh 𝔸 f a b # (π • f).val := by + rw [← StepModel.fresh, ← Rel.equivariant 𝔸 NominalSet.IsFresh, StepModel.fresh] + exact hcf + have hca' : π • chooseFresh 𝔸 f a b ≠ π • a := by + intro hcontra + have h : π⁻¹ • π • chooseFresh 𝔸 f a b = π⁻¹ • π • a := by rw [hcontra] + rw [inv_smul_smul, inv_smul_smul] at h; contradiction + have hcb' : π • chooseFresh 𝔸 f a b ≠ π • b := by + intro hcontra + have h : π⁻¹ • π • chooseFresh 𝔸 f a b = π⁻¹ • π • b := by rw [hcontra] + rw [inv_smul_smul, inv_smul_smul] at h; contradiction + have h := Req1.choose_restriction 𝔸 (π • f).val (π • f).prop.left (π • a) (π • b) _ _ hcf' hdf hca' hda hcb' hdb + rw [smul_val, PermSet.Finsupp.smul_val, PermSet.Finsupp.smul_val] at h + rw [h] + rw [show (d \ (⸨π • a,d⸩ • π • f.val).val (π • b)) = (restrict' 𝔸 (π • ⟪a⟫ f)).val (π • b) from rfl] + rw [show restrict' 𝔸 (π • ⟪a⟫ f) = π • restrict' 𝔸 (⟪a⟫ f) by + apply Subtype.eq + simp only [restrict', PermSet.Finsupp.smul_val] + rw [Function.equivariant 𝔸 (restrict'' 𝔸)]] + rw [show π • restrict' 𝔸 (⟪a⟫ f) = restrict' 𝔸 (⟪a⟫ f) from NominalSet.supp_is_support 𝔸 hπ₁] + rw [hπ₂] + +private lemma restrict_req2 {a : 𝔸} {f : StepModel 𝔸 X} : Req2 𝔸 (restrict' 𝔸 (⟪a⟫ f)) := by + intro b c hcfresh hcb + have hinf : (NominalSet.supp 𝔸 f.val ∪ {a} ∪ {b} ∪ {c})ᶜ.Infinite := by + apply Set.Finite.infinite_compl + rw [Set.finite_union, Set.finite_union, Set.finite_union] + constructor + · constructor + · constructor + · apply NominalSet.supp_finite + · apply Set.finite_singleton + · apply Set.finite_singleton + · apply Set.finite_singleton + obtain ⟨d, hd⟩ := hinf.nonempty + simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hd + have hdf : d # f.val := hd.left.left.left + have hda : d ≠ a := hd.left.left.right + have hdb : d ≠ b := hd.left.right + have hdc : d ≠ c := hd.right + have hinf' : (NominalSet.supp 𝔸 (⸨a, d⸩ • f).val ∪ NominalSet.supp 𝔸 (restrict' 𝔸 (⟪a⟫ f)) ∪ {b} ∪ {d})ᶜ.Infinite := by + apply Set.Finite.infinite_compl + rw [Set.finite_union, Set.finite_union, Set.finite_union] + constructor + · constructor + · constructor + · apply NominalSet.supp_finite + · apply NominalSet.supp_finite + · apply Set.finite_singleton + · apply Set.finite_singleton + obtain ⟨e, he⟩ := hinf'.nonempty + simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at he + have hef : e # (⸨a, d⸩ • f).val := he.left.left.left + have hefresh : e # restrict' 𝔸 (⟪a⟫ f) := he.left.left.right + have heb : e ≠ b := he.left.right + have hed : e ≠ d := he.right + rw [Req1.choose_restriction 𝔸 (restrict' 𝔸 (⟪a⟫ f)) (restrict_req1 𝔸) b b _ _ hcfresh hefresh hcb heb hcb heb] + simp only [restrict', restrict'', Quotient.lift_mk] + nth_rw 3 [PermSet.Finsupp.smul_val] + rw [PermSet.smul_function] + simp only [FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left] + have ⟨hdf₁, hda₁, hdb₁⟩ := chooseFresh_fresh 𝔸 f a b + have ⟨hdf₂, hda₂, hde₂⟩ := chooseFresh_fresh 𝔸 f a e + rw [Req1.choose_restriction 𝔸 f.val f.prop.left a b _ _ hdf₁ hdf hda₁ hda hdb₁ hdb] + rw [Req1.choose_restriction 𝔸 f.val f.prop.left a e _ _ hdf₂ hdf hda₂ hda hde₂ (Ne.symm hed)] + have h := (⸨a,d⸩ • f).prop.right b e hef heb + simp only [smul_val, PermSet.Finsupp.smul_val] at h + nth_rw 3 [PermSet.smul_function] at h + simp only [FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left] at h + simp only [PermSet.Finsupp.smul_val] + nth_rw 1 [h] + rw [AlgebraStructure.ax_distributive] + rw [AlgebraStructure.res_equivariant] + rw [show ⸨b,e⸩ • d = d from FPerm.swap_apply_of_ne_of_ne hdb (Ne.symm hed)] + rw [AlgebraStructure.ax_swap] end StepModel |