Theorem: sigma_mk_preimage_image' (ExtrDisc/Basic.lean)

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

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