Restructure support_inter proof

1 files changed, 84 insertions, 99 deletions

diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index 7875ad3..6a1d4d9 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -50,115 +50,100 @@ lemma support_superset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆
 
 /-- For two finite supports, the intersection is also a support. -/
 lemma support_inter [Infinite 𝔸] {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite → HasSupport 𝔸 x T → T.Finite → HasSupport 𝔸 x (S ∩ T) := by
-  intro hsuppS hfinS hsuppT hfinT π hfixπ
-  have h_cod_inf : ((π.val.supp ∪ S ∪ T)ᶜ).Infinite := by
+  intro h_S_support h_S_finite h_T_support h_T_finite π h_π_fix
+  let π' := π.val
+  let h_π_fin := π.prop
+
+  -- First we obtain an injection m : S \ T → (π'.supp ∪ S ∪ T)ᶜ.
+  have h_cod_inf : ((π'.supp ∪ S ∪ T)ᶜ).Infinite := by
     apply Set.Finite.infinite_compl
-    simp; exact ⟨⟨π.val_prop, hfinS⟩, hfinT⟩
-  have h_dom_fin : (S \ T).Finite := Set.Finite.diff hfinS
-  have hle : (S \ T).encard ≤ ((π.val.supp ∪ S ∪ T)ᶜ).encard := by
-    rw [Set.Infinite.encard_eq h_cod_inf, Set.Finite.encard_eq_coe h_dom_fin]
-    simp
-  obtain ⟨σ, ⟨hpreσ, hinjσ⟩⟩ := Set.Finite.exists_injOn_of_encard_le h_dom_fin hle
-  have himσ {a : 𝔸} : a ∈ S \ T → σ a ∉ S \ T := by
-    intro ha
-    suffices : σ a ∈ (π.val.supp ∪ S ∪ T)ᶜ
-    · have h : S \ T ⊆ π.val.supp ∪ S ∪ T := by calc
-          S \ T ⊆ S                  := Set.diff_subset
-          _     ⊆ π.val.supp ∪ S     := Set.subset_union_right
-          _     ⊆ π.val.supp ∪ S ∪ T := Set.subset_union_left
-      exact Set.notMem_subset h (hpreσ ha)
-    · rw [← Set.image_subset_iff] at hpreσ
-      exact hpreσ (Set.mem_image_of_mem σ ha)
-  have himσ' {a : 𝔸} : a ∈ S \ T → σ a ∉ π.val.supp := by
-    intro ha
-    suffices : σ a ∈ (π.val.supp ∪ S ∪ T)ᶜ
-    · have h : π.val.supp ⊆ π.val.supp ∪ S ∪ T := by calc
-          π.val.supp ⊆ π.val.supp ∪ S     := Set.subset_union_left
-          _          ⊆ π.val.supp ∪ S ∪ T := Set.subset_union_left
-      exact Set.notMem_subset h (hpreσ ha)
-    · rw [← Set.image_subset_iff] at hpreσ
-      exact hpreσ (Set.mem_image_of_mem σ ha)
-  rw [Set.injOn_iff_injective] at hinjσ
-  obtain hσinv := Function.partialInv_of_injective hinjσ
+    simp; exact ⟨⟨h_π_fin, h_S_finite⟩, h_T_finite⟩
+  have h_dom_fin : (S \ T).Finite :=
+    Set.Finite.diff h_S_finite
+
+  obtain ⟨m, ⟨h_m_preimage, h_m_injective⟩⟩ :=
+    Set.Finite.exists_injOn_of_encard_le h_dom_fin (by
+      rw [Set.Infinite.encard_eq h_cod_inf, Set.Finite.encard_eq_coe h_dom_fin]
+      simp)
+  let m' := (S \ T).restrict m
+  rw [Set.injOn_iff_injective, show (S \ T).restrict m = m' by rfl] at h_m_injective
+  obtain h_m_inv := Function.partialInv_of_injective h_m_injective
+  have h_m_image : m '' (S \ T) ⊆ (π'.supp ∪ S ∪ T)ᶜ :=
+    Set.image_subset_iff.mpr h_m_preimage
+
+  -- Show some trivial statements about subsets of (π'.supp ∪ S ∪ T), i.e. the atoms excluded from the image of m.
+  have h_sub_π   : π'.supp ⊆ (π'.supp ∪ S ∪ T) := Set.subset_union_of_subset_left Set.subset_union_left T
+  have h_sub_S   : S       ⊆ (π'.supp ∪ S ∪ T) := Set.subset_union_of_subset_left Set.subset_union_right T
+  have h_sub_T   : T       ⊆ (π'.supp ∪ S ∪ T) := Set.subset_union_right
+  have h_sub_dom : (S \ T) ⊆ (π'.supp ∪ S ∪ T) := by trans; exact Set.diff_subset; exact h_sub_S
+  have h_m_image_notIn_sub {U : Set 𝔸} (h_sub_U : U ⊆ π'.supp ∪ S ∪ T) {a : 𝔸} (h_a_dom : a ∈ S \ T) : m a ∉ U := by
+    suffices m a ∈ (π'.supp ∪ S ∪ T)ᶜ by
+      exact Set.notMem_subset h_sub_U (h_m_preimage h_a_dom)
+    exact h_m_image (Set.mem_image_of_mem m h_a_dom)
+
+  -- Next, extend m to a new permutation σ, about which we will then prove some properties.
   have {a : 𝔸} : Decidable (a ∈ S \ T) := Classical.propDecidable (a ∈ S \ T)
-  let τ : 𝔸 → 𝔸 := fun a =>
-    if h : a ∈ S \ T then (S \ T).restrict σ ⟨a, h⟩
-    else if let .some b := ((S \ T).restrict σ).partialInv a then b
+  let σ' : 𝔸 → 𝔸 := fun a =>
+    if h : a ∈ S \ T then m' ⟨a, h⟩
+    else if let .some b := m'.partialInv a then b
     else a
-  have hselfinvτ : ∀ a, τ (τ a) = a := by
+
+  -- First, σ is self-inverse and finitely supported, making it an element of FPerm 𝔸.
+  have h_σ_involutive : Function.Involutive σ' := by
     intro a
     by_cases h₁ : a ∈ S \ T
-    · have h₂ : ((S \ T).restrict σ).partialInv (((S \ T).restrict σ) ⟨a, h₁⟩) = .some ⟨a, h₁⟩ :=
-        Function.partialInv_left hinjσ ⟨a, h₁⟩
-      simp at h₂
-      simp [τ, h₁, himσ h₁, h₂]
-    · cases h₂ : ((S \ T).restrict σ).partialInv a with
-      | some b => simp [τ, h₂, h₁]
-                  rwa [← Set.restrict_apply σ (S \ T) b, ← hσinv]
-      | none   => simp [τ, h₂, h₁]
-  have hfinsuppτ : {a | τ a ≠ a}.Finite := by
+    · have h := Function.partialInv_left h_m_injective ⟨a, h₁⟩
+      simp [σ', m', h₁, h_m_image_notIn_sub h_sub_dom h₁, h] at *
+    · cases h₂ : m'.partialInv a with
+      | some b => simp [σ', h₂, h₁]; rwa [← h_m_inv]
+      | none   => simp [σ', h₂, h₁]
+  have h_σ_simple_case (a : 𝔸) (h₁ : a ∉ S \ T) (h₂ : a ∉ m '' (S \ T)) : σ' a = a := by
+    cases h : m'.partialInv a with
+    | some b => rw [h_m_inv] at h
+                have : a ∈ (m '' (S \ T)) := by rw [← h, Set.mem_image]; use b; simp [m']
+                contradiction
+    | none   => simp [σ', h₁, h]
+  have h_σ_fin : {a | σ' a ≠ a}.Finite := by
     apply Set.Finite.subset
-    · exact Set.finite_union.mpr ⟨h_dom_fin, Set.Finite.image σ h_dom_fin⟩
+    · exact Set.finite_union.mpr ⟨h_dom_fin, Set.Finite.image m h_dom_fin⟩
     · intro a ha₁; by_contra ha₂
       rw [← Set.mem_compl_iff, Set.compl_union, Set.mem_inter_iff] at ha₂
-      suffices τ a = a by contradiction
-      have ha₃ : a ∉ S \ T := by rw [← Set.mem_compl_iff]; exact ha₂.left
-      cases ha₄ : ((S \ T).restrict σ).partialInv a with
-      | some b => rw [hσinv, Set.restrict_apply] at ha₄
-                  have : a ∈ (σ '' (S \ T)) := by rw [← ha₄, Set.mem_image]; use b; simp
-                  have : a ∉ (σ '' (S \ T)) := Set.notMem_of_mem_diff ha₂
-                  contradiction
-      | none   => simp [τ, ha₃, ha₄]
-  let τ' : FPerm 𝔸 := ⟨⟨τ, τ, hselfinvτ, hselfinvτ⟩, hfinsuppτ⟩
-  have h₁ : τ' ∈ fix 𝔸 T := by
-    intro a haT; show τ a = a
-    have ha₁ : a ∉ S \ T := Set.notMem_diff_of_mem haT
-    have h₁ : σ '' (S \ T) ⊆ (π.val.supp ∪ S ∪ T)ᶜ := by rwa [Set.image_subset_iff]
-    have h₂ : a ∉ (π.val.supp ∪ S ∪ T)ᶜ := by
-      rw [Set.notMem_compl_iff]
-      apply Set.mem_union_right; assumption
-    cases ha₂ : ((S \ T).restrict σ).partialInv a with
-    | some b => rw [hσinv, Set.restrict_apply] at ha₂
-                have : a ∈ (σ '' (S \ T)) := by rw [← ha₂, Set.mem_image]; use b; simp
-                have : a ∉ (σ '' (S \ T)) := fun x => h₂ (h₁ x)
-                contradiction
-    | none   => simp [τ, ha₁, ha₂]
-  have h₂ : (τ' * π * τ') ∈ fix 𝔸 S := by
-    intro a haS; show τ (π (τ a)) = a
+      suffices σ' a = a by contradiction
+      apply h_σ_simple_case
+      · rw [← Set.mem_compl_iff]; exact ha₂.left
+      · exact Set.notMem_of_mem_diff ha₂
+  let σ : FPerm 𝔸 := ⟨⟨σ', σ', h_σ_involutive, h_σ_involutive⟩, h_σ_fin⟩
+
+  -- Second, σ fixes T and σπσ fixes S.
+  have h_σ_fixT : σ ∈ fix 𝔸 T := by
+    intro a haT; show σ a = a
+    apply h_σ_simple_case
+    · exact Set.notMem_diff_of_mem haT
+    · exact fun h => h_m_image h (h_sub_T haT)
+  have h_σ_fixS : (σ * π * σ) ∈ fix 𝔸 S := by
+    intro a haS; show σ (π (σ a)) = a
     by_cases haT : a ∈ T
-    · have ht : τ a = a := by
-        -- XXX: copied from above
-        have ha₁ : a ∉ S \ T := Set.notMem_diff_of_mem haT
-        have h₁ : σ '' (S \ T) ⊆ (π.val.supp ∪ S ∪ T)ᶜ := by rwa [Set.image_subset_iff]
-        have h₂ : a ∉ (π.val.supp ∪ S ∪ T)ᶜ := by
-          rw [Set.notMem_compl_iff]
-          apply Set.mem_union_right; assumption
-        cases ha₂ : ((S \ T).restrict σ).partialInv a with
-        | some b => rw [hσinv, Set.restrict_apply] at ha₂
-                    have : a ∈ (σ '' (S \ T)) := by rw [← ha₂, Set.mem_image]; use b; simp
-                    have : a ∉ (σ '' (S \ T)) := fun x => h₂ (h₁ x)
-                    contradiction
-        | none   => simp [τ, ha₁, ha₂]
-      calc
-        τ (π (τ a)) = τ (π a)   := by rw [ht]
-        _           = τ (π • a) := rfl
-        _           = τ a       := by rw [hfixπ a (Set.mem_inter haS haT)]
-        _           = a         := by rw [ht]
-    · have h₁ : a ∈ S \ T := Set.mem_diff_of_mem haS haT
-      have h₂ : π (τ a) = τ a := by
-        apply Equiv.Perm.supp_notin
-        rw [show τ a = σ a by simp [τ, h₁]]
-        exact himσ' h₁
-      rw [h₂]
-      exact hselfinvτ a
+    · calc
+        σ (π (σ a)) = σ (π (σ • a)) := rfl
+        _           = σ (π a)       := by rw [h_σ_fixT a haT]
+        _           = σ (π • a)     := rfl
+        _           = σ a           := by rw [h_π_fix a (Set.mem_inter haS haT)]
+        _           = σ • a         := rfl
+        _           = a             := by rw [h_σ_fixT a haT]
+    · suffices π (σ a) = σ a by rw [this]; exact h_σ_involutive a
+      apply Equiv.Perm.supp_notin
+      rw [show σ a = m a by simp [σ, σ', (Set.mem_diff_of_mem haS haT), m']]
+      exact h_m_image_notIn_sub h_sub_π (Set.mem_diff_of_mem haS haT)
+
+  -- Using this carefully constructed σ, we can finally prove the statement.
   calc
-    π • x = (1 * π * 1) • x                     := rfl
-    _     = ((τ' * τ'⁻¹) * π * (τ' * τ'⁻¹)) • x := by rw [@mul_inv_cancel]
-    _     = ((τ' * τ' * π * τ') * τ') • x       := rfl
-    _     = (τ' * τ' * π * τ') • x              := by rw [@mul_smul, hsuppT h₁]
-    _     = (τ' * (τ' * π * τ')) • x            := rfl
-    _     = τ' • x                              := by rw [@mul_smul, hsuppS h₂]
-    _     = x                                   := by rw [hsuppT h₁]
+    π • x = (1 * π * 1) • x                 := rfl
+    _     = ((σ * σ⁻¹) * π * (σ * σ⁻¹)) • x := by rw [@mul_inv_cancel]
+    _     = ((σ * σ * π * σ) * σ) • x       := rfl
+    _     = (σ * σ * π * σ) • x             := by rw [@mul_smul, h_T_support h_σ_fixT]
+    _     = (σ * (σ * π * σ)) • x           := rfl
+    _     = σ • x                           := by rw [@mul_smul, h_S_support h_σ_fixS]
+    _     = x                               := by rw [h_T_support h_σ_fixT]
 
 /-- For a finite number of finite supports, the intersection is also a support. -/
 lemma support_sInter [Infinite 𝔸] {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C) := by