Theorem: Matroid.iUnion_preimage_image_sigma_mk_eq (Matroid/Constructions/DirectSum.lean)

State before:
α✝ : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
α : ι → Type u_5
f : (i : ι) → Set (α i)
j : ι
⊢ ⋃ i, Sigma.mk j ⁻¹' (Sigma.mk i '' f i) = f j
Tactic:
aesop
State after:
no goals