import Mathlib
import Nominal.Support
import Nominal.Equivariance
import Nominal.Category
import Nominal.Permutations
import Nominal.Instances.Basic
import Nominal.Instances.Abstraction
import Nominal.NameRestriction.Finsupp

variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]

-- M₀ algebra structure: Equivariant join semilattices with name restriction

class AlgebraStructure (X : Type) [NominalSet 𝔸 X] where
  bot : Unit →ₑ[𝔸] X
  join : (X × X) →ₑ[𝔸] X
  res : NameAbstraction 𝔸 X →ₑ[𝔸] X
  ax_neutral : ∀ x, join (x, bot ()) = x
  ax_idempotent : ∀ x, join (x, x) = x
  ax_commutative : ∀ x y, join (x, y) = join (y, x)
  ax_associative : ∀ x y z, join (join (x, y), z) = join (x, join (y, z))
  ax_fresh : ∀ a x, a # x → res (⟪a⟫ x) = x
  ax_swap : ∀ a b x, res (⟪a⟫ res (⟪b⟫ x)) = res (⟪b⟫ res (⟪a⟫ x))
  ax_distributive : ∀ a x y, res (⟪a⟫ join (x, y)) = join (res (⟪a⟫ x), res (⟪a⟫ y))
  ax_redundant : ∀ a x, x = join (x, res (⟪a⟫ x))

private abbrev AlgebraStructure.bot' {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] :=
  (AlgebraStructure.bot : Unit →ₑ[𝔸] X)
private abbrev AlgebraStructure.join' {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] :=
  (AlgebraStructure.join : (X × X) →ₑ[𝔸] X)

notation "⊥[" A "]" => AlgebraStructure.bot' A ()
notation:60 x " ∨[" A "] " y => AlgebraStructure.join' A (x, y)
notation:60 a " \\ " x => AlgebraStructure.res (⟪a⟫ x)

-- M₁ algebra structure

class Depth1AlgebraStructure (X : Type) [NominalSet 𝔸 X] (Y : Type) [NominalSet 𝔸 Y] [AlgebraStructure 𝔸 Y] extends AlgebraStructure 𝔸 X where
  pre : (𝔸 × Y) →ₑ[𝔸] X
  abs : NameAbstraction 𝔸 Y →ₑ[𝔸] X
  ax_pre_distributive : ∀ a x y, pre (a, x ∨[𝔸] y) = join (pre (a, x), pre (a, y))
  ax_pre_bot : ∀ a, pre (a, ⊥[𝔸]) = bot ()
  ax_pre_restrict_self : ∀ a x, res (⟪a⟫ pre (a, x)) = bot ()
  ax_pre_restrict_other : ∀ a b x, a ≠ b → res (⟪a⟫ pre (b, x)) = pre (b, a \ x)
  ax_abs_distributive : ∀ a x y, abs (⟪a⟫ x ∨[𝔸] y) = join (abs (⟪a⟫ x), abs (⟪a⟫ y))
  ax_abs_bot : ∀ a, abs (⟪a⟫ ⊥[𝔸]) = bot ()
  ax_abs_restrict_other : ∀ a b x, a ≠ b → abs (⟪a⟫ (b \ x)) = res (⟪b⟫ abs (⟪a⟫ x))
  ax_local : ∀ a x, abs (⟪a⟫ x) = join (abs (⟪a⟫ x), pre (a, x))

-- Structure Definitions

-- (F'X)₀
def BaseModel (X : Type) [NominalSet 𝔸 X] : Type :=
  PermSet.FinSet 𝔸 X

def Req2 {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) :=
  -- Traces for all atoms include those from bound traces
  ∀ a c, c # f → c ≠ a → f.val a = f.val a ∨[𝔸] (c \ (⸨a, c⸩ • f).val a)

def permissibleFunctions (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] :=
  { f : PermSet.FinsuppFunction 𝔸 𝔸 X | Req2 𝔸 f }

-- (F'X)ₙ₊₁
def StepModel (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] : Type :=
  permissibleFunctions 𝔸 X

namespace AlgebraStructure

variable {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X]

lemma bot_supp : NominalSet.supp 𝔸 (⊥[𝔸] : X) = ∅ := by
  rw [← Set.subset_empty_iff]
  show NominalSet.supp 𝔸 ((bot' 𝔸).toFun ()) ⊆ ∅
  grw [Function.Equivariant.supp_subset]
  simp

lemma bot_fresh {a : 𝔸} : a # (⊥[𝔸] : X) := by
  simp [NominalSet.IsFresh, bot_supp]

lemma bot_equivariant {π : FPerm 𝔸} : π • (⊥[𝔸] : X) = ⊥[𝔸] := by
  show π ∈ PermSet.fix' 𝔸 (bot' 𝔸 ())
  apply NominalSet.supp_is_support
  rw [bot_supp]
  intro a ha; contradiction

lemma join_equivariant {x y : X} {π : FPerm 𝔸} : π • (x ∨[𝔸] y) = (π • x) ∨[𝔸] (π • y) := by
  show π • (join' 𝔸).toFun (x, y) = (join' 𝔸).toFun (π • (x, y))
  rw [← Function.equivariant]

lemma res_equivariant {a : 𝔸} {x : X} {π : FPerm 𝔸} : π • (a \ x) = (π • a) \ (π • x) := by
  show π • res.toFun (⟪a⟫ x) = res.toFun (π • (⟪a⟫ x))
  rw [← Function.equivariant]

lemma res_fresh {a : 𝔸} {x : X} : a # (a \ x) := by
  show a # res.toFun (⟪a⟫ x)
  apply Function.Equivariant.preserve_fresh
  rw [NameAbstraction.fresh]; right; rfl

lemma res_self {a : 𝔸} {x : X} : (a \ (a \ x)) = (a \ x) := by
  apply ax_fresh
  apply res_fresh

lemma res_bot {a : 𝔸} : (a \ ⊥[𝔸]) = (⊥[𝔸] : X) := by
  apply ax_fresh
  apply bot_fresh

end AlgebraStructure

-- Base Model Definitions

namespace BaseModel

variable {X : Type} [NominalSet 𝔸 X]

instance : NominalSet 𝔸 (BaseModel 𝔸 X) := PermSet.FinSet.instNominalSet 𝔸
instance : EmptyCollection (BaseModel 𝔸 X) := PermSet.FinSet.instEmptyCollection 𝔸
instance : Union (BaseModel 𝔸 X) := PermSet.FinSet.instUnion 𝔸
instance : Inter (BaseModel 𝔸 X) := PermSet.FinSet.instInter 𝔸
instance : SDiff (BaseModel 𝔸 X) := PermSet.FinSet.instSDiff 𝔸

@[simp] lemma empty_val : (∅ : BaseModel 𝔸 X).val = ∅ := rfl
@[simp] lemma union_val {S₁ S₂ : BaseModel 𝔸 X} : (S₁ ∪ S₂).val = S₁.val ∪ S₂.val := rfl
@[simp] lemma inter_val {S₁ S₂ : BaseModel 𝔸 X} : (S₁ ∩ S₂).val = S₁.val ∩ S₂.val := rfl
@[simp] lemma sdiff_val {S₁ S₂ : BaseModel 𝔸 X} : (S₁ \ S₂).val = S₁.val \ S₂.val := rfl
@[simp] lemma smul_val {L : BaseModel 𝔸 X} {π : FPerm 𝔸} : (π • L).val = π • L.val := rfl

def bot : Unit → BaseModel 𝔸 X :=
  fun _ ↦ ∅

instance : Function.Equivariant 𝔸 (bot 𝔸 : Unit → BaseModel 𝔸 X) := by
  constructor; intro _ π
  apply Subtype.eq; simp [bot]

def union : (BaseModel 𝔸 X × BaseModel 𝔸 X) → BaseModel 𝔸 X := PermSet.FinSet.union 𝔸

instance : Function.Equivariant 𝔸 (union 𝔸 : (BaseModel 𝔸 X × BaseModel 𝔸 X) → BaseModel 𝔸 X) :=
  PermSet.FinSet.instEquivariantProdUnion 𝔸

def restrict : NameAbstraction 𝔸 (BaseModel 𝔸 X) → BaseModel 𝔸 X := Quotient.lift
  (fun ⟨a, S⟩ ↦ ⟨{x ∈ S.val | a # x}, by
    apply Set.Finite.subset S.prop; simp⟩)
  (by
    intro ⟨a₁, S₁⟩ ⟨a₂, S₂⟩ haeq
    apply Subtype.eq
    simp only
    rw [← NameAbstraction.eq_iff_alpha_eq 𝔸 (BaseModel 𝔸 X), NameAbstraction.eq_iff_cases] at haeq
    cases haeq with
    | inl h => rw [h.left, h.right]
    | inr h =>
      ext x; constructor
      · intro ⟨hx, ha₁⟩
        have hx' : ⸨a₁, a₂⸩ • x ∈ S₂.val := by
          rw [← Set.mem_inv_smul_set_iff, FPerm.swap_inv]
          show x ∈ (⸨a₁, a₂⸩ • S₂).val
          rw [← h.right.right]; exact hx
        have ha₂ := h.right.left
        rw [PermSet.FinSet.fresh] at ha₂
        specialize ha₂ (⸨a₁, a₂⸩ • x) hx'
        nth_rw 1 [show a₁ = ⸨a₁, a₂⸩ • a₂ by simp] at ha₂
        rw [← Rel.equivariant 𝔸 NominalSet.IsFresh] at ha₂
        constructor
        · rw [← show ⸨a₁, a₂⸩ • x = x from NominalSet.fresh_swap_fix 𝔸 ha₁ ha₂]
          exact hx'
        · exact ha₂
      · intro ⟨hx, ha₂⟩
        have hx' : ⸨a₁, a₂⸩ • x ∈ S₁.val := by
          rw [← Set.mem_inv_smul_set_iff, FPerm.swap_inv]
          show x ∈ (⸨a₁, a₂⸩ • S₁).val
          rw [h.right.right, ← MulAction.mul_smul, FPerm.swap_mul_self, MulAction.one_smul]
          exact hx
        have ha₁ := h.right.left
        rw [PermSet.FinSet.fresh] at ha₁
        specialize ha₁ x hx
        rw [← show ⸨a₁, a₂⸩ • x = x from NominalSet.fresh_swap_fix 𝔸 ha₁ ha₂] at hx'
        rw [← MulAction.mul_smul, FPerm.swap_mul_self, MulAction.one_smul] at hx'
        exact ⟨hx', ha₁⟩)

instance : Function.Equivariant 𝔸 (restrict 𝔸 : NameAbstraction 𝔸 (BaseModel 𝔸 X) → BaseModel 𝔸 X) := by
  constructor
  apply Quotient.ind
  intro ⟨a, S⟩ π
  apply Subtype.eq
  simp only [restrict, NameAbstraction.smul, Quotient.lift_mk, smul_val]
  ext x; constructor
  · intro ⟨hx, hfresh⟩
    rw [Set.mem_smul_set_iff_inv_smul_mem]; constructor
    · rw [← Set.mem_smul_set_iff_inv_smul_mem]; exact hx
    · rw [show a = π⁻¹ • π • a by simp, ← Rel.equivariant 𝔸 NominalSet.IsFresh]
      exact hfresh
  · rw [Set.mem_smul_set_iff_inv_smul_mem]
    intro ⟨hx, hfresh⟩; constructor
    · rw [Set.mem_smul_set_iff_inv_smul_mem]; exact hx
    · rw [show x = π • π⁻¹ • x by simp, ← Rel.equivariant 𝔸 NominalSet.IsFresh]
      exact hfresh

lemma restrict_eq {a : 𝔸} {S : BaseModel 𝔸 X} :
    (restrict 𝔸 (⟪a⟫ S)).val = {x ∈ S.val | a # x} := rfl

instance : AlgebraStructure 𝔸 (BaseModel 𝔸 X) where
  bot := ⟨bot 𝔸, inferInstance⟩
  join := ⟨union 𝔸, inferInstance⟩
  res := ⟨restrict 𝔸, inferInstance⟩
  ax_neutral x := by
    apply Subtype.eq
    show x.val ∪ ∅ = x.val
    simp
  ax_idempotent x := by
    apply Subtype.eq
    show x.val ∪ x.val = x.val
    simp
  ax_commutative x y := by
    apply Subtype.eq
    show x.val ∪ y.val = y.val ∪ x.val
    apply Set.union_comm
  ax_associative x y z := by
    apply Subtype.eq
    show (x.val ∪ y.val) ∪ z.val = x.val ∪ (y.val ∪ z.val)
    apply Set.union_assoc
  ax_fresh a S := by
    intro hfresh
    show restrict 𝔸 (⟪a⟫ S) = S
    apply Subtype.eq
    rw [restrict_eq]
    rw [PermSet.FinSet.fresh] at hfresh
    ext x; constructor
    · intro ⟨hS, _⟩; exact hS
    · intro hS; exact ⟨hS, hfresh x hS⟩
  ax_swap a b S := by
    show restrict 𝔸 (⟪a⟫ restrict 𝔸 (⟪b⟫ S)) = restrict 𝔸 (⟪b⟫ restrict 𝔸 (⟪a⟫ S))
    apply Subtype.eq
    ext x
    simp only [restrict_eq, Set.mem_setOf_eq]
    ac_nf
  ax_distributive a S₁ S₂ := by
    show restrict 𝔸 (⟪a⟫ S₁ ∪ S₂) = restrict 𝔸 (⟪a⟫ S₁) ∪ restrict 𝔸 (⟪a⟫ S₂)
    apply Subtype.eq
    simp [restrict_eq]
  ax_redundant a S := by
    show S = S ∪ restrict 𝔸 (⟪a⟫ S)
    apply Subtype.eq; ext x
    simp only [union_val, restrict_eq, Set.mem_union, Set.mem_setOf_eq, iff_self_or, and_imp]
    intro h _; exact h

@[simp] lemma bot_eq : (⊥[𝔸] : BaseModel 𝔸 X) = ∅ := rfl
@[simp] lemma join_eq {S₁ S₂ : BaseModel 𝔸 X} : (S₁ ∨[𝔸] S₂) = S₁ ∪ S₂ := rfl
@[simp] lemma res_eq {a : 𝔸} {S : BaseModel 𝔸 X} : (a \ S) = restrict 𝔸 (⟪a⟫ S) := rfl

end BaseModel

-- Step Model: \bar{M₁} X

lemma supp_image {X : Type} [NominalSet 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) :
    ∀ a, PermSet.HasSupport 𝔸 (f.val a) (NominalSet.supp 𝔸 f ∪ {a}) := by
  intro a
  have := PermSet.FinsuppFunction.supp_image 𝔸 f a
  rw [NominalSet.supp_atom] at this
  exact this

lemma choose_restriction'
    {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) :
    ∀ (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 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 𝔸 (supp_image 𝔸 f 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 *
    · 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 𝔸 (supp_image 𝔸 f 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 𝔸 (supp_image 𝔸 f b) (by simp [NominalSet.supp_finite]) hcontra
        simp only [Set.union_singleton, Set.mem_insert_iff] at h
        cases h <;> contradiction]

namespace StepModel

variable {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X]

private lemma permissibleFunctions_req2
    (f : PermSet.FinsuppFunction 𝔸 𝔸 X) (π : FPerm 𝔸) : Req2 𝔸 f → Req2 𝔸 (π • f) := by
  intro hf a c hcf hca
  specialize hf (π⁻¹ • a) (π⁻¹ • c)
  specialize hf (by
    rw [show f = π⁻¹ • π • f by simp]
    rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]
    exact hcf)
  specialize hf (by
    intro hcontra
    have : π • π⁻¹ • c = π • π⁻¹ • a := by rw [hcontra]
    simp only [smul_inv_smul] at this
    exact hca this)
  simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap,
    Equiv.swap_apply_left]
  nth_rw 1 [hf]
  rw [AlgebraStructure.join_equivariant, AlgebraStructure.res_equivariant]
  simp only [smul_inv_smul, PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv,
    PermSet.atom_swap, Equiv.swap_apply_left]
  suffices π • ⸨π⁻¹ • a,π⁻¹ • c⸩ • f.val (π⁻¹ • c) = ⸨a, c⸩ • π • f.val (π⁻¹ • c) by rw [this]
  rw [← MulAction.mul_smul, ← MulAction.mul_smul]
  suffices π * ⸨π⁻¹ • a,π⁻¹ • c⸩ = ⸨a,c⸩ * π by rw [this]
  rw [FPerm.mul_swap_eq_swap_mul, show π⁻¹ • a = π⁻¹ a from rfl, show π⁻¹ • c = π⁻¹ c from rfl]
  simp

instance : Set.Equivariant 𝔸 (permissibleFunctions 𝔸 X) := by
  constructor; exact permissibleFunctions_req2 𝔸

instance : NominalSet 𝔸 (StepModel 𝔸 X) := Subtype.instNominalSetElem 𝔸

@[simp] lemma smul_val (π : FPerm 𝔸) (f : StepModel 𝔸 X) : (π • f).val = π • f.val :=
  Subtype.smul_val 𝔸 π f

instance instValEquivariant : Function.Equivariant 𝔸 (Subtype.val : StepModel 𝔸 X → PermSet.FinsuppFunction 𝔸 𝔸 X) :=
  Subtype.instValEquivariant 𝔸

@[simp] lemma supp {f : StepModel 𝔸 X} : NominalSet.supp 𝔸 f = NominalSet.supp 𝔸 f.val :=
  Subtype.supp 𝔸

@[simp] lemma fresh {a : 𝔸} {f : StepModel 𝔸 X} : a # f ↔ a # f.val :=
  Subtype.fresh 𝔸

lemma choose_restriction (f : StepModel 𝔸 X) :
    ∀ (a b c d : 𝔸), c # f → d # f → c ≠ a → d ≠ a → c ≠ b → d ≠ b →
      (c \ (⸨a, c⸩ • f.val).val b) = (d \ (⸨a, d⸩ • f.val).val b) := by
  intro a b c d hcf hdf hca hda hcb hdb
  rw [fresh] at hcf hdf
  exact choose_restriction' 𝔸 f.val a b c d hcf hdf hca hda hcb hdb

private def bot' : PermSet.FinsuppFunction 𝔸 𝔸 X :=
  ⟨fun _ ↦ ⊥[𝔸], by
    use ∅; constructor
    · intro π hπ; ext a
      simp [AlgebraStructure.bot_equivariant]
    · exact Set.finite_empty⟩

private lemma bot_req2 : Req2 𝔸 (bot' 𝔸 : PermSet.FinsuppFunction 𝔸 𝔸 X) := by
  intro a c _ _
  simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, bot']
  rw [AlgebraStructure.bot_equivariant]
  rw [AlgebraStructure.ax_fresh c (⊥[𝔸]) (AlgebraStructure.bot_fresh 𝔸)]
  rw [AlgebraStructure.ax_idempotent]

def bot : Unit → StepModel 𝔸 X :=
  fun _ ↦ ⟨bot' 𝔸, bot_req2 𝔸⟩

instance : Function.Equivariant 𝔸 (bot 𝔸 : Unit → StepModel 𝔸 X) := by
  constructor; intro _ π
  apply Subtype.eq; ext a
  simp [bot, bot', AlgebraStructure.bot_equivariant]

private def union'' : (StepModel 𝔸 X × StepModel 𝔸 X) → 𝔸 → X :=
  fun (f, g) ↦ fun a ↦ f.val.val a ∨[𝔸] g.val.val a

instance : Function.Equivariant 𝔸 (union'' 𝔸 : (StepModel 𝔸 X × StepModel 𝔸 X) → 𝔸 → X) := by
  constructor; intro (f, g) π
  ext a
  simp only [union'', smul_val, PermSet.Finsupp.smul_val, PermSet.smul_function]
  rw [AlgebraStructure.join_equivariant]

private def union' : (StepModel 𝔸 X × StepModel 𝔸 X) → PermSet.FinsuppFunction 𝔸 𝔸 X :=
  fun p ↦ ⟨union'' 𝔸 p, by
    use NominalSet.supp 𝔸 p; constructor
    · apply Function.Equivariant.preserve_support
      apply NominalSet.supp_is_support
    · apply NominalSet.supp_finite⟩

private lemma union_req2 {f g : StepModel 𝔸 X} : Req2 𝔸 (union' 𝔸 (f, g)) := by
  intro a c hcfresh hca
  have hinf : (NominalSet.supp 𝔸 (union' 𝔸 (f, g)) ∪ NominalSet.supp 𝔸 f ∪ NominalSet.supp 𝔸 g ∪ {a})ᶜ.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 NominalSet.supp_finite
    · apply Set.finite_singleton
  obtain ⟨d, hd⟩ := hinf.nonempty
  simp only [supp, Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hd
  have hdfresh : d # union' 𝔸 (f, g) := hd.left.left.left
  have hdf : d # f.val := hd.left.left.right
  have hdg : d # g.val := hd.left.right
  have hda : d ≠ a := hd.right
  simp only [PermSet.Finsupp.smul_val]
  have h := choose_restriction' 𝔸 (union' 𝔸 (f, g)) 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,
    Equiv.swap_apply_left]
  nth_rw 1 [show d = ⸨a, d⸩ • a by simp]
  rw [← AlgebraStructure.res_equivariant]
  rw [AlgebraStructure.ax_distributive]
  rw [AlgebraStructure.join_equivariant]
  rw [AlgebraStructure.res_equivariant]
  rw [AlgebraStructure.res_equivariant]
  rw [AlgebraStructure.ax_associative]
  nth_rw 3 [AlgebraStructure.ax_commutative]
  rw [AlgebraStructure.ax_associative]
  rw [← AlgebraStructure.ax_associative]
  nth_rw 4 [AlgebraStructure.ax_commutative]
  rw [show ⸨a, d⸩ • a = d by simp]
  have hf := f.prop a d hdf hda
  have hg := g.prop a d hdg hda
  simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap,
    Equiv.swap_apply_left] at hf hg
  rw [← hf, ← hg]

def union : (StepModel 𝔸 X × StepModel 𝔸 X) → StepModel 𝔸 X :=
  fun (f, g) ↦ ⟨union' 𝔸 (f, g), union_req2 𝔸⟩

instance : Function.Equivariant 𝔸 (union 𝔸 : (StepModel 𝔸 X × StepModel 𝔸 X) → StepModel 𝔸 X) := by
  constructor; intro x π
  apply Subtype.eq; ext a
  simp only [union, union', Prod.mk.eta, smul_val, PermSet.Finsupp.smul_val]
  rw [show (π • x.fst, π • x.snd) = π • x by ext <;> simp]
  rw [← Function.equivariant]

private noncomputable def chooseFresh {X : Type} [NominalSet 𝔸 X] (x : X) (a b : 𝔸) : 𝔸 :=
  have hinf : (NominalSet.supp 𝔸 x ∪ {a} ∪ {b})ᶜ.Infinite := by
    apply Set.Finite.infinite_compl
    simp only [Set.union_singleton, Set.finite_insert]
    apply NominalSet.supp_finite
  Classical.choose hinf.nonempty

private lemma chooseFresh_fresh {X : Type} [NominalSet 𝔸 X] (x : X) (a b : 𝔸) :
    chooseFresh 𝔸 x a b # x ∧ chooseFresh 𝔸 x a b ≠ a ∧ chooseFresh 𝔸 x a b ≠ b := by
  have h : chooseFresh 𝔸 x a b ∈ (NominalSet.supp 𝔸 x ∪ {a} ∪ {b})ᶜ := Classical.choose_spec _
  simp only [Set.union_singleton, Set.mem_compl_iff, Set.mem_insert_iff, not_or] at h
  exact ⟨h.right.right, h.right.left, h.left⟩

private noncomputable def restrict'' : NameAbstraction 𝔸 (StepModel 𝔸 X) → 𝔸 → X := Quotient.lift
  (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
    rw [← NameAbstraction.eq_iff_alpha_eq 𝔸 (StepModel 𝔸 X), NameAbstraction.eq_iff_cases] at haeq
    cases haeq with
    | inl h => rw [h.left, h.right]
    | inr h =>
      simp only
      have hinf : (NominalSet.supp 𝔸 f₁ ∪ NominalSet.supp 𝔸 f₂ ∪ {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₁ := hc.left.left.left.left
      have hcf₂ : c # f₂ := 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 [choose_restriction 𝔸 f₁ a₁ b _ c hfreshf₁ hcf₁ hfresha₁ hca₁ hfreshb₁ hcb]
      rw [choose_restriction 𝔸 f₂ 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
      · simp [*] at *
      · simp [*] at *
      · rw [← supp] at hd
        rw [hdc] at hd
        contradiction
      · 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 := by
    nth_rw 2 [show f = π⁻¹ • π • f by simp]
    rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]
    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 := choose_restriction 𝔸 f 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_req2 {a : 𝔸} {f : StepModel 𝔸 X} : Req2 𝔸 (restrict' 𝔸 (⟪a⟫ f)) := by
  intro b c hcfresh hcb
  have hinf : (NominalSet.supp 𝔸 f ∪ {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 := 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 [choose_restriction' 𝔸 (restrict' 𝔸 (⟪a⟫ f)) 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 [choose_restriction 𝔸 f a b _ _ hdf₁ hdf hda₁ hda hdb₁ hdb]
  rw [choose_restriction 𝔸 f a e _ _ hdf₂ hdf hda₂ hda hde₂ (Ne.symm hed)]
  have h := (⸨a,d⸩ • f).prop 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]

noncomputable def restrict : NameAbstraction 𝔸 (StepModel 𝔸 X) → StepModel 𝔸 X :=
  fun p ↦ ⟨restrict' 𝔸 p, by
    suffices ∀ p, Req2 𝔸 (restrict' 𝔸 p) by apply this
    apply Quotient.ind; intro ⟨a, x⟩
    apply restrict_req2⟩

instance : Function.Equivariant 𝔸 (restrict 𝔸 : NameAbstraction 𝔸 (StepModel 𝔸 X) → StepModel 𝔸 X) := by
  constructor; intro x π
  apply Subtype.eq; apply Subtype.eq
  simp only [restrict, restrict', smul_val, PermSet.Finsupp.smul_val]
  rw [← Function.equivariant]

@[simp] lemma bot_eq {a : 𝔸} :
    (bot 𝔸 () : StepModel 𝔸 X).val.val a = ⊥[𝔸] := rfl

@[simp] lemma union_eq {f₁ f₂ : StepModel 𝔸 X} {a : 𝔸} :
    (union 𝔸 (f₁, f₂)).val.val a = f₁.val.val a ∨[𝔸] f₂.val.val a := rfl

lemma restrict_eq' {a : 𝔸} {f : StepModel 𝔸 X} {b : 𝔸} :
    (restrict 𝔸 (⟪a⟫ f)).val.val b =  ((chooseFresh 𝔸 f a b) \ (⸨a, (chooseFresh 𝔸 f a b)⸩ • f.val).val b) := rfl

lemma restrict_eq {a : 𝔸} {f : StepModel 𝔸 X} {b : 𝔸} :
    ∀ c, c # f → c ≠ a → c ≠ b →
      (restrict 𝔸 (⟪a⟫ f)).val.val b =  (c \ (⸨a, c⸩ • f.val).val b) := by
  intro d hdf hda hdb
  have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b
  apply choose_restriction 𝔸 f a b _ _ hcf hdf hca hda hcb hdb

lemma restrict_supp (f : StepModel 𝔸 X) (a c : 𝔸) :
    c # f → c # (restrict 𝔸 (⟪a⟫ f)) := by
  intro hf hcontra
  have h : NominalSet.supp 𝔸 (restrict 𝔸 (⟪a⟫ f)) ⊆ NominalSet.supp 𝔸 (⟪a⟫ f) :=
    Function.Equivariant.supp_subset 𝔸
  specialize h hcontra
  simp only [NameAbstraction.supp, supp, Set.mem_diff, Set.mem_singleton_iff] at h
  have := h.left
  rw [← supp] at this
  contradiction

lemma mem_fresh (f : StepModel 𝔸 X) (a c : 𝔸) : c # f → c ≠ a → c # f.val.val a := by
  intro hf hb hcontra
  rw [fresh] at hf
  have h : NominalSet.supp 𝔸 (f.val.val a) ⊆ NominalSet.supp 𝔸 f.val ∪ {a} :=
    NominalSet.support_subset_supp 𝔸 (supp_image 𝔸 f.val a) (by
      simp only [Set.union_singleton, Set.finite_insert]
      apply NominalSet.supp_finite)
  specialize h hcontra
  simp only [Set.union_singleton, Set.mem_insert_iff] at h
  cases h <;> contradiction

lemma restrict_fresh (f : StepModel 𝔸 X) (a b : 𝔸) :
    a ≠ b → (restrict 𝔸 (⟪a⟫ f)).val.val b = a \ (f.val.val b) := by
  intro hne
  let c := chooseFresh 𝔸 f a b
  have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b
  simp only [restrict_eq', PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv]
  rw [show ⸨a,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hne) (Ne.symm hcb)]
  suffices ⟪a⟫ f.val.val b = ⟪c⟫ ⸨a,c⸩ • f.val.val b by rw [this]
  rw [NameAbstraction.eq_iff_cases]; right
  constructor
  · exact Ne.symm hca
  · constructor
    · nth_rw 1 [show a = ⸨a,c⸩ • c by simp]
      rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]
      apply mem_fresh 𝔸 _ _ _ hcf hcb
    · rw [← MulAction.mul_smul]
      rw [FPerm.swap_mul_self]
      rw [MulAction.one_smul]

noncomputable instance : AlgebraStructure 𝔸 (StepModel 𝔸 X) where
  bot := ⟨bot 𝔸, inferInstance⟩
  join := ⟨union 𝔸, inferInstance⟩
  res := ⟨restrict 𝔸, inferInstance⟩
  ax_neutral x := by
    show union 𝔸 (x, (bot 𝔸 ())) = x
    apply Subtype.eq; apply Subtype.eq; ext a
    simp [AlgebraStructure.ax_neutral]
  ax_idempotent x := by
    show union 𝔸 (x, x) = x
    apply Subtype.eq; apply Subtype.eq; ext a
    simp [AlgebraStructure.ax_idempotent]
  ax_commutative x y := by
    show union 𝔸 (x, y) = union 𝔸 (y, x)
    apply Subtype.eq; apply Subtype.eq; ext a
    simp [AlgebraStructure.ax_commutative]
  ax_associative x y z := by
    show union 𝔸 (union 𝔸 (x, y), z) = union 𝔸 (x, union 𝔸 (y, z))
    apply Subtype.eq; apply Subtype.eq; ext a
    simp [AlgebraStructure.ax_associative]
  ax_fresh a f := by
    intro hfresh
    show restrict 𝔸 (⟪a⟫ f) = f
    apply Subtype.eq; apply Subtype.eq; ext b
    have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b
    rw [restrict_eq', ← smul_val]
    rw [show ⸨a,chooseFresh 𝔸 f a b⸩ • f = f from NominalSet.fresh_swap_fix 𝔸 hfresh hcf]
    apply AlgebraStructure.ax_fresh
    intro hcontra
    have h := NominalSet.support_subset_supp 𝔸 (supp_image 𝔸 f.val b) (by simp [NominalSet.supp_finite]) hcontra
    simp only [Set.union_singleton, Set.mem_insert_iff] at h
    rw [← supp] at h
    cases h <;> contradiction
  ax_swap a₁ a₂ f := by
    show restrict 𝔸 (⟪a₁⟫ (restrict 𝔸 (⟪a₂⟫ f))) = restrict 𝔸 (⟪a₂⟫ (restrict 𝔸 (⟪a₁⟫ f)))
    apply Subtype.eq; apply Subtype.eq; ext b
    by_cases heq : a₁ = a₂
    · rw [heq]
    · have hinf : (NominalSet.supp 𝔸 f ∪ {a₁} ∪ {a₂} ∪ {b})ᶜ.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 ⟨c₁, hc₁⟩ := hinf.nonempty
      simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hc₁
      have hc₁f : c₁ # f := hc₁.left.left.left
      have hc₁a₁ : c₁ ≠ a₁ := hc₁.left.left.right
      have hc₁a₂ : c₁ ≠ a₂ := hc₁.left.right
      have hc₁b : c₁ ≠ b := hc₁.right
      have hinf' : (NominalSet.supp 𝔸 f ∪ {a₁} ∪ {a₂} ∪ {b} ∪ {c₁})ᶜ.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 Set.finite_singleton
            · 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 hc₂f : c₂ # f := hc₂.left.left.left.left
      have hc₂a₁ : c₂ ≠ a₁ := hc₂.left.left.left.right
      have hc₂a₂ : c₂ ≠ a₂ := hc₂.left.left.right
      have hc₂b : c₂ ≠ b := hc₂.left.right
      have hc₂c₁ : c₂ ≠ c₁ := hc₂.right
      have hc₁f' : c₁ # (⸨a₂,c₂⸩ • f) := by
        intro hcontra
        rw [Function.equivariant 𝔸 (NominalSet.supp 𝔸)] at hcontra
        rw [← PermSet.atom_set_swap_ne_ne 𝔸 hc₁a₂ (Ne.symm hc₂c₁)] at hcontra
        contradiction
      have hc₂f' : c₂ # (⸨a₁,c₁⸩ • f) := by
        intro hcontra
        rw [Function.equivariant 𝔸 (NominalSet.supp 𝔸)] at hcontra
        rw [← PermSet.atom_set_swap_ne_ne 𝔸 hc₂a₁ hc₂c₁] at hcontra
        contradiction
      rw [restrict_eq 𝔸 c₁ (restrict_supp 𝔸 f a₂ c₁ hc₁f) hc₁a₁ hc₁b]
      rw [← smul_val, ← Function.equivariant 𝔸 (restrict 𝔸), NameAbstraction.smul]
      rw [show ⸨a₁,c₁⸩ • a₂ = a₂ from FPerm.swap_apply_of_ne_of_ne (Ne.symm heq) (Ne.symm hc₁a₂)]
      rw [restrict_eq 𝔸 c₂ hc₂f' hc₂a₂ hc₂b]
      rw [smul_val, PermSet.Finsupp.smul_val, PermSet.Finsupp.smul_val]
      rw [restrict_eq 𝔸 c₂ (restrict_supp 𝔸 f a₁ c₂ hc₂f) hc₂a₂ hc₂b]
      rw [← smul_val, ← Function.equivariant 𝔸 (restrict 𝔸), NameAbstraction.smul]
      rw [show ⸨a₂,c₂⸩ • a₁ = a₁ from FPerm.swap_apply_of_ne_of_ne heq (Ne.symm hc₂a₁)]
      rw [restrict_eq 𝔸 c₁ hc₁f' hc₁a₁ hc₁b]
      rw [smul_val, PermSet.Finsupp.smul_val, PermSet.Finsupp.smul_val]
      rw [AlgebraStructure.ax_swap]
      rw [← MulAction.mul_smul, ← MulAction.mul_smul]
      suffices ⸨a₂,c₂⸩ * ⸨a₁,c₁⸩ = ⸨a₁,c₁⸩ * ⸨a₂,c₂⸩ by rw [this]
      rw [FPerm.mul_swap_eq_swap_mul]
      rw [FPerm.swap_apply_of_ne_of_ne heq (Ne.symm hc₂a₁)]
      rw [FPerm.swap_apply_of_ne_of_ne hc₁a₂ (Ne.symm hc₂c₁)]
  ax_distributive a f g := by
    show restrict 𝔸 (⟪a⟫ (union 𝔸 (f, g))) = union 𝔸 (restrict 𝔸 (⟪a⟫ f), restrict 𝔸 (⟪a⟫ g))
    apply Subtype.eq; apply Subtype.eq; ext b
    rw [union_eq]
    have hinf : (NominalSet.supp 𝔸 (union 𝔸 (f, g)) ∪ NominalSet.supp 𝔸 f ∪ NominalSet.supp 𝔸 g ∪ {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 NominalSet.supp_finite
        · 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 hcfg : c # (union 𝔸 (f, g)) := hc.left.left.left.left
    have hcf : c # f := hc.left.left.left.right
    have hcg : c # g := hc.left.left.right
    have hca : c ≠ a := hc.left.right
    have hcb : c ≠ b := hc.right
    rw [restrict_eq 𝔸 c hcfg hca hcb]
    rw [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, union_eq]
    rw [AlgebraStructure.join_equivariant]
    rw [AlgebraStructure.ax_distributive]
    rw [restrict_eq 𝔸 c hcf hca hcb]
    rw [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv]
    rw [restrict_eq 𝔸 c hcg hca hcb]
    rw [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv]
  ax_redundant a f := by
    show f = union 𝔸 (f, restrict 𝔸 (⟪a⟫ f))
    apply Subtype.eq; apply Subtype.eq; ext b
    rw [union_eq]
    by_cases heq : a = b
    · rw [heq, restrict_eq']
      have ⟨hcf, hcb, _⟩ := chooseFresh_fresh 𝔸 f b b
      rw [fresh] at hcf
      exact f.prop b _ hcf hcb
    · rw [restrict_eq']
      let c := chooseFresh 𝔸 f a b
      have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b
      rw [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv]
      rw [show ⸨a,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm heq) (Ne.symm hcb)]
      rw [show ⟪c⟫ ⸨a,c⸩ • f.val.val b = ⸨a,c⸩ • ⟪a⟫ f.val.val b by simp]
      rw [show ⸨a,c⸩ • ⟪a⟫ f.val.val b = ⟪a⟫ f.val.val b by
        apply NominalSet.fresh_swap_fix
        · rw [NameAbstraction.fresh]; right; rfl
        · rw [NameAbstraction.fresh]; left
          apply mem_fresh 𝔸 f b c hcf hcb]
      apply AlgebraStructure.ax_redundant

private lemma abs_choice {x : X} {a b : 𝔸} :
    ∀ (c d : 𝔸), c # x → d # x → c ≠ a → d ≠ a → c ≠ b → d ≠ b →
      ⸨b,c⸩ • (b \ (⸨a,c⸩ • x)) = ⸨b,d⸩ • (b \ (⸨a,d⸩ • x)) := by
  intro c d hcx hdx hca hda hcb hdb
  by_cases heq : c = d
  · rw [heq]
  · rw [AlgebraStructure.res_equivariant, AlgebraStructure.res_equivariant]
    simp only [PermSet.atom_swap, Equiv.swap_apply_left]
    suffices ⟪c⟫ ⸨b,c⸩ • ⸨a,c⸩ • x = ⟪d⟫ ⸨b,d⸩ • ⸨a,d⸩ • x by rw [this]
    rw [NameAbstraction.eq_iff_cases]; right
    constructor
    · exact heq
    · constructor
      · rw [← show ⸨b,d⸩ • c = c from FPerm.swap_apply_of_ne_of_ne hcb heq]
        rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]
        rw [← show ⸨a,d⸩ • c = c from FPerm.swap_apply_of_ne_of_ne hca heq]
        rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]
        exact hcx
      . nth_rw 2 [← MulAction.mul_smul]
        rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne (Ne.symm hcb) (Ne.symm hdb)]
        rw [MulAction.mul_smul]
        nth_rw 3 [← MulAction.mul_smul]
        rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne (Ne.symm hca) (Ne.symm hda)]
        rw [MulAction.mul_smul]
        rw [show ⸨c,d⸩ • x = x from NominalSet.fresh_swap_fix 𝔸 hcx hdx]

private noncomputable def abs'' : NameAbstraction 𝔸 X → 𝔸 → X := Quotient.lift
  (fun ⟨a, x⟩ b ↦
    let c := chooseFresh 𝔸 x a b
    ⸨b,c⸩ • (b \ (⸨a,c⸩ • x)))
  (by
    intro ⟨a, x⟩ ⟨a', x'⟩ haeq
    ext b
    simp only
    rw [← NameAbstraction.eq_iff_alpha_eq 𝔸 X, NameAbstraction.eq_iff_cases] at haeq
    cases haeq with
    | inl h => rw [h.left, h.right]
    | inr h =>
      have hinf : (NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 x' ∪ {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 hcx : c # x := hc.left.left.left.left
      have hcx' : c # x' := 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 ⟨hdx, hda, hdb⟩ := chooseFresh_fresh 𝔸 x a b
      rw [abs_choice 𝔸 _ _ hdx hcx hda hca hdb hcb]
      have ⟨hex', hea', heb⟩ := chooseFresh_fresh 𝔸 x' a' b
      rw [abs_choice 𝔸 _ _ hex' hcx' hea' hca' heb hcb]
      suffices ⸨a,c⸩ • x = ⸨a',c⸩ • x' by rw [this]
      rw [h.right.right, ← MulAction.mul_smul]
      rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_left, FPerm.swap_apply_of_ne_of_ne (Ne.symm h.left) (Ne.symm hca')]
      rw [MulAction.mul_smul, FPerm.swap_comm]
      nth_rw 2 [NominalSet.fresh_swap_fix 𝔸]
      · exact h.right.left
      · exact hcx')

instance : Function.Equivariant 𝔸 (abs'' 𝔸 : NameAbstraction 𝔸 X → 𝔸 → X) := by
  constructor
  apply Quotient.ind
  intro ⟨a, x⟩ π
  ext b
  simp only [abs'', NameAbstraction.smul, Quotient.lift_mk, PermSet.smul_function]
  have ⟨hcx, hca, hcb⟩ := chooseFresh_fresh 𝔸 (π • x) (π • a) b
  have ⟨hdx, hda, hdb⟩ := chooseFresh_fresh 𝔸 x a (π⁻¹ • b)
  have hcx' : π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b # x := by
    nth_rw 2 [show x = π⁻¹ • π • x by simp]
    rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]
    exact hcx
  have hca' : π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b ≠ a := by
    intro hcontra
    have h : π • π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b = π • a := by rw [hcontra]
    rw [smul_inv_smul] at h
    contradiction
  have hcb' : π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b ≠ π⁻¹ • b := by
    intro hcontra
    have h : π • π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b = π • π⁻¹ • b := by rw [hcontra]
    rw [smul_inv_smul, smul_inv_smul] at h
    contradiction
  rw [abs_choice 𝔸 _ _ hdx hcx' hda hca' hdb hcb']
  nth_rw 2 [← MulAction.mul_smul]
  rw [show π * ⸨π⁻¹ • b,π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b⸩ = ⸨π • π⁻¹ • b,π • π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b⸩ * π from FPerm.mul_swap_eq_swap_mul]
  rw [smul_inv_smul, smul_inv_smul, MulAction.mul_smul]
  nth_rw 2 [AlgebraStructure.res_equivariant]
  rw [smul_inv_smul]
  nth_rw 2 [← MulAction.mul_smul]
  rw [show π * ⸨a,π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b⸩ = ⸨π • a,π • π⁻¹ • chooseFresh 𝔸 (π • x) (π • a) b⸩ * π from FPerm.mul_swap_eq_swap_mul]
  rw [smul_inv_smul, MulAction.mul_smul]

private noncomputable def abs' : NameAbstraction 𝔸 X → PermSet.FinsuppFunction 𝔸 𝔸 X :=
  fun p ↦ ⟨abs'' 𝔸 p, by
    use NominalSet.supp 𝔸 p; constructor
    · apply Function.Equivariant.preserve_support
      apply NominalSet.supp_is_support
    · apply NominalSet.supp_finite⟩

private lemma abs_req2 {a : 𝔸} {x : X} : Req2 𝔸 (abs' 𝔸 (⟪a⟫ x)) := by
  intro b c hcfresh hcb
  have hinf : (NominalSet.supp 𝔸 x ∪ {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 hdx : d # x := 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⸩ • x) ∪ NominalSet.supp 𝔸 (abs' 𝔸 (⟪a⟫ x)) ∪ {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 hex : e # (⸨a, d⸩ • x) := he.left.left.left
  have hefresh : e # abs' 𝔸 (⟪a⟫ x) := he.left.left.right
  have heb : e ≠ b := he.left.right
  have hed : e ≠ d := he.right
  rw [choose_restriction' 𝔸 (abs' 𝔸 (⟪a⟫ x)) b b _ _ hcfresh hefresh hcb heb hcb heb]
  simp only [abs', abs'', Quotient.lift_mk, PermSet.Finsupp.smul_val, PermSet.smul_function,
    FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left]
  have ⟨hdx₁, hda₁, hdb₁⟩ := chooseFresh_fresh 𝔸 x a b
  have ⟨hdx₂, hda₂, hde₂⟩ := chooseFresh_fresh 𝔸 x a e
  rw [abs_choice 𝔸 _ _ hdx₁ hdx hda₁ hda hdb₁ hdb]
  rw [abs_choice 𝔸 _ _ hdx₂ hdx hda₂ hda hde₂ (Ne.symm hed)]
  nth_rw 1 [show e = ⸨b,e⸩ • b by simp]
  rw [← AlgebraStructure.res_equivariant]
  nth_rw 6 [← show ⸨e,d⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm heb) (Ne.symm hdb)]
  rw [← AlgebraStructure.res_equivariant]
  rw [← MulAction.mul_smul]
  rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne hdb (Ne.symm hed)]
  rw [MulAction.mul_smul]
  rw [show ⸨b,e⸩ • (b \ (e \ (⸨a,d⸩ • x))) = (b \ (e \ (⸨a,d⸩ • x))) by
    apply NominalSet.fresh_swap_fix
    · show b # AlgebraStructure.res.toFun (⟪b⟫ AlgebraStructure.res (⟪e⟫ ⸨a,d⸩ • x))
      apply Function.Equivariant.preserve_fresh
      rw [NameAbstraction.fresh]; right; rfl
    · show e # AlgebraStructure.res.toFun (⟪b⟫ AlgebraStructure.res (⟪e⟫ ⸨a,d⸩ • x))
      apply Function.Equivariant.preserve_fresh
      rw [NameAbstraction.fresh]; left
      show e # AlgebraStructure.res.toFun (⟪e⟫ ⸨a,d⸩ • x)
      apply Function.Equivariant.preserve_fresh
      rw [NameAbstraction.fresh]; right; rfl]
  rw [AlgebraStructure.ax_swap]
  nth_rw 3 [AlgebraStructure.res_equivariant]
  rw [show ⸨b,d⸩ • e = e from FPerm.swap_apply_of_ne_of_ne heb hed]
  apply AlgebraStructure.ax_redundant

noncomputable def abs : NameAbstraction 𝔸 X → StepModel 𝔸 X :=
  fun p ↦ ⟨abs' 𝔸 p, by
    suffices ∀ p, Req2 𝔸 (abs' 𝔸 p) by apply this
    apply Quotient.ind; intro ⟨a, x⟩
    apply abs_req2⟩

instance : Function.Equivariant 𝔸 (abs 𝔸 : NameAbstraction 𝔸 X → StepModel 𝔸 X) := by
  constructor; intro x π
  apply Subtype.eq; apply Subtype.eq
  simp only [abs, abs', smul_val, PermSet.Finsupp.smul_val]
  rw [← Function.equivariant]

lemma abs_eq' {a : 𝔸} {x : X} {b : 𝔸} :
    (abs 𝔸 (⟪a⟫ x)).val.val b = ⸨b,chooseFresh 𝔸 x a b⸩ • (b \ ⸨a,chooseFresh 𝔸 x a b⸩ • x) := rfl

lemma abs_eq {a : 𝔸} {x : X} {b : 𝔸} :
    ∀ c, c # x → c ≠ a → c ≠ b →
      (abs 𝔸 (⟪a⟫ x)).val.val b = ⸨b,c⸩ • (b \ ⸨a,c⸩ • x) := by
  intro d hdx hda hdb
  have ⟨hcx, hca, hcb⟩ := chooseFresh_fresh 𝔸 x a b
  apply abs_choice 𝔸 _ _ hcx hdx hca hda hcb hdb

private def pre'' : (𝔸 × X) → 𝔸 → X :=
  fun (a, x) ↦
    fun b ↦ if b = a then x else ⊥[𝔸]

instance : Function.Equivariant 𝔸 (pre'' 𝔸 : (𝔸 × X) → 𝔸 → X) := by
  constructor; intro (a, x) π; ext b
  simp only [Prod.smul_mk, PermSet.smul_function]
  by_cases heq : b = π • a
  · rw [heq]; simp [pre'']
  · have hne : π⁻¹ • b ≠ a := by
      intro hcontra
      rw [← hcontra] at heq
      simp at heq
    simp [pre'', heq, hne, AlgebraStructure.bot_equivariant]

private noncomputable def pre' : (𝔸 × X) → PermSet.FinsuppFunction 𝔸 𝔸 X :=
  fun p ↦ ⟨pre'' 𝔸 p, by
    use NominalSet.supp 𝔸 p; constructor
    · apply Function.Equivariant.preserve_support
      apply NominalSet.supp_is_support
    · apply NominalSet.supp_finite⟩

private lemma pre_req2 {a : 𝔸} {x : X} : Req2 𝔸 (pre' 𝔸 (a, x)) := by
  intro b c hcpre hcb
  have hinf : (NominalSet.supp 𝔸 (pre' 𝔸 (a, x)) ∪ {a} ∪ {b})ᶜ.Infinite := by
    apply Set.Finite.infinite_compl
    rw [Set.finite_union, Set.finite_union]
    constructor
    · constructor
      · apply NominalSet.supp_finite
      · 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 hdpre : d # pre' 𝔸 (a, x) := hd.left.left
  have hda : d ≠ a := hd.left.right
  have hdb : d ≠ b := hd.right
  rw [choose_restriction' 𝔸 _ _ _ _ _ hcpre hdpre hcb hdb hcb hdb]
  simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left]
  rw [show (pre' 𝔸 (a, x)).val d = ⊥[𝔸] by simp [pre', pre'', hda]]
  rw [AlgebraStructure.bot_equivariant]
  rw [AlgebraStructure.res_bot]
  rw [AlgebraStructure.ax_neutral]

noncomputable def pre : (𝔸 × X )→ StepModel 𝔸 X :=
  fun p ↦ ⟨pre' 𝔸 p, by
    suffices ∀ p, Req2 𝔸 (pre' 𝔸 p) by apply this
    intro ⟨a, x⟩
    apply pre_req2⟩

instance : Function.Equivariant 𝔸 (pre 𝔸 : (𝔸 × X) → StepModel 𝔸 X) := by
  constructor; intro x π
  apply Subtype.eq; apply Subtype.eq
  simp only [pre, pre', smul_val, PermSet.Finsupp.smul_val]
  rw [← Function.equivariant]

@[simp] lemma pre_eq_if_eq {a : 𝔸} {x : X} : (pre 𝔸 (a, x)).val.val a = x := by
  simp [pre, pre', pre'']

lemma pre_eq_if_ne {a b : 𝔸} {x : X} : a ≠ b → (pre 𝔸 (a, x)).val.val b = ⊥[𝔸] := by
  intro hne
  simp [pre, pre', pre'', Ne.symm hne]

noncomputable instance : Depth1AlgebraStructure 𝔸 (StepModel 𝔸 X) X where
  pre := ⟨pre 𝔸, inferInstance⟩
  abs := ⟨abs 𝔸, inferInstance⟩
  ax_pre_distributive a x y := by
    show pre 𝔸 (a, x ∨[𝔸] y) = union 𝔸 (pre 𝔸 (a, x), pre 𝔸 (a, y))
    apply Subtype.eq; apply Subtype.eq; ext b
    by_cases heq : b = a
    · rw [heq, pre_eq_if_eq, union_eq, pre_eq_if_eq, pre_eq_if_eq]
    · rw [union_eq]
      rw [pre_eq_if_ne 𝔸 (Ne.symm heq)]
      rw [pre_eq_if_ne 𝔸 (Ne.symm heq)]
      rw [pre_eq_if_ne 𝔸 (Ne.symm heq)]
      rw [AlgebraStructure.ax_idempotent]
  ax_pre_bot a := by
    show pre 𝔸 (a, ⊥[𝔸]) = bot 𝔸 ()
    apply Subtype.eq; apply Subtype.eq; ext b
    by_cases heq : b = a
    · rw [heq, pre_eq_if_eq, bot_eq]
    · rw [pre_eq_if_ne 𝔸 (Ne.symm heq), bot_eq]
  ax_pre_restrict_self a x := by
    show restrict 𝔸 (⟪a⟫ pre 𝔸 (a, x)) = bot 𝔸 ()
    apply Subtype.eq; apply Subtype.eq; ext b
    simp only [restrict_eq', PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv,
      bot_eq]
    let c := chooseFresh 𝔸 (pre 𝔸 (a, x)) a b
    have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 (pre 𝔸 (a, x)) a b
    have hne : ⸨a,chooseFresh 𝔸 (pre 𝔸 (a, x)) a b⸩ • b ≠ a := by
      by_cases heq : b = a
      · nth_rw 2 [heq]
        simp only [PermSet.atom_swap, Equiv.swap_apply_left]
        exact hca
      · rw [show ⸨a,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne heq (Ne.symm hcb)]
        exact heq
    rw [pre_eq_if_ne 𝔸 (Ne.symm hne)]
    rw [AlgebraStructure.bot_equivariant]
    rw [AlgebraStructure.res_bot]
  ax_pre_restrict_other a b x := by
    intro hne
    show restrict 𝔸 (⟪a⟫ pre 𝔸 (b, x)) = pre 𝔸 (b, a \ x)
    apply Subtype.eq; apply Subtype.eq; ext l
    have hinf : (NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 (pre 𝔸 (b, x)) ∪ {a} ∪ {b} ∪ {l})ᶜ.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 hcx : c # x := hc.left.left.left.left
    have hcpre : c # pre 𝔸 (b, x) := hc.left.left.left.right
    have hca : c ≠ a := hc.left.left.right
    have hcb : c ≠ b := hc.left.right
    have hcl : c ≠ l := hc.right
    have hcres : c # (a \ x) := by
      show c # AlgebraStructure.res.toFun (⟪a⟫ x)
      apply Function.Equivariant.preserve_fresh
      rw [NameAbstraction.fresh]; left; exact hcx
    rw [restrict_eq 𝔸 c hcpre hca hcl]
    simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv]
    by_cases heq : l = b
    · rw [heq]
      rw [show ⸨a,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hne) (Ne.symm hcb)]
      rw [pre_eq_if_eq, pre_eq_if_eq]
      nth_rw 1 [← show ⸨a, c⸩ • a = c by simp]
      rw [← AlgebraStructure.res_equivariant]
      rw [NominalSet.fresh_swap_fix 𝔸 (AlgebraStructure.res_fresh 𝔸) hcres]
    · have hne : ⸨a,c⸩ • l ≠ b := by
        by_cases heq' : l = a
        · simp [heq', hcb]
        · rw [show ⸨a,c⸩ • l = l from FPerm.swap_apply_of_ne_of_ne heq' (Ne.symm hcl)]
          exact heq
      rw [pre_eq_if_ne 𝔸 (Ne.symm hne)]
      rw [pre_eq_if_ne 𝔸 (Ne.symm heq)]
      rw [AlgebraStructure.bot_equivariant]
      rw [AlgebraStructure.res_bot]
  ax_abs_distributive a x y := by
    show abs 𝔸 (⟪a⟫ x ∨[𝔸] y) = union 𝔸 (abs 𝔸 (⟪a⟫ x), abs 𝔸 (⟪a⟫ y))
    apply Subtype.eq; apply Subtype.eq; ext b
    have hinf : (NominalSet.supp 𝔸 (x ∨[𝔸] y) ∪ NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 y ∪ {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 NominalSet.supp_finite
        · 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 hcxy : c # (x ∨[𝔸] y) := hc.left.left.left.left
    have hcx : c # x := hc.left.left.left.right
    have hcy : c # y := hc.left.left.right
    have hca : c ≠ a := hc.left.right
    have hcb : c ≠ b := hc.right
    rw [abs_eq 𝔸 c hcxy hca hcb]
    rw [union_eq]
    rw [abs_eq 𝔸 c hcx hca hcb]
    rw [abs_eq 𝔸 c hcy hca hcb]
    rw [AlgebraStructure.join_equivariant]
    rw [AlgebraStructure.ax_distributive]
    rw [← AlgebraStructure.join_equivariant]
  ax_abs_bot a := by
    show abs 𝔸 (⟪a⟫ ⊥[𝔸]) = bot 𝔸 ()
    apply Subtype.eq; apply Subtype.eq; ext b
    rw [abs_eq', bot_eq]
    rw [AlgebraStructure.bot_equivariant]
    rw [AlgebraStructure.res_bot]
    rw [AlgebraStructure.bot_equivariant]
  ax_abs_restrict_other a b x := by
    intro hne
    show abs 𝔸 (⟪a⟫ (b \ x)) = restrict 𝔸 (⟪b⟫ abs 𝔸 (⟪a⟫ x))
    apply Subtype.eq; apply Subtype.eq; ext l
    by_cases heq : l = b
    · rw [heq]
      have hinf : (NominalSet.supp 𝔸 x ∪ {a} ∪ {b})ᶜ.Infinite := by
        apply Set.Finite.infinite_compl
        rw [Set.finite_union, Set.finite_union]
        constructor
        · constructor
          · apply NominalSet.supp_finite
          · 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 hcx : c # x := hc.left.left
      have hcres : c # b \ x := by
        show c # AlgebraStructure.res.toFun (⟪b⟫ x)
        apply Function.Equivariant.preserve_fresh
        rw [NameAbstraction.fresh]; left; exact hcx
      have hcabs : c # abs 𝔸 (⟪a⟫ x) := by
        apply Function.Equivariant.preserve_fresh
        rw [NameAbstraction.fresh]; left; exact hcx
      have hca : c ≠ a := hc.left.right
      have hcb : c ≠ b := hc.right
      have hinf' : (NominalSet.supp 𝔸 x ∪ {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 hdx : d # x := hd.left.left.left
      have hdres : d # b \ x := by
        show d # AlgebraStructure.res.toFun (⟪b⟫ x)
        apply Function.Equivariant.preserve_fresh
        rw [NameAbstraction.fresh]; left; exact hdx
      have hda : d ≠ a := hd.left.left.right
      have hdb : d ≠ b := hd.left.right
      have hdc : d ≠ c := hd.right
      rw [abs_eq 𝔸 c hcres hca hcb]
      nth_rw 2 [← show ⸨a,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hne) (Ne.symm hcb)]
      rw [← AlgebraStructure.res_equivariant]
      rw [← MulAction.mul_smul]
      rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne hne (Ne.symm hca)]
      rw [MulAction.mul_smul]
      rw [AlgebraStructure.res_self]
      rw [NominalSet.fresh_swap_fix 𝔸 (AlgebraStructure.res_fresh 𝔸) hcres]
      rw [restrict_eq 𝔸 c hcabs hcb hcb]
      simp only [PermSet.atom_swap, Equiv.swap_apply_left, PermSet.Finsupp.smul_val,
        PermSet.smul_function, FPerm.swap_inv]
      nth_rw 1 [← show ⸨b, c⸩ • b = c by simp]
      rw [← AlgebraStructure.res_equivariant]
      rw [abs_eq 𝔸 d hdx hda hdc]
      nth_rw 4 [← show ⸨c, d⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hcb) (Ne.symm hdb)]
      rw [← AlgebraStructure.res_equivariant]
      nth_rw 3 [← show ⸨a, d⸩ • c = c from FPerm.swap_apply_of_ne_of_ne hca (Ne.symm hdc)]
      rw [← AlgebraStructure.res_equivariant]
      rw [show (c \ x) = x from AlgebraStructure.ax_fresh c x hcx]
      nth_rw 4 [← show ⸨a, d⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hne) (Ne.symm hdb)]
      rw [← AlgebraStructure.res_equivariant]
      nth_rw 2 [← MulAction.mul_smul]
      rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne (Ne.symm hca) (Ne.symm hda)]
      rw [MulAction.mul_smul]
      rw [NominalSet.fresh_swap_fix 𝔸 hcres hdres]
      rw [← MulAction.mul_smul]
      rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne hne (Ne.symm hca)]
      rw [MulAction.mul_smul]
      rw [NominalSet.fresh_swap_fix 𝔸 (AlgebraStructure.res_fresh 𝔸) hcres]
    · rw [restrict_fresh 𝔸 _ _ _ (Ne.symm heq)]
      have hinf : (NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 (b \ x) ∪ {a} ∪ {b} ∪ {l})ᶜ.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 hcx : c # x := hc.left.left.left.left
      have hcx' : c # (b \ x) := hc.left.left.left.right
      have hca : c ≠ a := hc.left.left.right
      have hcb : c ≠ b := hc.left.right
      have hcl : c ≠ l := hc.right
      rw [abs_eq 𝔸 c hcx' hca hcl]
      rw [abs_eq 𝔸 c hcx hca hcl]
      nth_rw 2 [AlgebraStructure.res_equivariant]
      rw [show ⸨a,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hne) (Ne.symm hcb)]
      nth_rw 2 [← show ⸨l,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm heq) (Ne.symm hcb)]
      rw [← AlgebraStructure.res_equivariant]
      rw [AlgebraStructure.ax_swap]
  ax_local a x := by
    show abs 𝔸 (⟪a⟫ x) = union 𝔸 (abs 𝔸 (⟪a⟫ x), pre 𝔸 (a, x))
    apply Subtype.eq; apply Subtype.eq; ext b
    by_cases heq : b = a
    · rw [heq, union_eq, pre_eq_if_eq]
      have ⟨hx, _, _⟩ := chooseFresh_fresh 𝔸 x a a
      rw [abs_eq']
      rw [AlgebraStructure.res_equivariant]
      rw [PermSet.atom_swap, Equiv.swap_apply_left]
      rw [← MulAction.mul_smul, FPerm.swap_mul_self, MulAction.one_smul]
      rw [AlgebraStructure.ax_fresh _ x hx]
      rw [AlgebraStructure.ax_idempotent]
    · rw [union_eq, pre_eq_if_ne 𝔸 (Ne.symm heq)]
      rw [AlgebraStructure.ax_neutral]

end StepModel

private noncomputable def ModelBundle (X : Type) [NominalSet 𝔸 X] : ℕ → ((T : Type) × ((_ : NominalSet 𝔸 T) × AlgebraStructure 𝔸 T))
| 0 => ⟨BaseModel 𝔸 X, inferInstance, inferInstance⟩
| n + 1 =>
  let ⟨Y, _, _⟩ := ModelBundle X n
  ⟨StepModel 𝔸 Y, inferInstance, inferInstance⟩

def Model (X : Type) [NominalSet 𝔸 X] (n : ℕ) := (ModelBundle 𝔸 X n).fst

namespace Model

variable {X : Type} [NominalSet 𝔸 X] {n : ℕ}

noncomputable instance : NominalSet 𝔸 (Model 𝔸 X n) := (ModelBundle 𝔸 X n).snd.fst
noncomputable instance : AlgebraStructure 𝔸 (Model 𝔸 X n) := (ModelBundle 𝔸 X n).snd.snd

end Model