LeanSolver code for creating an affine transformation matrix from 4 points.

affine.lean

import tactic

def transform : ℚ × ℚ × ℚ × ℚ × ℚ × ℚ → ℚ × ℚ → ℚ × ℚ
| (a, b, c, d, e, f) (x, y) := ((a * x + b * y + c) / (0 * x + 0 * y + 1), (d * x + e * y + f) / (0 * x + 0 * y + 1))

def xy : ℚ × ℚ := (0, 0)
def xy' : ℚ × ℚ := (0, 1)
def x'y' : ℚ × ℚ := (1, 1)
def x'y : ℚ × ℚ := (1, 0)


example (x1 y1 x2 y2 x3 y3 x4 y4 a b c d e f : ℚ)
  : transform (a, b, c, d, e, f) xy = (x1, y1)
  ∧ transform (a, b, c, d, e, f) xy' = (x2, y2)
  ∧ transform (a, b, c, d, e, f) x'y' = (x3, y3)
  ∧ transform (a, b, c, d, e, f) x'y = (x4, y4)
  → false :=

begin
  unfold xy xy' x'y' x'y transform,
  simp only [mul_one, mul_neg, mul_zero, add_zero, zero_add, prod.ext_iff],
  rintros ⟨⟨h1, h2⟩, ⟨h3, h4⟩, ⟨h5, h6⟩, ⟨h7, h8⟩⟩,
  rw div_eq_iff at *,
  rotate, sorry, sorry, sorry, sorry, sorry, sorry, sorry, sorry,
  simp only [mul_one] at *,
  rw h1 at h3 h5 h7,
  rw h2 at h4 h6 h8,
  rw ← eq_sub_iff_add_eq at h7,
  rw h7 at h5,
  rw ← eq_sub_iff_add_eq at h3,
  rw h3 at h5,
  rw ← eq_sub_iff_add_eq at h8,
  rw h8 at h6,
  rw ← eq_sub_iff_add_eq at h4,
  rw h4 at h6,
  --- Solution for a-f given.
  sorry,
end