Updates available and ready to merge

equational_theories/ManuallyProved/Equation1729/MagmaConstruction.lean

@@ -122,16 +122,23 @@ lemma PartialSolution.inv_L₀' {sol : PartialSolution} {x : N} (h: x ∈ sol.Do
 noncomputable abbrev Set.choose {α: Type} {S: Set α} {P: α → Prop} (h: ∃ s ∈ S, P s) : S := ⟨_, (Classical.choose_spec h).1⟩
 
 -- for Mathlib?
-lemma Set.choose_spec {α: Type} {S: Set α} {P: α → Prop} (h: ∃ s ∈ S, P s) : P (Set.choose h) := (Classical.choose_spec h).2
+lemma Set.choose_spec {α: Type} {S: Set α} {P: α → Prop}
+    (h: ∃ s ∈ S, P s) : P (Set.choose h) :=
+  (Classical.choose_spec h).2
 
 -- for Mathlib?
-lemma IsChain.IsDirected {α: Type} [Preorder α] {s: Set α} (h: IsChain (fun x y ↦ x ≤ y) s) [Nonempty s] : IsDirected s (fun x y ↦ x ≤ y) := by
+lemma IsChain.IsDirected {α: Type} [Preorder α] {s: Set α} (h: IsChain (fun x y ↦ x ≤ y) s) [Nonempty s]
+    : IsDirected s (fun x y ↦ x ≤ y) := by
   rw [← directedOn_univ_iff]
   convert (directedOn_image (s := Set.univ) (f := Subtype.val) (r := fun x y ↦ x ≤ y)).mp _
   convert IsChain.directedOn h
   exact Subtype.coe_image_univ s
 
-lemma use_chain {sols : Set PartialSolution} (hchain: IsChain (fun (sol1 sol2 : PartialSolution) => sol1 ≤ sol2) sols ) (hnon: Nonempty sols) (htotal_L₀' : ∀ x : N, ∃ sol ∈ sols, x ∈ sol.Dom_L₀') (htotal_S' : ∀ x : N, ∃ sol ∈ sols, x ∈ sol.Dom_S') (htotal_op : ∀ (x y : N), ∃ sol ∈ sols, (x,y) ∈ sol.Dom_op) : ∃ (G: Type) (_: Magma G), Equation1729 G ∧ ¬ Equation817 G := by
+lemma use_chain {sols : Set PartialSolution}
+    (hchain: IsChain (fun (sol1 sol2 : PartialSolution) => sol1 ≤ sol2) sols ) (hnon: Nonempty sols)
+    (htotal_L₀' : ∀ x : N, ∃ sol ∈ sols, x ∈ sol.Dom_L₀') (htotal_S' : ∀ x : N, ∃ sol ∈ sols, x ∈ sol.Dom_S')
+    (htotal_op : ∀ (x y : N), ∃ sol ∈ sols, (x,y) ∈ sol.Dom_op)
+    : ∃ (G: Type) (_: Magma G), Equation1729 G ∧ ¬ Equation817 G := by
   let f := Filter.atTop (α := sols)
   have fnon : f.NeBot := Filter.atTop_neBot_iff.mpr ⟨hnon, IsChain.IsDirected hchain⟩
   let S' (x : N) := (Set.choose (htotal_S' x)).1.S' x
@@ -204,7 +211,17 @@ lemma use_chain {sols : Set PartialSolution} (hchain: IsChain (fun (sol1 sol2 :
   aesop
 
 /-- All the elements of `SM` that are involved in a partial solution, plus an additional set of extra elements of `N`-/
-abbrev PartialSolution.involved_elements (sol: PartialSolution) (extras: Finset M) : Finset SM := Finset.biUnion sol.Predom_L₀' basis_elements ∪ Finset.biUnion sol.Dom_S' basis_elements ∪ Finset.image  sol.S' sol.Dom_S' ∪ Finset.biUnion sol.Dom_op (fun (x, _) ↦ basis_elements x) ∪ Finset.biUnion sol.Dom_op (fun (_, y) ↦ basis_elements y) ∪ Finset.biUnion sol.Dom_op (fun (x, y) ↦ basis_elements' (sol.op x y)) ∪ Finset.biUnion sol.I (fun (x, _, _) ↦ basis_elements x) ∪ Finset.biUnion sol.I (fun (_, y, _) ↦ basis_elements y) ∪ Finset.biUnion sol.I (fun (_, _, z) ↦ basis_elements z) ∪ Finset.biUnion extras basis_elements'
+abbrev PartialSolution.involved_elements (sol: PartialSolution) (extras: Finset M) : Finset SM :=
+  Finset.biUnion sol.Predom_L₀' basis_elements
+  ∪ Finset.biUnion sol.Dom_S' basis_elements
+  ∪ Finset.image  sol.S' sol.Dom_S'
+  ∪ Finset.biUnion sol.Dom_op (fun (x, _) ↦ basis_elements x)
+  ∪ Finset.biUnion sol.Dom_op (fun (_, y) ↦ basis_elements y)
+  ∪ Finset.biUnion sol.Dom_op (fun (x, y) ↦ basis_elements' (sol.op x y))
+  ∪ Finset.biUnion sol.I (fun (x, _, _) ↦ basis_elements x)
+  ∪ Finset.biUnion sol.I (fun (_, y, _) ↦ basis_elements y)
+  ∪ Finset.biUnion sol.I (fun (_, _, z) ↦ basis_elements z)
+  ∪ Finset.biUnion extras basis_elements'
 
 abbrev PartialSolution.directly_sees (sol:PartialSolution) (extras: Finset M) (x : N) := basis_elements x ⊆ sol.involved_elements extras
 
@@ -218,18 +235,21 @@ lemma PartialSolution.see_direct (sol:PartialSolution) {extras: Finset M} {x : N
 
 lemma PartialSolution.see_direct' (sol:PartialSolution) {extras: Finset M} {x : M} (h: sol.directly_sees' extras x) : sol.sees' extras x := generators_mono h
 
-lemma PartialSolution.sees_mul (sol: PartialSolution) {extras: Finset M} {x y:N} (hx: sol.sees extras x) (hy: sol.sees extras y) : sol.sees extras (x * y) := calc
-  _ ⊆ generators (basis_elements x ∪ basis_elements y)  := generators_mono <| basis_elements_of_mul x y
-  _ = generators (basis_elements x) ∪ generators (basis_elements y) := generators_union ..
-  _ ⊆ _ := Finset.union_subset hx hy
+lemma PartialSolution.sees_mul (sol: PartialSolution) {extras: Finset M} {x y:N}
+    (hx: sol.sees extras x) (hy: sol.sees extras y) : sol.sees extras (x * y) :=
+  calc
+    _ ⊆ generators (basis_elements x ∪ basis_elements y)  := generators_mono <| basis_elements_of_mul x y
+    _ = generators (basis_elements x) ∪ generators (basis_elements y) := generators_union ..
+    _ ⊆ _ := Finset.union_subset hx hy
 
 lemma PartialSolution.sees_inv (sol: PartialSolution) {extras: Finset M} {x : N} (hx: sol.sees extras x)  : sol.sees extras x⁻¹ := by
   dsimp [PartialSolution.sees]
   convert hx using 2
   exact basis_elements_of_inv x
 
 
-abbrev PartialSolution.reaches (sol: PartialSolution) (extras: Finset M) (a : SM) := in_generators (sol.involved_elements extras) a
+abbrev PartialSolution.reaches (sol: PartialSolution) (extras: Finset M) (a : SM) :=
+  in_generators (sol.involved_elements extras) a
 
 lemma PartialSolution.sees_iff (sol:PartialSolution) (extras: Finset M) (x : N) : sol.sees extras x ↔ ∀ a ∈ basis_elements x, sol.reaches extras a := generators_subset_iff
 
@@ -352,7 +372,9 @@ lemma PartialSolution.fresh_invis_pow (sol : PartialSolution) (extras: Finset M)
 open Classical in
 /-- Extend a map L₀' to map (R' 0)^n x to (R' 0)^n y and (R' 0)^n y to (R' 0)^(n-1) x for all integers n·  One should also add x and y to the predomain when extending· -/
 noncomputable abbrev PartialSolution.extend {sol:PartialSolution} (x y:N) (z : N): N :=
-  if z ≈ x then z * x⁻¹ * y else (if z ≈ y then z * y⁻¹ * (e 0)⁻¹ * x else sol.L₀' z)
+  if z ≈ x
+    then z * x⁻¹ * y
+    else (if z ≈ y then z * y⁻¹ * (e 0)⁻¹ * x else sol.L₀' z)
 
 lemma PartialSolution.extend_not_rel {sol:PartialSolution} {x y:N} {z : N} (hx: ¬ z ≈ x) (hy: ¬ z ≈ y) : sol.extend x y z = sol.L₀' z := by
   simp only [extend, hx, hy, if_false, if_false]
@@ -700,7 +722,8 @@ lemma PartialSolution_with_axioms.d₀_neq_d₁ (sol: PartialSolution_with_axiom
   by_contra! this
   exact zero_ne_one <| fresh_injective _ <| E_inj this
 
-lemma PartialSolution_with_axioms.d_injective (sol: PartialSolution_with_axioms) {y z y' z': N} (h: sol.d y z = sol.d y' z') : y = y' ∧ z = z' :=  (Prod.mk.injEq _ _ _ _) ▸ (enum_injective <| fresh_injective _ <| E_inj h)
+lemma PartialSolution_with_axioms.d_injective (sol: PartialSolution_with_axioms) {y z y' z': N} (h: sol.d y z = sol.d y' z') : y = y' ∧ z = z' :=
+  (Prod.mk.injEq _ _ _ _) ▸ (enum_injective <| fresh_injective _ <| E_inj h)
 
 lemma PartialSolution_with_axioms.test (sol: PartialSolution_with_axioms) {a b : SM} (i:ℕ) (h: a (sol.m i) ≠ b (sol.m i)) : a ≠ b :=
   fun x ↦ h (congrFun (congrArg DFunLike.coe x) (sol.m i))
@@ -712,6 +735,7 @@ lemma PartialSolution_with_axioms.Sd₀_neq_d₀ (sol: PartialSolution_with_axio
 
 lemma PartialSolution_with_axioms.Sd₀_neq_d₁  (sol: PartialSolution_with_axioms) : S sol.d₀ ≠ sol.d₁ := by
   apply sol.test 1
+
   simp only [S_eval, E_apply, add_right_inj]
   decide
 
@@ -1006,7 +1030,9 @@ lemma PartialSolution_with_axioms.neq_one_if_shift_to {sol:PartialSolution_with_
   simp only [ha, y₀]
   exact R'_axiom_iib _ _
 
-lemma PartialSolution_with_axioms.L₀'_no_collide_2 {sol: PartialSolution_with_axioms} {data data' : L₀'_data sol} (hneq: data ≠ data') : ¬ (sol.L₀'_pair data).1 ≈ (sol.L₀'_pair data').1 ∧ ¬ (sol.L₀'_pair data).2 ≈ (sol.L₀'_pair data').2 := by
+lemma PartialSolution_with_axioms.L₀'_no_collide_2 {sol: PartialSolution_with_axioms} {data data' : L₀'_data sol}
+    (hneq: data ≠ data') :
+    ¬ (sol.L₀'_pair data).1 ≈ (sol.L₀'_pair data').1 ∧ ¬ (sol.L₀'_pair data).2 ≈ (sol.L₀'_pair data').2 := by
   rcases data with ⟨⟩ | ⟨⟩ | ⟨a,ha⟩ | ⟨a,ha⟩ | ⟨y,z,hz⟩
   all_goals rcases data' with ⟨⟩ | ⟨⟩ | ⟨a',ha'⟩ | ⟨a',ha'⟩ | ⟨y',z',hz'⟩
   all_goals try simp at hneq
@@ -1135,7 +1161,8 @@ lemma PartialSolution_with_axioms.L₀'_no_collide_2 {sol: PartialSolution_with_
     exact sol.d_injective h.symm
   simp [h]
 
-lemma PartialSolution_with_axioms.L₀'_no_collide_3 (sol: PartialSolution_with_axioms) (data data' : L₀'_data sol) : ¬ (sol.L₀'_pair data).1 ≈ (sol.L₀'_pair data').2 := by
+lemma PartialSolution_with_axioms.L₀'_no_collide_3 (sol: PartialSolution_with_axioms) (data data' : L₀'_data sol) :
+    ¬ (sol.L₀'_pair data).1 ≈ (sol.L₀'_pair data').2 := by
   rcases data with ⟨⟩ | ⟨⟩ | ⟨a,ha⟩ | ⟨a,ha⟩ | ⟨y,z,hz⟩
   all_goals rcases data' with ⟨⟩ | ⟨⟩ | ⟨a',ha'⟩ | ⟨a',ha'⟩ | ⟨y',z',hz'⟩
   all_goals simp [PartialSolution_with_axioms.L₀'_pair,R']
@@ -1202,57 +1229,62 @@ lemma zpow_of_e_inj (a : SM) : Function.Injective (fun n:ℤ ↦ (e a)^n) :=
   injective_zpow_iff_not_isOfFinOrder.mpr (FreeGroup.infinite_order _ (FreeGroup.of_ne_one a))
 
 
-noncomputable abbrev PartialSolution_with_axioms.L₀'_embed (sol: PartialSolution_with_axioms) : (L₀'_data sol) × ℤ × Bool ↪ N := {
-    toFun := fun input ↦ match input with
-    | (data, n, true) => (e 0)^n * (sol.L₀'_pair data).1
-    | (data, n, false) => (e 0)^n * (sol.L₀'_pair data).2
-    inj' := by
-      intro (data,n,b) (data',n',b') h
-      by_cases hb:b
-      · by_cases hb':b'
-        · simp [hb, hb'] at h ⊢
-          have : (sol.L₀'_pair data).1 ≈ (sol.L₀'_pair data').1 := calc
-            _ ≈ (e 0)^n * (sol.L₀'_pair data).1 := rel_of_mul _ n
-            _ ≈ (e 0)^n' * (sol.L₀'_pair data').1 := by rw [h]
-            _ ≈ _ := Setoid.symm <| rel_of_mul _ n'
-          have heq : data = data' := by
-            contrapose! this
-            exact (sol.L₀'_no_collide_2 this).1
-          simp [heq] at h ⊢
-          exact zpow_of_e_inj 0 h
-        simp [hb, hb'] at h ⊢
-        have : (sol.L₀'_pair data).1 ≈ (sol.L₀'_pair data').2 := calc
-            _ ≈ (e 0)^n * (sol.L₀'_pair data).1 := rel_of_mul _ n
-            _ ≈ (e 0)^n' * (sol.L₀'_pair data').2 := by rw [h]
-            _ ≈ _ := Setoid.symm <| rel_of_mul _ n'
-        exact sol.L₀'_no_collide_3 _ _ this
-      by_cases hb':b'
-      · simp [hb, hb'] at h
-        simp [hb, hb'] at h ⊢
-        have : (sol.L₀'_pair data).2 ≈ (sol.L₀'_pair data').1 := calc
-            _ ≈ (e 0)^n * (sol.L₀'_pair data).2 := rel_of_mul _ n
-            _ ≈ (e 0)^n' * (sol.L₀'_pair data').1 := by rw [h]
-            _ ≈ _ := Setoid.symm <| rel_of_mul _ n'
-        exact sol.L₀'_no_collide_3 _ _ <| Setoid.symm this
+noncomputable abbrev PartialSolution_with_axioms.L₀'_embed (sol: PartialSolution_with_axioms) :
+    (L₀'_data sol) × ℤ × Bool ↪ N := {
+  toFun := fun input ↦ match input with
+  | (data, n, true) => (e 0)^n * (sol.L₀'_pair data).1
+  | (data, n, false) => (e 0)^n * (sol.L₀'_pair data).2
+  inj' := by
+    intro (data,n,b) (data',n',b') h
+    by_cases hb:b
+    · by_cases hb':b'
+      · simp [hb, hb'] at h ⊢
+        have : (sol.L₀'_pair data).1 ≈ (sol.L₀'_pair data').1 := calc
+          _ ≈ (e 0)^n * (sol.L₀'_pair data).1 := rel_of_mul _ n
+          _ ≈ (e 0)^n' * (sol.L₀'_pair data').1 := by rw [h]
+          _ ≈ _ := Setoid.symm <| rel_of_mul _ n'
+        have heq : data = data' := by
+          contrapose! this
+          exact (sol.L₀'_no_collide_2 this).1
+        simp [heq] at h ⊢
+        exact zpow_of_e_inj 0 h
       simp [hb, hb'] at h ⊢
-      have : (sol.L₀'_pair data).2 ≈ (sol.L₀'_pair data').2 := calc
-        _ ≈ (e 0)^n * (sol.L₀'_pair data).2 := rel_of_mul _ n
-        _ ≈ (e 0)^n' * (sol.L₀'_pair data').2 := by rw [h]
-        _ ≈ _ := Setoid.symm <| rel_of_mul _ n'
-      have heq : data = data' := by
-        contrapose! this
-        exact (sol.L₀'_no_collide_2 this).2
-      simp [heq] at h ⊢
-      exact zpow_of_e_inj 0 h
+      have : (sol.L₀'_pair data).1 ≈ (sol.L₀'_pair data').2 := calc
+          _ ≈ (e 0)^n * (sol.L₀'_pair data).1 := rel_of_mul _ n
+          _ ≈ (e 0)^n' * (sol.L₀'_pair data').2 := by rw [h]
+          _ ≈ _ := Setoid.symm <| rel_of_mul _ n'
+      exact sol.L₀'_no_collide_3 _ _ this
+    by_cases hb':b'
+    · simp [hb, hb'] at h
+      simp [hb, hb'] at h ⊢
+      have : (sol.L₀'_pair data).2 ≈ (sol.L₀'_pair data').1 := calc
+          _ ≈ (e 0)^n * (sol.L₀'_pair data).2 := rel_of_mul _ n
+          _ ≈ (e 0)^n' * (sol.L₀'_pair data').1 := by rw [h]
+          _ ≈ _ := Setoid.symm <| rel_of_mul _ n'
+      exact sol.L₀'_no_collide_3 _ _ <| Setoid.symm this
+    simp [hb, hb'] at h ⊢
+    have : (sol.L₀'_pair data).2 ≈ (sol.L₀'_pair data').2 := calc
+      _ ≈ (e 0)^n * (sol.L₀'_pair data).2 := rel_of_mul _ n
+      _ ≈ (e 0)^n' * (sol.L₀'_pair data').2 := by rw [h]
+      _ ≈ _ := Setoid.symm <| rel_of_mul _ n'
+    have heq : data = data' := by
+      contrapose! this
+      exact (sol.L₀'_no_collide_2 this).2
+    simp [heq] at h ⊢
+    exact zpow_of_e_inj 0 h
   }
 
-noncomputable abbrev PartialSolution_with_axioms.L₀'_pre_embed_base (sol: PartialSolution_with_axioms) (input: L₀'_data sol × Bool) : N := match input with
+noncomputable abbrev PartialSolution_with_axioms.L₀'_pre_embed_base (sol: PartialSolution_with_axioms)
+    (input: L₀'_data sol × Bool) : N :=
+  match input with
     | (data, true) => (sol.L₀'_pair data).1
     | (data, false) => (sol.L₀'_pair data).2
 
-lemma PartialSolution_with_axioms.L₀'_pre_embed_base_eq (sol: PartialSolution_with_axioms) (data: L₀'_data sol) (b: Bool) : sol.L₀'_pre_embed_base (data, b) = sol.L₀'_embed (data,0,b) := match b with
-  | true => by simp
-  | false => by simp
+lemma PartialSolution_with_axioms.L₀'_pre_embed_base_eq (sol: PartialSolution_with_axioms)
+    (data: L₀'_data sol) (b: Bool) : sol.L₀'_pre_embed_base (data, b) = sol.L₀'_embed (data,0,b) :=
+  match b with
+    | true => by simp
+    | false => by simp
 
 noncomputable abbrev PartialSolution_with_axioms.L₀'_pre_embed (sol: PartialSolution_with_axioms) : L₀'_data sol × Bool ↪ N := {
     toFun := sol.L₀'_pre_embed_base
@@ -1306,11 +1338,12 @@ lemma PartialSolution_with_axioms.mem_new_predom' (sol : PartialSolution_with_ax
     exact sol.L₀'_pre_embed.attains_image (data, false)
 
 /- Construction of the new `op`·  Each op_data object `data` produces an instance of the operation `op`: `sol.op (op_triple d₀ d data).1 (op_triple d₀ d data).2.1 = (op_triple d₀ d data).2.2· -/
-noncomputable abbrev PartialSolution_with_axioms.op_triple (sol : PartialSolution_with_axioms) : op_data sol → N × N × M := fun data ↦ match data with
-  | op_data.old y z _hop => (y, z, sol.op y z)
-  | op_data.v => (sol.x, sol.x, Sum.inl sol.d₀)
-  | op_data.P₁ y z _hI => (z, sol.x, Sum.inr <| (R' (S sol.d₀)).symm <| e <| sol.d y z)
-  | op_data.P₂ y z _hI _hz => ((R' (S sol.d₀)).symm <| e <| sol.d y z, z, Sum.inr <| (R' (S (sol.S' z))).symm <| sol.L₀' <| R' 0 <| R' (sol.S' z) x)
+noncomputable abbrev PartialSolution_with_axioms.op_triple (sol : PartialSolution_with_axioms) : op_data sol → N × N × M :=
+  fun data ↦ match data with
+    | op_data.old y z _hop => (y, z, sol.op y z)
+    | op_data.v => (sol.x, sol.x, Sum.inl sol.d₀)
+    | op_data.P₁ y z _hI => (z, sol.x, Sum.inr <| (R' (S sol.d₀)).symm <| e <| sol.d y z)
+    | op_data.P₂ y z _hI _hz => ((R' (S sol.d₀)).symm <| e <| sol.d y z, z, Sum.inr <| (R' (S (sol.S' z))).symm <| sol.L₀' <| R' 0 <| R' (sol.S' z) x)
 
 noncomputable abbrev PartialSolution_with_axioms.op_embed (sol : PartialSolution_with_axioms) : op_data sol ↪ N × N := {
     toFun := fun data ↦ ((sol.op_triple data).1, (sol.op_triple data).2.1)

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e2e51a0e33b348f7cd11a3cdd5fa5d695f17f596",
+   "rev": "a83204ac13fd058983747480f63d5a3eaf588ff8",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a91df8da4ca1c8e0a80c0807f2c1e8a9ea9011e2",
+   "rev": "6ea68a87c1a3887fc0a9150cec021206d5a0d024",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c",
+   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "417f5fba2ea46d1117c5a8d795d383062b02688e",
+   "rev": "a1cfb751fd148b5dedfc3ebe2f638d71d7ecad0c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1a8afbb6f95c4de139dca63cc7454862cb54099a",
+   "rev": "233a67fdba5cb0ff0e2136d7eded5fb29916dc2b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.20.0-rc5
+leanprover/lean4:v4.20.0-rc5