InfModel: Add another Austin pair

commentary/Equation206.md

@@ -1,3 +1 @@
-Discussed [here](https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/1648.20!.3D.3E.20206).  It implies [Equation 1648](https://teorth.github.io/equational_theories/implications/?1648) for finite magmas.  For infinite magmas, the implication appears to be false, with [one construction based on the infinite 3-regular tree](https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/1648.20!.3D.3E.20206/near/476985846).
-
-It remains open whether 1648 implies 206 for finite magmas.
+Discussed [here](https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/1648.20!.3D.3E.20206).  It implies [Equation 1648](https://teorth.github.io/equational_theories/implications/?1648) for finite magmas. For infinite magmas, the implication is false, with [one construction based on the infinite 3-regular tree](https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/1648.20!.3D.3E.20206/near/476985846).

equational_theories/InfModel.lean

@@ -472,4 +472,23 @@ theorem Equation3588_not_implies_Equation3994 : ∃ (G : Type) (_ : Magma G), Eq
   · have h2 : Equation3994 (Op G') ↔ Equation3588 G' := forall_comm
     rwa [←h2] at h3588
 
+-- Another Austin pair, this one with only two variables in both equations.
+-- https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/1648.20!.3D.3E.20206/near/476842251
+theorem Finite.Equation206_implies_Equation1648 (G : Type*) [Magma G] [Finite G] (h : Equation206 G) : Equation1648 G := by
+  intro x y
+  let S : Set G := Set.univ
+  have m1 : S.MapsTo (· ◇ y) S := by
+    intro
+    simp [S]
+  have t : S.SurjOn (· ◇ y) S := by
+    intro x _
+    let z := x ◇ (x ◇ y)
+    use z
+    simp [S, z]
+    apply Eq.symm (h x y)
+  rw [Set.Finite.surjOn_iff_bijOn_of_mapsTo (Set.toFinite _) m1] at t
+  apply t.injOn (by simp [S]) (by simp [S])
+  simp
+  apply h (x ◇ y)
+
 end InfModel