Multiplying both halves of a fraction (Lean 4)

Stream: new members

[Jeremy Tan]

How can I do this proof (if possible, using calc mode)?

theorem xxx (m n : ℚ) (hm : m ≠ 0) : 2 * (n / m) / (1 + (n / m) ^ 2)
    = 2 * m * n / (m ^ 2 + n ^ 2) := by
    (_)

[Jeremy Tan]

Somehow I need to multiply both halves of the fraction by m ^ 2 and then expand both halves. What's the best way to do this

[Eric Wieser]

tactic#field_simp, maybe?

[Ruben Van de Velde]

You could start with

theorem xxx (m n : ℚ) (hm : m ≠ 0) : 2 * (n / m) / (1 + (n / m) ^ 2)
    = 2 * m * n / (m ^ 2 + n ^ 2) := by
  rw [←mul_left_inj' (pow_ne_zero 2 hm)]
  sorry

[Michael Stoll]

If you give field_simp the information that m^2 + n^2 is nonzero, then field_simp; ring should work (untested, but it worked for me in similar cases in Lean 3).

[Jeremy Tan]

Actually the context for this question is !4#3022

[Jeremy Tan]

so at line 512 I have hv2 : v = 2 * m * n / ((m : ℚ) ^ 2 + (n : ℚ) ^ 2), and I do have the fact that m^2 + n^2 != 0

[Jeremy Tan]

but if I try field_simp (after rewriting v, see below) it somehow expands into a jumble of x y zs

[Jeremy Tan]

It's easy to calc from v to 2 * (n / m) / (1 + (n / m) ^ 2), and this is where the original question came from

[Michael Stoll]

You could state the identity you want as a have help : \forall (m n : rat) (hm : m \ne 0), ... = ... and prove this by establishing m^2 + n^2 \ne 0, then field_simp; ring, and use help to prove the calc step.

[Michael Stoll]

This avoids m and n to be replaced by their definitions.

[Jeremy Tan]

It doesn't work though, the field_simp doesn't clear all denominators:

import Mathlib.Algebra.Field.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.FieldSimp

theorem helper (j k : ℚ) (h₁ : k ≠ 0) (h₂ : j ^ 2 + k ^ 2 ≠ 0) :
    2 * (j / k) / (1 + (j / k) ^ 2) = 2 * j * k / (j ^ 2 + k ^ 2) := by
  field_simp
  ring

[Eric Wieser]

Does it work in Lean3?

[Michael Stoll]

You also need k * (k ^ 2 + j ^ 2) ≠ 0 (note the swapping of the summands).

[Michael Stoll]

(Tested in Lean 3.)

[Michael Stoll]

theorem helper (j k : ℚ) (h₁ : k ≠ 0) (h₂ : j ^ 2 + k ^ 2 ≠ 0) :
    2 * (j / k) / (1 + (j / k) ^ 2) = 2 * j * k / (j ^ 2 + k ^ 2) :=
begin
  have h₃ : k * (k ^ 2 + j ^ 2) ≠ 0 := mul_ne_zero h₁ (by rwa add_comm at h₂),
  field_simp,
  ring
end

[Jeremy Tan]

OK I've made some progress:

have helper {j k : ℚ} (h₁ : k ≠ 0) (h₂ : j ^ 2 + k ^ 2 ≠ 0) :
      2 * (j / k) / (1 + (j / k) ^ 2) = 2 * j * k / (j ^ 2 + k ^ 2) :=
    have h₃ : k * (k ^ 2 + j ^ 2) ≠ 0 := mul_ne_zero h₁ (by rwa [add_comm] at h₂)
    by field_simp; ring
  have hv2 : v = 2 * m * n / ((m : ℚ) ^ 2 + (n : ℚ) ^ 2) := by
    calc
      v = 2 * q / (1 + q ^ 2) := by apply ht4.1
      _ = 2 * (n / m) / (1 + (↑n / ↑m) ^ 2) := by rw [hq2]
      _ = _ := by exact helper (Rat.cast_ne_zero.mpr hm0) hm2n20

There's just one little nit left for this part

[Jeremy Tan]

The known hypothesis hm0 : m != 0 has m an integer, whereas the helper needs m to be a rational

[Jeremy Tan]

how can I get (m : Rat) != 0 from (m : Int) != 0 (the Rat.cast... part is the only thing not working)?

[Eric Wieser]

Nat.cast_ne_zero.mpr not Rat.cast_ne_zero.mpr

[Eric Wieser]

It refers to the type being cast _from_

[Eric Wieser]

Though that doesn't seem to help

[Eric Wieser]

I pushed some unrelated fixes to that PR

[Michael Stoll]

Int.cast_ne_zero.mpr? docs4#Int.cast_ne_zero

[Jeremy Tan]

@Michael Stoll that indeed worked (with the usual tweaking of arguments to fit the actual context)