Split an equation into an OR of 2 equations

Stream: Is there code for X?

[Mark Andrew Gerads]

I need EqSplit for my proof, but BetterEqSplit is an acceptable generalization. I do not know how to show this, so I appreciate help.

import Mathlib

lemma EqSplit (r x₀ : ℝ) : x₀ = r * x₀ * 2 → (x₀ = 0 ∨ r = 1 / 2) := by
  sorry

lemma BetterEqSplit (r x₀ a : ℝ) (h : a ≠ 0): x₀ = r * x₀ * a → (x₀ = 0 ∨ r = 1 / a) := by
  sorry

[Kevin Buzzard]

Do you know a maths proof?

[Mark Andrew Gerads]

I do not know the math proof for this statement. From the equation, it looks right, but my best guess is to try proof by contradiction. I'll try that and see if I succeed.

[Alex J. Best]

Well like Kevin says you should probably think about how you would do this on paper first, that said

import Mathlib

lemma EqSplit (r x₀ : ℝ) : x₀ = r * x₀ * 2 → (x₀ = 0 ∨ r = 1 / 2) := by
  sorry

lemma BetterEqSplit (r x₀ a : ℝ) (h : a ≠ 0): x₀ = r * x₀ * a → (x₀ = 0 ∨ r = 1 / a) := by
  intro h
  have : x₀ *(1 - r * a) = 0 := by linarith
  simp at this
  apply this.imp_right
  intro h
  field_simp
  linarith

[Kyle Miller]

There's a bug in linarith (#8573), but once that's fixed you can use it for a proof of the first one:

import Mathlib.Tactic.Linarith
import Mathlib.Data.Real.Basic

lemma EqSplit (r x₀ : ℝ) (h' : x₀ = r * x₀ * 2) : x₀ = 0 ∨ r = 1 / 2 := by
  by_contra h''
  push_neg at h''
  nlinarith (config := {splitNe := true})