Doubts

Stream: LftCM Bangalore 2025

[Divakaran Divakaran]

Why is the rewrite tactic failing in line 126?
Screenshot 2025-04-28 at 7.48.39 AM.png

[Riccardo Brasca]

Please try to post a #mwe, it's much easier to debug (don't worry to make it really minimal, but please post some working code). In the specific case I think that the problem is that sub_eq_zero says a-b=0 ↔ a = b, so Lean looks for a - b (for some a and b) and it doesn't find anything. Do you want to rewrite in the other direction, using rw [← sub_eq_zero]?

[Riccardo Brasca]

Ah, maybe you want docs#sub_self instead of docs#sub_eq_zero

[Divakaran Divakaran]

Thanks Ricardo. It worked with rw[sub_self].

import MIL.Common
import Mathlib.Data.Real.Basic

example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  rw [mul_sub]
  rw [add_mul]
  rw [add_mul]
  rw [← add_sub]
  rw [← sub_sub]
  rw [mul_comm b a]
  rw [add_sub]
  rw [sub_self]
  rw [add_zero]
  rw [pow_two]
  rw [pow_two]