Theorem: Disjoint.sumSubtypeEmbedding_preimage_inl (Matroid/Constructions/DirectSum.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s t r : Set α
h : Disjoint s t
⊢ ↑(Sum.inl ⁻¹' (⇑h.sumSubtypeEmbedding ⁻¹' r)) = r ∩ s
Tactic:
ext
State after:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s t r : Set α
h : Disjoint s t
x✝ : α
⊢ x✝ ∈ ↑(Sum.inl ⁻¹' (⇑h.sumSubtypeEmbedding ⁻¹' r)) ↔ x✝ ∈ r ∩ s

State before:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s t r : Set α
h : Disjoint s t
x✝ : α
⊢ x✝ ∈ ↑(Sum.inl ⁻¹' (⇑h.sumSubtypeEmbedding ⁻¹' r)) ↔ x✝ ∈ r ∩ s
Tactic:
simp
State after:
no goals