Theorem: sigma_mk_preimage_image_eq_self (ExtrDisc/Basic.lean)

State before:
α✝ : Type u_1
i : α✝
β✝ : α✝ → Type u_2
U : Set (β✝ i)
⊢ Sigma.mk i ⁻¹' (Sigma.mk i '' U) = U
Tactic:
change Sigma.mk i ⁻¹' {⟨i, u⟩ | u ∈ U} = U
State after:
α✝ : Type u_1
i : α✝
β✝ : α✝ → Type u_2
U : Set (β✝ i)
⊢ Sigma.mk i ⁻¹' {x | ∃ u, u ∈ U ∧ { fst := i, snd := u } = x} = U

State before:
α✝ : Type u_1
i : α✝
β✝ : α✝ → Type u_2
U : Set (β✝ i)
⊢ Sigma.mk i ⁻¹' {x | ∃ u, u ∈ U ∧ { fst := i, snd := u } = x} = U
Tactic:
simp
State after:
no goals