Prove tSet_ext in matin induction

Signed-off-by: zeramorphic <zeramorphic@proton.me>

ConNF/Construction/MainInduction.lean

@@ -82,6 +82,8 @@ structure Hypothesis {α : Λ} (M : Motive α) (N : (β : Λ) → (β : TypeInde
     ∃ ρ : M.data.AllPerm,
       (∀ (β : Λ) (hβ : (β : TypeIndex) < α), allPermSderiv hβ ρ = ρs hβ) ∧
       allPermBotSderiv ρ = π
+  tSet_ext (β : Λ) (hβ : (β : TypeIndex) < α) (x y : M.data.TSet) :
+    (∀ z : (N β hβ).data.TSet, z ∈[hβ] x ↔ z ∈[hβ] y) → x = y
 
 def castTSet {α β : TypeIndex} {D₁ : ModelData α} {D₂ : ModelData β}
     (h₁ : α = β) (h₂ : HEq D₁ D₂) :
@@ -95,6 +97,9 @@ def castTangle {α β : TypeIndex} {D₁ : ModelData α} {D₂ : ModelData β}
     (h₁ : α = β) (h₂ : HEq D₁ D₂) :
     (letI := D₁; Tangle α) ≃ (letI := D₂; Tangle β) := by cases h₁; rw [eq_of_heq h₂]
 
+theorem castTSet_forget {α : TypeIndex} {D₁ D₂ : ModelData α} (h₂ : HEq D₁ D₂) (ρ : D₁.TSet) :
+    D₂.tSetForget (castTSet rfl h₂ ρ) = D₁.tSetForget ρ := by cases h₂; rfl
+
 theorem castAllPerm_forget {α : TypeIndex} {D₁ D₂ : ModelData α} (h₂ : HEq D₁ D₂) (ρ : D₁.AllPerm) :
     D₂.allPermForget (castAllPerm rfl h₂ ρ) = D₁.allPermForget ρ := by cases h₂; rfl
 
@@ -217,6 +222,16 @@ def castTangleLeEq {β : Λ} (hβ : (β : TypeIndex) = α) :
     TangleLe M β hβ.le ≃ (letI := newModelData' M; Tangle α) :=
   castTangle hβ (by cases hβ; exact heq_of_eq <| leData_data_eq M)
 
+theorem castTSetLeLt_forget {β : Λ} (hβ : (β : TypeIndex) < α) (x : TSetLe M β hβ.le) :
+    (M β hβ).data.tSetForget (castTSetLeLt M hβ x) =
+    letI : Level := ⟨α⟩; letI : LeLevel β := ⟨hβ.le⟩; ((leData M).data β).tSetForget x :=
+  castTSet_forget _ _
+
+theorem castTSetLeEq_forget (x : TSetLe M α le_rfl) :
+    (newModelData' M).tSetForget (castTSetLeEq M rfl x) =
+    letI : Level := ⟨α⟩; letI : LeLevel α := ⟨le_rfl⟩; ((leData M).data α).tSetForget x :=
+  castTSet_forget _ _
+
 theorem castAllPermLeLt_forget {β : Λ} (hβ : (β : TypeIndex) < α) (ρ : AllPermLe M β hβ.le) :
     (M β hβ).data.allPermForget (castAllPermLeLt M hβ ρ) =
     letI : Level := ⟨α⟩; letI : LeLevel β := ⟨hβ.le⟩; ((leData M).data β).allPermForget ρ :=
@@ -487,6 +502,41 @@ theorem preCoherentData_allPerm_of_smulFuzz
       rw [← castAllPermLeLt_forget M LtLevel.elim] at this
       exact this
 
+theorem preCoherent_tSet_ext
+    (H : (β : Λ) → (h : (β : TypeIndex) < α) → Hypothesis (M β h) λ γ h' ↦ M γ (h'.trans h))
+    {β γ : Λ}
+    [iβ : letI : Level := ⟨α⟩; LeLevel β] [iγ : letI : Level := ⟨α⟩; LeLevel γ]
+    (hγ : (γ : TypeIndex) < β) (x y : letI : Level := ⟨α⟩; TSetLe M β LeLevel.elim)
+    (hxy : letI : Level := ⟨α⟩; ∀ (z : TSetLe M γ LeLevel.elim), z ∈[hγ] x ↔ z ∈[hγ] y) :
+    x = y := by
+  letI : Level := ⟨α⟩
+  by_cases h : (β : TypeIndex) = α
+  · cases coe_injective h
+    apply (castTSetLeEq M rfl).injective
+    letI : LtLevel γ := ⟨hγ⟩
+    letI := ltData M
+    apply newModelData_ext γ
+    intro z
+    simp only [← TSet.forget_mem_forget] at hxy ⊢
+    convert hxy ((castTSetLeLt M hγ).symm z) using 2
+    · have := castTSetLeLt_forget M hγ ((castTSetLeLt M hγ).symm z)
+      rwa [Equiv.apply_symm_apply] at this
+    · exact castTSetLeEq_forget M x
+    · have := castTSetLeLt_forget M hγ ((castTSetLeLt M hγ).symm z)
+      rwa [Equiv.apply_symm_apply] at this
+    · exact castTSetLeEq_forget M y
+  · apply (castTSetLeLt M (LeLevel.elim.lt_of_ne h)).injective
+    apply (H β _).tSet_ext γ hγ
+    intro z
+    simp only [← TSet.forget_mem_forget] at hxy ⊢
+    convert hxy ((castTSetLeLt M (hγ.trans_le LeLevel.elim)).symm z) using 2
+    · have := castTSetLeLt_forget M (hγ.trans_le LeLevel.elim) ((castTSetLeLt M _).symm z)
+      rwa [Equiv.apply_symm_apply] at this
+    · exact castTSetLeLt_forget M _ x
+    · have := castTSetLeLt_forget M (hγ.trans_le LeLevel.elim) ((castTSetLeLt M _).symm z)
+      rwa [Equiv.apply_symm_apply] at this
+    · exact castTSetLeLt_forget M _ y
+
 def coherentData :
     letI : Level := ⟨α⟩; CoherentData :=
   letI : Level := ⟨α⟩
@@ -498,7 +548,7 @@ def coherentData :
     smul_fuzz := preCoherentData_smul_fuzz M H
     allPerm_of_basePerm := λ π ↦ ⟨π, rfl⟩
     allPerm_of_smulFuzz := preCoherentData_allPerm_of_smulFuzz M H
-    tSet_ext := sorry
+    tSet_ext := preCoherent_tSet_ext M H
     typedMem_singleton_iff := sorry
   }
 
@@ -536,6 +586,7 @@ def constructHypothesis (α : Λ) (M : (β : Λ) → (β : TypeIndex) < α → M
     pos_nearLitter_lt_pos := sorry
     smul_fuzz := sorry
     smul_fuzz_bot := sorry
+    allPerm_of_smul_fuzz := sorry
   }
 
 instance : IsTrans Λ λ β γ ↦ (β : TypeIndex) < (γ : TypeIndex) :=

ConNF/Construction/NewModelData.lean

@@ -403,6 +403,31 @@ def newSingleton {γ : Λ} [LtLevel γ] (x : TSet γ) : NewSet :=
 
 local instance : ModelData α := newModelData
 
+theorem not_mem_none {β : TypeIndex} [LtLevel β] (z : TSet β) :
+    ¬z ∈[LtLevel.elim] (show TSet α from none) := by
+  unfold TypedMem.typedMem instTypedMemTSet
+  change zᵁ ∉ _
+  erw [Equiv.apply_symm_apply]
+  exact id
+
+theorem newModelData_ext (β : Λ) [LtLevel β] (x y : TSet α)
+    (h : ∀ z : TSet β, z ∈[LtLevel.elim] x ↔ z ∈[LtLevel.elim] y) :
+    x = y := by
+  obtain (_ | x) := x <;> obtain (_ | y) := y
+  · rfl
+  · obtain ⟨z, hz⟩ := Code.members_nonempty y.hc β
+    rw [NewSet.mem_members] at hz
+    cases not_mem_none z ((h z).mpr hz)
+  · obtain ⟨z, hz⟩ := Code.members_nonempty x.hc β
+    rw [NewSet.mem_members] at hz
+    cases not_mem_none z ((h z).mp hz)
+  · apply congr_arg some
+    apply NewSet.ext
+    apply Code.ext x.hc y.hc β
+    ext z
+    rw [NewSet.mem_members, NewSet.mem_members]
+    exact h z
+
 def newPositionDeny (t : Tangle α) : Set μ :=
   pos '' {N | t.set = some (newTyped N)} ∪
     pos '' (t.supportᴬ.image Prod.snd : Set Atom) ∪