Lean Code for the Unit Square transformation from points (x1,x1), (x2,y2), (x3,y3), (x4,y4) to (0,0), (0,1), (1,1), (1,0).

unitsquare.lean

import tactic

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

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 g h i : ℚ)
  : transform (a, b, c, d, e, f, g, h, i) xy = (x1, y1)
  ∧ transform (a, b, c, d, e, f, g, h, i) xy' = (x2, y2)
  ∧ transform (a, b, c, d, e, f, g, h, i) x'y' = (x3, y3)
  ∧ transform (a, b, c, d, e, f, g, h, i) 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,
  -- solve for g and h
  rw [← add_neg_eq_zero] at h5 h6,
  simp only [left_distrib] at h5 h6,

  rw (by ring: x4 * g + x4 * i - x1 * i + (x2 * h + x2 * i - x1 * i) + x1 * i + -(x3 * g + x3 * h + x3 * i) = g * (x4 - x3) + -(-i * (x4 - x3 + x2 - x1) - h * (x2 - x3)))  at h5,
  rw (by ring: y4 * g + y4 * i - y1 * i + (y2 * h + y2 * i - y1 * i) + y1 * i + -(y3 * g + y3 * h + y3 * i) = h * (y2 - y3) + -(-i * (y4 - y3 + y2 - y1) - g * (y4 - y3)))  at h6,
  rw [add_neg_eq_iff_eq_add] at h5 h6,
  rw [← eq_div_iff] at h5 h6,
  rotate, sorry, sorry,
  rw (by ring: (0 + (-i * (y4 - y3 + y2 - y1) - g * (y4 - y3))) / (y2 - y3) = i * ((-y4 + y3 - y2 + y1) / (y2 - y3)) - g * ((y4 - y3) / (y2 - y3))) at h6, 
  rw (by ring: (0 + (-i * (x4 - x3 + x2 - x1) - h * (x2 - x3))) / (x4 - x3) = i * ((-x4 + x3 - x2 + x1) / (x4 - x3)) - h * ((x2 - x3) / (x4 - x3))) at h5,
  generalize j_def: (-y4 + y3 - y2 + y1) / (y2 - y3) = j,
  generalize k_def: (-x4 + x3 - x2 + x1) / (x4 - x3) = k,
  generalize m_def: (y4 - y3) / (y2 - y3) = m,
  generalize n_def: (x2 - x3) / (x4 - x3) = n,
  rw [j_def] at h6,
  rw [m_def] at h6,
  rw [k_def] at h5,
  rw [n_def] at h5,
  have h9 : h = i * j - g * m,
  sorry,
  --  inplace rewrite h5 into h6 and vice-versa.
  rw h5 at h6,
  rw h9 at h5,
  rw [← add_neg_eq_zero] at h5 h6,
  rw (by ring: h + -(i * j - (i * k - h * n) * m) =  h * (1 - n * m) + -(-(i * (k * m - j)))) at h6,
  rw (by ring: g + -(i * k - (i * j - g * m) * n) =  g * (1 - m * n) + -(-(i * (j * n - k)))) at h5,
  rw ← eq_sub_iff_add_eq at h5 h6,
  rw [← eq_div_iff] at h5 h6,
  rotate, sorry, sorry,
  simp at h5 h6,
  rw (by ring: -(i * (k * m - j)) / (1 - n * m) = i * (j - k * m) / (1 - m * n)) at h6,
  rw (by ring: -(i * (j * n - k)) / (1 - m * n) = i * (k - j * n) / (1 - m * n)) at h5,
  sorry,
end

https://leanprover-community.github.io/lean-web-editor/#url=https%3A%2F%2Fgist.githubusercontent.com%2Ftatarize%2Ff4361ebdd563de07d76ec5cb5226122d%2Fraw%2F077066a6cecb785ad5c1d5a3d376b86b605e39ba%2Funitsquare.lean

        i = 1
        try:
            j = (y1 - y2 + y3 - y4) / (y2 - y3)
            k = (x1 - x2 + x3 - x4) / (x4 - x3)
            m = (y4 - y3) / (y2 - y3)
            n = (x2 - x3) / (x4 - x3)

            h = i * (j - k * m) / (1 - m * n)
            g = i * (k - j * n) / (1 - m * n)
        except ZeroDivisionError:
            h = 0.0
            g = 0.0

        c = x1 * i
        f = y1 * i
        a = x4 * (g + i) - x1 * i
        b = x2 * (h + i) - x1 * i
        d = y4 * (g + i) - y1 * i
        e = y2 * (h + i) - y1 * i