awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → ContinuousMap.{u_2, u_3} (↑s : Type u_2) Y
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    Eq.{u_3 + 1} (α := Y) ((f s₁ hs₁ : (a : (↑s₁ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁) : Y)
      ((f s₂ hs₂ : (a : (↑s₂ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₂) x hxs₂) : Y)
mpr :
  Tendsto F l (𝓝 (liftCover' (fun (s : Set X) ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h ⋯))
⊢ ∃ (f : C(X, Y)), Tendsto F l (𝓝 f)

Tactic:
refine ⟨liftCover' _ _ h exists_compact_mem_nhds, ?_⟩
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → ContinuousMap.{u_2, u_3} (↑s : Type u_2) Y
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    Eq.{u_3 + 1} (α := Y) ((f s₁ hs₁ : (a : (↑s₁ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁) : Y)
      ((f s₂ hs₂ : (a : (↑s₂ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₂) x hxs₂) : Y)
mpr :
  ∀ (K : Set X),
    IsCompact K →
      Tendsto (fun (i : ι) ↦ restrict K (F i)) l
        (𝓝
          (restrict K
            (liftCover' (fun (s : Set X) ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h ⋯)))
⊢ Tendsto F l (𝓝 (liftCover' (fun (s : Set X) ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h ⋯))

Tactic:
rw [tendsto_compactOpen_iff_forall]

Premises used: ContinuousMap.tendsto_compactOpen_iff_forall
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → ContinuousMap.{u_2, u_3} (↑s : Type u_2) Y
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    Eq.{u_3 + 1} (α := Y) ((f s₁ hs₁ : (a : (↑s₁ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁) : Y)
      ((f s₂ hs₂ : (a : (↑s₂ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₂) x hxs₂) : Y)
s : Set X
hs : IsCompact s
mpr : Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 (f s hs))
rw :
  Membership.mem (γ := Set (Set X)) (fun (s : Set X) ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) s
⊢ Tendsto (fun (i : ι) ↦ restrict s (F i)) l
    (𝓝 (restrict s (liftCover' (fun (s : Set X) ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h ⋯)))

Tactic:
rw [liftCover_restrict']

Premises used: ContinuousMap.liftCover_restrict'
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → ContinuousMap.{u_2, u_3} (↑s : Type u_2) Y
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    Eq.{u_3 + 1} (α := Y) ((f s₁ hs₁ : (a : (↑s₁ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁) : Y)
      ((f s₂ hs₂ : (a : (↑s₂ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₂) x hxs₂) : Y)
s : Set X
hs : IsCompact s
⊢ Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 (f s hs))

Tactic:
hf s hs
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
y : Y
s : Set X
⊢ (⇑(coev X Y y) : (a : X) → Y × X) '' s = SProd.sprod (α := Set Y) {y} s

Tactic:
simp [singleton_prod]

Premises used: Set.singleton_prod
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Continuous[inst_1, _] (coev X Y)

Tactic:
((continuous_prodMk_const (X := Y) (Y := X) (Z := X)).comp
    (.prodMk continuous_id (continuous_const (y := ContinuousMap.id _))) :)

Premises used: ContinuousMap.continuous_prodMk_const, Continuous.comp, continuous_const, ContinuousMap.coev, continuous_id, ContinuousMap.prodMk, Continuous.prodMk
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K : Set X
U : Set Y
f : C(X × Y, Z)
a : X
⊢ Continuous[inst_1, instTopologicalSpaceProd] (Prod.mk a)

Tactic:
fun_prop
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X × Y, Z)
a : X
b : Y
⊢ Eq.{u_4 + 1} (α := Z) ((((f.curry : (a : X) → C(Y, Z)) a : C(Y, Z)) : (a : Y) → Z) b : Z)
    ((f : (a : X × Y) → Z) (a, b) : Z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → C(Y, Z)
h : Continuous[instTopologicalSpaceProd, inst_2] (Function.uncurry fun (x : X) (y : Y) ↦ (f x : (a : Y) → Z) y)
⊢ Continuous[inst, _] f

Tactic:
(curry ⟨_, h⟩).2

Premises used: ContinuousMap.curry, ContinuousMap.mk, ContinuousMap.continuous_toFun
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
s : Set X
f : X → C(Y, Z)
h :
  ContinuousOn (Y := Z) (Function.uncurry fun (x : X) (y : Y) ↦ (f x : (a : Y) → Z) y) (SProd.sprod (β := Set Y) s univ)
⊢ ContinuousOn f s

Tactic:
continuousOn_iff_continuous_restrict.mpr <| continuous_of_continuous_uncurry _ <|
    h.comp_continuous (continuous_subtype_val.prodMap continuous_id) (fun x ↦ ⟨x.1.2, trivial⟩)

Premises used: Iff.mpr, trivial, continuous_subtype_val, Continuous.prodMap, ContinuousOn.comp_continuous, ContinuousMap.continuous_of_continuous_uncurry, Prod.fst, continuous_id, continuousOn_iff_continuous_restrict, And.intro, Subtype.property
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace (X × Y)
h :
  Continuous[instTopologicalSpaceProd, _]
    (Function.uncurry fun (x : C(X × Y, Z)) (y : X) ↦ (x.curry : (a : X) → C(Y, Z)) y)
⊢ Continuous (X := C(X × Y, Z)) curry

Tactic:
apply continuous_of_continuous_uncurry

Premises used: ContinuousMap.continuous_of_continuous_uncurry
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace (X × Y)
h :
  Continuous[instTopologicalSpaceProd, inst_2]
    (Function.uncurry fun (x : C(X × Y, Z) × X) (y : Y) ↦
      (Function.uncurry (fun (x : C(X × Y, Z)) (y : X) ↦ (x.curry : (a : X) → C(Y, Z)) y) x : (a : Y) → Z) y)
⊢ Continuous[instTopologicalSpaceProd, _]
    (Function.uncurry fun (x : C(X × Y, Z)) (y : X) ↦ (x.curry : (a : X) → C(Y, Z)) y)

Tactic:
apply continuous_of_continuous_uncurry

Premises used: ContinuousMap.continuous_of_continuous_uncurry
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace (X × Y)
h :
  Continuous[instTopologicalSpaceProd, inst_2]
    (Function.comp (β := (C(X × Y, Z) × X) × Y)
      (Function.uncurry fun (x : C(X × Y, Z) × X) (y : Y) ↦
        (Function.uncurry (fun (x : C(X × Y, Z)) (y : X) ↦ (x.curry : (a : X) → C(Y, Z)) y) x : (a : Y) → Z) y)
      (⇑(Homeomorph.symm (Homeomorph.prodAssoc C(X × Y, Z) X Y)) : (a : C(X × Y, Z) × X × Y) → (C(X × Y, Z) × X) × Y))
⊢ Continuous[instTopologicalSpaceProd, inst_2]
    (Function.uncurry fun (x : C(X × Y, Z) × X) (y : Y) ↦
      (Function.uncurry (fun (x : C(X × Y, Z)) (y : X) ↦ (x.curry : (a : X) → C(Y, Z)) y) x : (a : Y) → Z) y)

Tactic:
rw [← (Homeomorph.prodAssoc _ _ _).symm.comp_continuous_iff']

Premises used: Homeomorph.comp_continuous_iff', Homeomorph.symm, Homeomorph.prodAssoc
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace (X × Y)
⊢ Continuous[instTopologicalSpaceProd, inst_2]
    (Function.comp (β := (C(X × Y, Z) × X) × Y)
      (Function.uncurry fun (x : C(X × Y, Z) × X) (y : Y) ↦
        (Function.uncurry (fun (x : C(X × Y, Z)) (y : X) ↦ (x.curry : (a : X) → C(Y, Z)) y) x : (a : Y) → Z) y)
      (⇑(Homeomorph.symm (Homeomorph.prodAssoc C(X × Y, Z) X Y)) : (a : C(X × Y, Z) × X × Y) → (C(X × Y, Z) × X) × Y))

Tactic:
continuous_eval

Premises used: ContinuousEval.continuous_eval
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace (X × Y)
⊢ Continuous[instTopologicalSpaceProd, inst_2]
    (Function.comp (β := (C(X × Y, Z) × X) × Y)
      (Function.uncurry fun (x : C(X × Y, Z) × X) (y : Y) ↦
        (Function.uncurry (fun (x : C(X × Y, Z)) (y : X) ↦ (x.curry : (a : X) → C(Y, Z)) y) x : (a : Y) → Z) y)
      (⇑(Homeomorph.symm (Homeomorph.prodAssoc C(X × Y, Z) X Y)) : (a : C(X × Y, Z) × X × Y) → (C(X × Y, Z) × X) × Y))

Tactic:
exact continuous_eval

Premises used: ContinuousEval.continuous_eval
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace Y
f : C(X, C(Y, Z))
⊢ Continuous[instTopologicalSpaceProd, inst_2]
    (Function.uncurry fun (x : X) (y : Y) ↦ (((f : (a : X) → C(Y, Z)) x : C(Y, Z)) : (a : Y) → Z) y)

Tactic:
continuous_eval.comp <| f.continuous.prodMap continuous_id

Premises used: ContinuousMap.continuous, Continuous.prodMap, Continuous.comp, continuous_id, ContinuousEval.continuous_eval
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace X
inst_4 : LocallyCompactSpace Y
h :
  Continuous[instTopologicalSpaceProd, inst_2]
    (Function.uncurry fun (x : C(X, C(Y, Z))) (y : X × Y) ↦ (x.uncurry : (a : X × Y) → Z) y)
⊢ Continuous (X := C(X, C(Y, Z))) uncurry

Tactic:
apply continuous_of_continuous_uncurry

Premises used: ContinuousMap.continuous_of_continuous_uncurry
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace X
inst_4 : LocallyCompactSpace Y
h :
  Continuous[instTopologicalSpaceProd, inst_2]
    (Function.comp (β := C(X, C(Y, Z)) × X × Y)
      (Function.uncurry fun (x : C(X, C(Y, Z))) (y : X × Y) ↦ (x.uncurry : (a : X × Y) → Z) y)
      (⇑(Homeomorph.prodAssoc C(X, C(Y, Z)) X Y) : (a : (C(X, C(Y, Z)) × X) × Y) → C(X, C(Y, Z)) × X × Y))
⊢ Continuous[instTopologicalSpaceProd, inst_2]
    (Function.uncurry fun (x : C(X, C(Y, Z))) (y : X × Y) ↦ (x.uncurry : (a : X × Y) → Z) y)

Tactic:
rw [← (Homeomorph.prodAssoc _ _ _).comp_continuous_iff']

Premises used: Homeomorph.comp_continuous_iff', Homeomorph.prodAssoc
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace X
inst_4 : LocallyCompactSpace Y
h :
  Continuous[instTopologicalSpaceProd, inst_2] fun (x : (C(X, C(Y, Z)) × X) × Y) ↦
    Function.uncurry
      (fun (x : C(X, C(Y, Z))) (y : X × Y) ↦
        Function.uncurry (fun (x_1 : X) (y : Y) ↦ (((x : (a : X) → C(Y, Z)) x_1 : C(Y, Z)) : (a : Y) → Z) y) y)
      ((Homeomorph.prodAssoc C(X, C(Y, Z)) X Y : (a : (C(X, C(Y, Z)) × X) × Y) → C(X, C(Y, Z)) × X × Y) x)
⊢ Continuous[instTopologicalSpaceProd, inst_2]
    (Function.comp (β := C(X, C(Y, Z)) × X × Y)
      (Function.uncurry fun (x : C(X, C(Y, Z))) (y : X × Y) ↦ (x.uncurry : (a : X × Y) → Z) y)
      (⇑(Homeomorph.prodAssoc C(X, C(Y, Z)) X Y) : (a : (C(X, C(Y, Z)) × X) × Y) → C(X, C(Y, Z)) × X × Y))

Tactic:
dsimp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace X
inst_4 : LocallyCompactSpace Y
⊢ Continuous[instTopologicalSpaceProd, inst_2] fun (x : (C(X, C(Y, Z)) × X) × Y) ↦
    Function.uncurry
      (fun (x : C(X, C(Y, Z))) (y : X × Y) ↦
        Function.uncurry (fun (x_1 : X) (y : Y) ↦ (((x : (a : X) → C(Y, Z)) x_1 : C(Y, Z)) : (a : Y) → Z) y) y)
      ((Homeomorph.prodAssoc C(X, C(Y, Z)) X Y : (a : (C(X, C(Y, Z)) × X) × Y) → C(X, C(Y, Z)) × X × Y) x)

Tactic:
(continuous_fst.fst.eval continuous_fst.snd).eval continuous_snd

Premises used: Continuous.snd, continuous_snd, continuous_fst, Continuous.fst, Continuous.eval
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace X
inst_4 : LocallyCompactSpace Y
⊢ Continuous[instTopologicalSpaceProd, inst_2] fun (x : (C(X, C(Y, Z)) × X) × Y) ↦
    Function.uncurry
      (fun (x : C(X, C(Y, Z))) (y : X × Y) ↦
        Function.uncurry (fun (x_1 : X) (y : Y) ↦ (((x : (a : X) → C(Y, Z)) x_1 : C(Y, Z)) : (a : Y) → Z) y) y)
      ((Homeomorph.prodAssoc C(X, C(Y, Z)) X Y : (a : (C(X, C(Y, Z)) × X) × Y) → C(X, C(Y, Z)) × X × Y) x)

Tactic:
exact (continuous_fst.fst.eval continuous_fst.snd).eval continuous_snd

Premises used: Continuous.snd, continuous_snd, continuous_fst, Continuous.fst, Continuous.eval
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Eq (α := (a : Y) → C(X, Y)) (⇑const' : (a : Y) → C(X, Y)) (const X)

Tactic:
rfl

Premises used: ContinuousMap.const, rfl
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Continuous[inst_1, _] (const X)

Tactic:
const'.continuous

Premises used: ContinuousMap.continuous, ContinuousMap.const', ContinuousMap.const
-- 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
f : T → X → Y
g : C(X, Y)
f_cont : Continuous[instTopologicalSpaceProd, inst_1] (Function.uncurry f)
⊢ ∀ (x : T), Continuous[inst, inst_1] (f x)

Tactic:
have (x : _) : Continuous (f x) := f_cont.comp (Continuous.prodMk_right x)
-- 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
f : T → X → Y
g : C(X, Y)
f_cont : Continuous[instTopologicalSpaceProd, inst_1] (Function.uncurry f)
this : ∀ (x : T), Continuous[inst, inst_1] (f x)
⊢ Continuous[inst_2, _] fun (x : T) ↦ mkD (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
f : T → X → Y
g : C(X, Y)
f_cont : Continuous[instTopologicalSpaceProd, inst_1] (Function.uncurry f)
this : ∀ (x : T), Continuous[inst, inst_1] (f x)
refine :
  Continuous[instTopologicalSpaceProd, inst_1] (Function.uncurry fun (x : T) (y : X) ↦ (mkD (f x) g : (a : X) → Y) y)
⊢ Continuous[inst_2, _] fun (x : T) ↦ mkD (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
f : T → X → Y
g : C(X, Y)
f_cont : Continuous[instTopologicalSpaceProd, inst_1] (Function.uncurry f)
this : ∀ (x : T), Continuous[inst, inst_1] (f x)
x : T
y : X
rw : { toFun := f x, continuous_toFun := ⋯ : C(X, Y) }
| mkD (f x) g

Tactic:
rw [mkD_of_continuous (this x)]

Premises used: ContinuousMap.mkD_of_continuous
-- 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
f : T → X → Y
g : C(X, Y)
f_cont : Continuous[instTopologicalSpaceProd, inst_1] (Function.uncurry f)
this : ∀ (x : T), Continuous[inst, inst_1] (f x)
conv :
  Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : T) (y : X) ↦ ({ toFun := f x, continuous_toFun := ⋯ : C(X, Y) } : (a : X) → Y) y)
⊢ Continuous[instTopologicalSpaceProd, inst_1] (Function.uncurry fun (x : T) (y : X) ↦ (mkD (f x) g : (a : X) → Y) y)

Tactic:
conv in mkD _ _ => rw [mkD_of_continuous (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
f : T → X → Y
g : C(X, Y)
f_cont : Continuous[instTopologicalSpaceProd, inst_1] (Function.uncurry f)
this : ∀ (x : T), Continuous[inst, inst_1] (f x)
⊢ Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : T) (y : X) ↦ ({ toFun := f x, continuous_toFun := ⋯ : C(X, Y) } : (a : X) → Y) y)

Tactic:
f_cont
-- 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
f : T → X → Y
g : C(X, Y)
f_cont : Continuous[instTopologicalSpaceProd, inst_1] (Function.uncurry f)
this : ∀ (x : T), Continuous[inst, inst_1] (f x)
⊢ Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : T) (y : X) ↦ ({ toFun := f x, continuous_toFun := ⋯ : C(X, Y) } : (a : X) → Y) y)

Tactic:
exact f_cont
-- 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
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (β := Set X) s univ)
⊢ ∀ (x : T) (hx : x ∈ s), Continuous[inst, inst_1] (f x)

Tactic:
have (x) (hx : x ∈ s) : Continuous (f x) := f_cont.comp_continuous
    (Continuous.prodMk_right x) fun _ ↦ ⟨hx, trivial⟩
-- 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
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (β := Set X) s univ)
this : ∀ (x : T) (hx : x ∈ s), Continuous[inst, inst_1] (f x)
simp_rw : Continuous[instTopologicalSpaceSubtype, _] fun (x : (↑s : Type u_5)) ↦ mkD (f (↑x : T)) g
⊢ ContinuousOn (Y := C(X, Y)) (fun (x : T) ↦ mkD (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
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (β := Set X) s univ)
this : ∀ (x : T) (hx : x ∈ s), Continuous[inst, inst_1] (f x)
⊢ Continuous[instTopologicalSpaceSubtype, _] fun (x : (↑s : Type u_5)) ↦ mkD (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
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (β := Set X) s univ)
this : ∀ (x : T) (hx : x ∈ s), Continuous[inst, inst_1] (f x)
refine :
  Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : (↑s : Type u_5)) (y : X) ↦ (mkD (f (↑x : T)) g : (a : X) → Y) y)
⊢ Continuous[instTopologicalSpaceSubtype, _] fun (x : (↑s : Type u_5)) ↦ mkD (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
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (β := Set X) s univ)
this : ∀ (x : T) (hx : x ∈ s), Continuous[inst, inst_1] (f x)
x : (↑s : Type u_5)
y : X
rw : { toFun := f (↑x : T), continuous_toFun := ⋯ : C(X, Y) }
| mkD (f (↑x : T)) g

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

Premises used: Subtype.val, ContinuousMap.mkD_of_continuous, 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
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (β := Set X) s univ)
this : ∀ (x : T) (hx : x ∈ s), Continuous[inst, inst_1] (f x)
conv :
  Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : (↑s : Type u_5)) (y : X) ↦
      ({ toFun := f (↑x : T), continuous_toFun := ⋯ : C(X, Y) } : (a : X) → Y) y)
⊢ Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : (↑s : Type u_5)) (y : X) ↦ (mkD (f (↑x : T)) g : (a : X) → Y) y)

Tactic:
conv in mkD _ _ => rw [mkD_of_continuous (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
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (β := Set X) s univ)
this : ∀ (x : T) (hx : x ∈ s), Continuous[inst, inst_1] (f x)
⊢ Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : (↑s : Type u_5)) (y : X) ↦
      ({ toFun := f (↑x : T), continuous_toFun := ⋯ : C(X, Y) } : (a : X) → Y) y)

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

Premises used: trivial, continuous_subtype_val, Continuous.prodMap, ContinuousOn.comp_continuous, Prod.fst, continuous_id, And.intro, 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
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (SProd.sprod (β := Set X) s univ)
this : ∀ (x : T) (hx : x ∈ s), Continuous[inst, inst_1] (f x)
⊢ Continuous[instTopologicalSpaceProd, inst_1]
    (Function.uncurry fun (x : (↑s : Type u_5)) (y : X) ↦
      ({ toFun := f (↑x : T), continuous_toFun := ⋯ : C(X, Y) } : (a : X) → Y) y)

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

Premises used: trivial, continuous_subtype_val, Continuous.prodMap, ContinuousOn.comp_continuous, Prod.fst, continuous_id, And.intro, Subtype.property