simple

Stream: new members

[edklencl]

import Mathlib.Tactic
import Mathlib.Data.Real.Sqrt
example (m n k : ℕ) (h : m ≤ n) : n^2 - m^2 = (n-m)*(n+m):=
by
  have hk : ∃ k, n = m + k
  · use n-m
  obtain ⟨k,hk⟩:=hk
  have : (m+k)^2 = m^2 + (2*m*k + k^2)
  · sorry
  sorry

[edklencl]

why does ring cant help

[Riccardo Brasca]

ring can prove you first sorry. It is not designed to work with natural subtraction, so it is no surprisingly it cannot finish the proof of hk. You can use omega or zify [h]; ring for that.

[BANGJI HU]

can you be more specific

[BANGJI HU]

import Mathlib.Tactic
import Mathlib.Data.Real.Sqrt

example (m n : ℕ) (h : m ≤ n) : n^2 - m^2 = (n-m)*(n+m):=
by
  have hk : ∃ k, n = m + k
  use n-m
  have : (m+k)^2 = m^2 + (2*m*k + k^2)
  ring
  zify [h]
  ring
  rw [Nat.pow_two_sub_pow_two]
  rw [Nat.mul_comm]

[BANGJI HU]

thanks

[Riccardo Brasca]

You can also do

import Mathlib

example (m n : ℕ) (h : m ≤ n) : n^2 - m^2 = (n-m)*(n+m):= by
  have h' : m^2 ≤ n^2 := Nat.pow_le_pow_of_le_left h 2 --find by exact?
  zify [h, h']
  ring

[BANGJI HU]

what does zify stand for

[Yaël Dillies]

It means "ℤ-ify", as in "turn into ℤ"

[BANGJI HU]

(deleted)