How to do this in Lean?

Stream: new members

[Yagub Aliyev]

I have these as assumptions:
h3: x ∈ B ∨ x ∈ C
h0: x ∉ B
My Goal is:
x ∈ C
How do you recommend to complete the proof?

[Richard Copley]

rw? at h3.

example (α : Type*) (x : α) (B C : Set α) (h3: x ∈ B ∨ x ∈ C) (h0: x ∉ B) : x ∈ C := by
  rwa [propext (or_iff_right h0)] at h3

[Yagub Aliyev]

Thank you it worked.
What do rwa, propext and or_iff_right do here?

[Richard Copley]

Can you check their docstrings and come back if you still have question?

[Richard Copley]

The propext is weird. It would be better to just omit it (and don't worry about what it means until you need to).
rwa is rw followed by assumption.
or_iff_right is an ordinary theorem that you can look up.

I just wanted to show you that you could use the library-search rw? to make progress here. A proof that is easier to read (but unnecessarily long) is:

example (α : Type*) (x : α) (B C : Set α) (h3: x ∈ B ∨ x ∈ C) (h0: x ∉ B) : x ∈ C := by
  have h : x ∈ B ∨ x ∈ C ↔ x ∈ C := or_iff_right h0
  rewrite [h] at h3
  exact h3

[Ruben Van de Velde]

I wonder why library search doesn't find this

import Mathlib
example (α : Type*) (x : α) (B C : Set α) (h3: x ∈ B ∨ x ∈ C) (h0: x ∉ B) : x ∈ C := by
  exact Or.resolve_left h3 h0

[Eric Rodriguez]

tauto should work too, and I think docs#Or.resolve_left (that is, exact Or.resolve_left h3 h0, which can also be spelt h3.resolve_left h0)

[Richard Copley]

Ruben Van de Velde said:

I wonder why library search doesn't find this

import Mathlib
example (α : Type*) (x : α) (B C : Set α) (h3: x ∈ B ∨ x ∈ C) (h0: x ∉ B) : x ∈ C := by
  exact Or.resolve_left h3 h0

Funnily enough, std_exact? does

[Yagub Aliyev]

One more stupid question, I am sorry:
If you have:
h: x ∈ A
h4: x ∈ C
How do you prove your Goal:
x ∈ A ∧ x ∈ C

[Ruben Van de Velde]

exact \< h, h4 \>

[Ruben Van de Velde]

or constructor; exact h; exact h4

[Dan Velleman]

Or exact And.intro h h4.

[Dan Velleman]

For your original question in this thread, another possibility would have been to break your proof into cases, based on h3 : x ∈ B ∨ x ∈ C. In the first case you can use proof by contradiction to prove the goal, and in the second you already have the goal as an assumption.