duplicate goals - what is best practice?

Stream: new members

[rzeta0]

Consider proving

$$x^2 = 0 \implies x = 0 \text{ for } x \in \mathbb{R}$$

In school we learned that $x=0$ twice, a repeated root.

This seems to have popped up in my learning to write Lean proofs as a duplicate goal.

Question: how do I tell Lean that I don't need to prove the same goal twice?

A better question: what is best practice when dealing with duplicate goals?

import Mathlib.Tactic

example {x : ℝ} (h: x*x = 0) : x = 0 := by
  have h1 := eq_zero_or_eq_zero_of_mul_eq_zero h
  obtain ha | hb := h1 -- <-- ha and hb are the same x=0
  · rw [ha] -- the same as below
  · rw [hb] -- the same as above

(Also I'm new to the focussed dot, did I use it correctly above? )

[Ruben Van de Velde]

For example:

import Mathlib.Tactic

example {x : ℝ} (h: x*x = 0) : x = 0 := by
  have h1 := eq_zero_or_eq_zero_of_mul_eq_zero h
  obtain ha | ha := h1 -- <-- in both cases, ha is x=0
  <;> -- <-- run the next thing on both subgoals
  · rw [ha] -- <-- this works in either case

[Ruben Van de Velde]

Another way could be

import Mathlib.Tactic

example {x : ℝ} (h: x*x = 0) : x = 0 := by
  have h1 := eq_zero_or_eq_zero_of_mul_eq_zero h
  rw [or_self] at h1
  exact h1