confusion about how to orelse

Stream: new members

[Xiyu Zhai]

Hi, all. I'm confused about the behavior of orelse and first in lean4.

import Mathlib

-- success
example (x : ℝ) (h : x > 0) : 1/x + 1 = (x+1)/x := by
  field_simp; ring

-- unsolved goals
-- x : ℝ
-- h : x > 0
-- ⊢ 1 + x⁻¹ = x * x⁻¹ + x⁻¹Lean 4
example (x : ℝ) (h : x > 0) : 1/x + 1 = (x+1)/x := by
  ring <;> (field_simp ;ring)

-- unsolved goals
-- x : ℝ
-- h : x > 0
-- ⊢ 1 + x⁻¹ = x * x⁻¹ + x⁻¹Lean 4
example (x : ℝ) (h : x > 0) : 1/x + 1 = (x+1)/x := by
  first | ring | (field_simp ;ring)

For example, since the first in the above code succeed, I would expect all followings will succeed too.

Claude Sonnet seems to agree with me. Please enlight me and Claude.

[Daniel Weber]

In the second example I'm seeing no goals to be solved on the second ring, because the field_simp solved it.

In the third, first uses the first tactic that succeeds, where succeeds means "throws no errors". You can change ring to (ring; done) to assert that all goals are solved, and then that will fail and the second tactic sequence (field_simp; ring) will act

[Xiyu Zhai]

wow, excellent!

[Xiyu Zhai]

Thanks a lot!!

[Xiyu Zhai]

Now I understand that if only one goal is solved, it counts as success.