From eb1ee011f38ec7ea092ae486bd730577a80e3ce1 Mon Sep 17 00:00:00 2001 From: Andrii Kurdiumov Date: Sat, 28 Sep 2024 18:12:51 +0500 Subject: [PATCH 1/2] Eq3 implications --- equational_theories/Subgraph.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean index 5e412f36..4e5a0dc7 100644 --- a/equational_theories/Subgraph.lean +++ b/equational_theories/Subgraph.lean @@ -105,9 +105,15 @@ theorem Equation5_implies_Equation4512 (G: Type*) [Magma G] (h: Equation5 G) : E theorem Equation6_implies_Equation2 (G: Type*) [Magma G] (h: Equation6 G) : Equation2 G := fun a _ ↦ by rw [h a a, ← h] +theorem Equation6_implies_Equation3 (G: Type*) [Magma G] (h: Equation6 G) : Equation3 G := + fun a ↦ h a a + theorem Equation7_implies_Equation2 (G: Type*) [Magma G] (h: Equation7 G) : Equation2 G := fun a _ ↦ by rw [h a a a, ← h] +theorem Equation7_implies_Equation3 (G: Type*) [Magma G] (h: Equation7 G) : Equation3 G := + fun a ↦ h a a a + theorem Equation7_implies_Equation41 (G: Type*) [Magma G] (h: Equation7 G) : Equation41 G := fun _ _ _ ↦ by rw [← h] From ce73a89eff460fb775296e700b6832574100ad5c Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 28 Sep 2024 16:45:22 +0200 Subject: [PATCH 2/2] use implicit arguments --- equational_theories/Subgraph.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean index 4e5a0dc7..3af92f94 100644 --- a/equational_theories/Subgraph.lean +++ b/equational_theories/Subgraph.lean @@ -106,13 +106,13 @@ theorem Equation6_implies_Equation2 (G: Type*) [Magma G] (h: Equation6 G) : Equa fun a _ ↦ by rw [h a a, ← h] theorem Equation6_implies_Equation3 (G: Type*) [Magma G] (h: Equation6 G) : Equation3 G := - fun a ↦ h a a + fun _ ↦ h _ _ theorem Equation7_implies_Equation2 (G: Type*) [Magma G] (h: Equation7 G) : Equation2 G := fun a _ ↦ by rw [h a a a, ← h] theorem Equation7_implies_Equation3 (G: Type*) [Magma G] (h: Equation7 G) : Equation3 G := - fun a ↦ h a a a + fun _ ↦ h _ _ _ theorem Equation7_implies_Equation41 (G: Type*) [Magma G] (h: Equation7 G) : Equation41 G := fun _ _ _ ↦ by rw [← h]