Having trouble reasoning about Sigma types

Stream: new members

[Ching-Tsun Chou]

I'm having trouble proving the following trivial result. Any advice about how to proceed?

import Mathlib.Data.Set.Card
import Mathlib.Data.Sigma.Basic

class C where
  T : Type*
  s : Set T

example (I : Type*) (F : I → C) (i : I) (x : (F i).T)
    (h : ⟨i, x⟩ ∈ ⋃ i, Sigma.mk i '' (F i).s) : x ∈ (F i).s := by
  sorry

[Kyle Miller]

example (I : Type*) (F : I → C) (i : I) (x : (F i).T)
    (h : ⟨i, x⟩ ∈ ⋃ i, Sigma.mk i '' (F i).s) : x ∈ (F i).s := by
  simp only [Set.mem_iUnion, Set.mem_image, Sigma.mk.injEq] at h -- from simp?
  obtain ⟨i, x, hx, rfl, h⟩ := h
  rw [heq_eq_eq] at h
  cases h
  assumption

[Ching-Tsun Chou]

Thanks! I got as far as the simp only. But then I used rcases to deconstruct h and got an HEq between two different types (C i).T and (C i').T and the additional assumption that i' = i. Then I was not able to use heq_eq_eq because of the two different types and did not know how to proceed. Rewriting using i' = i in the HEq doesn't work. How come the obtain doesn't introduce a new index variable i'?

[Ruben Van de Velde]

The rfl pattern in obtain does the same as

  obtain ⟨i, x, hx, H, h⟩ := h
  subst H

which rewrites i = i' everywhere all at once

[Ching-Tsun Chou]

Thanks for the explanation. I wonder if I should have worked with Set.sigma, instead of Sigma types:

example (I : Type*) (F : I → C) (i : I) (x : (F i).T)
    (h : ⟨i, x⟩ ∈ Set.univ.sigma (fun i ↦ (F i).s)) : x ∈ (F i).s := by
  simp [Set.mk_sigma_iff] at h
  assumption

Any opinions?

[Robert Maxton]

In general, I think it's preferable to work with base types than introduce dependencies on unrelated parts of the library.