4-to-4 matrix lean.

4-to-4.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))


example (ax1 ay1 ax2 ay2 ax3 ay3 ax4 ay4 bx1 by1 bx2 by2 bx3 by3 bx4 by4 a b c d e f g h i : ℚ)
  : transform (a, b, c, d, e, f, g, h, i)(ax1, ay1) = (bx1, by1)
  ∧ transform (a, b, c, d, e, f, g, h, i)(ax2, ay2) = (bx2, by2)
  ∧ transform (a, b, c, d, e, f, g, h, i)(ax3, ay3) = (bx3, by3)
  ∧ transform (a, b, c, d, e, f, g, h, i)(ax4, ay4) = (bx4, by4)
→ false :=

begin
  unfold 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⟩⟩,
  sorry,
end