Finish main induction

Signed-off-by: zeramorphic <[email protected]>

ConNF/Construction/ConstructHypothesis.lean

@@ -42,32 +42,54 @@ def constructSingleton {β : Λ} (h : (β : TypeIndex) < α)
 theorem constructMotive_allPermSderiv_forget {β : Λ} (h : (β : TypeIndex) < α)
     (ρ : (constructMotive α M H).data.AllPerm) :
     (M β h).data.allPermForget (constructAllPermSderiv M H h ρ) =
-    (constructMotive α M H).data.allPermForget ρ ↘ h := sorry
+    (constructMotive α M H).data.allPermForget ρ ↘ h :=
+  letI : Level := ⟨α⟩
+  letI := ltData M
+  letI : LtLevel β := ⟨h⟩
+  (NewPerm.forget_sderiv ρ β).symm
 
 theorem constructMotive_allPermBotSderiv_forget (ρ : (constructMotive α M H).data.AllPerm) :
     botModelData.allPermForget (constructAllPermBotSderiv M H ρ) =
-    (constructMotive α M H).data.allPermForget ρ ↘ bot_lt_coe _ := sorry
+    (constructMotive α M H).data.allPermForget ρ ↘ bot_lt_coe _ :=
+  letI : Level := ⟨α⟩
+  letI := ltData M
+  (NewPerm.forget_sderiv ρ ⊥).symm
 
 theorem constructMotive_pos_atom_lt_pos :
     letI := (constructMotive α M H).data; letI := (constructMotive α M H).pos
-    ∀ (t : Tangle α) (A : α ↝ ⊥) (a : Atom), a ∈ (t.support ⇘. A)ᴬ → pos a < pos t := sorry
+    ∀ (t : Tangle α) (A : α ↝ ⊥) (a : Atom), a ∈ (t.support ⇘. A)ᴬ → pos a < pos t :=
+  letI : Level := ⟨α⟩
+  letI := ltData M
+  λ t A a ↦ pos_atom_lt_newPosition _ t a A
 
 theorem constructMotive_pos_nearLitter_lt_pos :
     letI := (constructMotive α M H).data; letI := (constructMotive α M H).pos
-    ∀ (t : Tangle α) (A : α ↝ ⊥) (M : NearLitter), M ∈ (t.support ⇘. A)ᴺ → pos M < pos t := sorry
+    ∀ (t : Tangle α) (A : α ↝ ⊥) (M : NearLitter), M ∈ (t.support ⇘. A)ᴺ → pos M < pos t :=
+  letI : Level := ⟨α⟩
+  letI := ltData M
+  λ t A N ↦ pos_nearLitter_lt_newPosition _ t N A
 
 theorem constructMotive_smul_fuzz {β γ : Λ} (hβ : (β : TypeIndex) < α)
     (hγ : (γ : TypeIndex) < α) (hβγ : (β : TypeIndex) ≠ γ) :
     letI := (M β hβ).data; letI := (M β hβ).pos
     ∀ (ρ : (constructMotive α M H).data.AllPerm) (t : Tangle β),
       (constructMotive α M H).data.allPermForget ρ ↘ hγ ↘. • fuzz hβγ t =
-      fuzz hβγ (constructAllPermSderiv M H hβ ρ • t) := sorry
+      fuzz hβγ (constructAllPermSderiv M H hβ ρ • t) :=
+  letI : Level := ⟨α⟩
+  letI := ltData M
+  letI : LtLevel β := ⟨hβ⟩
+  letI : LtLevel γ := ⟨hγ⟩
+  λ ρ ↦ ρ.smul_fuzz hβγ
 
 theorem constructMotive_smul_fuzz_bot {γ : Λ} (hγ : (γ : TypeIndex) < α) :
     letI := botModelData; letI := botPosition
     ∀ (ρ : (constructMotive α M H).data.AllPerm) (t : Tangle ⊥),
     (constructMotive α M H).data.allPermForget ρ ↘ hγ ↘. • fuzz (bot_ne_coe (a := γ)) t =
-      fuzz (bot_ne_coe (a := γ)) (constructAllPermBotSderiv M H ρ • t) := sorry
+      fuzz (bot_ne_coe (a := γ)) (constructAllPermBotSderiv M H ρ • t) :=
+  letI : Level := ⟨α⟩
+  letI := ltData M
+  letI : LtLevel γ := ⟨hγ⟩
+  λ ρ ↦ ρ.smul_fuzz bot_ne_coe
 
 theorem constructMotive_allPerm_of_smul_fuzz :
     ∀ (ρs : {β : Λ} → (hβ : (β : TypeIndex) < α) → (M β hβ).data.AllPerm)
@@ -81,15 +103,38 @@ theorem constructMotive_allPerm_of_smul_fuzz :
       (ρs hγ)ᵁ ↘. • fuzz (bot_ne_coe (a := γ)) t = fuzz (bot_ne_coe (a := γ)) (π • t)) →
     ∃ ρ : (constructMotive α M H).data.AllPerm,
       (∀ (β : Λ) (hβ : (β : TypeIndex) < α), constructAllPermSderiv M H hβ ρ = ρs hβ) ∧
-      constructAllPermBotSderiv M H ρ = π := sorry
+      constructAllPermBotSderiv M H ρ = π := by
+  letI : Level := ⟨α⟩
+  letI := ltData M
+  intro ρs π h₁ h₂
+  refine ⟨⟨λ β iβ ↦ β.recBotCoe (λ _ ↦ π) (λ β iβ ↦ ρs iβ.elim) iβ, ?_⟩, ?_, ?_⟩
+  · intro β
+    induction β using recBotCoe with
+    | bot =>
+      intro γ _ _ hβγ t
+      exact h₂ LtLevel.elim t
+    | coe β =>
+      intro γ _ _
+      exact h₁ LtLevel.elim LtLevel.elim
+  · intro β hβ
+    rfl
+  · rfl
 
 theorem constructMotive_tSet_ext (β : Λ) (hβ : (β : TypeIndex) < α)
     (x y : (constructMotive α M H).data.TSet) :
-    (∀ z : (M β hβ).data.TSet, z ∈[hβ] x ↔ z ∈[hβ] y) → x = y := sorry
+    (∀ z : (M β hβ).data.TSet, z ∈[hβ] x ↔ z ∈[hβ] y) → x = y :=
+  letI : Level := ⟨α⟩
+  letI := ltData M
+  letI : LtLevel β := ⟨hβ⟩
+  newModelData_ext β x y
 
 theorem constructMotive_typedMem_singleton_iff {β : Λ} (hβ : (β : TypeIndex) < α)
     (x y : (M β hβ).data.TSet) :
-    y ∈[hβ] constructSingleton M H hβ x ↔ y = x := sorry
+    y ∈[hβ] constructSingleton M H hβ x ↔ y = x :=
+  letI : Level := ⟨α⟩
+  letI := ltData M
+  letI : LtLevel β := ⟨hβ⟩
+  mem_newSingleton_iff x y
 
 def constructHypothesis (α : Λ) (M : (β : Λ) → (β : TypeIndex) < α → Motive β)
     (H : (β : Λ) → (h : (β : TypeIndex) < α) → Hypothesis (M β h) λ γ h' ↦ M γ (h'.trans h)) :

ConNF/Construction/NewModelData.lean

@@ -443,6 +443,22 @@ theorem card_newPositionDeny (t : Tangle α) :
 def newPosition (h : #(Tangle α) ≤ #μ) : Position (Tangle α) where
   pos := ⟨funOfDeny h newPositionDeny card_newPositionDeny, funOfDeny_injective _ _ _⟩
 
+theorem pos_atom_lt_newPosition (h : #(Tangle α) ≤ #μ) (t : Tangle α) (a : Atom)
+    (A : α ↝ ⊥) (ha : a ∈ (t.support ⇘. A)ᴬ) :
+    pos a < (newPosition h).pos t := by
+  apply funOfDeny_gt_deny
+  obtain ⟨i, hi⟩ := ha
+  refine Or.inl (Or.inr ⟨_, ?_, rfl⟩)
+  exact ⟨i, ⟨A, a⟩, hi, rfl⟩
+
+theorem pos_nearLitter_lt_newPosition (h : #(Tangle α) ≤ #μ) (t : Tangle α) (N : NearLitter)
+    (A : α ↝ ⊥) (hN : N ∈ (t.support ⇘. A)ᴺ) :
+    pos N < (newPosition h).pos t := by
+  apply funOfDeny_gt_deny
+  obtain ⟨i, hi⟩ := hN
+  refine Or.inr ⟨_, ?_, rfl⟩
+  exact ⟨i, ⟨A, N⟩, hi, rfl⟩
+
 def newTypedNearLitters (h : #(Tangle α) ≤ #μ) :
     letI := newPosition h; TypedNearLitters α :=
   letI := newPosition h