-- Mathlib/Topology/Constructions.lean
theorem continuous_sInf_dom₂ {X Y Z} {f : X → Y → Z} {tas : Set (TopologicalSpace X)}
    {tbs : Set (TopologicalSpace Y)} {tX : TopologicalSpace X} {tY : TopologicalSpace Y}
    {tc : TopologicalSpace Z} (hX : tX ∈ tas) (hY : tY ∈ tbs)
    (hf : Continuous fun p : X × Y => f p.1 p.2) : by
    haveI := sInf tas; haveI := sInf tbs
    exact @Continuous _ _ _ tc fun p : X × Y => f p.1 p.2

Proof state:
X✝ : Type u
Y✝ : Type v
Z✝ : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z✝
inst✝² : TopologicalSpace W
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
X : Type ?u.28829
Y : Type ?u.28833
Z : Type ?u.28842
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous fun p => f p.1 p.2
this : TopologicalSpace X
⊢ Sort ?u.29025

Tactic:
haveI := sInf tbs

Result:
X✝ : Type u
Y✝ : Type v
Z✝ : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z✝
inst✝² : TopologicalSpace W
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
X : Type ?u.28829
Y : Type ?u.28833
Z : Type ?u.28842
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous fun p => f p.1 p.2
this✝ : TopologicalSpace X
this : TopologicalSpace Y
⊢ Sort ?u.29025

Proof state:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX✝ : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous fun p => f p.1 p.2
hX : Continuous id
⊢ Continuous fun p => f p.1 p.2

Tactic:
have hY := continuous_sInf_dom hY continuous_id

Result:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX✝ : tX ∈ tas
hY✝ : tY ∈ tbs
hf : Continuous fun p => f p.1 p.2
hX : Continuous id
hY : Continuous id
⊢ Continuous fun p => f p.1 p.2

Proof state:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX✝ : tX ∈ tas
hY✝ : tY ∈ tbs
hf : Continuous fun p => f p.1 p.2
hX : Continuous id
hY : Continuous id
h_continuous_id : Continuous (Prod.map id id)
⊢ Continuous fun p => f p.1 p.2

Tactic:
exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ hf h_continuous_id

Result:
no goals

Proof state:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX✝ : tX ∈ tas
hY✝ : tY ∈ tbs
hf : Continuous fun p => f p.1 p.2
hX : Continuous id
hY : Continuous id
⊢ Continuous fun p => f p.1 p.2

Tactic:
have h_continuous_id := @Continuous.prodMap _ _ _ _ tX tY (sInf tas) (sInf tbs) _ _ hX hY

Result:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX✝ : tX ∈ tas
hY✝ : tY ∈ tbs
hf : Continuous fun p => f p.1 p.2
hX : Continuous id
hY : Continuous id
h_continuous_id : Continuous (Prod.map id id)
⊢ Continuous fun p => f p.1 p.2

Proof state:
X✝ : Type u
Y✝ : Type v
Z✝ : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z✝
inst✝² : TopologicalSpace W
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
X : Type ?u.28829
Y : Type ?u.28833
Z : Type ?u.28842
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous fun p => f p.1 p.2
⊢ Sort ?u.29025

Tactic:
haveI := sInf tas

Result:
X✝ : Type u
Y✝ : Type v
Z✝ : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z✝
inst✝² : TopologicalSpace W
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
X : Type ?u.28829
Y : Type ?u.28833
Z : Type ?u.28842
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous fun p => f p.1 p.2
this : TopologicalSpace X
⊢ Sort ?u.29025

Proof state:
X✝ : Type u
Y✝ : Type v
Z✝ : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z✝
inst✝² : TopologicalSpace W
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
X : Type ?u.28829
Y : Type ?u.28833
Z : Type ?u.28842
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous fun p => f p.1 p.2
this✝ : TopologicalSpace X
this : TopologicalSpace Y
⊢ Sort ?u.29025

Tactic:
exact @Continuous _ _ _ tc fun p : X × Y => f p.1 p.2

Result:
no goals

Proof state:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous fun p => f p.1 p.2
⊢ Continuous fun p => f p.1 p.2

Tactic:
have hX := continuous_sInf_dom hX continuous_id

Result:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX✝ : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous fun p => f p.1 p.2
hX : Continuous id
⊢ Continuous fun p => f p.1 p.2