Simple algebra proof

Stream: new members

[Alex Gu]

I wrote and proved a simple theorem, but it seems to be more complex than it needs to be. Could anybody please help to clean the proof up a bit? Is there a more idiomatic way to do proofs like this? Thanks!

theorem thm2 (x : ℝ) (h : x^2 / (1+x^2) = 2) :
  1/(1+x^2)=-1 := by

  have h1 : 1 - x^2 / (1 + x^2) = 1 - 2 := by
    congr

  have h2 : 1 - x^2 / (1 + x^2) = 1 / (1 + x^2) := by
    have h3 : 1 = (1 + x^2) / (1 + x^2) := by
      rw [div_self]
      have h4 : 1 + x^2 > 0 := by
        apply add_pos_of_pos_of_nonneg
        · norm_num
        · exact sq_nonneg x
      apply ne_of_gt
      exact h4

    conv =>
      lhs
      lhs
      rw [h3]

    rw [← sub_div]
    congr
    ring

  rw [← h2]
  rw [h1]
  norm_num

[Bjørn Kjos-Hanssen]

You can do this:

import Mathlib

theorem thm2 (x : ℝ) (h : x^2 / (1+x^2) = 2) :
  1/(1+x^2)=-1 := by
  exfalso
  have h₀: x^2 ≤ (1 + x^2) := by linarith
  have h₁: 0 ≤ 1 + x^2 := by positivity
  have h₂: x^2 / (1 + x^2) ≤ 1 := div_le_one_of_le₀ h₀ h₁
  aesop

[Alex Gu]

Thanks! Is there a way to do it without magical tactics like aesop?

[Bjørn Kjos-Hanssen]

You can write aesop? instead of aesop to get more details.

[Heather Macbeth]

Alternative automation:

theorem thm2 (x : ℝ) (h : x^2 / (1+x^2) = 2) :
    1/(1+x^2)=-1 := by
  field_simp at *
  linear_combination -h

[Bjørn Kjos-Hanssen]

So the -h is basically adding h to the goal equation...

[Kevin Buzzard]

The first line says "clear denominators everywhere" and the second says "modulo shuffling things from one side to the other, the goal is just -h."

[rzeta0]

slightly off topic - but how do you type the subscripts in a Lean-aware editor? eg to get h₀

[Marc Huisinga]

rzeta0 said:

slightly off topic - but how do you type the subscripts in a Lean-aware editor? eg to get h₀

\_0. In VS Code, you can find the full list of abbreviations in the abbreviation view (forall menu > Documentation > Docs: Show Unicode Input Abbreviations).

By the way, you can find detailed information on all Lean VS Code features in the VS Code extension manual. You can also read it from within VS Code via Documentation > Docs: Show Manual.

[Damiano Testa]

For some numerals, just \0 might work, no underscore.