awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed[inst] s
Y : Type v
inst_2 : TopologicalSpace Y
f : ContinuousMap.{u, v} (↑s : Type u) Y
t : Set Y
hf : ∀ (x : (↑s : Type u)), Membership.mem (α := Y) t ((f : (a : (↑s : Type u)) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
obtain :
  ∀ (g : ContinuousMap.{u, v} X (↑t : Type v))
    (hg : restrict s g = { toFun := Set.codRestrict (⇑f : (a : (↑s : Type u)) → Y) t hf, continuous_toFun := ⋯ }),
    ∃ (g : C(X, Y)), (∀ (x : X), Membership.mem (α := Y) t ((g : (a : X) → Y) x : Y)) ∧ restrict s g = f
⊢ ∃ (g : C(X, Y)), (∀ (x : X), Membership.mem (α := Y) t ((g : (a : X) → Y) x : Y)) ∧ restrict s g = f

Tactic:
obtain ⟨g, hg⟩ := mk _ (map_continuous f |>.codRestrict hf) |>.exists_restrict_eq hs

Premises used: ContinuousMap.mk, Continuous.codRestrict, ContinuousMap.exists_restrict_eq, ContinuousMapClass.map_continuous
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed[inst] s
Y : Type v
inst_2 : TopologicalSpace Y
f : ContinuousMap.{u, v} (↑s : Type u) Y
t : Set Y
hf : ∀ (x : (↑s : Type u)), Membership.mem (α := Y) t ((f : (a : (↑s : Type u)) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
g : ContinuousMap.{u, v} X (↑t : Type v)
hg : restrict s g = { toFun := Set.codRestrict (⇑f : (a : (↑s : Type u)) → Y) t hf, continuous_toFun := ⋯ }
⊢ Continuous[instTopologicalSpaceSubtype, inst_2] (Subtype.val (p := fun (x : Y) ↦ x ∈ t))

Tactic:
fun_prop
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed[inst] s
Y : Type v
inst_2 : TopologicalSpace Y
f : ContinuousMap.{u, v} (↑s : Type u) Y
t : Set Y
hf : ∀ (x : (↑s : Type u)), Membership.mem (α := Y) t ((f : (a : (↑s : Type u)) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
g : ContinuousMap.{u, v} X (↑t : Type v)
hg : restrict s g = { toFun := Set.codRestrict (⇑f : (a : (↑s : Type u)) → Y) t hf, continuous_toFun := ⋯ }
⊢ ∀ (x : X),
    Membership.mem (α := Y) t
      ((comp { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ t), continuous_toFun := ⋯ : C({ x : Y // x ∈ t }, Y) } g :
            (a : X) → Y)
          x :
        Y)

Tactic:
simp
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed[inst] s
Y : Type v
inst_2 : TopologicalSpace Y
f : ContinuousMap.{u, v} (↑s : Type u) Y
t : Set Y
hf : ∀ (x : (↑s : Type u)), Membership.mem (α := Y) t ((f : (a : (↑s : Type u)) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
g : ContinuousMap.{u, v} X (↑t : Type v)
hg : restrict s g = { toFun := Set.codRestrict (⇑f : (a : (↑s : Type u)) → Y) t hf, continuous_toFun := ⋯ }
h :
  ∀ (x : (↑s : Type u)),
    Eq.{v + 1} (α := Y)
      ((restrict s
              (comp
                { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ t), continuous_toFun := ⋯ : C({ x : Y // x ∈ t }, Y) }
                g) :
            (a : (↑s : Type u)) → Y)
          x :
        Y)
      ((f : (a : (↑s : Type u)) → Y) x : Y)
⊢ restrict s
      (comp { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ t), continuous_toFun := ⋯ : C({ x : Y // x ∈ t }, Y) } g) =
    f

Tactic:
ext x
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed[inst] s
Y : Type v
inst_2 : TopologicalSpace Y
f : ContinuousMap.{u, v} (↑s : Type u) Y
t : Set Y
hf : ∀ (x : (↑s : Type u)), Membership.mem (α := Y) t ((f : (a : (↑s : Type u)) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
g : ContinuousMap.{u, v} X (↑t : Type v)
hg : restrict s g = { toFun := Set.codRestrict (⇑f : (a : (↑s : Type u)) → Y) t hf, continuous_toFun := ⋯ }
x : (↑s : Type u)
⊢ Eq.{v + 1} (α := Y)
    ((restrict s
            (comp { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ t), continuous_toFun := ⋯ : C({ x : Y // x ∈ t }, Y) }
              g) :
          (a : (↑s : Type u)) → Y)
        x :
      Y)
    ((f : (a : (↑s : Type u)) → Y) x : Y)

Tactic:
congrm(($(hg) x : Y))
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed[inst] s
Y : Type v
inst_2 : TopologicalSpace Y
f : ContinuousMap.{u, v} (↑s : Type u) Y
t : Set Y
hf : ∀ (x : (↑s : Type u)), Membership.mem (α := Y) t ((f : (a : (↑s : Type u)) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
g : ContinuousMap.{u, v} X (↑t : Type v)
hg : restrict s g = { toFun := Set.codRestrict (⇑f : (a : (↑s : Type u)) → Y) t hf, continuous_toFun := ⋯ }
⊢ ∃ (g : C(X, Y)), (∀ (x : X), Membership.mem (α := Y) t ((g : (a : X) → Y) x : Y)) ∧ restrict s g = f

Tactic:
exact ⟨comp ⟨Subtype.val, by fun_prop⟩ g, by simp, by ext x; congrm(($(hg) x : Y))⟩
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
e : X₁ → X
he : IsClosedEmbedding e
Y : Type v
inst_3 : TopologicalSpace Y
f : C(X₁, Y)
t : Set Y
hf : ∀ (x : X₁), Membership.mem (α := Y) t ((f : (a : X₁) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
obtain :
  ∀ (g : ContinuousMap.{u, v} X (↑t : Type v))
    (hg :
      g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } =
        { toFun := Set.codRestrict (⇑f : (a : X₁) → Y) t hf, continuous_toFun := ⋯ }),
    ∃ (g : C(X, Y)),
      (∀ (x : X), Membership.mem (α := Y) t ((g : (a : X) → Y) x : Y)) ∧
        g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } = f
⊢ ∃ (g : C(X, Y)),
    (∀ (x : X), Membership.mem (α := Y) t ((g : (a : X) → Y) x : Y)) ∧
      g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } = f

Tactic:
obtain ⟨g, hg⟩ := mk _ (map_continuous f |>.codRestrict hf) |>.exists_extension he

Premises used: ContinuousMap.mk, Continuous.codRestrict, ContinuousMap.exists_extension, ContinuousMapClass.map_continuous
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
e : X₁ → X
he : IsClosedEmbedding e
Y : Type v
inst_3 : TopologicalSpace Y
f : C(X₁, Y)
t : Set Y
hf : ∀ (x : X₁), Membership.mem (α := Y) t ((f : (a : X₁) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
g : ContinuousMap.{u, v} X (↑t : Type v)
hg :
  g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } =
    { toFun := Set.codRestrict (⇑f : (a : X₁) → Y) t hf, continuous_toFun := ⋯ }
⊢ Continuous[instTopologicalSpaceSubtype, inst_3] (Subtype.val (p := fun (x : Y) ↦ x ∈ t))

Tactic:
fun_prop
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
e : X₁ → X
he : IsClosedEmbedding e
Y : Type v
inst_3 : TopologicalSpace Y
f : C(X₁, Y)
t : Set Y
hf : ∀ (x : X₁), Membership.mem (α := Y) t ((f : (a : X₁) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
g : ContinuousMap.{u, v} X (↑t : Type v)
hg :
  g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } =
    { toFun := Set.codRestrict (⇑f : (a : X₁) → Y) t hf, continuous_toFun := ⋯ }
⊢ ∀ (x : X),
    Membership.mem (α := Y) t
      ((comp { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ t), continuous_toFun := ⋯ : C({ x : Y // x ∈ t }, Y) } g :
            (a : X) → Y)
          x :
        Y)

Tactic:
simp
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
e : X₁ → X
he : IsClosedEmbedding e
Y : Type v
inst_3 : TopologicalSpace Y
f : C(X₁, Y)
t : Set Y
hf : ∀ (x : X₁), Membership.mem (α := Y) t ((f : (a : X₁) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
g : ContinuousMap.{u, v} X (↑t : Type v)
hg :
  g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } =
    { toFun := Set.codRestrict (⇑f : (a : X₁) → Y) t hf, continuous_toFun := ⋯ }
h :
  ∀ (x : X₁),
    Eq.{v + 1} (α := Y)
      (((comp { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ t), continuous_toFun := ⋯ : C({ x : Y // x ∈ t }, Y) }
                  g).comp
              { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } :
            (a : X₁) → Y)
          x :
        Y)
      ((f : (a : X₁) → Y) x : Y)
⊢ (comp { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ t), continuous_toFun := ⋯ : C({ x : Y // x ∈ t }, Y) } g).comp
      { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } =
    f

Tactic:
ext x
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
e : X₁ → X
he : IsClosedEmbedding e
Y : Type v
inst_3 : TopologicalSpace Y
f : C(X₁, Y)
t : Set Y
hf : ∀ (x : X₁), Membership.mem (α := Y) t ((f : (a : X₁) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
g : ContinuousMap.{u, v} X (↑t : Type v)
hg :
  g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } =
    { toFun := Set.codRestrict (⇑f : (a : X₁) → Y) t hf, continuous_toFun := ⋯ }
x : X₁
⊢ Eq.{v + 1} (α := Y)
    (((comp { toFun := Subtype.val (p := fun (x : Y) ↦ x ∈ t), continuous_toFun := ⋯ : C({ x : Y // x ∈ t }, Y) }
                g).comp
            { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } :
          (a : X₁) → Y)
        x :
      Y)
    ((f : (a : X₁) → Y) x : Y)

Tactic:
congrm(($(hg) x : Y))
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
e : X₁ → X
he : IsClosedEmbedding e
Y : Type v
inst_3 : TopologicalSpace Y
f : C(X₁, Y)
t : Set Y
hf : ∀ (x : X₁), Membership.mem (α := Y) t ((f : (a : X₁) → Y) x : Y)
ht : TietzeExtension.{u, v} (↑t : Type v)
g : ContinuousMap.{u, v} X (↑t : Type v)
hg :
  g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } =
    { toFun := Set.codRestrict (⇑f : (a : X₁) → Y) t hf, continuous_toFun := ⋯ }
⊢ ∃ (g : C(X, Y)),
    (∀ (x : X), Membership.mem (α := Y) t ((g : (a : X) → Y) x : Y)) ∧
      g.comp { toFun := e, continuous_toFun := ⋯ : C(X₁, X) } = f

Tactic:
exact ⟨comp ⟨Subtype.val, by fun_prop⟩ g, by simp, by ext x; congrm(($(hg) x : Y))⟩
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
s_1 : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
ι : Type u_1
Y : ι → Type v
inst_5 : (i : ι) → TopologicalSpace (Y i)
inst_6 : ∀ (i : ι), TietzeExtension.{u, v} (Y i)
X_1 : Type u
inst_7 : TopologicalSpace X_1
inst_8 : NormalSpace X_1
s : Set X_1
hs : IsClosed[inst_7] s
f : C((↑s : Type u), (i : ι) → Y i)
obtain :
  ∀ (g' : (x : ι) → ContinuousMap.{u, v} X_1 (Y x))
    (hg' :
      ∀ (x : ι),
        ContinuousMap.restrict s (g' x) =
          (Equiv.symm (ContinuousMap.piEquiv (↑s : Type u) Y) :
              (a : C((↑s : Type u), (i : ι) → Y i)) → (i : ι) → C((↑s : Type u), Y i))
            f x),
    ∃ (g : C(X_1, (i : ι) → Y i)), ContinuousMap.restrict s g = f
⊢ ∃ (g : C(X_1, (i : ι) → Y i)), ContinuousMap.restrict s g = f

Tactic:
obtain ⟨g', hg'⟩ := Classical.skolem.mp <| fun i ↦
      ContinuousMap.exists_restrict_eq hs (ContinuousMap.piEquiv _ _ |>.symm f i)

Premises used: Classical.skolem, Set.Elem, ContinuousMap.exists_restrict_eq, Iff.mp, Equiv.symm, DFunLike.coe, ContinuousMap.piEquiv
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
s_1 : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
ι : Type u_1
Y : ι → Type v
inst_5 : (i : ι) → TopologicalSpace (Y i)
inst_6 : ∀ (i : ι), TietzeExtension.{u, v} (Y i)
X_1 : Type u
inst_7 : TopologicalSpace X_1
inst_8 : NormalSpace X_1
s : Set X_1
hs : IsClosed[inst_7] s
f : C((↑s : Type u), (i : ι) → Y i)
g' : (x : ι) → ContinuousMap.{u, v} X_1 (Y x)
hg' :
  ∀ (x : ι),
    ContinuousMap.restrict s (g' x) =
      (Equiv.symm (ContinuousMap.piEquiv (↑s : Type u) Y) :
          (a : C((↑s : Type u), (i : ι) → Y i)) → (i : ι) → C((↑s : Type u), Y i))
        f x
h :
  ∀ (x : (↑s : Type u)) (i : ι),
    Eq.{v + 1} (α := Y i)
      ((ContinuousMap.restrict s
              ((ContinuousMap.piEquiv X_1 Y : (a : (i : ι) → C(X_1, Y i)) → C(X_1, (i : ι) → Y i)) g') :
            (a : (↑s : Type u)) → (i : ι) → Y i)
          x i :
        Y i)
      ((f : (a : (↑s : Type u)) → (i : ι) → Y i) x i : Y i)
⊢ ContinuousMap.restrict s ((ContinuousMap.piEquiv X_1 Y : (a : (i : ι) → C(X_1, Y i)) → C(X_1, (i : ι) → Y i)) g') = f

Tactic:
ext x i
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
s_1 : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
ι : Type u_1
Y : ι → Type v
inst_5 : (i : ι) → TopologicalSpace (Y i)
inst_6 : ∀ (i : ι), TietzeExtension.{u, v} (Y i)
X_1 : Type u
inst_7 : TopologicalSpace X_1
inst_8 : NormalSpace X_1
s : Set X_1
hs : IsClosed[inst_7] s
f : C((↑s : Type u), (i : ι) → Y i)
g' : (x : ι) → ContinuousMap.{u, v} X_1 (Y x)
hg' :
  ∀ (x : ι),
    ContinuousMap.restrict s (g' x) =
      (Equiv.symm (ContinuousMap.piEquiv (↑s : Type u) Y) :
          (a : C((↑s : Type u), (i : ι) → Y i)) → (i : ι) → C((↑s : Type u), Y i))
        f x
x : (↑s : Type u)
i : ι
⊢ Eq.{v + 1} (α := Y i)
    ((ContinuousMap.restrict s
            ((ContinuousMap.piEquiv X_1 Y : (a : (i : ι) → C(X_1, Y i)) → C(X_1, (i : ι) → Y i)) g') :
          (a : (↑s : Type u)) → (i : ι) → Y i)
        x i :
      Y i)
    ((f : (a : (↑s : Type u)) → (i : ι) → Y i) x i : Y i)

Tactic:
congrm($(hg' i) x)
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
s_1 : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
ι : Type u_1
Y : ι → Type v
inst_5 : (i : ι) → TopologicalSpace (Y i)
inst_6 : ∀ (i : ι), TietzeExtension.{u, v} (Y i)
X_1 : Type u
inst_7 : TopologicalSpace X_1
inst_8 : NormalSpace X_1
s : Set X_1
hs : IsClosed[inst_7] s
f : C((↑s : Type u), (i : ι) → Y i)
g' : (x : ι) → ContinuousMap.{u, v} X_1 (Y x)
hg' :
  ∀ (x : ι),
    ContinuousMap.restrict s (g' x) =
      (Equiv.symm (ContinuousMap.piEquiv (↑s : Type u) Y) :
          (a : C((↑s : Type u), (i : ι) → Y i)) → (i : ι) → C((↑s : Type u), Y i))
        f x
⊢ ∃ (g : C(X_1, (i : ι) → Y i)), ContinuousMap.restrict s g = f

Tactic:
exact ⟨ContinuousMap.piEquiv _ _ g', by ext x i; congrm($(hg' i) x)⟩
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
s_1 : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
Y : Type v
Z : Type w
inst_5 : TopologicalSpace Y
inst_6 : TietzeExtension Y
inst_7 : TopologicalSpace Z
inst_8 : TietzeExtension Z
X_1 : Type u
inst_9 : TopologicalSpace X_1
inst_10 : NormalSpace X_1
s : Set X_1
hs : IsClosed[inst_9] s
f : C((↑s : Type u), Y × Z)
obtain :
  ∀ (g₁ : C(X_1, Y)) (hg₁ : ContinuousMap.restrict s g₁ = ContinuousMap.comp ContinuousMap.fst f),
    ∃ (g : C(X_1, Y × Z)), ContinuousMap.restrict s g = f
⊢ ∃ (g : C(X_1, Y × Z)), ContinuousMap.restrict s g = f

Tactic:
obtain ⟨g₁, hg₁⟩ := (ContinuousMap.fst.comp f).exists_restrict_eq hs

Premises used: ContinuousMap.comp, ContinuousMap.exists_restrict_eq, ContinuousMap.fst
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
s_1 : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
Y : Type v
Z : Type w
inst_5 : TopologicalSpace Y
inst_6 : TietzeExtension Y
inst_7 : TopologicalSpace Z
inst_8 : TietzeExtension Z
X_1 : Type u
inst_9 : TopologicalSpace X_1
inst_10 : NormalSpace X_1
s : Set X_1
hs : IsClosed[inst_9] s
f : C((↑s : Type u), Y × Z)
g₁ : C(X_1, Y)
hg₁ : ContinuousMap.restrict s g₁ = ContinuousMap.comp ContinuousMap.fst f
obtain :
  ∀ (g₂ : C(X_1, Z)) (hg₂ : ContinuousMap.restrict s g₂ = ContinuousMap.comp ContinuousMap.snd f),
    ∃ (g : C(X_1, Y × Z)), ContinuousMap.restrict s g = f
⊢ ∃ (g : C(X_1, Y × Z)), ContinuousMap.restrict s g = f

Tactic:
obtain ⟨g₂, hg₂⟩ := (ContinuousMap.snd.comp f).exists_restrict_eq hs

Premises used: ContinuousMap.comp, ContinuousMap.snd, ContinuousMap.exists_restrict_eq
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
s_1 : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
Y : Type v
Z : Type w
inst_5 : TopologicalSpace Y
inst_6 : TietzeExtension Y
inst_7 : TopologicalSpace Z
inst_8 : TietzeExtension Z
X_1 : Type u
inst_9 : TopologicalSpace X_1
inst_10 : NormalSpace X_1
s : Set X_1
hs : IsClosed[inst_9] s
f : C((↑s : Type u), Y × Z)
g₁ : C(X_1, Y)
hg₁ : ContinuousMap.restrict s g₁ = ContinuousMap.comp ContinuousMap.fst f
g₂ : C(X_1, Z)
hg₂ : ContinuousMap.restrict s g₂ = ContinuousMap.comp ContinuousMap.snd f
h :
  ∀ (x : (↑s : Type u)),
    Eq (α := Y × Z) ((ContinuousMap.restrict s (g₁.prodMk g₂) : (a : (↑s : Type u)) → Y × Z) x : Y × Z)
      ((f : (a : (↑s : Type u)) → Y × Z) x : Y × Z)
⊢ ContinuousMap.restrict s (g₁.prodMk g₂) = f

Tactic:
ext1 x
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
s_1 : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
Y : Type v
Z : Type w
inst_5 : TopologicalSpace Y
inst_6 : TietzeExtension Y
inst_7 : TopologicalSpace Z
inst_8 : TietzeExtension Z
X_1 : Type u
inst_9 : TopologicalSpace X_1
inst_10 : NormalSpace X_1
s : Set X_1
hs : IsClosed[inst_9] s
f : C((↑s : Type u), Y × Z)
g₁ : C(X_1, Y)
hg₁ : ContinuousMap.restrict s g₁ = ContinuousMap.comp ContinuousMap.fst f
g₂ : C(X_1, Z)
hg₂ : ContinuousMap.restrict s g₂ = ContinuousMap.comp ContinuousMap.snd f
x : (↑s : Type u)
⊢ Eq (α := Y × Z) ((ContinuousMap.restrict s (g₁.prodMk g₂) : (a : (↑s : Type u)) → Y × Z) x : Y × Z)
    ((f : (a : (↑s : Type u)) → Y × Z) x : Y × Z)

Tactic:
congrm(($(hg₁) x), $(hg₂) x)
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
s_1 : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
Y : Type v
Z : Type w
inst_5 : TopologicalSpace Y
inst_6 : TietzeExtension Y
inst_7 : TopologicalSpace Z
inst_8 : TietzeExtension Z
X_1 : Type u
inst_9 : TopologicalSpace X_1
inst_10 : NormalSpace X_1
s : Set X_1
hs : IsClosed[inst_9] s
f : C((↑s : Type u), Y × Z)
g₁ : C(X_1, Y)
hg₁ : ContinuousMap.restrict s g₁ = ContinuousMap.comp ContinuousMap.fst f
g₂ : C(X_1, Z)
hg₂ : ContinuousMap.restrict s g₂ = ContinuousMap.comp ContinuousMap.snd f
⊢ ∃ (g : C(X_1, Y × Z)), ContinuousMap.restrict s g = f

Tactic:
exact ⟨g₁.prodMk g₂, by ext1 x; congrm(($(hg₁) x), $(hg₂) x)⟩
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
s : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
Y : Type v
inst_5 : TopologicalSpace Y
inst_6 : Nonempty Y
inst_7 : Subsingleton Y
X_1 : Type u
inst_8 : TopologicalSpace X_1
inst_9 : NormalSpace X_1
x : Set X_1
h_1 : IsClosed[inst_8] x
f : ContinuousMap.{u, v} (↑x : Type u) Y
y : Y
h :
  ∀ (a : (↑x : Type u)),
    Eq.{v + 1} (α := Y) ((ContinuousMap.restrict x (ContinuousMap.const X_1 y) : (a : (↑x : Type u)) → Y) a : Y)
      ((f : (a : (↑x : Type u)) → Y) a : Y)
⊢ ContinuousMap.restrict x (ContinuousMap.const X_1 y) = f

Tactic:
ext
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X₁ : Type u₁
inst : TopologicalSpace X₁
X : Type u
inst_1 : TopologicalSpace X
inst_2 : NormalSpace X
s : Set X
e : X₁ → X
Y_1 : Type v
inst_3 : TopologicalSpace Y_1
inst_4 : TietzeExtension Y_1
Y : Type v
inst_5 : TopologicalSpace Y
inst_6 : Nonempty Y
inst_7 : Subsingleton Y
X_1 : Type u
inst_8 : TopologicalSpace X_1
inst_9 : NormalSpace X_1
x : Set X_1
h : IsClosed[inst_8] x
f : ContinuousMap.{u, v} (↑x : Type u) Y
y : Y
a : (↑x : Type u)
⊢ Eq.{v + 1} (α := Y) ((ContinuousMap.restrict x (ContinuousMap.const X_1 y) : (a : (↑x : Type u)) → Y) a : Y)
    ((f : (a : (↑x : Type u)) → Y) a : Y)

Tactic:
subsingleton
-- Module: Mathlib.Topology.TietzeExtension
Goal:
Y : Type v
Z : Type w
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
inst_2 : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X : Type u
inst_3 : TopologicalSpace X
inst_4 : NormalSpace X
s : Set X
hs : IsClosed[inst_3] s
f : ContinuousMap.{u, v} (↑s : Type u) Y
obtain : ∀ (g : C(X, Z)) (hg : ContinuousMap.restrict s g = ι.comp f), ∃ (g : C(X, Y)), ContinuousMap.restrict s g = f
⊢ ∃ (g : C(X, Y)), ContinuousMap.restrict s g = f

Tactic:
obtain ⟨g, hg⟩ := (ι.comp f).exists_restrict_eq hs

Premises used: ContinuousMap.comp, ContinuousMap.exists_restrict_eq
-- Module: Mathlib.Topology.TietzeExtension
Goal:
Y : Type v
Z : Type w
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
inst_2 : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X : Type u
inst_3 : TopologicalSpace X
inst_4 : NormalSpace X
s : Set X
hs : IsClosed[inst_3] s
f : ContinuousMap.{u, v} (↑s : Type u) Y
g : C(X, Z)
hg : ContinuousMap.restrict s g = ι.comp f
h₁ : ContinuousMap.restrict s (r.comp g) = f
⊢ ∃ (g : C(X, Y)), ContinuousMap.restrict s g = f

Tactic:
use r.comp g

Premises used: ContinuousMap.comp
-- Module: Mathlib.Topology.TietzeExtension
Goal:
Y : Type v
Z : Type w
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
inst_2 : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X : Type u
inst_3 : TopologicalSpace X
inst_4 : NormalSpace X
s : Set X
hs : IsClosed[inst_3] s
f : ContinuousMap.{u, v} (↑s : Type u) Y
g : C(X, Z)
hg : ContinuousMap.restrict s g = ι.comp f
h₁ :
  ∀ (x : (↑s : Type u)),
    Eq.{v + 1} (α := Y) ((ContinuousMap.restrict s (r.comp g) : (a : (↑s : Type u)) → Y) x : Y)
      ((f : (a : (↑s : Type u)) → Y) x : Y)
⊢ ContinuousMap.restrict s (r.comp g) = f

Tactic:
ext1 x
-- Module: Mathlib.Topology.TietzeExtension
Goal:
Y : Type v
Z : Type w
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
inst_2 : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X : Type u
inst_3 : TopologicalSpace X
inst_4 : NormalSpace X
s : Set X
hs : IsClosed[inst_3] s
f : ContinuousMap.{u, v} (↑s : Type u) Y
g : C(X, Z)
hg : ContinuousMap.restrict s g = ι.comp f
x : (↑s : Type u)
⊢ r.comp (ContinuousMap.restrict s g) = r.comp (ι.comp f)

Tactic:
have := congr(r.comp $(hg))
-- Module: Mathlib.Topology.TietzeExtension
Goal:
Y : Type v
Z : Type w
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
inst_2 : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X : Type u
inst_3 : TopologicalSpace X
inst_4 : NormalSpace X
s : Set X
hs : IsClosed[inst_3] s
f : ContinuousMap.{u, v} (↑s : Type u) Y
g : C(X, Z)
hg : ContinuousMap.restrict s g = ι.comp f
x : (↑s : Type u)
this : r.comp (ContinuousMap.restrict s g) = r.comp (ι.comp f)
⊢ r.comp (ContinuousMap.restrict s g) = f

Tactic:
rw [← r.comp_assoc ι, h, f.id_comp] at this

Premises used: ContinuousMap.id_comp, ContinuousMap.comp_assoc
-- Module: Mathlib.Topology.TietzeExtension
Goal:
Y : Type v
Z : Type w
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
inst_2 : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X : Type u
inst_3 : TopologicalSpace X
inst_4 : NormalSpace X
s : Set X
hs : IsClosed[inst_3] s
f : ContinuousMap.{u, v} (↑s : Type u) Y
g : C(X, Z)
hg : ContinuousMap.restrict s g = ι.comp f
x : (↑s : Type u)
this : r.comp (ContinuousMap.restrict s g) = f
⊢ Eq.{v + 1} (α := Y) ((ContinuousMap.restrict s (r.comp g) : (a : (↑s : Type u)) → Y) x : Y)
    ((f : (a : (↑s : Type u)) → Y) x : Y)

Tactic:
congrm($this x)