awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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.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)
have 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))
Tactic: rw [← (Homeomorph.prodAssoc _ _ _).symm.comp_continuous_iff']
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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 (X := C(X, C(Y, Z))) uncurry
have h : Continuous[instTopologicalSpaceProd, inst_2]
  (Function.uncurry fun (x : C(X, C(Y, Z))) (y : X × Y) ↦ (x.uncurry : (a : X × Y) → Z) y)
Tactic: apply continuous_of_continuous_uncurry
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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]
    (Function.uncurry fun (x : C(X, C(Y, Z))) (y : X × Y) ↦ (x.uncurry : (a : X × Y) → Z) y)
have 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))
Tactic: rw [← (Homeomorph.prodAssoc _ _ _).comp_continuous_iff']
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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]
    (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))
have 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)
Tactic: dsimp [Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (hypothesis)
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)
⊢ Continuous[inst_2, _] fun (x : T) ↦ mkD (f x) g
have this : ∀ (x : T), Continuous[inst, inst_1] (f x)
Tactic: have (x : _) : Continuous (f x) := f_cont.comp (Continuous.prodMk_right x)
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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
have refine : Continuous[instTopologicalSpaceProd, inst_1] (Function.uncurry fun (x : T) (y : X) ↦ (mkD (f x) g : (a : X) → Y) y)
Tactic: refine continuous_of_continuous_uncurry _ ?_
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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
| mkD (f x) g
have rw : { toFun := f x, continuous_toFun := sorry : C(X, Y) }
Tactic: rw [mkD_of_continuous (this x)]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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) ↦ (mkD (f x) g : (a : X) → Y) y)
have conv : Continuous[instTopologicalSpaceProd, inst_1]
  (Function.uncurry fun (x : T) (y : X) ↦ ({ toFun := f x, continuous_toFun := sorry : C(X, Y) } : (a : X) → Y) y)
Tactic: conv in mkD _ _ => rw [mkD_of_continuous (this x)]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (hypothesis)
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)
⊢ ContinuousOn (Y := C(X, Y)) (fun (x : T) ↦ mkD (f x) g) s
have this : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)
⊢ ContinuousOn (Y := C(X, Y)) (fun (x : T) ↦ mkD (f x) g) s
have simp_rw : Continuous[instTopologicalSpaceSubtype, _] fun (x : (↑s : Type u_5)) ↦ mkD (f (↑x : T)) g
Tactic: simp_rw [continuousOn_iff_continuous_restrict, s.restrict_def]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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
have refine : Continuous[instTopologicalSpaceProd, inst_1]
  (Function.uncurry fun (x : (↑s : Type u_5)) (y : X) ↦ (mkD (f (↑x : T)) g : (a : X) → Y) y)
Tactic: refine continuous_of_continuous_uncurry _ ?_
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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
| mkD (f (↑x : T)) g
have rw : { toFun := f (↑x : T), continuous_toFun := sorry : C(X, Y) }
Tactic: rw [mkD_of_continuous (this x x.2)]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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) ↦ (mkD (f (↑x : T)) g : (a : X) → Y) y)
have conv : Continuous[instTopologicalSpaceProd, inst_1]
  (Function.uncurry fun (x : (↑s : Type u_5)) (y : X) ↦
    ({ toFun := f (↑x : T), continuous_toFun := sorry : C(X, Y) } : (a : X) → Y) y)
Tactic: conv in mkD _ _ => rw [mkD_of_continuous (this x x.2)]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (hypothesis)
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)
⊢ Continuous[inst_2, _] fun (x : T) ↦ mkD (t.restrict (π := fun (a : X) ↦ Y) (f x)) g
have this : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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
have 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)
Tactic: refine continuous_of_continuous_uncurry _ ?_
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)
| mkD (t.restrict (π := fun (a : X) ↦ Y) (f x)) g
have rw : { toFun := t.restrict (π := fun (a : X) ↦ Y) (f x), continuous_toFun := sorry : ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y }
Tactic: rw [mkD_of_continuousOn (this x)]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)) ↦
      (mkD (t.restrict (π := fun (a : X) ↦ Y) (f x)) g : (a : (↑t : Type u_2)) → Y) y)
have 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 := sorry :
          ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y } :
        (a : (↑t : Type u_2)) → Y)
      y)
Tactic: conv in mkD _ _ => rw [mkD_of_continuousOn (this x)]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (hypothesis)
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)
⊢ 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
have this : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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
⊢ 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
have simp_rw : Continuous[instTopologicalSpaceSubtype, _] fun (x : (↑s : Type u_5)) ↦
  mkD (t.restrict (π := fun (a : X) ↦ Y) (f (↑x : T))) g
Tactic: simp_rw [continuousOn_iff_continuous_restrict, s.restrict_def]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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
have 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)
Tactic: refine continuous_of_continuous_uncurry _ ?_
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)
| mkD (t.restrict (π := fun (a : X) ↦ Y) (f (↑x : T))) g
have rw : { toFun := t.restrict (π := fun (a : X) ↦ Y) (f (↑x : T)), continuous_toFun := sorry :
  ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y }
Tactic: rw [mkD_of_continuousOn (this x x.2)]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)) ↦
      (mkD (t.restrict (π := fun (a : X) ↦ Y) (f (↑x : T))) g : (a : (↑t : Type u_2)) → Y) y)
have 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 := sorry :
          ContinuousMap.{u_2, u_3} (↑t : Type u_2) Y } :
        (a : (↑t : Type u_2)) → Y)
      y)
Tactic: conv in mkD _ _ => rw [mkD_of_continuousOn (this x x.2)]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)
⊢ x.curry.uncurry = x
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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))
⊢ x.uncurry.curry = x
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)
⊢ const X ((fun (f : C(X, Y)) ↦ ((f : (a : X) → Y) default : Y)) f) = f
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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) x : Y)
    ((f : (a : X) → Y) x : Y)
have 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)
Tactic: rw [Unique.eq_default x]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)
have obtain : ∀ (x₀ : X₀), Continuous[inst_2, inst_3] fun (y : Y) ↦ g (f x₀, y)
Tactic: obtain ⟨x₀, rfl⟩ := hf.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (hypothesis)
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
⊢ Continuous[instTopologicalSpaceProd, inst_3] g
have h : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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
have rw : Continuous[inst, _] (G ∘ f)
Tactic: rw [hf.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (hypothesis)
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[instTopologicalSpaceProd, inst_3] g
have this : Continuous[inst_1, _] G
Tactic: have : Continuous G := by
    rw [hf.continuous_iff]
    exact Gf.continuous
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (hypothesis)
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] g
have this : 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
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (hypothesis)
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] g
have this₁ : 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
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
x₁ x₂ : X
⊢ (↑x₁ : OnePoint X) = (↑x₂ : OnePoint X) ↔ x₁ = x₂
have rw : ((↑x₁ : OnePoint X) = (↑x₂ : OnePoint X)) = (x₁ = x₂)
Tactic: rw [iff_eq_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
s : Set X
⊢ (some '' s)ᶜ = some '' sᶜ ∪ {∞}
have rw : some '' sᶜ ∪ (range some)ᶜ = some '' sᶜ ∪ {∞}
Tactic: rw [coe_injective.compl_image_eq, compl_range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
s : Set X
rw : some '' sᶜ ∪ (range some)ᶜ = some '' sᶜ ∪ {∞}
⊢ (some '' s)ᶜ = some '' sᶜ ∪ {∞}
have rw₁ : some '' sᶜ ∪ {∞} = some '' sᶜ ∪ {∞}
Tactic: rw [coe_injective.compl_image_eq, compl_range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
x : OnePoint X
⊢ x ≠ ∞ ↔ ∃ (y : X), (↑y : OnePoint X) = x
have infty : Ne.{u_1 + 1} (α := OnePoint X) ∞ ∞ ↔ ∃ (y : X), (↑y : OnePoint X) = ∞
Tactic: induction x using OnePoint.rec
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
x : OnePoint X
infty : Ne.{u_1 + 1} (α := OnePoint X) ∞ ∞ ↔ ∃ (y : X), (↑y : OnePoint X) = ∞
⊢ x ≠ ∞ ↔ ∃ (y : X), (↑y : OnePoint X) = x
have coe : ∀ (x : X), (↑x : OnePoint X) ≠ ∞ ↔ ∃ (y : X), (↑y : OnePoint X) = (↑x : OnePoint X)
Tactic: induction x using OnePoint.rec
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
x : OnePoint X
⊢ x ∉ range some ↔ x = ∞
have rw : Membership.mem (γ := Set (OnePoint X)) (range some)ᶜ x ↔ x = ∞
Tactic: rw [← mem_compl_iff, compl_range_coe, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
x : OnePoint X
rw : Membership.mem (γ := Set (OnePoint X)) (range some)ᶜ x ↔ x = ∞
⊢ x ∉ range some ↔ x = ∞
have rw₁ : Membership.mem (γ := Set (OnePoint X)) {∞} x ↔ x = ∞
Tactic: rw [← mem_compl_iff, compl_range_coe, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
x : OnePoint X
rw : Membership.mem (γ := Set (OnePoint X)) (range some)ᶜ x ↔ x = ∞
rw₁ : Membership.mem (γ := Set (OnePoint X)) {∞} x ↔ x = ∞
⊢ x ∉ range some ↔ x = ∞
have rw₂ : x = ∞ ↔ x = ∞
Tactic: rw [← mem_compl_iff, compl_range_coe, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
⊢ Eq (α := Set X) (some ⁻¹' {∞}) ∅
have h : ∀ (x : X), Membership.mem (γ := Set X) (some ⁻¹' {∞}) x ↔ Membership.mem (γ := Set X) ∅ x
Tactic: ext