From a9301dcb2681d0cdb4cdd833643b9a22a42bd561 Mon Sep 17 00:00:00 2001 From: Franklin Pezzuti Dyer <46753556+franklindyer@users.noreply.github.com> Date: Mon, 7 Oct 2024 01:09:04 -0600 Subject: [PATCH] Metatheorem resolving all consequences of Equation1571 (#341) This is some intermediate work as I work towards #221, which involves a special case of commutative semigroups. But it also includes some metatheorems that could be generally useful for working with associativity. Includes: - a convenience function for fully right-associating any operation tree when the operation is associative - definition and `Magma` instance of a free semigroup - proof that evaluation in any semigroup is a homomorphism - proof that the variable names can be sorted in a free semigroup expression without affecting the evaluated value, so long as the codomain semigroup is commutative - all of this is combined to write a metatheorem `ProveEquation1571Consequence` that *should be* capable of automatically proving any consequence of `Equation1571` Any revisions to shorten my proofs or make the naming/notation more convenient is welcome :-) --------- Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> --- equational_theories/AllEquations.lean | 4 +- equational_theories/Equations.lean | 3 + equational_theories/FreeSemigroup.lean | 194 +++++++++++++++++++++++++ equational_theories/Subgraph.lean | 60 +++++--- 4 files changed, 242 insertions(+), 19 deletions(-) create mode 100644 equational_theories/FreeSemigroup.lean diff --git a/equational_theories/AllEquations.lean b/equational_theories/AllEquations.lean index cc37d9ea..cf0121ab 100644 --- a/equational_theories/AllEquations.lean +++ b/equational_theories/AllEquations.lean @@ -3185,7 +3185,7 @@ equation 3163 := x = (((y ◇ y) ◇ z) ◇ y) ◇ x equation 3164 := x = (((y ◇ y) ◇ z) ◇ y) ◇ y equation 3165 := x = (((y ◇ y) ◇ z) ◇ y) ◇ z equation 3166 := x = (((y ◇ y) ◇ z) ◇ y) ◇ w -equation 3167 := x = (((y ◇ y) ◇ z) ◇ z) ◇ x +-- equation 3167 := x = (((y ◇ y) ◇ z) ◇ z) ◇ x equation 3168 := x = (((y ◇ y) ◇ z) ◇ z) ◇ y equation 3169 := x = (((y ◇ y) ◇ z) ◇ z) ◇ z equation 3170 := x = (((y ◇ y) ◇ z) ◇ z) ◇ w @@ -4674,7 +4674,7 @@ equation 4652 := (x ◇ y) ◇ x = (z ◇ w) ◇ w equation 4653 := (x ◇ y) ◇ x = (z ◇ w) ◇ u equation 4654 := (x ◇ y) ◇ y = (x ◇ y) ◇ z equation 4655 := (x ◇ y) ◇ y = (x ◇ z) ◇ y -equation 4656 := (x ◇ y) ◇ y = (x ◇ z) ◇ z +-- equation 4656 := (x ◇ y) ◇ y = (x ◇ z) ◇ z equation 4657 := (x ◇ y) ◇ y = (x ◇ z) ◇ w equation 4658 := (x ◇ y) ◇ y = (y ◇ x) ◇ x equation 4659 := (x ◇ y) ◇ y = (y ◇ x) ◇ z diff --git a/equational_theories/Equations.lean b/equational_theories/Equations.lean index 92a5da5f..156268e9 100644 --- a/equational_theories/Equations.lean +++ b/equational_theories/Equations.lean @@ -90,6 +90,8 @@ equation 1689 := x = (y ◇ x) ◇ ((x ◇ z) ◇ z) equation 2662 := x = ((x ◇ y) ◇ (x ◇ y)) ◇ x +abbrev Equation3167 (G: Type _) [Magma G] := ∀ x y z : G, x = (((y ◇ y) ◇ z) ◇ z) ◇ x + /-- From Putnam 1978, Problem A4, part (a) -/ equation 3722 := x ◇ y = (x ◇ y) ◇ (x ◇ y) @@ -114,6 +116,7 @@ equation 4579 := x ◇ (y ◇ z) = (w ◇ u) ◇ z /-- all products of three values are the same, regardless bracketing -/ equation 4582 := x ◇ (y ◇ z) = (w ◇ u) ◇ v +abbrev Equation4656 (G: Type _) [Magma G] := ∀ x y z : G, (x ◇ y) ◇ y = (x ◇ z) ◇ z /- Some order 5 laws -/ diff --git a/equational_theories/FreeSemigroup.lean b/equational_theories/FreeSemigroup.lean new file mode 100644 index 00000000..1be24ce2 --- /dev/null +++ b/equational_theories/FreeSemigroup.lean @@ -0,0 +1,194 @@ +import Mathlib.Logic.Basic + +import equational_theories.Equations +import equational_theories.FreeMagma +import equational_theories.Homomorphisms +import equational_theories.MagmaLaw + +open FreeMagma +open Law + +def treeConcat {α : Type _} (t : FreeMagma α) : List α := + match t with + | Lf a => [a] + | (tl ⋆ tr) => treeConcat tl ++ treeConcat tr + +def rightJoinTrees {α : Type _} (t1 t2 : FreeMagma α) : FreeMagma α := + match t1 with + | Lf a => Lf a ⋆ t2 + | (tl ⋆ tr) => tl ⋆ (rightJoinTrees tr t2) + +def rightAssociateTree {α : Type _} (t : FreeMagma α) : FreeMagma α := + match t with + | Lf a => Lf a + | (tl ⋆ tr) => rightJoinTrees (rightAssociateTree tl) (rightAssociateTree tr) + +theorem AssocImpliesForkEquivRightJoin {α : Type _} {G : Type _} [Magma G] + (assoc : Equation4512 G) (f : α → G) (tl tr : FreeMagma α) + : evalInMagma f (tl ⋆ tr) = evalInMagma f (rightJoinTrees tl tr) := + match tl with + | Lf _ => Eq.refl _ + | (tl1 ⋆ tl2) => Eq.trans + (Eq.symm $ assoc (evalInMagma f tl1) (evalInMagma f tl2) (evalInMagma f tr)) + (congrArg (fun t ↦ (evalInMagma f tl1) ◇ t) (AssocImpliesForkEquivRightJoin assoc f tl2 tr)) + +/- Associativity allows us to fully right-associate an entire operation tree -/ +theorem AssocFullyRightAssociate {α : Type _} {G : Type _} [Magma G] + (assoc : Equation4512 G) (f : α → G) (t : FreeMagma α) + : evalInMagma f t = evalInMagma f (rightAssociateTree t) := + match t with + | Lf _ => Eq.refl _ + | (tl ⋆ tr) => Eq.trans + (congrArg (fun s ↦ s ◇ (evalInMagma f tr)) (AssocFullyRightAssociate assoc f tl)) $ Eq.trans + (congrArg (fun s ↦ (evalInMagma f (rightAssociateTree tl)) ◇ s) (AssocFullyRightAssociate assoc f tr)) + (AssocImpliesForkEquivRightJoin assoc f (rightAssociateTree tl) (rightAssociateTree tr)) + +/-- Example usage of AssocFullyRightAssociate -/ +theorem Assoc4 {G : Type _} [Magma G] (assoc : Equation4512 G) + : ∀ x y z w : G, ((x ◇ y) ◇ z) ◇ w = x ◇ (y ◇ (z ◇ w)) := + fun x y z w ↦ AssocFullyRightAssociate + assoc + (fun | 0 => x | 1 => y | 2 => z | 3 => w : Fin 4 → G) + (((Lf 0 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 3) + +inductive FreeSemigroup (α : Type _) + | Singleton : α → FreeSemigroup α + | Cons : α → FreeSemigroup α → FreeSemigroup α + +local postfix:61 ".+" => FreeSemigroup.Singleton +local infixr:60 " ,+ " => FreeSemigroup.Cons + +def semigroupConcat {α : Type _} (s1 s2 : FreeSemigroup α) : FreeSemigroup α := + match s1 with + | a .+ => a ,+ s2 + | a ,+ s1tail => a ,+ (semigroupConcat s1tail s2) + +instance (α : Type _) : Magma (FreeSemigroup α) where + op := semigroupConcat + +theorem FreeSgrAssoc {α : Type} : Equation4512 (FreeSemigroup α) := + fun ls1 ls2 ls3 ↦ match ls1 with + | _ .+ => Eq.refl _ + | a ,+ ls1' => congrArg (fun ls ↦ a ,+ ls) (FreeSgrAssoc ls1' ls2 ls3) + +/- "Flatten" a FreeMagma tree expression into its semigroup representation -/ +def freeMagmaToFreeSgr {α : Type _} : MagmaHom (FreeMagma α) (FreeSemigroup α) where + toFun := fun t ↦ evalInMagma FreeSemigroup.Singleton t + map_op' := fun s _ ↦ match s with + | Lf _ => Eq.refl _ + | _ ⋆ _ => Eq.refl _ + +local postfix:70 " ↠Sgr " => freeMagmaToFreeSgr.toFun + +def evalInSgr {α : Type _} {G : Type _} [Magma G] (f : α → G) (ls : FreeSemigroup α) : G := + match ls with + | a .+ => f a + | a ,+ lstail => f a ◇ evalInSgr f lstail + +def evalInSgrHom {α : Type _} {G : Type _} [Magma G] (assoc : Equation4512 G) (f : α → G) : MagmaHom (FreeSemigroup α) G where + toFun := evalInSgr f + map_op' := let rec mapper : ∀ ls1 ls2 : FreeSemigroup α, evalInSgr f (ls1 ◇ ls2) = evalInSgr f ls1 ◇ evalInSgr f ls2 := + fun ls1 ls2 ↦ match ls1 with + | _ .+ => Eq.refl _ + | a ,+ ls1' => Eq.trans + (congrArg (fun x ↦ f a ◇ x) (mapper ls1' ls2)) + (assoc (f a) (evalInSgr f ls1') (evalInSgr f ls2)) + mapper + +def foldFreeSemigroup {G : Type _} [Magma G] (ls : FreeSemigroup G) : G := + match ls with + | a .+ => a + | a ,+ lstail => a ◇ (foldFreeSemigroup lstail) + +/- When evaluating in an associative structure, we may reduce a FreeMagma tree to a FreeSemigroup list -/ +theorem AssocImpliesSgrProjFaithful {α : Type _} {G : Type _} [Magma G] (assoc : Equation4512 G) (f : α → G) (t : FreeMagma α) + : evalInMagma f t = evalInSgr f (freeMagmaToFreeSgr t) := + match t with + | Lf a => Eq.refl _ + | Lf a ⋆ tr => congrArg (fun y ↦ (f a) ◇ y) (AssocImpliesSgrProjFaithful assoc f tr) + | (tl1 ⋆ tl2) ⋆ tr => by + apply Eq.symm + apply Eq.trans $ congrArg (evalInSgr f) $ freeMagmaToFreeSgr.map_op' (tl1 ⋆ tl2) tr + apply Eq.trans $ congrArg (fun s ↦ evalInSgr f (s ◇ tr ↠Sgr)) $ freeMagmaToFreeSgr.map_op' tl1 tl2 + apply Eq.trans $ (evalInSgrHom assoc f).map_op' (tl1 ↠Sgr ◇ tl2 ↠Sgr) (tr ↠Sgr) + apply Eq.trans $ congrArg (fun s ↦ s ◇ (evalInSgr f (tr ↠Sgr))) $ (evalInSgrHom assoc f).map_op' (tl1 ↠Sgr) (tl2 ↠Sgr) + apply Eq.symm + apply Eq.trans $ congrArg (fun s ↦ _ ◇ s) (AssocImpliesSgrProjFaithful assoc f tr) + apply Eq.trans $ congrArg (fun s ↦ (s ◇ _) ◇ _) (AssocImpliesSgrProjFaithful assoc f tl1) + apply Eq.trans $ congrArg (fun s ↦ (_ ◇ s) ◇ _) (AssocImpliesSgrProjFaithful assoc f tl2) + trivial + +def insertSgrSorted {n : Nat} (i : Fin n) (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) := + match ls with + | j .+ => if i ≤ j then i ,+ j .+ else j ,+ i .+ + | j ,+ lstail => if i ≤ j then i ,+ j ,+ lstail else j ,+ i ,+ lstail + +def insertionSortSgr {n : Nat} (ls : FreeSemigroup (Fin n)) : FreeSemigroup (Fin n) := + match ls with + | i .+ => i .+ + | i ,+ lstail => insertSgrSorted i (insertionSortSgr lstail) + +theorem CommSgrImpliesInsertSortedFaithful {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G) + : ∀ i : Fin n, ∀ ls : FreeSemigroup (Fin n), evalInSgr f (insertSgrSorted i ls) = (f i) ◇ evalInSgr f ls := + fun i ls ↦ match ls with + | j .+ => by + have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j .+) (j ,+ i .+) + cases eqor with + | inl eq1 => apply Eq.trans (congrArg (evalInSgr f) eq1); exact Eq.refl _ + | inr eq2 => apply Eq.trans (congrArg (evalInSgr f) eq2); exact comm (f j) (f i) + | j ,+ lstail => by + have eqor := ite_eq_or_eq (i ≤ j) (i ,+ j ,+ lstail) (j ,+ i ,+ lstail) + cases eqor with + | inl eq1 => + apply Eq.trans (congrArg (evalInSgr f) eq1); + exact Eq.refl _ + | inr eq2 => + apply Eq.trans (congrArg (evalInSgr f) eq2); + apply Eq.trans $ assoc (f j) (f i) _; + rw [comm (f j) (f i)]; + exact Eq.symm $ assoc (f i) (f j) _ + +theorem CommSgrImpliesInsertionSortFaithful {n : Nat} {G : Type _} [Magma G] (assoc : Equation4512 G) (comm : Equation43 G) (f : Fin n → G) + : ∀ ls : FreeSemigroup (Fin n), evalInSgr f ls = evalInSgr f (insertionSortSgr ls) + | _ .+ => Eq.refl _ + | i ,+ lstail => Eq.trans + (congrArg (fun s ↦ (f i) ◇ s) (CommSgrImpliesInsertionSortFaithful assoc comm f lstail)) + (Eq.symm $ CommSgrImpliesInsertSortedFaithful assoc comm f i (insertionSortSgr lstail)) + +def involutionReduce {α : Type _} [DecidableEq α] (ls : FreeSemigroup α) : FreeSemigroup α := + match ls with + | a .+ => a .+ + | a ,+ b .+ => a ,+ b .+ + | a ,+ b ,+ lstail => if (a = b) then involutionReduce lstail else a ,+ involutionReduce (b ,+ lstail) + +def InvolutiveImpliesInvolutionReduceFaithful {α : Type _} [DecidableEq α] {G : Type _} [Magma G] (ls : FreeSemigroup α) (invol : Equation16 G) (f : α → G) + : evalInSgr f ls = evalInSgr f (involutionReduce ls) := + match ls with + | a .+ => Eq.refl _ + | a ,+ b .+ => Eq.refl _ + | a ,+ b ,+ lstail => by + have eqor := dite_eq_or_eq (P := a = b) (A := fun _ ↦ involutionReduce lstail) (B := fun _ ↦ a ,+ involutionReduce (b ,+ lstail)) + cases eqor with + | inl eqcase => + apply Eq.trans $ congrArg (fun s ↦ (f s) ◇ (f b ◇ (evalInSgr f lstail))) eqcase.1 + apply Eq.trans $ Eq.symm $ invol (evalInSgr f lstail) (f b) + apply Eq.trans $ InvolutiveImpliesInvolutionReduceFaithful lstail invol f + exact Eq.symm $ congrArg (evalInSgr f) eqcase.2 + | inr neqcase => + apply Eq.symm + apply Eq.trans $ congrArg (evalInSgr f) neqcase.2 + exact congrArg (fun s ↦ f a ◇ s) $ Eq.symm $ InvolutiveImpliesInvolutionReduceFaithful (b ,+ lstail) invol f + +def equation1571Reducer {n : Nat} (t : FreeMagma (Fin (n+1))) : FreeSemigroup (Fin (n+1)) := + involutionReduce $ insertionSortSgr $ freeMagmaToFreeSgr (t ⋆ (Lf (Fin.last n) ⋆ Lf (Fin.last n))) + +def AbGrpPow2ImpliesEquation1571ReducerFaithful {n : Nat} {G : Type _} [Magma G] (t : FreeMagma (Fin (n+1))) (f : Fin (n+1) → G) + (assoc : Equation4512 G) (comm : Equation43 G) (invol : Equation16 G) + : evalInMagma f t = evalInSgr f (equation1571Reducer t) := by + apply Eq.symm + apply Eq.trans $ Eq.symm $ InvolutiveImpliesInvolutionReduceFaithful _ invol f + apply Eq.trans $ Eq.symm $ CommSgrImpliesInsertionSortFaithful assoc comm f _ + apply Eq.trans $ Eq.symm $ AssocImpliesSgrProjFaithful assoc f _ + apply Eq.trans $ comm (evalInMagma f t) _ + apply Eq.trans $ Eq.symm $ assoc _ _ _ + exact Eq.symm $ invol (evalInMagma f t) (f $ Fin.last n) diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean index 5a389882..a829dcbd 100644 --- a/equational_theories/Subgraph.lean +++ b/equational_theories/Subgraph.lean @@ -4,6 +4,8 @@ import equational_theories.EquationalResult import equational_theories.Closure import equational_theories.Equations import equational_theories.FactsSyntax +import equational_theories.FreeSemigroup +import equational_theories.MagmaLaw /- This is a subproject of the main project to completely describe a small subgraph of the entire implication graph. The list of equations under consideration can be found at https://teorth.github.io/equational_theories/blueprint/subgraph-eq.html @@ -282,44 +284,68 @@ theorem Lemma_eq1689_implies_h8 (G: Type*) [Magma G] (h: Equation1689 G) : ∀ a /-- The below results for Equation1571 are out of order because early ones are lemmas for later ones -/ @[equational_result] -theorem Equation1571_implies_Equation2662 (G: Type*) [Magma G] (h: Equation1571 G) : Equation2662 G := - fun _ _ ↦ (h _ _ _).trans (congrArg _ (h _ _ _).symm) +theorem Equation1571_implies_Equation2662 (G: Type _) [Magma G] (h: Equation1571 G) : Equation2662 G := + fun x y ↦ Eq.trans (h x (x ◇ y) (x ◇ y)) (congrArg (fun z ↦ ((x ◇ y) ◇ (x ◇ y)) ◇ z) + (Eq.symm $ h x x y)) @[equational_result] -theorem Equation1571_implies_Equation40 (G: Type*) [Magma G] (h: Equation1571 G) : Equation40 G := by - have sqRotate (x y z : G) : (x ◇ y) ◇ (x ◇ y) = (y ◇ z) ◇ (y ◇ z) := - (congrArg (fun w ↦ (x ◇ y) ◇ (x ◇ w)) (Equation1571_implies_Equation2662 G h _ _)).trans - (h _ _ _).symm - exact fun x y ↦ h x x x ▸ h y y y ▸ (sqRotate _ _ _).trans (sqRotate _ _ _) +theorem Equation1571_implies_Equation40 (G: Type _) [Magma G] (h: Equation1571 G) : Equation40 G := by + have sqRotate : ∀ x y z : G, (x ◇ y) ◇ (x ◇ y) = (y ◇ z) ◇ (y ◇ z) := + fun x y z ↦ Eq.trans (congrArg (fun w ↦ (x ◇ y) ◇ (x ◇ w)) + (Equation1571_implies_Equation2662 G h y z)) (Eq.symm $ h ((y ◇ z) ◇ (y ◇ z)) x y) + have sqConstInImage : ∀ x y z w : G, (x ◇ y) ◇ (x ◇ y) = (z ◇ w) ◇ (z ◇ w) := + fun x y z w ↦ Eq.trans (sqRotate x y z) (sqRotate y z w) + exact fun x y ↦ h x x x ▸ h y y y ▸ sqConstInImage (x ◇ x) (x ◇ (x ◇ x)) (y ◇ y) (y ◇ (y ◇ y)) @[equational_result] -theorem Equation1571_implies_Equation23 (G: Type*) [Magma G] (h: Equation1571 G) : Equation23 G := by +theorem Equation1571_implies_Equation23 (G: Type _) [Magma G] (h: Equation1571 G) : Equation23 G := by refine fun x ↦ (h x (x ◇ x) (x ◇ x)).trans ?_ rw [← h x x x, ← Equation1571_implies_Equation40 G h x (x ◇ x)] @[equational_result] -theorem Equation1571_implies_Equation8 (G: Type*) [Magma G] (h: Equation1571 G) : Equation8 G := - fun x ↦ (h x x x).trans ((congrArg (· ◇ (x ◇ (x ◇ x))) (Equation1571_implies_Equation40 G h x - (x ◇ (x ◇ x)))).trans (Equation1571_implies_Equation23 G h (x ◇ (x ◇ x))).symm) +theorem Equation1571_implies_Equation8 (G: Type _) [Magma G] (h: Equation1571 G) : Equation8 G := + fun x ↦ Eq.trans (h x x x) (((congrArg (fun a ↦ a ◇ (x ◇ (x ◇ x)))) + (Equation1571_implies_Equation40 G h x (x ◇ (x ◇ x)))).trans + (((Equation1571_implies_Equation23 G h (x ◇ (x ◇ x))).symm).trans rfl)) @[equational_result] -theorem Equation1571_implies_Equation16 (G: Type*) [Magma G] (h: Equation1571 G) : Equation16 G := +theorem Equation1571_implies_Equation16 (G: Type _) [Magma G] (h: Equation1571 G) : Equation16 G := fun x y ↦ ((congrArg (fun w ↦ y ◇ (y ◇ w)) (Equation1571_implies_Equation8 G h x)).trans - (Equation1571_implies_Equation40 G h x y ▸ ((congrArg (· ◇ (y ◇ (x ◇ (y ◇ y))))) - (Equation1571_implies_Equation8 G h y)).trans (h x y (y ◇ y)).symm)).symm + ((Equation1571_implies_Equation40 G h x y ▸ ((congrArg (fun w ↦ w ◇ (y ◇ (x ◇ (y ◇ y))))) + (Equation1571_implies_Equation8 G h y)).trans (h x y (y ◇ y)).symm))).symm @[equational_result] -theorem Equation1571_implies_Equation43 (G: Type*) [Magma G] (h: Equation1571 G) : Equation43 G := by +theorem Equation1571_implies_Equation43 (G: Type _) [Magma G] (h: Equation1571 G) : Equation43 G := by refine fun x y ↦ (h _ (x ◇ x) (x ◇ (x ◇ y))).trans ?_ rw [← h x x y, ← Equation1571_implies_Equation23 G h x, ← Equation1571_implies_Equation16 G h y x, Equation1571_implies_Equation40 G h x y, ← Equation1571_implies_Equation23 G h y] @[equational_result] -theorem Equation1571_implies_Equation4512 (G: Type*) [Magma G] (h: Equation1571 G) : Equation4512 G := by +theorem Equation1571_implies_Equation4512 (G: Type _) [Magma G] (h: Equation1571 G) : Equation4512 G := by refine fun x y z ↦ (h (x ◇ (y ◇ z)) y x).trans ?_ rw [Equation1571_implies_Equation43 G h (x ◇ (y ◇ z)) x, ← Equation1571_implies_Equation16 G h (y ◇ z) x, ← Equation1571_implies_Equation16 G h z y, - Equation1571_implies_Equation43 G h y x] + Equation1571_implies_Equation43 G h y x] + +theorem ProveEquation1571Consequence {n : Nat} {G : Type _} [Magma G] (eq1571 : Equation1571 G) + (law : Law.MagmaLaw (Fin (n+1))) (eq : equation1571Reducer law.lhs = equation1571Reducer law.rhs) + : G ⊧ law := + fun _ ↦ (AbGrpPow2ImpliesEquation1571ReducerFaithful law.lhs _ + (Equation1571_implies_Equation4512 G eq1571) (Equation1571_implies_Equation43 G eq1571) + (Equation1571_implies_Equation16 G eq1571)).trans ((congrArg (evalInSgr _) eq).trans + (AbGrpPow2ImpliesEquation1571ReducerFaithful law.rhs _ + (Equation1571_implies_Equation4512 G eq1571) (Equation1571_implies_Equation43 G eq1571) + (Equation1571_implies_Equation16 G eq1571)).symm) + +/- Example usage of the general-purpose prover ProveEquation1571Consequence -/ +theorem Equation1571_implies_Equation3167 {G : Type} [Magma G] (h : Equation1571 G) : Equation3167 G := + fun x y z ↦ ProveEquation1571Consequence (n := 2) h + {lhs := Lf 0, rhs := (((Lf 1 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 2) ⋆ Lf 0} rfl fun | 0 => x | 1 => y | 2 => z + +/- Example usage of the general-purpose prover ProveEquation1571Consequence -/ +theorem Equation1571_implies_Equation4656 {G : Type} [Magma G] (h : Equation1571 G) : Equation4656 G := + fun x y z ↦ ProveEquation1571Consequence (n := 2) h + {lhs := (Lf 0 ⋆ Lf 1) ⋆ Lf 1, rhs := (Lf 0 ⋆ Lf 2) ⋆ Lf 2} rfl fun | 0 => x | 1 => y | 2 => z /-- This result was first obtained by Kisielewicz in 1997 via computer assistance. -/ @[equational_result]