'We conclude' sometimes too powerful ?

[jnarboux]

In this context:

x_mem: f x ∈ B ∪ B'
⊢ x ∈ f ⁻¹' B ∪ f ⁻¹' B'

Help suggest to use We conclude with x_mem.
We conclude with x_mem solves the goal.
For professional users it is ok, but I wonder if it is not too powerful for beginners ? in this exercise I wonder if the union should not be opaque.

[PatrickMassot]

Thanks Julien. This is a slightly tricky one that will require some library support. As you know, the goal is indeed definitionaly equal to x_mem. We can indeed redefine the union as opaque (or even irreducible is enough, no need to add axioms) using something like:

section SetUnion
irreducible_def SetUnion {X : Type*} (A B : Set X) := A ∪ B

/-- `a ∪ b` is the union of`a` and `b`. -/
infixl:65 (priority := high) " ∪ " => SetUnion

variable {X : Type*} {A B : Set X}

lemma mem_setUnion_of_mem_left  {x} (hxA : x ∈ A) : x ∈ A ∪ B := by
  rw [SetUnion_def]
  tauto

lemma mem_setUnion_of_mem_right  {x} (hxB : x ∈ B) : x ∈ A ∪ B := by
  rw [SetUnion_def]
  tauto

lemma mem_or_mem_of_mem_setUnion  {x} (hx : x ∈ A ∪ B) : x ∈ A ∨ x ∈ B := by
  rwa [SetUnion_def] at hx
end SetUnion

where the irreducible_def command from Mathlib creates both a irreducible definition and the corresponding SetUnion_def lemma. And then we override the union notation by giving ours a higher priority. We could also use the same trick with inverse image if you want to avoid students relying on its definition.

The tricky part is that after doing that the We proceed using x_mem tactic will no longer work. You would need We proceed using mem_or_mem_of_mem_setUnion x_mem. The obvious solution is to add a new category of anonymous lemmas to be used by We proceed. This is easy to do, but I have some administration work to do right now.