matrix.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 : ℚ × ℚ := (1, 1)
def xy' : ℚ × ℚ := (1, -1)
def x'y' : ℚ × ℚ := (-1, -1)
def x'y : ℚ × ℚ := (-1, 1)

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_eq_neg_mul_symm, 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,
  -- solve for a
  rw [← eq_sub_iff_add_eq, sub_eq_add_neg, ← eq_sub_iff_add_eq, sub_eq_add_neg] at h1,
  rw h1 at h3 h5 h7,
  -- solve for b
  rw (by ring : x1 * (g + h + i) + -c + -b + -b + c = -((b * 2) + -(x1 * (g + h + i)))) at h3,
  rw [neg_eq_iff_neg_eq, eq_comm, add_neg_eq_iff_eq_add, add_comm, ← eq_div_iff] at h3,
  rotate, sorry,
  rw h3 at h7,
  --solve for c
  rw (by ring : -(x1 * (g + h + i) + -c + -b) + -b + c = c * 2 + -(x1 * (g + h + i))) at h5,
  rw [add_neg_eq_iff_eq_add, add_comm, ← eq_div_iff] at h5,
  rotate, sorry,
  rw h5 at h7,
  -- solve for d
  rw [← eq_sub_iff_add_eq, sub_eq_add_neg, ← eq_sub_iff_add_eq, sub_eq_add_neg] at h2,
  rw h2 at h4 h6 h8,
  -- solve for e
  rw (by ring : y1 * (g + h + i) + -f + -e + -e + f = -((e * 2) + -(y1 * (g + h + i)))) at h4,
  rw [neg_eq_iff_neg_eq, eq_comm, add_neg_eq_iff_eq_add, add_comm, ← eq_div_iff] at h4,
  rotate, sorry,
  rw h4 at h8,
  -- solve for f
  rw (by ring : -(y1 * (g + h + i) + -f + -e) + -e + f = f * 2 + -(y1 * (g + h + i))) at h6,
  rw [add_neg_eq_iff_eq_add, add_comm, ← eq_div_iff] at h6,
  rotate, sorry,
  rw h6 at h8,
  -- solve for g
  rw (by ring : -(x1 * (g + h + i) + -((x1 * (g + h + i) + x3 * (-g + -h + i)) / 2) + -((x1 * (g + h + i) + -(x2 * (g + -h + i))) / 2)) + (x1 * (g + h + i) + -(x2 * (g + -h + i))) / 2 + (x1 * (g + h + i) + x3 * (-g + -h + i)) / 2 = x1 * (g + h + i) + x3 * (-g + -h + i) + -(x2 * (g + -h + i))) at h7,
  rw [← add_neg_eq_zero] at h7,
  simp only [left_distrib, neg_add, ← add_assoc] at h7,
  rw [← eq_add_neg_iff_add_eq, ← eq_add_neg_iff_add_eq, add_comm] at h7,
  simp only [← add_assoc] at h7,
  rw [← eq_add_neg_iff_add_eq, ← eq_add_neg_iff_add_eq, add_comm] at h7,
  simp only [← add_assoc] at h7,
  rw [← eq_add_neg_iff_add_eq, ← eq_add_neg_iff_add_eq, add_comm] at h7,
  simp only [← add_assoc] at h7,
  rw [← eq_add_neg_iff_add_eq, ← eq_add_neg_iff_add_eq, add_comm] at h7,
  simp only [← add_assoc] at h7,
  simp only [zero_add, mul_neg_eq_neg_mul_symm, neg_neg, neg_mul_eq_neg_mul] at h7,
  rw (by ring : x4 * i + x4 * h + x2 * i + -x2 * h + -x3 * i + x3 * h + -x1 * i + -x1 * h = -x1 * h + -x2 * h + x3 * h + x4 * h + (-x1 * i + x2 * i + -x3 * i + x4 * i)) at h7,
  simp_rw [← right_distrib, add_right_comm x1] at h7,
  -- solve for h
  rw (by ring : -(y1 * (g + h + i) + -((y1 * (g + h + i) + y3 * (-g + -h + i)) / 2) + -((y1 * (g + h + i) + -(y2 * (g + -h + i))) / 2)) + (y1 * (g + h + i) + -(y2 * (g + -h + i))) / 2 + (y1 * (g + h + i) + y3 * (-g + -h + i)) / 2 = y1 * (g + h + i) + y3 * (-g + -h + i) + -(y2 * (g + -h + i))) at h8,
  rw [← add_neg_eq_zero] at h8,
  simp only [left_distrib, neg_add, ← add_assoc] at h8,
  rw [← eq_add_neg_iff_add_eq, ← eq_add_neg_iff_add_eq, add_comm] at h8,
  simp only [← add_assoc] at h8,
  rw [← eq_add_neg_iff_add_eq, ← eq_add_neg_iff_add_eq, add_comm] at h8,
  simp only [← add_assoc] at h8,
  rw [← eq_add_neg_iff_add_eq, ← eq_add_neg_iff_add_eq, add_comm] at h8,
  simp only [← add_assoc] at h8,
  rw [← eq_add_neg_iff_add_eq, ← eq_add_neg_iff_add_eq, add_comm] at h8,
  simp only [← add_assoc] at h8,
  simp only [zero_add, mul_neg_eq_neg_mul_symm, neg_neg, neg_mul_eq_neg_mul] at h8,
  rw (by ring : y4 * i + y4 * h + y2 * i + -y2 * h + -y3 * i + y3 * h + -y1 * i + -y1 * h = -y1 * h + -y2 * h + y3 * h + y4 * h + (-y1 * i + y2 * i + -y3 * i + y4 * i)) at h8,
  simp_rw [← right_distrib, add_right_comm y1] at h8,
  -- finish g and h
  generalize j_def : x1 + -x2 + -x3 + x4 = j,
  generalize k_def : -x1 + -x2 + x3 + x4 = k,
  generalize l_def : -x1 + x2 + -x3 + x4 = l,
  generalize m_def : y1 + -y2 + -y3 + y4 = m,
  generalize n_def : -y1 + -y2 + y3 + y4 = n,
  generalize o_def : -y1 + y2 + -y3 + y4 = o,
  simp_rw [j_def, k_def, l_def, m_def, n_def, o_def] at h7 h8,
  rw [mul_comm, ← eq_div_iff] at h7,
  rotate, sorry,
  rw h7 at h8,
  rw [mul_div_assoc', div_eq_iff, mul_comm _ j] at h8,
  rotate, sorry,
  simp only [left_distrib, ← mul_assoc] at h8,
  rw [← eq_add_neg_iff_add_eq, add_assoc, add_comm, ← add_neg_eq_iff_eq_add] at h8,
  simp only [neg_mul_eq_neg_mul, ← right_distrib] at h8,
  rw [mul_comm, ← eq_div_iff] at h8,
  rotate, sorry,
  -- clean up
  simp only [← neg_mul_eq_neg_mul] at h8,
  simp only [← sub_eq_add_neg] at *,
  sorry,
end

19:2: error:
unknown identifier 'mul_neg_eq_neg_mul_symm'
state:
x1 y1 x2 y2 x3 y3 x4 y4 a b c d e f g h i : ℚ
⊢ ((a * 1 + b * 1 + c) / (g * 1 + h * 1 + i), (d * 1 + e * 1 + f) / (g * 1 + h * 1 + i)) = (x1, y1) ∧
    ((a * 1 + b * -1 + c) / (g * 1 + h * -1 + i), (d * 1 + e * -1 + f) / (g * 1 + h * -1 + i)) = (x2, y2) ∧
      ((a * -1 + b * -1 + c) / (g * -1 + h * -1 + i), (d * -1 + e * -1 + f) / (g * -1 + h * -1 + i)) = (x3, y3) ∧
        ((a * -1 + b * 1 + c) / (g * -1 + h * 1 + i), (d * -1 + e * 1 + f) / (g * -1 + h * 1 + i)) = (x4, y4) →
  false

https://leanprover-community.github.io/lean-web-editor/#url=https%3A%2F%2Fgist.githubusercontent.com%2Fkendfrey%2F28c49ebc1c28e543ca6322e167fb8fd8%2Fraw%2F1460cf2ca2d0c0bb35d4f73ac00994265f7768c0%2Fmatrix.lean

leanprover-community/mathlib#11925

mul_neg_eq_neg_mul_symm -> mul_neg
neg_mul_eq_neg_mul -> neg_mul