awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set T) univ t)
⊢ ∀ (x : T), ContinuousOn (f x) t

Tactic:
have (x : _) : ContinuousOn (f x) t :=
    f_cont.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨trivial, hz⟩
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set T) univ t)
this : ∀ (x : T), ContinuousOn (f x) t
⊢ Continuous[inst_2, _] fun (x : T) ↦ mkD (t.restrict (π := fun (a : X) ↦ Y) (f x)) g

Tactic:
continuous_of_continuous_uncurry _ ?_

Premises used: ContinuousMap.continuous_of_continuous_uncurry
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set T) univ t)
this : ∀ (x : T), ContinuousOn (f x) t
refine :
  Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : T) (y : (↑t : Type u_2)) ↦
      (mkD (t.restrict (π := fun (a : X) ↦ Y) (f x)) g : (a : (↑t : Type u_2)) → Y) y)
⊢ Continuous[inst_2, _] fun (x : T) ↦ mkD (t.restrict (π := fun (a : X) ↦ Y) (f x)) g

Tactic:
refine continuous_of_continuous_uncurry _ ?_

Premises used: ContinuousMap.continuous_of_continuous_uncurry
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set T) univ t)
this : ∀ (x : T), ContinuousOn (f x) t
x : T
y : (↑t : Type u_2)
rw :
  { toFun := t.restrict (π := fun (a : X) ↦ Y) (f x), continuous_toFun := ⋯ :
    ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y }
| mkD (t.restrict (π := fun (a : X) ↦ Y) (f x)) g

Tactic:
rw [mkD_of_continuousOn (this x)]

Premises used: ContinuousMap.mkD_of_continuousOn
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set T) univ t)
this : ∀ (x : T), ContinuousOn (f x) t
conv :
  Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : T) (y : (↑t : Type u_2)) ↦
      ({ toFun := t.restrict (π := fun (a : X) ↦ Y) (f x), continuous_toFun := ⋯ :
            ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y } :
          (a : (↑t : Type u_2)) → Y)
        y)
⊢ Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : T) (y : (↑t : Type u_2)) ↦
      (mkD (t.restrict (π := fun (a : X) ↦ Y) (f x)) g : (a : (↑t : Type u_2)) → Y) y)

Tactic:
conv in mkD _ _ => rw [mkD_of_continuousOn (this x)]

Premises used: ContinuousMap.mkD
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set T) univ t)
this : ∀ (x : T), ContinuousOn (f x) t
⊢ Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : T) (y : (↑t : Type u_2)) ↦
      ({ toFun := t.restrict (π := fun (a : X) ↦ Y) (f x), continuous_toFun := ⋯ :
            ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y } :
          (a : (↑t : Type u_2)) → Y)
        y)

Tactic:
f_cont.comp_continuous (.prodMap continuous_id continuous_subtype_val)
    fun xz ↦ ⟨trivial, xz.2.2⟩

Premises used: trivial, continuous_subtype_val, Continuous.prodMap, ContinuousOn.comp_continuous, continuous_id, And.intro, Set.restrict, Prod.snd, Subtype.property
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set T) univ t)
this : ∀ (x : T), ContinuousOn (f x) t
⊢ Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : T) (y : (↑t : Type u_2)) ↦
      ({ toFun := t.restrict (π := fun (a : X) ↦ Y) (f x), continuous_toFun := ⋯ :
            ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y } :
          (a : (↑t : Type u_2)) → Y)
        y)

Tactic:
exact f_cont.comp_continuous (.prodMap continuous_id continuous_subtype_val)
    fun xz ↦ ⟨trivial, xz.2.2⟩

Premises used: trivial, continuous_subtype_val, Continuous.prodMap, ContinuousOn.comp_continuous, continuous_id, And.intro, Prod.snd, Subtype.property
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
s : Set T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
⊢ ∀ (x : T) (hx : x ∈ s), ContinuousOn (f x) t

Tactic:
have (x) (hx : x ∈ s) : ContinuousOn (f x) t :=
    f_cont.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨hx, hz⟩
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
s : Set T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
this : ∀ (x : T) (hx : x ∈ s), ContinuousOn (f x) t
simp_rw :
  Continuous[instTopologicalSpaceSubtype, _] fun (x : (↑s : Type u_5)) ↦
    mkD (t.restrict (π := fun (a : X) ↦ Y) (f (↑x : T))) g
⊢ ContinuousOn (Y := ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y)
    (fun (x : T) ↦ mkD (t.restrict (π := fun (a : X) ↦ Y) (f x)) g) s

Tactic:
simp_rw [continuousOn_iff_continuous_restrict, s.restrict_def]

Premises used: Set.restrict_def, continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
s : Set T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
this : ∀ (x : T) (hx : x ∈ s), ContinuousOn (f x) t
⊢ Continuous[instTopologicalSpaceSubtype, _] fun (x : (↑s : Type u_5)) ↦
    mkD (t.restrict (π := fun (a : X) ↦ Y) (f (↑x : T))) g

Tactic:
continuous_of_continuous_uncurry _ ?_

Premises used: ContinuousMap.continuous_of_continuous_uncurry
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
s : Set T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
this : ∀ (x : T) (hx : x ∈ s), ContinuousOn (f x) t
refine :
  Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : (↑s : Type u_5)) (y : (↑t : Type u_2)) ↦
      (mkD (t.restrict (π := fun (a : X) ↦ Y) (f (↑x : T))) g : (a : (↑t : Type u_2)) → Y) y)
⊢ Continuous[instTopologicalSpaceSubtype, _] fun (x : (↑s : Type u_5)) ↦
    mkD (t.restrict (π := fun (a : X) ↦ Y) (f (↑x : T))) g

Tactic:
refine continuous_of_continuous_uncurry _ ?_

Premises used: ContinuousMap.continuous_of_continuous_uncurry
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
s : Set T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
this : ∀ (x : T) (hx : x ∈ s), ContinuousOn (f x) t
x : (↑s : Type u_5)
y : (↑t : Type u_2)
rw :
  { toFun := t.restrict (π := fun (a : X) ↦ Y) (f (↑x : T)), continuous_toFun := ⋯ :
    ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y }
| mkD (t.restrict (π := fun (a : X) ↦ Y) (f (↑x : T))) g

Tactic:
rw [mkD_of_continuousOn (this x x.2)]

Premises used: ContinuousMap.mkD_of_continuousOn, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
s : Set T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
this : ∀ (x : T) (hx : x ∈ s), ContinuousOn (f x) t
conv :
  Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : (↑s : Type u_5)) (y : (↑t : Type u_2)) ↦
      ({ toFun := t.restrict (π := fun (a : X) ↦ Y) (f (↑x : T)), continuous_toFun := ⋯ :
            ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y } :
          (a : (↑t : Type u_2)) → Y)
        y)
⊢ Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : (↑s : Type u_5)) (y : (↑t : Type u_2)) ↦
      (mkD (t.restrict (π := fun (a : X) ↦ Y) (f (↑x : T))) g : (a : (↑t : Type u_2)) → Y) y)

Tactic:
conv in mkD _ _ => rw [mkD_of_continuousOn (this x x.2)]

Premises used: ContinuousMap.mkD
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
s : Set T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
this : ∀ (x : T) (hx : x ∈ s), ContinuousOn (f x) t
⊢ Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : (↑s : Type u_5)) (y : (↑t : Type u_2)) ↦
      ({ toFun := t.restrict (π := fun (a : X) ↦ Y) (f (↑x : T)), continuous_toFun := ⋯ :
            ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y } :
          (a : (↑t : Type u_2)) → Y)
        y)

Tactic:
f_cont.comp_continuous (.prodMap continuous_subtype_val continuous_subtype_val)
    fun xz ↦ ⟨xz.1.2, xz.2.2⟩

Premises used: continuous_subtype_val, Continuous.prodMap, ContinuousOn.comp_continuous, Prod.fst, And.intro, Set.restrict, Prod.snd, Subtype.property
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace T
s : Set T
t : Set X
f : T → X → Y
g : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
this : ∀ (x : T) (hx : x ∈ s), ContinuousOn (f x) t
⊢ Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : (↑s : Type u_5)) (y : (↑t : Type u_2)) ↦
      ({ toFun := t.restrict (π := fun (a : X) ↦ Y) (f (↑x : T)), continuous_toFun := ⋯ :
            ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y } :
          (a : (↑t : Type u_2)) → Y)
        y)

Tactic:
exact f_cont.comp_continuous (.prodMap continuous_subtype_val continuous_subtype_val)
    fun xz ↦ ⟨xz.1.2, xz.2.2⟩

Premises used: continuous_subtype_val, Continuous.prodMap, ContinuousOn.comp_continuous, Prod.fst, And.intro, Prod.snd, Subtype.property
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace X
inst_4 : LocallyCompactSpace Y
x : C(X × Y, Z)
h : ∀ (a : X × Y), Eq.{u_3 + 1} (α := Z) ((x.curry.uncurry : (a : X × Y) → Z) a : Z) ((x : (a : X × Y) → Z) a : Z)
⊢ x.curry.uncurry = x

Tactic:
ext
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace X
inst_4 : LocallyCompactSpace Y
x : C(X × Y, Z)
a : X × Y
⊢ Eq.{u_3 + 1} (α := Z) ((x.curry.uncurry : (a : X × Y) → Z) a : Z) ((x : (a : X × Y) → Z) a : Z)

Tactic:
rfl
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace X
inst_4 : LocallyCompactSpace Y
x : C(X, C(Y, Z))
h :
  ∀ (a : X) (a_1 : Y),
    Eq.{u_3 + 1} (α := Z) ((((x.uncurry.curry : (a : X) → C(Y, Z)) a : C(Y, Z)) : (a : Y) → Z) a_1 : Z)
      ((((x : (a : X) → C(Y, Z)) a : C(Y, Z)) : (a : Y) → Z) a_1 : Z)
⊢ x.uncurry.curry = x

Tactic:
ext
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace X
inst_4 : LocallyCompactSpace Y
x : C(X, C(Y, Z))
a : X
a_1 : Y
⊢ Eq.{u_3 + 1} (α := Z) ((((x.uncurry.curry : (a : X) → C(Y, Z)) a : C(Y, Z)) : (a : Y) → Z) a_1 : Z)
    ((((x : (a : X) → C(Y, Z)) a : C(Y, Z)) : (a : Y) → Z) a_1 : Z)

Tactic:
rfl
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : Unique X
f : C(X, Y)
h :
  ∀ (x : X),
    Eq.{u_2 + 1} (α := Y) ((const X ((fun (f : C(X, Y)) ↦ ((f : (a : X) → Y) default : Y)) f) : (a : X) → Y) x : Y)
      ((f : (a : X) → Y) x : Y)
⊢ const X ((fun (f : C(X, Y)) ↦ ((f : (a : X) → Y) default : Y)) f) = f

Tactic:
ext x
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : Unique X
f : C(X, Y)
x : X
h :
  Eq.{u_2 + 1} (α := Y) ((const X ((fun (f : C(X, Y)) ↦ ((f : (a : X) → Y) default : Y)) f) : (a : X) → Y) default : Y)
    ((f : (a : X) → Y) default : Y)
⊢ Eq.{u_2 + 1} (α := Y) ((const X ((fun (f : C(X, Y)) ↦ ((f : (a : X) → Y) default : Y)) f) : (a : X) → Y) x : Y)
    ((f : (a : X) → Y) x : Y)

Tactic:
rw [Unique.eq_default x]

Premises used: Unique.eq_default
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : Unique X
f : C(X, Y)
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((const X ((fun (f : C(X, Y)) ↦ ((f : (a : X) → Y) default : Y)) f) : (a : X) → Y) default : Y)
    ((f : (a : X) → Y) default : Y)

Tactic:
rfl
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Unique X
y : Y
x : X
⊢ (((continuousMapOfUnique : (a : Y) → C(X, Y)) y : C(X, Y)) : (a : X) → Y) x = y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Unique X
f : C(X, Y)
⊢ Eq.{u_2 + 1} (α := Y) ((Homeomorph.symm continuousMapOfUnique : (a : C(X, Y)) → Y) f : Y)
    ((f : (a : X) → Y) default : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.CompactOpen
Goal:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X₀
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
inst_4 : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun (p : X₀ × Y) ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
x : X
obtain : ∀ (x₀ : X₀), Continuous[inst_2, inst_3] fun (y : Y) ↦ g (f x₀, y)
⊢ Continuous[inst_2, inst_3] fun (y : Y) ↦ g (x, y)

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

Premises used: Topology.IsQuotientMap.surjective, rfl
-- Module: Mathlib.Topology.CompactOpen
Goal:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X₀
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
inst_4 : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun (p : X₀ × Y) ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
x₀ : X₀
⊢ Continuous[inst_2, inst_3] fun (y : Y) ↦ g (f x₀, y)

Tactic:
(Gf x₀).continuous

Premises used: ContinuousMap.continuous, DFunLike.coe
-- Module: Mathlib.Topology.CompactOpen
Goal:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X₀
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
inst_4 : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun (p : X₀ × Y) ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
x₀ : X₀
⊢ Continuous[inst_2, inst_3] fun (y : Y) ↦ g (f x₀, y)

Tactic:
exact (Gf x₀).continuous

Premises used: ContinuousMap.continuous, DFunLike.coe
-- Module: Mathlib.Topology.CompactOpen
Goal:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X₀
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
inst_4 : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun (p : X₀ × Y) ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
⊢ ∀ (x : X), Continuous[inst_2, inst_3] fun (y : Y) ↦ g (x, y)

Tactic:
have h : ∀ x : X, Continuous fun y => g (x, y) := by
    intro x
    obtain ⟨x₀, rfl⟩ := hf.surjective x
    exact (Gf x₀).continuous
-- Module: Mathlib.Topology.CompactOpen
Goal:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X₀
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
inst_4 : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun (p : X₀ × Y) ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous[inst_2, inst_3] fun (y : Y) ↦ g (x, y)
G : X → C(Y, Z) := fun (x : X) ↦ { toFun := fun (y : Y) ↦ g (x, y), continuous_toFun := ⋯ }
rw : Continuous[inst, _] (G ∘ f)
⊢ Continuous[inst_1, _] G

Tactic:
rw [hf.continuous_iff]

Premises used: Topology.IsQuotientMap.continuous_iff
-- Module: Mathlib.Topology.CompactOpen
Goal:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X₀
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
inst_4 : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun (p : X₀ × Y) ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous[inst_2, inst_3] fun (y : Y) ↦ g (x, y)
G : X → C(Y, Z) := fun (x : X) ↦ { toFun := fun (y : Y) ↦ g (x, y), continuous_toFun := ⋯ }
⊢ Continuous[inst, _] (G ∘ f)

Tactic:
Gf.continuous

Premises used: ContinuousMap.continuous
-- Module: Mathlib.Topology.CompactOpen
Goal:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X₀
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
inst_4 : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun (p : X₀ × Y) ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous[inst_2, inst_3] fun (y : Y) ↦ g (x, y)
G : X → C(Y, Z) := fun (x : X) ↦ { toFun := fun (y : Y) ↦ g (x, y), continuous_toFun := ⋯ }
⊢ Continuous[inst, _] (G ∘ f)

Tactic:
exact Gf.continuous

Premises used: ContinuousMap.continuous
-- Module: Mathlib.Topology.CompactOpen
Goal:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X₀
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
inst_4 : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun (p : X₀ × Y) ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous[inst_2, inst_3] fun (y : Y) ↦ g (x, y)
G : X → C(Y, Z) := fun (x : X) ↦ { toFun := fun (y : Y) ↦ g (x, y), continuous_toFun := ⋯ }
⊢ Continuous[inst_1, _] G

Tactic:
have : Continuous G := by
    rw [hf.continuous_iff]
    exact Gf.continuous
-- Module: Mathlib.Topology.CompactOpen
Goal:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X₀
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
inst_4 : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun (p : X₀ × Y) ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous[inst_2, inst_3] fun (y : Y) ↦ g (x, y)
G : X → C(Y, Z) := fun (x : X) ↦ { toFun := fun (y : Y) ↦ g (x, y), continuous_toFun := ⋯ }
this : Continuous[inst_1, _] G
⊢ Continuous[instTopologicalSpaceProd, inst_3] g

Tactic:
ContinuousMap.continuous_uncurry_of_continuous ⟨G, this⟩

Premises used: ContinuousMap.mk, ContinuousMap.continuous_uncurry_of_continuous
-- Module: Mathlib.Topology.CompactOpen
Goal:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X₀
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
inst_4 : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun (p : X₀ × Y) ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous[inst_2, inst_3] fun (y : Y) ↦ g (x, y)
G : X → C(Y, Z) := fun (x : X) ↦ { toFun := fun (y : Y) ↦ g (x, y), continuous_toFun := ⋯ }
this : Continuous[inst_1, _] G
⊢ Continuous[instTopologicalSpaceProd, inst_3] g

Tactic:
exact ContinuousMap.continuous_uncurry_of_continuous ⟨G, this⟩

Premises used: ContinuousMap.mk, ContinuousMap.continuous_uncurry_of_continuous
-- Module: Mathlib.Topology.CompactOpen
Goal:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X₀
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
inst_4 : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : Y × X → Z
hg : Continuous[instTopologicalSpaceProd, inst_3] fun (p : Y × X₀) ↦ g (p.1, f p.2)
⊢ Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ g (p.swap.1, f p.swap.2)

Tactic:
have : Continuous fun p : X₀ × Y => g ((Prod.swap p).1, f (Prod.swap p).2) :=
    hg.comp continuous_swap
-- Module: Mathlib.Topology.CompactOpen
Goal:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X₀
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
inst_4 : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : Y × X → Z
hg : Continuous[instTopologicalSpaceProd, inst_3] fun (p : Y × X₀) ↦ g (p.1, f p.2)
this : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ g (p.swap.1, f p.swap.2)
⊢ Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ (g ∘ Prod.swap) (f p.1, p.2)

Tactic:
have : Continuous fun p : X₀ × Y => (g ∘ Prod.swap) (f p.1, p.2) := this
-- Module: Mathlib.Topology.CompactOpen
Goal:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X₀
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
inst_4 : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : Y × X → Z
hg : Continuous[instTopologicalSpaceProd, inst_3] fun (p : Y × X₀) ↦ g (p.1, f p.2)
this_1 : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ g (p.swap.1, f p.swap.2)
this : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ (g ∘ Prod.swap) (f p.1, p.2)
⊢ Continuous[instTopologicalSpaceProd, inst_3] g

Tactic:
(hf.continuous_lift_prod_left this).comp continuous_swap

Premises used: Continuous.comp, continuous_swap, Topology.IsQuotientMap.continuous_lift_prod_left, Prod.swap