-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem pullback_map_isOpenEmbedding {W X Y Z S T : TopCat.{u}} (f₁ : W ⟶ S)
    (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) {i₁ : W ⟶ Y} {i₂ : X ⟶ Z} (H₁ : IsOpenEmbedding i₁)
    (H₂ : IsOpenEmbedding i₂) (i₃ : S ⟶ T) [H₃ : Mono i₃] (eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁)
    (eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) : IsOpenEmbedding (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)

Proof state:
case toIsEmbedding
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsEmbedding ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))

Tactic:
apply
  pullback_map_isEmbedding f₁ f₂ g₁ g₂ H₁.isEmbedding H₂.isEmbedding i₃ eq₁ eq₂

Result:
no goals

Proof state:
case isOpen_range.ht.a
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom i₂))

Tactic:
exact H₂.isOpen_range

Result:
no goals

Proof state:
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))

Tactic:
constructor

Result:
case toIsEmbedding
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsEmbedding ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))

case isOpen_range
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)))

Proof state:
case isOpen_range.hs.a
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom i₁))

Tactic:
exact H₁.isOpen_range

Result:
no goals

Proof state:
case isOpen_range.hs.self
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Continuous ⇑(ConcreteCategory.hom (pullback.fst g₁ g₂))

Tactic:
apply ContinuousMap.continuous_toFun

Result:
no goals

Proof state:
case isOpen_range.ht.self
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Continuous ⇑(ConcreteCategory.hom (pullback.snd g₁ g₂))

Tactic:
apply ContinuousMap.continuous_toFun

Result:
no goals

Proof state:
case isOpen_range
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)))

Tactic:
rw [range_pullback_map]

Result:
case isOpen_range
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen
    (⇑(ConcreteCategory.hom (pullback.fst g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₁) ∩
      ⇑(ConcreteCategory.hom (pullback.snd g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₂))

Proof state:
case isOpen_range
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen
    (⇑(ConcreteCategory.hom (pullback.fst g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₁) ∩
      ⇑(ConcreteCategory.hom (pullback.snd g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₂))

Tactic:
apply IsOpen.inter <;> apply Continuous.isOpen_preimage

Result:
case isOpen_range.hs.self
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Continuous ⇑(ConcreteCategory.hom (pullback.fst g₁ g₂))

case isOpen_range.hs.a
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom i₁))

case isOpen_range.ht.self
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Continuous ⇑(ConcreteCategory.hom (pullback.snd g₁ g₂))

case isOpen_range.ht.a
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom i₂))