The separation between hypothesis and what needs to be proved: ⊢ could be replaced.
XYZ: Type
AA': Set X
f: X → Y
g: Y → Z
BB': Set Y
x: X
x_mem: x ∈ f ⁻¹' (B ∪ B')
⊢ x ∈ f ⁻¹' B ∪ f ⁻¹' B'
Could be displayed in a more user friendly manner, something like (with a translation in the french version):
The word goal should be kept for denoting the pair (hypotheses, conclusion), so it should be avoided to denote what needs to be proved.
Hypothesis:
XYZ: Type
AA': Set X
f: X → Y
g: Y → Z
BB': Set Y
x: X
x_mem: x ∈ f ⁻¹' (B ∪ B')
We need to prove that:
x ∈ f ⁻¹' B ∪ f ⁻¹' B'
The separation between hypothesis and what needs to be proved: ⊢ could be replaced.
XYZ: Type
AA': Set X
f: X → Y
g: Y → Z
BB': Set Y
x: X
x_mem: x ∈ f ⁻¹' (B ∪ B')
⊢ x ∈ f ⁻¹' B ∪ f ⁻¹' B'
Could be displayed in a more user friendly manner, something like (with a translation in the french version):
The word goal should be kept for denoting the pair (hypotheses, conclusion), so it should be avoided to denote what needs to be proved.
Hypothesis:
XYZ: Type
AA': Set X
f: X → Y
g: Y → Z
BB': Set Y
x: X
x_mem: x ∈ f ⁻¹' (B ∪ B')
We need to prove that:
x ∈ f ⁻¹' B ∪ f ⁻¹' B'