wip

Author: SnO2WMaN

Foundation/Modal/Kripke/ExtendRoot.lean

@@ -40,9 +40,9 @@ instance isFinite [F.IsFinite] : (F.extendRoot n).IsFinite := by
 
 instance fintype [Fintype F] : Fintype (F.extendRoot n) := instFintypeSum (Fin n) F
 
-protected abbrev root (F n) : (extendRoot F n).Root := ⟨.inl ⟨n - 1, by simp⟩, by grind⟩
+protected abbrev defaultRoot (F n) : (extendRoot F n).Root := ⟨.inl ⟨n - 1, by simp⟩, by grind⟩
 
-instance : (F.extendRoot n).IsRooted := ⟨extendRoot.root F n⟩
+instance : (F.extendRoot n).IsRooted := ⟨extendRoot.defaultRoot F n⟩
 
 protected abbrev chain (F n) : List (extendRoot F n) := List.finRange n |>.reverse.map (extend ·)
 
@@ -68,40 +68,6 @@ protected abbrev pMorphism : F →ₚ F.extendRoot n where
   forth := by grind;
   back {x y} h := by grind;
 
-lemma not_root_of_from_root (r : F.Root) (x : F.extendRoot n) (h : (extendRoot.root F n) ≺ x) :
-  (∃ i : Fin n, x = extend i) ∨ x = r ∨ r ≺ x := by
-  match x with
-  | .inl i =>
-    left;
-    use i;
-  | .inr x =>
-    by_cases e : x = r;
-    . tauto;
-    . right;
-      right;
-      apply extendRoot.pMorphism.forth;
-      grind;
-
-lemma not_root_of_from_root' (r : F.Root) (x : F.extendRoot n) (h : (extendRoot.root F n) ≺ x) :
-  (∃ i : Fin n, x = extend i) ∨ x = r ∨ ∃ x₀ : F, x = x₀ ∧ r ≺ x₀ := by
-  rcases not_root_of_from_root r x h with (h | h | h)
-  · tauto;
-  · tauto;
-  · right; right;
-    rcases extendRoot.pMorphism.back h with ⟨x₀, rfl, hx₀⟩;
-    exact ⟨x₀, rfl, hx₀⟩
-
-lemma not_root_of_from_root₁ (r : F.Root) [F.IsIrreflexive] (x : F.extendRoot 1) (h : (extendRoot.root F 1) ≺ x) :
-  x = r ∨ embed r ≺ x := by
-  rcases not_root_of_from_root r x h with (⟨i, hi, rfl⟩ | hr | hr) <;> simp_all [extendRoot.root]
-
-lemma not_root_of_from_root'₁ (r : F.Root) [F.IsIrreflexive] (x : F.extendRoot 1) (h : (extendRoot.root F 1) ≺ x) :
-  x = r ∨ ∃ x₀ : F, x = x₀ ∧ r ≺ x₀ := by
-  rcases not_root_of_from_root' r x h with (⟨i, hi, rfl⟩ | hr | hr) <;> simp_all [extendRoot.root]
-
-lemma eq_inr_of_root_rel (r : F.Root) [F.IsIrreflexive] (x : F.extendRoot 1) (h : (extendRoot.root F 1) ≺ x) :
-  ∃ x₀ : F, x = x₀ := by
-  rcases not_root_of_from_root'₁ r x h with (rfl | ⟨x₀, rfl, hx₀⟩) <;> grind;
 
 @[simp]
 lemma embed_rel_embed_iff_rel {i j : F} : embed (n := n) i ≺ embed j ↔ i ≺ j :=
@@ -111,8 +77,55 @@ lemma embed_rel_embed_iff_rel {i j : F} : embed (n := n) i ≺ embed j ↔ i ≺
 lemma embed_rel_iterate_embed_iff_rel {i j : F} : embed (n := n) i ≺^[k] embed j ↔ i ≺^[k] j :=
   extendRoot.pMorphism.toFun_rel_iterate_toFun_iff_of_inj Sum.inr_injective
 
+
+@[simp, grind .]
+lemma eq_defaultRoot_root [F.IsIrreflexive] [F.IsTransitive] : (F.extendRoot n).root = (extendRoot.defaultRoot F n) := by
+  apply root_uniqueness_of_irrefl_trans;
+
+@[simp, grind .]
+lemma rel_defaultRoot_original_root [F.IsRooted] [F.IsTransitive] [F.IsIrreflexive] : (F.extendRoot n).root.1 ≺ F.root.1 := by
+  grind [eq_defaultRoot_root];
+
+@[grind →]
+lemma not_eq_defaultRoot_of_rel_defaultRoot (x : F.extendRoot n) (h : (extendRoot.defaultRoot F n) ≺ x) : x ≠ (extendRoot.defaultRoot F n) := by grind;
+
+@[grind →]
+lemma not_eq_extendRoot_root_of_rel_original_root [F.IsIrreflexive] [F.IsTransitive] (x : F.extendRoot n) (h : (extendRoot F n).root ≺ x) : x ≠ (extendRoot F n).root := by grind;
+
+
+lemma eq_extend_or_eq_original (x : F.extendRoot n)
+  : (∃ i : Fin n, x = extend i) ∨ (∃ x₀ : F, x = x₀) := by
+  match x with
+  | .inl i => left; use i;
+  | .inr x => grind;
+
+
+section
+
+lemma eq_original_of_rel_defaultRoot₁ [F.IsIrreflexive] (x : F.extendRoot 1) (h : (extendRoot.defaultRoot F 1) ≺ x)
+  : ∃ x₀ : F, x = x₀ := by
+  rcases eq_extend_or_eq_original x with (⟨i, hi, rfl⟩ | _) <;> simp_all;
+
+lemma eq_root_or_rel_original_root_of_neq_defaultRoot₁ [F.IsIrreflexive] (x : F.extendRoot 1) (h : x ≠ (extendRoot.defaultRoot F 1))
+  : ∃ x₀ : F, x = x₀ := by
+  apply eq_original_of_rel_defaultRoot₁;
+  grind;
+
+lemma eq_root_or_rel_original_root_of_rel_extendRoot_root₁ [F.IsIrreflexive] (x : F.extendRoot 1) (h : (extendRoot F 1).root ≺ x)
+  : ∃ x₀ : F, x = x₀ := by
+  apply eq_original_of_rel_defaultRoot₁;
+  grind;
+
+lemma eq_root_or_rel_original_root_of_neq_extendRoot_root₁ [F.IsIrreflexive] [F.IsTransitive] (x : F.extendRoot 1) (h : x ≠ (extendRoot F 1).root)
+  : ∃ x₀ : F, x = x₀ := by
+  apply eq_root_or_rel_original_root_of_neq_defaultRoot₁;
+  grind [eq_defaultRoot_root];
+
+end
+
 end Frame.extendRoot
 
+
 abbrev Model.extendRoot (M : Kripke.Model) (r : M.Root) (n : ℕ+) : Kripke.Model where
   toFrame := M.toFrame.extendRoot n
   Val a x :=
@@ -124,31 +137,9 @@ namespace Model.extendRoot
 
 variable {M : Model} {r : M.Root} {x y : M.World} {n : ℕ+} {i : Fin n} {φ}
 
--- abbrev extend (i : Fin n) : M.extendRoot r n := .inl i
-
 @[coe] abbrev extend (i : Fin n) : M.extendRoot r n := .inl i
 @[coe] abbrev embed (x : M) : M.extendRoot r n := .inr x
 
--- instance : Coe (M.World) ((M.extendRoot r n).World) := ⟨embed⟩
-
--- protected abbrev root (M) := Frame.extendRoot.root (M.toFrame) (n := n)
-
-/-
-instance isFinite [M.IsFinite] : (M.extendRoot r n).IsFinite := Frame.extendRoot.isFinite
-
-instance fintype [Fintype M] : Fintype (M.extendRoot r n) := Frame.extendRoot.fintype
-
-instance isTransitive [M.IsTransitive] : (M.extendRoot n).IsTransitive := Frame.extendRoot.isTransitive
-
-instance isAsymmetric [M.IsAsymmetric] : (M.extendRoot n).IsAsymmetric := Frame.extendRoot.isAsymmetric
-
-instance isRooted [M.IsRootedBy r] : (M.extendRoot n).IsRootedBy extendRoot.root := Frame.extendRoot.instIsRooted
-
-instance isTree [M.IsTree r] : (M.extendRoot n).IsTree extendRoot.root := Frame.extendRoot.isTree
-
-instance isFiniteTree [M.IsFiniteTree r] : (M.extendRoot n).IsFiniteTree extendRoot.root := Frame.extendRoot.isFiniteTree
--/
-
 def pMorphism : M →ₚ M.extendRoot r n := PseudoEpimorphism.ofAtomic Frame.extendRoot.pMorphism $ by grind;
 
 lemma modal_equivalence_original_world : (embed x : M.extendRoot r n) ↭ x :=

Foundation/Modal/Kripke/Logic/GL/Completeness.lean

@@ -217,8 +217,8 @@ instance FFP : Complete Modal.GL Kripke.FrameClass.finite_GL := ⟨by
 theorem finite_completeness_TFAE : [
   Modal.GL ⊢ φ,
   FrameClass.finite_GL ⊧ φ,
-  ∀ F : Kripke.Frame, [F.IsFinite] → [F.IsTransitive] → [F.IsIrreflexive] → F.IsRooted → F ⊧ φ,
-  ∀ M : Kripke.Model, [M.IsFinite] → [M.IsTransitive] → [M.IsIrreflexive] → ∀ r : M.Root, r.1 ⊧ φ,
+  ∀ F : Kripke.Frame, [F.IsFinite] → [F.IsTransitive] → [F.IsIrreflexive] → [F.IsRooted] → F ⊧ φ,
+  ∀ M : Kripke.Model, [M.IsFinite] → [M.IsTransitive] → [M.IsIrreflexive] → [M.IsRooted] → M.root.1 ⊧ φ,
 ].TFAE := by
   tfae_have 1 → 2 := by apply Sound.sound;
   tfae_have 2 → 1 := by apply Complete.complete;
@@ -229,33 +229,30 @@ theorem finite_completeness_TFAE : [
   tfae_have 3 → 4 := by
     intro h F _ _ _ r;
     apply h;
-    exact ⟨r⟩;
   tfae_have 4 → 2 := by
     rintro H F ⟨_, F_trans, F_irrefl⟩ V x;
     let M : Kripke.Model := ⟨F, V⟩;
-    exact Model.pointGenerate.pMorphism M x |>.modal_equivalence _ |>.mp $ H (M↾x) (⟨⟨x, by grind⟩, by grind⟩);
+    simpa [Frame.pointGenerate.eq_root_pointGenerate_root] using Model.pointGenerate.pMorphism M x |>.modal_equivalence _ |>.mp $ H (M↾x);
   tfae_finish;
 
-lemma iff_unprovable_exists_finite_rooted_model : Modal.GL ⊬ φ ↔ ∃ M : Model, ∃ _ : M.IsFinite, ∃ _ : M.IsTransitive, ∃ _ : M.IsIrreflexive, ∃ r : M.Root, ¬r.1 ⊧ φ := by
+lemma iff_unprovable_exists_finite_rooted_model : Modal.GL ⊬ φ ↔ ∃ M : Model, ∃ _ : M.IsFinite, ∃ _ : M.IsTransitive, ∃ _ : M.IsIrreflexive, ∃ _ : M.IsRooted, ¬M.root.1 ⊧ φ := by
   apply Iff.not_left;
   apply Iff.trans $ finite_completeness_TFAE (φ := φ) |>.out 0 3;
   push_neg;
   tauto;
 
 theorem fintype_completeness_TFAE : [
   Modal.GL ⊢ φ,
-  ∀ F : Kripke.Frame, [Fintype F] → [F.IsTransitive] → [F.IsIrreflexive] → F.IsRooted → F ⊧ φ,
-  ∀ M : Kripke.Model, [Fintype M] → [M.IsTransitive] → [M.IsIrreflexive] → ∀ r : M.Root, r.1 ⊧ φ,
+  ∀ F : Kripke.Frame, [Fintype F] → [F.IsTransitive] → [F.IsIrreflexive] → [F.IsRooted] → F ⊧ φ,
+  ∀ M : Kripke.Model, [Fintype M] → [M.IsTransitive] → [M.IsIrreflexive] → [M.IsRooted] → M.root.1 ⊧ φ,
 ].TFAE := by
   tfae_have 1 → 2 := by
     rintro h F _ _ Fcwf _ _;
     have := finite_completeness_TFAE.out 0 2 |>.mp h;
     apply this;
-    assumption;
   tfae_have 2 → 3 := by
-    intro h F _ _ _ r;
+    intro h F _ _ _ _;
     apply h;
-    exact ⟨r⟩;
   tfae_have 3 → 1 := by
     intro h;
     apply finite_completeness_TFAE (φ := φ) |>.out 3 0 |>.mp;
@@ -264,7 +261,7 @@ theorem fintype_completeness_TFAE : [
     apply h;
   tfae_finish;
 
-lemma iff_unprovable_exists_fintype_rooted_model : Modal.GL ⊬ φ ↔ ∃ M : Model, ∃ _ : Fintype M, ∃ _ : M.IsTransitive, ∃ _ : M.IsIrreflexive, ∃ r : M.Root, ¬r.1 ⊧ φ := by
+lemma iff_unprovable_exists_fintype_rooted_model : Modal.GL ⊬ φ ↔ ∃ M : Model, ∃ _ : Fintype M, ∃ _ : M.IsTransitive, ∃ _ : M.IsIrreflexive, ∃ _ : M.IsRooted, ¬M.root.1 ⊧ φ := by
   apply Iff.not_left;
   apply Iff.trans $ fintype_completeness_TFAE (φ := φ) |>.out 0 2;
   push_neg;

Foundation/Modal/Kripke/Logic/GL/MDP.lean

@@ -49,38 +49,8 @@ instance [F₁.IsTransitive] [F₂.IsTransitive] : (mdpCounterexmpleFrame F₁ F
     | .inl _, .inr (.inr _), .inr (.inr _)
     | .inl _, .inr (.inl _), .inr (.inl _) => grind;
 
-
-/-
-instance {F₁ F₂ : Frame} -- {r₁ : outParam F₁.World} {r₂ : outParam F₂.World}
-  -- [tree₁ : F₁.IsFiniteTree r₁] [tree₂ : F₂.IsFiniteTree r₂]
-  : (mdpCounterexmpleFrame F₁ F₂ r₁ r₂).IsFiniteTree (.inl ()) where
-  root_generates := by
-    intro x hx;
-    match x with
-    | .inl x => contradiction;
-    | .inr _ =>
-      apply Relation.TransGen.single;
-      tauto;
-  asymm := by
-    intro x y hxy;
-    match x, y with
-    | .inr (.inl x), .inr (.inl y) => exact tree₁.asymm _ _ hxy;
-    | .inr (.inr x), .inr (.inr y) => apply tree₂.asymm _ _ hxy;
-    | .inl x, .inl y => contradiction;
-    | .inl x, .inr y => simp;
-  trans := by
-    intro x y z hxy hyz;
-    match x, y, z with
-    | .inr (.inl x), .inr (.inl y), .inr (.inl z) => apply tree₁.trans _ _ _ hxy hyz;
-    | .inr (.inr x), .inr (.inr y), .inr (.inr z) => apply tree₂.trans _ _ _ hxy hyz;
-    | .inl _, .inr (.inr _), .inr (.inr _) => simp;
-    | .inl _, .inr (.inl _), .inr (.inl _) => simp;
-
--- TODO: remove?
-instance : (mdpCounterexmpleFrame F₁ F₂ r₁ r₂).IsIrreflexive := ⟨by simp⟩
--/
-
-protected abbrev root (F₁ F₂) : (mdpCounterexmpleFrame F₁ F₂).Root := ⟨.inl (), by grind⟩
+protected abbrev defaultRoot (F₁ F₂) : (mdpCounterexmpleFrame F₁ F₂).Root := ⟨.inl (), by grind⟩
+instance : (mdpCounterexmpleFrame F₁ F₂).IsRooted := ⟨mdpCounterexmpleFrame.defaultRoot F₁ F₂⟩
 
 def pMorphism₁ (F₁ F₂) : F₁ →ₚ (mdpCounterexmpleFrame F₁ F₂) where
   toFun x := .inr (.inl x)
@@ -92,7 +62,7 @@ def pMorphism₂ (F₁ F₂) : F₂ →ₚ (mdpCounterexmpleFrame F₁ F₂) whe
   forth := by intro x y hxy; exact hxy;
   back {x y} h := by match y with | .inr (.inr y) => use y;
 
-lemma through_original_root (r₁ : F₁.Root) (r₂ : F₂.Root) (x : (mdpCounterexmpleFrame F₁ F₂).World) (h : mdpCounterexmpleFrame.root F₁ F₂ ≺ x)
+lemma through_original_root (r₁ : F₁.Root) (r₂ : F₂.Root) (x : (mdpCounterexmpleFrame F₁ F₂).World) (h : mdpCounterexmpleFrame.defaultRoot F₁ F₂ ≺ x)
   : (x = r₁ ∨ (Sum.inr (Sum.inl r₁.1) ≺ x)) ∨ (x = r₂ ∨ (Sum.inr (Sum.inr r₂.1) ≺ x)) := by
   match x with
   | .inl x => grind;
@@ -125,7 +95,7 @@ variable {M₁ M₂ : Model} -- {r₁ : M₁.World} {r₂ : M₂.World} [tree₁
 -- instance : Coe (M₁.World) (mdpCounterexmpleModel M₁ M₂ r₁ r₂).World := ⟨Sum.inr ∘ Sum.inl⟩
 -- instance : Coe (M₂.World) (mdpCounterexmpleModel M₁ M₂ r₁ r₂).World := ⟨Sum.inr ∘ Sum.inr⟩
 
--- abbrev root : (mdpCounterexmpleModel M₁ M₂).World := mdpCounterexmpleFrame.root (F₁ := M₁.toFrame) (F₂ := M₂.toFrame) (r₁ := r₁) (r₂ := r₂)
+-- abbrev root : (mdpCounterexmpleModel M₁ M₂).World := mdpCounterexmpleFrame.defaultRoot (F₁ := M₁.toFrame) (F₂ := M₂.toFrame) (r₁ := r₁) (r₂ := r₂)
 
 def pMorphism₁ (M₁ M₂) : M₁ →ₚ (mdpCounterexmpleModel M₁ M₂) :=
   Model.PseudoEpimorphism.ofAtomic (mdpCounterexmpleFrame.pMorphism₁ M₁.toFrame M₂.toFrame) $ by
@@ -157,14 +127,16 @@ lemma MDP_Aux {X : Set _} (h : (□'X) *⊢[Modal.GL] □φ₁ ⋎ □φ₂) : (
     by_contra! hC;
     have ⟨h₁, h₂⟩ : (Modal.GL ⊬ ⊡c ➝ φ₁) ∧ (Modal.GL ⊬ ⊡c ➝ φ₂) := hC;
 
-    obtain ⟨M₁, _, _, _, r₁, hM₁⟩ := GL.Kripke.iff_unprovable_exists_finite_rooted_model.mp h₁;
-    obtain ⟨M₂, _, _, _, r₂, hM₂⟩ := GL.Kripke.iff_unprovable_exists_finite_rooted_model.mp h₂;
+    obtain ⟨M₁, _, _, _, _, hM₁⟩ := GL.Kripke.iff_unprovable_exists_finite_rooted_model.mp h₁;
+    obtain ⟨M₂, _, _, _, _, hM₂⟩ := GL.Kripke.iff_unprovable_exists_finite_rooted_model.mp h₂;
 
+    let r₁ := M₁.root;
+    let r₂ := M₂.root;
     let M₀ := Kripke.mdpCounterexmpleModel M₁ M₂;
-    let r₀ : M₀.Root := Kripke.mdpCounterexmpleFrame.root _ _;
+    let r₀ : M₀.Root := Kripke.mdpCounterexmpleFrame.defaultRoot _ _;
 
-    replace hM₁ : Satisfies M₀ ↑r₁ (⊡c ⋏ ∼φ₁) := Kripke.mdpCounterexmpleModel.modal_equivalence_original_world₁.mp (Formula.Kripke.Satisfies.not_imp.mp hM₁);
-    replace hM₂ : Satisfies M₀ ↑r₂ (⊡c ⋏ ∼φ₂) := Kripke.mdpCounterexmpleModel.modal_equivalence_original_world₂.mp (Formula.Kripke.Satisfies.not_imp.mp hM₂);
+    replace hM₁ : Satisfies M₀ r₁ (⊡c ⋏ ∼φ₁) := Kripke.mdpCounterexmpleModel.modal_equivalence_original_world₁.mp (Formula.Kripke.Satisfies.not_imp.mp hM₁);
+    replace hM₂ : Satisfies M₀ r₂ (⊡c ⋏ ∼φ₂) := Kripke.mdpCounterexmpleModel.modal_equivalence_original_world₂.mp (Formula.Kripke.Satisfies.not_imp.mp hM₂);
 
     have hc : Satisfies M₀ r₀ (□c) := by
       intro x Rrx;
@@ -194,8 +166,8 @@ lemma MDP_Aux {X : Set _} (h : (□'X) *⊢[Modal.GL] □φ₁ ⋎ □φ₂) : (
       exact ⟨hp₁, hp₂⟩;
     have : ¬(Satisfies M₀ r₀ (□c ➝ (□φ₁ ⋎ □φ₂))) := _root_.not_imp.mpr ⟨hc, this⟩;
     have : Modal.GL ⊬ □c ➝ □φ₁ ⋎ □φ₂ := GL.Kripke.iff_unprovable_exists_finite_rooted_model.mpr $ by
-      use M₀, inferInstance, inferInstance, inferInstance, r₀;
-      exact this;
+      use M₀, inferInstance, inferInstance, inferInstance, inferInstance;
+      rwa [Frame.root_uniqueness_of_irrefl_trans r₀] at this;
     contradiction;
 
   rcases this with (h | h) <;> {

Foundation/Modal/Kripke/Logic/GL/Unnecessitation.lean

@@ -17,33 +17,32 @@ lemma imply_boxdot_plain_of_imply_box_box : Modal.GL ⊢ □φ ➝ □ψ → Mod
   contrapose;
 
   intro h;
-  obtain ⟨M, _, _, _, r, hs⟩ := GL.Kripke.iff_unprovable_exists_finite_rooted_model.mp h;
+  obtain ⟨M, _, _, _, _, hs⟩ := GL.Kripke.iff_unprovable_exists_finite_rooted_model.mp h;
 
-  let M₀ := M.extendRoot r 1;
-  let r₀ : M₀.Root := Frame.extendRoot.root M.toFrame 1;
 
   apply GL.Kripke.iff_unprovable_exists_finite_rooted_model.mpr;
-  use M₀, inferInstance, inferInstance, inferInstance, r₀;
+  use (M.extendRoot M.root 1), inferInstance, inferInstance, inferInstance, inferInstance;
 
-  have hs : Satisfies M r (⊡φ ⋏ ∼ψ) := by simp_all [Satisfies];
-  replace hs := @Model.extendRoot.modal_equivalence_original_world (M := M) (r := r) (n := 1) r (⊡φ ⋏ ∼ψ) |>.mpr hs;
+  have hs : Satisfies M M.root (⊡φ ⋏ ∼ψ) := by simp_all [Satisfies];
+  replace hs := @Model.extendRoot.modal_equivalence_original_world (M := M) (r := M.root) (n := 1) M.root (⊡φ ⋏ ∼ψ) |>.mpr hs;
   have ⟨hs₁₂, hs₃⟩ := Satisfies.and_def.mp hs;
   have ⟨hs₁, hs₂⟩ := Satisfies.and_def.mp hs₁₂;
 
   apply Satisfies.not_imp_def.mpr;
   constructor;
-  . have hs : Satisfies M r (⊡φ ⋏ ∼ψ) := by simp_all [Satisfies];
-    replace hs := @Model.extendRoot.modal_equivalence_original_world (M := M) (r := r) (n := 1) r (⊡φ ⋏ ∼ψ) |>.mpr hs;
+  . have hs : Satisfies M M.root (⊡φ ⋏ ∼ψ) := by simp_all [Satisfies];
+    replace hs := @Model.extendRoot.modal_equivalence_original_world (M := M) (r := M.root) (n := 1) M.root (⊡φ ⋏ ∼ψ) |>.mpr hs;
     have ⟨hs₁₂, hs₃⟩ := Satisfies.and_def.mp hs;
     have ⟨hs₁, hs₂⟩ := Satisfies.and_def.mp hs₁₂;
-
     intro x hx;
-    rcases Frame.extendRoot.not_root_of_from_root₁ (F := M.toFrame) (x := x) r hx with (rfl | hr);
-    . assumption;
-    . apply hs₂; exact hr;
+    obtain ⟨x₀, rfl⟩ := Frame.extendRoot.eq_root_or_rel_original_root_of_neq_extendRoot_root₁ x (by grind);
+    by_cases e : x₀ = M.root;
+    . exact e ▸ hs₁;
+    . apply hs₂;
+      grind;
   . apply Satisfies.box_def.not.mpr;
     push_neg;
-    use (Sum.inr r);
+    use (Sum.inr M.root);
     constructor;
     . grind;
     . assumption;