-- Mathlib/Topology/CompactOpen.lean
theorem Topology.IsQuotientMap.continuous_lift_prod_left (hf : IsQuotientMap f) {g : X × Y → Z}
    (hg : Continuous fun p : X₀ × Y => g (f p.1, p.2)) : Continuous g

Proof state:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => { toFun := fun y => g (x, y), continuous_toFun := ⋯ }
this : Continuous G
⊢ Continuous g

Tactic:
exact ContinuousMap.continuous_uncurry_of_continuous ⟨G, this⟩

Result:
no goals

Proof state:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
⊢ Continuous g

Tactic:
let Gf : C(X₀, C(Y, Z)) := ContinuousMap.curry ⟨_, hg⟩

Result:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
⊢ Continuous g

Proof state:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => { toFun := fun y => g (x, y), continuous_toFun := ⋯ }
⊢ Continuous (G ∘ f)

Tactic:
exact Gf.continuous

Result:
no goals

Proof state:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => { toFun := fun y => g (x, y), continuous_toFun := ⋯ }
⊢ Continuous G

Tactic:
rw [hf.continuous_iff]

Result:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => { toFun := fun y => g (x, y), continuous_toFun := ⋯ }
⊢ Continuous (G ∘ f)

Proof state:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
⊢ ∀ (x : X), Continuous fun y => g (x, y)

Tactic:
intro x

Result:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
x : X
⊢ Continuous fun y => g (x, y)

Proof state:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous fun y => g (x, y)
⊢ Continuous g

Tactic:
let G : X → C(Y, Z) := fun x => ⟨_, h x⟩

Result:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => { toFun := fun y => g (x, y), continuous_toFun := ⋯ }
⊢ Continuous g

Proof state:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
x : X
⊢ Continuous fun y => g (x, y)

Tactic:
obtain ⟨x₀, rfl⟩ := hf.surjective x

Result:
case intro
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
x₀ : X₀
⊢ Continuous fun y => g (f x₀, y)

Proof state:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
⊢ Continuous g

Tactic:
have h : ∀ x : X, Continuous fun y => g (x, y) := by
  intro x
  obtain ⟨x₀, rfl⟩ := hf.surjective x
  exact (Gf x₀).continuous

Result:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous fun y => g (x, y)
⊢ Continuous g

Proof state:
case intro
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous fun p => g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p => g (f p.1, p.2), continuous_toFun := hg }.curry
x₀ : X₀
⊢ Continuous fun y => g (f x₀, y)

Tactic:
exact (Gf x₀).continuous

Result:
no goals