Minor progress

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

ConNF/Construction/MainInduction.lean

@@ -110,6 +110,25 @@ def liftCastDataLe (α : Λ) (M : (β : Λ) → β < α → Motive β)
     haveI : LtLevel β := ⟨LeLevel.elim.lt_of_ne h⟩
     cast (by rw [castData_eq_of_lt]) (fβ)
 
+theorem liftCastDataLe_eq_of_eq (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    {D : (β : TypeIndex) → ModelData β → Type _}
+    (fβ : letI : Level := ⟨α⟩; [LtLevel α] → D α ((ltData α M).data α))
+    (fα : D α (newModelData' α M)) :
+    letI : Level := ⟨α⟩; letI : LeLevel α := ⟨le_rfl⟩
+    liftCastDataLe α M α fβ fα = cast (by rw [castData_eq_of_eq]) fα := by
+  rw [liftCastDataLe, dif_pos rfl]
+
+theorem liftCastDataLe_eq_of_lt (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    {D : (β : TypeIndex) → ModelData β → Type _} (β : TypeIndex)
+    (fβ : letI : Level := ⟨α⟩; [LtLevel β] → D β ((ltData α M).data β))
+    (fα : D α (newModelData' α M))
+    [letI : Level := ⟨α⟩; LtLevel β] :
+    liftCastDataLe α M β fβ fα = cast (by rw [castData_eq_of_lt]) fβ := by
+  rw [liftCastDataLe, dif_neg]
+  rintro rfl
+  letI : Level := ⟨α⟩
+  exact LtLevel.elim.ne rfl
+
 def leData (α : Λ) (M : (β : Λ) → β < α → Motive β) :
     letI : Level := ⟨α⟩; LeData :=
   letI : Level := ⟨α⟩
@@ -119,6 +138,50 @@ def leData (α : Λ) (M : (β : Λ) → β < α → Motive β) :
       (D := λ β (x : ModelData β) ↦ Position (@Tangle _ β x)) (ltData α M).positions
   LeData.mk (data := data) (positions := positions)
 
+theorem leData_tangle_α (α : Λ) (M : (β : Λ) → β < α → Motive β) :
+    letI : Level := ⟨α⟩; letI : LeLevel α := ⟨le_rfl⟩
+    (letI := leData α M; Tangle α) = (letI := newModelData' α M; Tangle α) := by
+  simp only [leData, instModelDataOfLeDataOfLeLevel, castData_eq_of_eq]
+
+def leDataTangleα (α : Λ) (M : (β : Λ) → β < α → Motive β) :
+    letI : Level := ⟨α⟩; letI : LeLevel α := ⟨le_rfl⟩
+    (letI := leData α M; Tangle α) ≃ (letI := newModelData' α M; Tangle α) :=
+  Equiv.cast (by simp only [leData, instModelDataOfLeDataOfLeLevel, castData_eq_of_eq])
+
+theorem leData_tangle_lt (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    (β : TypeIndex) [letI : Level := ⟨α⟩; LtLevel β] :
+    letI : Level := ⟨α⟩
+    (letI := leData α M; Tangle β) = (letI := ltData α M; Tangle β) := by
+  simp only [leData, instModelDataOfLeDataOfLeLevel, castData_eq_of_lt]
+
+def leDataTangleLt (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    (β : TypeIndex) [letI : Level := ⟨α⟩; LtLevel β] :
+    letI : Level := ⟨α⟩
+    (letI := leData α M; Tangle β) ≃ (letI := ltData α M; Tangle β) :=
+  Equiv.cast (leData_tangle_lt α M β)
+
+theorem leData_allPerm_α (α : Λ) (M : (β : Λ) → β < α → Motive β) :
+    letI : Level := ⟨α⟩; letI : LeLevel α := ⟨le_rfl⟩
+    (letI := leData α M; AllPerm α) = (letI := newModelData' α M; AllPerm α) := by
+  simp only [leData, instModelDataOfLeDataOfLeLevel, castData_eq_of_eq]
+
+def leDataAllPermα (α : Λ) (M : (β : Λ) → β < α → Motive β) :
+    letI : Level := ⟨α⟩; letI : LeLevel α := ⟨le_rfl⟩
+    (letI := leData α M; AllPerm α) ≃ (letI := newModelData' α M; AllPerm α) :=
+  Equiv.cast (leData_allPerm_α α M)
+
+theorem leData_allPerm_lt (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    (β : TypeIndex) [letI : Level := ⟨α⟩; LtLevel β] :
+    letI : Level := ⟨α⟩
+    (letI := leData α M; AllPerm β) = (letI := ltData α M; AllPerm β) := by
+  simp only [leData, instModelDataOfLeDataOfLeLevel, castData_eq_of_lt]
+
+def leDataAllPermLt (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    (β : TypeIndex) [letI : Level := ⟨α⟩; LtLevel β] :
+    letI : Level := ⟨α⟩
+    (letI := leData α M; AllPerm β) ≃ (letI := ltData α M; AllPerm β) :=
+  Equiv.cast (leData_allPerm_lt α M β)
+
 def preCoherentData (α : Λ) (M : (β : Λ) → β < α → Motive β)
     (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) :
     letI : Level := ⟨α⟩; PreCoherentData :=
@@ -157,30 +220,54 @@ def preCoherentData (α : Λ) (M : (β : Λ) → β < α → Motive β)
       (λ h' ↦ (LeLevel.elim.not_lt h').elim) hγ x
   }
 
+theorem preCoherentData_allPermSderiv_coe_coe
+    (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h))
+    {β γ : Λ} [letI : Level := ⟨α⟩; LtLevel β] [letI : Level := ⟨α⟩; LtLevel γ]
+    (h : (γ : TypeIndex) < β) (ρ : letI : Level := ⟨α⟩; letI := leData α M; AllPerm β) :
+    letI : Level := ⟨α⟩
+    (preCoherentData α M H).allPermSderiv h ρ = (leDataAllPermLt α M γ).symm
+      ((H β (WithBot.coe_lt_coe.mp LtLevel.elim)).allPermSderiv (WithBot.coe_lt_coe.mp h)
+        (leDataAllPermLt α M β ρ)) := by
+  unfold PreCoherentData.allPermSderiv preCoherentData
+  simp only [WithBot.recBotCoe_coe, liftCastDataLe_eq_of_lt, leDataAllPermLt, Equiv.cast_symm,
+    Equiv.cast_apply]
+  sorry
+
+theorem preCoherentData_allPermSderiv_forget
+    (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h))
+    {β γ : TypeIndex} [letI : Level := ⟨α⟩; LeLevel β] [letI : Level := ⟨α⟩; LeLevel γ]
+    (h : γ < β) (ρ : letI : Level := ⟨α⟩; letI := leData α M; AllPerm β) :
+    ((preCoherentData α M H).allPermSderiv h ρ)ᵁ = ((leData α M).data β).allPermForget ρ ↘ h := by
+  sorry
+
 def coherentData
     (α : Λ) (M : (β : Λ) → β < α → Motive β)
     (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) :
     letI : Level := ⟨α⟩; CoherentData :=
   letI : Level := ⟨α⟩
   letI := preCoherentData α M H
-  ⟨sorry, sorry, sorry, sorry, sorry, sorry, sorry, sorry⟩
+  {
+    allPermSderiv_forget := preCoherentData_allPermSderiv_forget α M H
+    pos_atom_lt_pos := sorry
+    pos_nearLitter_lt_pos := sorry
+    smul_fuzz := sorry
+    allPerm_of_basePerm := sorry
+    allPerm_of_smulFuzz := sorry
+    tSet_ext := sorry
+    typedMem_singleton_iff := sorry
+  }
 
-theorem construct_tangle_le_μ' (α : Λ) (M : (β : Λ) → β < α → Motive β)
+theorem construct_tangle_le_μ (α : Λ) (M : (β : Λ) → β < α → Motive β)
     (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) :
-    letI : Level := ⟨α⟩
-    letI : LeLevel α := ⟨le_rfl⟩
-    letI := coherentData α M H
-    #(Tangle α) ≤ #μ :=
+    letI := newModelData' α M
+    #(Tangle α) ≤ #μ := by
+  rw [← leData_tangle_α]
   letI : Level := ⟨α⟩
   letI : LeLevel α := ⟨le_rfl⟩
   letI := coherentData α M H
-  card_tangle_le α
-
-theorem construct_tangle_le_μ (α : Λ) (M : (β : Λ) → β < α → Motive β)
-    (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) :
-    letI := newModelData' α M
-    #(Tangle α) ≤ #μ :=
-  sorry
+  exact card_tangle_le α
 
 def constructMotive (α : Λ) (M : (β : Λ) → β < α → Motive β)
     (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) :