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

State before:
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
⊢ Continuous (Set.restrict (↑f ⁻¹' Set.range ↑i) ↑f)
Tactic:
apply ContinuousOn.restrict
State after:
case a
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
⊢ ContinuousOn (↑f) (↑f ⁻¹' Set.range ↑i)

State before:
case a
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
⊢ ContinuousOn (↑f) (↑f ⁻¹' Set.range ↑i)
Tactic:
apply Continuous.continuousOn
State after:
case a.h
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
⊢ Continuous ↑f

State before:
case a.h
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
x✝ : OpenEmbedding ↑i
⊢ Continuous ↑f
Tactic:
exact f.continuous
State after:
no goals