Stream: new members

Topic: Multiplying both halves of a fraction (Lean 4)

Jeremy Tan (Mar 21 2023 at 16:24):

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 (Mar 21 2023 at 16:25):

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 (Mar 21 2023 at 16:40):

tactic#field_simp, maybe?

Ruben Van de Velde (Mar 21 2023 at 16:44):

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 (Mar 21 2023 at 17:01):

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 (Mar 21 2023 at 17:05):

Actually the context for this question is !4#3022

Jeremy Tan (Mar 21 2023 at 17:06):

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 (Mar 21 2023 at 17:06):

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

Jeremy Tan (Mar 21 2023 at 17:07):

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 (Mar 21 2023 at 17:10):

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 (Mar 21 2023 at 17:10):

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

Jeremy Tan (Mar 21 2023 at 17:37):

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 (Mar 21 2023 at 17:48):

Does it work in Lean3?

Michael Stoll (Mar 21 2023 at 17:49):

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

Michael Stoll (Mar 21 2023 at 17:50):

(Tested in Lean 3.)

Michael Stoll (Mar 21 2023 at 17:50):

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 (Mar 21 2023 at 18:15):

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 (Mar 21 2023 at 18:15):

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

Jeremy Tan (Mar 21 2023 at 18:16):

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

Eric Wieser (Mar 21 2023 at 18:34):

Nat.cast_ne_zero.mpr not Rat.cast_ne_zero.mpr

Eric Wieser (Mar 21 2023 at 18:34):

It refers to the type being cast _from_

Eric Wieser (Mar 21 2023 at 18:35):

Though that doesn't seem to help

Eric Wieser (Mar 21 2023 at 18:35):

I pushed some unrelated fixes to that PR

Michael Stoll (Mar 21 2023 at 18:47):

Int.cast_ne_zero.mpr? docs4#Int.cast_ne_zero

Jeremy Tan (Mar 21 2023 at 19:05):

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

Last updated: Dec 20 2023 at 11:08 UTC