Theorem: CategoryTheory.aux_forall_mem (ExtrDisc/Pullback.lean)

State before:
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
⊢ ∀ (x : ↑(↑f ⁻¹' Set.range ↑i)), ↑f ↑x ∈ Set.range ↑i
Tactic:
rintro ⟨x, hx⟩
State after:
case mk
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
x : CoeSort.coe X
hx : x ∈ ↑f ⁻¹' Set.range ↑i
⊢ ↑f ↑{ val := x, property := hx } ∈ Set.range ↑i

State before:
case mk
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
x : CoeSort.coe X
hx : x ∈ ↑f ⁻¹' Set.range ↑i
⊢ ↑f ↑{ val := x, property := hx } ∈ Set.range ↑i
Tactic:
simpa only [Set.mem_preimage]
State after:
no goals