Theorem: Set.PairwiseDisjoint.sigmaSubtypeEmbedding_preimage (Matroid/Constructions/DirectSum.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : ι → Set α
h : univ.PairwiseDisjoint s
i : ι
r : Set α
⊢ ↑(Sigma.mk i ⁻¹' (⇑h.sigmaSubtypeEmbedding ⁻¹' r)) = r ∩ s i
Tactic:
ext
State after:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s : ι → Set α
h : univ.PairwiseDisjoint s
i : ι
r : Set α
x✝ : α
⊢ x✝ ∈ ↑(Sigma.mk i ⁻¹' (⇑h.sigmaSubtypeEmbedding ⁻¹' r)) ↔ x✝ ∈ r ∩ s i

State before:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s : ι → Set α
h : univ.PairwiseDisjoint s
i : ι
r : Set α
x✝ : α
⊢ x✝ ∈ ↑(Sigma.mk i ⁻¹' (⇑h.sigmaSubtypeEmbedding ⁻¹' r)) ↔ x✝ ∈ r ∩ s i
Tactic:
simp
State after:
no goals