A probably too short proof for index sets

Stream: general

[Mattia Bottoni]

Hi everybody
I would like to prove that if I have one index set contained in another, then the union (and below the intersection) of sets over the two index sets are also contained in another. I managed to do this:

import Mathlib.Tactic
import Mathlib.Data.Real.Basic --This may not be used.

variable {α : Type _}
  variable (I J : Set α)
  variable (A : α → Set α)
  open Set

  --exercise 1.2.
  example (h1 : J ≠ ∅) (h2 : J ⊆ I) : (⋃ j, A j) ⊆ (⋃ i, A i) := by
  intro x
  intro h
  exact h
  done

  --exercise 1.3.
  example (h1 : J ≠ ∅) (h2 : J ⊆ I) : (⋂ i, A i) ⊆ (⋂ j, A j) := by
  intro x
  intro h
  exact h
  done

Now strangely, the proof does not use the hypotheses h1 and h2 and Lean also gives me a warning, that they are unused. But why does the proof still work when I don’t use h1 and h2. This proof shouldn’t even work.
Did I make a mistake with the definitions of index sets in Lean?
Thank you all in advance.
All the best
Matt

[Kevin Buzzard]

I agree that h2 is necessary but why do you think that h1 is necessary?

[Yaël Dillies]

Do you have a good intuition for what ⋃₀ ∅ and ⋂₀ ∅ are?

[Kevin Buzzard]

As for why the proof works, it's because your union is not over $i\in I$ or $j\in J$, I and J are never mentioned in the statement of your theorems other than as hypotheses which are not used. You presumably mean (⋃ j ∈ J, A j) ⊆ (⋃ i ∈ I, A i)?

[Mattia Bottoni]

Kevin Buzzard said:

I agree that h2 is necessary but why do you think that h1 is necessary?

h1 is not necessary for exercise 1.3., but in the exercise on paper, h1 is given (which is why I added it in Lean too).

[Kevin Buzzard]

So you've answered your own question about why Lean is complaining that h1 isn't used :-) It's also not needed for 1.2.

[Mattia Bottoni]

Kevin Buzzard said:

So you've answered your own question about why Lean is complaining that h1 isn't used :-) It's also not needed for 1.2.

That is true :big_smile: , but I should have formulated my question better:
Why was Lean still able to "prove" the statement without using h2. And you answered that with your other reply :)

[Mattia Bottoni]

Kevin Buzzard said:

As for why the proof works, it's because your union is not over $i\in I$ or $j\in J$, I and J are never mentioned in the statement of your theorems other than as hypotheses which are not used. You presumably mean (⋃ j ∈ J, A j) ⊆ (⋃ i ∈ I, A i)?

Yes, that is the "typo" I did. So now I just have to figure out how to combine my hypothesis h with h2 in order to prove the statement.

Thank you :)

[Mattia Bottoni]

Yaël Dillies said:

Do you have a good intuition for what ⋃₀ ∅ and ⋂₀ ∅ are?

I do. If I understand your notations right, they should be: ⋃₀ ∅ = ∅ and ⋂₀ ∅ = \alpha (the universal set)

[Kevin Buzzard]

Right, so both are true without the hypothesis.

[Antoine Chambert-Loir]

By the way you observed the first part of one of the great laws of Lean: sometimes it's easy to prove a theorem because it is not stating what you mean. (The second part is that you can essentially only discover that afterwards, when you try to apply it.)

[Patrick Massot]

Mattia Bottoni said:

Yaël Dillies said:

Do you have a good intuition for what ⋃₀ ∅ and ⋂₀ ∅ are?

I do. If I understand your notations right, they should be: ⋃₀ ∅ = ∅ and ⋂₀ ∅ = \alpha (the universal set)

⋂₀ ∅ = (univ : Set \alpha)

[Kevin Buzzard]

Lean distinguishes between the type \alpha and the subset univ. This was a bit of a shock to me at first, but now it's clear to me that this is necesary, because types are types, and subsets are terms.