awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : C(α, β)
x : α
⊢ ContinuousAt.{u_1, u_2} (Y := β) (⇑f : (a : α) → β) x

Tactic:
map_continuousAt f x

Premises used: map_continuousAt
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : C(α, β)
x y : α
h : x ⤳ y
⊢ Specializes.{u_2} (X := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
h.map f.2

Premises used: ContinuousMap.continuous_toFun, Specializes.map
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : C(α, β)
inst_4 : DiscreteTopology α
x : C(α, β)
h :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := β)
      (((fun (f : α → β) ↦ ({ toFun := f, continuous_toFun := ⋯ } : C(α, β)))
              ((fun (f : C(α, β)) ↦ ((⇑f : (a : α) → β) : (a : α) → β)) x) :
            (a : α) → β)
          a :
        β)
      ((x : (a : α) → β) a : β)
⊢ (fun (f : α → β) ↦ ({ toFun := f, continuous_toFun := ⋯ } : C(α, β)))
      ((fun (f : C(α, β)) ↦ ((⇑f : (a : α) → β) : (a : α) → β)) x) =
    x

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : C(α, β)
inst_4 : DiscreteTopology α
x : C(α, β)
a : α
⊢ Eq.{u_2 + 1} (α := β)
    (((fun (f : α → β) ↦ ({ toFun := f, continuous_toFun := ⋯ } : C(α, β)))
            ((fun (f : C(α, β)) ↦ ((⇑f : (a : α) → β) : (a : α) → β)) x) :
          (a : α) → β)
        a :
      β)
    ((x : (a : α) → β) a : β)

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : C(α, β)
inst_4 : DiscreteTopology α
x : α → β
h :
  ∀ (x_1 : α),
    (fun (f : C(α, β)) ↦ ((⇑f : (a : α) → β) : (a : α) → β))
        ((fun (f : α → β) ↦ ({ toFun := f, continuous_toFun := ⋯ } : C(α, β))) x) x_1 =
      x x_1
⊢ (fun (f : C(α, β)) ↦ ((⇑f : (a : α) → β) : (a : α) → β))
      ((fun (f : α → β) ↦ ({ toFun := f, continuous_toFun := ⋯ } : C(α, β))) x) =
    x

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : C(α, β)
inst_4 : DiscreteTopology α
x : α → β
x_1 : α
⊢ (fun (f : C(α, β)) ↦ ((⇑f : (a : α) → β) : (a : α) → β))
      ((fun (f : α → β) ↦ ({ toFun := f, continuous_toFun := ⋯ } : C(α, β))) x) x_1 =
    x x_1

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : DiscreteTopology α
⊢ Eq (α := (a : C(α, β)) → α → β) (⇑equivFnOfDiscrete : (a : C(α, β)) → α → β) (DFunLike.coe (β := fun (a : α) ↦ β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : DiscreteTopology α
f : α → β
⊢ (⇑((Equiv.symm equivFnOfDiscrete : (a : α → β) → C(α, β)) f : C(α, β)) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Eq (α := (a : α) → α) (⇑(ContinuousMap.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
b : β
⊢ (⇑(const α b) : (a : α) → β) = Function.const α b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
⊢ (ContinuousMap.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
b : β
a : α
⊢ (const α b : (a : α) → β) a = b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : C(β, γ)
g : C(α, β)
⊢ Eq (α := (a : α) → γ) (⇑(f.comp g) : (a : α) → γ)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : C(β, γ)
g : C(α, β)
a : α
⊢ Eq.{u_3 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : C(γ, δ)
g : C(β, γ)
h : C(α, β)
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: ContinuousMap.comp, rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : C(α, β)
⊢ comp (ContinuousMap.id β) f = f

Tactic:
ext fun _ => rfl

Premises used: ContinuousMap.ext, rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : C(α, β)
⊢ f.comp (ContinuousMap.id α) = f

Tactic:
ext fun _ => rfl

Premises used: ContinuousMap.ext, rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
c : γ
f : C(α, β)
⊢ Eq (α := C(α, γ)) (comp (const β c) f) (const α c)

Tactic:
ext fun _ => rfl

Premises used: ContinuousMap.ext, rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : C(β, γ)
b : β
⊢ Eq (α := C(α, γ)) (f.comp (const α b)) (const α ((f : (a : β) → γ) b))

Tactic:
ext fun _ => rfl

Premises used: ContinuousMap.ext, rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f₁ f₂ : C(β, γ)
g : C(α, β)
hg : Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑g : (a : α) → β)
⊢ f₁.comp g = f₂.comp g ↔ f₁ = f₂

Tactic:
⟨fun h => ext <| hg.forall.2 <| DFunLike.ext_iff.1 h, congr_arg (ContinuousMap.comp · g)⟩

Premises used: Iff.mpr, Function.Surjective.forall, ContinuousMap.comp, DFunLike.ext_iff, congr_arg, ContinuousMap.ext, Iff.intro, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : C(β, γ)
g₁ g₂ : C(α, β)
hf : Injective.{u_2 + 1, u_3 + 1} (α := β) (β := γ) (⇑f : (a : β) → γ)
h : f.comp g₁ = f.comp g₂
a : α
rw : Eq.{u_3 + 1} (α := γ) ((f.comp g₁ : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_3 + 1} (α := γ) ((f.comp g₂ : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := γ) ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_3 + 1} (α := γ) ((f : (a : β) → γ) ((g₁ : (a : α) → β) a : β) : γ)
    ((f : (a : β) → γ) ((g₂ : (a : α) → β) a : β) : γ)

Tactic:
rw [← comp_apply, h, comp_apply]

Premises used: ContinuousMap.comp_apply
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : C(α, β)
inst_4 : Nonempty α
inst_5 : Nontrivial β
⊢ Nontrivial C(α, β)

Tactic:
⟨let ⟨b₁, b₂, hb⟩ := exists_pair_ne β
  ⟨const _ b₁, const _ b₂, fun h => hb <| DFunLike.congr_fun h <| Classical.arbitrary α⟩⟩

Premises used: DFunLike.congr_fun, Exists, Ne, Nontrivial.mk, Exists.intro, Classical.arbitrary, ContinuousMap.const, _private.0.ContinuousMap.instNontrivialOfNonempty.match_1, exists_pair_ne
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : C(α, β)
X₁ : Type u_5
X₂ : Type u_6
Y₁ : Type u_7
Y₂ : Type u_8
inst_4 : TopologicalSpace X₁
inst_5 : TopologicalSpace X₂
inst_6 : TopologicalSpace Y₁
inst_7 : TopologicalSpace Y₂
e : X₁ ≃ₜ X₂
e' : Y₁ ≃ₜ Y₂
x : C(X₁, Y₁)
⊢ (fun (g : C(X₂, Y₂)) ↦
        { toFun := (⇑e'.symm : (a : Y₂) → Y₁), continuous_toFun := ⋯ : C(Y₂, Y₁) }.comp
          (g.comp { toFun := (⇑e : (a : X₁) → X₂), continuous_toFun := ⋯ : C(X₁, X₂) }))
      ((fun (f : C(X₁, Y₁)) ↦
          { toFun := (⇑e' : (a : Y₁) → Y₂), continuous_toFun := ⋯ : C(Y₁, Y₂) }.comp
            (f.comp { toFun := (⇑e.symm : (a : X₂) → X₁), continuous_toFun := ⋯ : C(X₂, X₁) }))
        x) =
    x

Tactic:
aesop
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : C(α, β)
X₁ : Type u_5
X₂ : Type u_6
Y₁ : Type u_7
Y₂ : Type u_8
inst_4 : TopologicalSpace X₁
inst_5 : TopologicalSpace X₂
inst_6 : TopologicalSpace Y₁
inst_7 : TopologicalSpace Y₂
e : X₁ ≃ₜ X₂
e' : Y₁ ≃ₜ Y₂
x : C(X₂, Y₂)
⊢ (fun (f : C(X₁, Y₁)) ↦
        { toFun := (⇑e' : (a : Y₁) → Y₂), continuous_toFun := ⋯ : C(Y₁, Y₂) }.comp
          (f.comp { toFun := (⇑e.symm : (a : X₂) → X₁), continuous_toFun := ⋯ : C(X₂, X₁) }))
      ((fun (g : C(X₂, Y₂)) ↦
          { toFun := (⇑e'.symm : (a : Y₂) → Y₁), continuous_toFun := ⋯ : C(Y₂, Y₁) }.comp
            (g.comp { toFun := (⇑e : (a : X₁) → X₂), continuous_toFun := ⋯ : C(X₁, X₂) }))
        x) =
    x

Tactic:
aesop
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β₁ : Type u_7
β₂ : Type u_8
inst_1 : TopologicalSpace β₁
inst_2 : TopologicalSpace β₂
f : C(α, β₁)
g : C(α, β₂)
a : α
⊢ Eq (α := β₁ × β₂) ((f.prodMk g : (a : α) → β₁ × β₂) a : β₁ × β₂)
    (((f : (a : α) → β₁) a, (g : (a : α) → β₂) a) : β₁ × β₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f_1 g : C(α, β)
I : Type u_5
A : Type u_6
X : I → Type u_7
inst_4 : TopologicalSpace A
inst_5 : (i : I) → TopologicalSpace (X i)
f : (i : I) → ContinuousMap.{u_7, u_6} (X i) A
⊢ Continuous[instTopologicalSpaceSigma, inst_4] fun (ig : (i : I) × X i) ↦
    (f (ig.fst (β := fun (i : I) ↦ X i)) : (a : X ig.fst) → A) (ig.snd (β := fun (i : I) ↦ X i))

Tactic:
continuity
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
I : Type u_5
A : Type u_6
X : I → Type u_7
inst : TopologicalSpace A
inst_1 : (i : I) → TopologicalSpace (X i)
f : (i : I) → ContinuousMap.{u_6, u_7} A (X i)
a : A
⊢ Eq (α := (i : I) → X i) ((pi (X := X) f : (a : A) → (i : I) → X i) a : (i : I) → X i) fun (i : I) ↦
    ((f i : (a : A) → X i) a : X i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : C(α, β)
⊢ Eq (α := (a : (↑s : Type u_1)) → β) ((⇑(restrict s f) : (a : (↑s : Type u_1)) → β) : (a : (↑s : Type u_1)) → β)
    (s.restrict (π := fun (a : α) ↦ β) (⇑f : (a : α) → β) : (a : (↑s : Type u_1)) → β)

Tactic:
rfl

Premises used: Set.restrict, rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : C(α, β)
s : Set α
x : (↑s : Type u_1)
⊢ Eq.{u_2 + 1} (α := β) ((restrict s f : (a : (↑s : Type u_1)) → β) x : β) ((f : (a : α) → β) (↑x : α) : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : C(α, β)
s : Set α
x : α
hx : x ∈ s
⊢ Eq.{u_2 + 1} (α := β) ((restrict s f : (a : (↑s : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) : β)
    ((f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : T2Space β
s : Set α
hs : Dense s
⊢ Injective (α := C(α, β)) (restrict s)

Tactic:
fun f g h ↦
  DFunLike.ext' <| (map_continuous f).ext_on hs (map_continuous g) <|
    Set.restrict_eq_restrict_iff.1 <| congr_arg DFunLike.coe h

Premises used: congr_arg, Continuous.ext_on, Iff.mp, ContinuousMapClass.map_continuous, Function.Injective, Set.restrict_eq_restrict_iff, DFunLike.ext', DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
g : C(α, β)
hf : Continuous[inst, inst_1] f
⊢ mkD f g = { toFun := f, continuous_toFun := hf }

Tactic:
simp only [mkD, hf, ↓reduceDIte]

Premises used: reduceDIte, ContinuousMap.mkD
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
g : C(α, β)
hf : ¬Continuous[inst, inst_1] f
⊢ mkD f g = g

Tactic:
simp only [mkD, hf, ↓reduceDIte]

Premises used: reduceDIte, ContinuousMap.mkD
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
g : C(α, β)
x : α
hf : Continuous[inst, inst_1] f
rw : ({ toFun := f, continuous_toFun := hf : C(α, β) } : (a : α) → β) x = f x
rw₁ rw₂ : f x = f x
⊢ (mkD f g : (a : α) → β) x = f x

Tactic:
rw [mkD_of_continuous hf, coe_mk]

Premises used: ContinuousMap.coe_mk, ContinuousMap.mkD_of_continuous
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
g : ContinuousMap.{u_1, u_2} (↑s : Type u_1) β
hf : ContinuousOn f s
⊢ mkD (s.restrict (π := fun (a : α) ↦ β) f) g = { toFun := s.restrict (π := fun (a : α) ↦ β) f, continuous_toFun := ⋯ }

Tactic:
mkD_of_continuous hf.restrict

Premises used: ContinuousOn.restrict, ContinuousMap.mkD_of_continuous
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
g : ContinuousMap.{u_1, u_2} (↑s : Type u_1) β
hf : ¬ContinuousOn f s
⊢ ¬Continuous[instTopologicalSpaceSubtype, inst_1] (s.restrict (π := fun (a : α) ↦ β) f)

Tactic:
rw [continuousOn_iff_continuous_restrict] at hf

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
g : ContinuousMap.{u_1, u_2} (↑s : Type u_1) β
hf : ¬Continuous[instTopologicalSpaceSubtype, inst_1] (s.restrict (π := fun (a : α) ↦ β) f)
⊢ mkD (s.restrict (π := fun (a : α) ↦ β) f) g = g

Tactic:
mkD_of_not_continuous hf

Premises used: ContinuousMap.mkD_of_not_continuous
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
g : ContinuousMap.{u_1, u_2} (↑s : Type u_1) β
hf : ¬Continuous[instTopologicalSpaceSubtype, inst_1] (s.restrict (π := fun (a : α) ↦ β) f)
⊢ mkD (s.restrict (π := fun (a : α) ↦ β) f) g = g

Tactic:
exact mkD_of_not_continuous hf

Premises used: ContinuousMap.mkD_of_not_continuous
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Set α
f : α → β
g : ContinuousMap.{u_1, u_2} (↑s : Type u_1) β
x : (↑s : Type u_1)
hf : ContinuousOn f s
rw :
  ({ toFun := s.restrict (π := fun (a : α) ↦ β) f, continuous_toFun := ⋯ :
          ContinuousMap.{u_1, u_2} (↑s : Type u_1) β } :
        (a : (↑s : Type u_1)) → β)
      x =
    f (↑x : α)
rw₁ : s.restrict (π := fun (a : α) ↦ β) f x = f (↑x : α)
rw₂ rw₃ : f (↑x : α) = f (↑x : α)
⊢ (mkD (s.restrict (π := fun (a : α) ↦ β) f) g : (a : (↑s : Type u_1)) → β) x = f (↑x : α)

Tactic:
rw [mkD_of_continuousOn hf, coe_mk, Set.restrict_apply]

Premises used: Set.restrict_apply, ContinuousMap.mkD_of_continuousOn, ContinuousMap.coe_mk
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : C(α, β)
⊢ mkD (⇑f : (a : α) → β) g = f

Tactic:
mkD_of_continuous f.continuous

Premises used: ContinuousMap.continuous, ContinuousMap.mkD_of_continuous
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → ContinuousMap.{u_1, u_2} (↑(S i) : Type u_1) β
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    Eq.{u_2 + 1} (α := β) ((φ i : (a : (↑(S i) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) : β)
      ((φ j : (a : (↑(S j) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj) : β)
hS : ∀ (x : α), ∃ (i : ι), S i ∈ 𝓝 x
H : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), S i) Set.univ
i : ι
rw :
  Continuous[instTopologicalSpaceSubtype, inst_1]
    ((S i).restrict (π := fun (a : α) ↦ β)
      (Set.liftCover S (fun (i : ι) ↦ (⇑(φ i) : (a : (↑(S i) : Type u_1)) → β)) hφ H))
⊢ ContinuousOn (Set.liftCover S (fun (i : ι) ↦ (⇑(φ i) : (a : (↑(S i) : Type u_1)) → β)) hφ H) (S i)

Tactic:
rw [continuousOn_iff_continuous_restrict]

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : C(α, β)
ι : Type u_5
S : ι → Set α
φ : (i : ι) → ContinuousMap.{u_1, u_2} (↑(S i) : Type u_1) β
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    Eq.{u_2 + 1} (α := β) ((φ i : (a : (↑(S i) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) : β)
      ((φ j : (a : (↑(S j) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj) : β)
hS : ∀ (x : α), ∃ (i : ι), S i ∈ 𝓝 x
H : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), S i) Set.univ
i : ι
⊢ Continuous[instTopologicalSpaceSubtype, inst_1]
    ((S i).restrict (π := fun (a : α) ↦ β)
      (Set.liftCover S (fun (i : ι) ↦ (⇑(φ i) : (a : (↑(S i) : Type u_1)) → β)) hφ H))

Tactic:
simpa +unfoldPartialApp only [Set.restrict, Set.liftCover_coe]
      using map_continuous (φ i)

Premises used: Set.liftCover_coe, ContinuousMapClass.map_continuous, Set.restrict
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → ContinuousMap.{u_1, u_2} (↑(S i) : Type u_1) β
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    Eq.{u_2 + 1} (α := β) ((φ i : (a : (↑(S i) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) : β)
      ((φ j : (a : (↑(S j) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj) : β)
hS : ∀ (x : α), ∃ (i : ι), S i ∈ 𝓝 x
i : ι
x : (↑(S i) : Type u_1)
rw :
  Eq.{u_2 + 1} (α := β)
    (({ toFun := Set.liftCover S (fun (i : ι) ↦ (⇑(φ i) : (a : (↑(S i) : Type u_1)) → β)) hφ ⋯, continuous_toFun := ⋯ :
            C(α, β) } :
          (a : α) → β)
        (↑x : α) :
      β)
    ((φ i : (a : (↑(S i) : Type u_1)) → β) x : β)
rw₁ :
  Set.liftCover S (fun (i : ι) ↦ (⇑(φ i) : (a : (↑(S i) : Type u_1)) → β)) hφ ⋯ (↑x : α) =
    (φ i : (a : (↑(S i) : Type u_1)) → β) x
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := β) ((φ i : (a : (↑(S i) : Type u_1)) → β) x : β) ((φ i : (a : (↑(S i) : Type u_1)) → β) x : β)
⊢ Eq.{u_2 + 1} (α := β) ((liftCover S φ hφ hS : (a : α) → β) (↑x : α) : β) ((φ i : (a : (↑(S i) : Type u_1)) → β) x : β)

Tactic:
rw [liftCover, coe_mk, Set.liftCover_coe _]

Premises used: Set.liftCover_coe, ContinuousMap.liftCover, ContinuousMap.coe_mk
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → ContinuousMap.{u_1, u_2} (↑(S i) : Type u_1) β
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    Eq.{u_2 + 1} (α := β) ((φ i : (a : (↑(S i) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) : β)
      ((φ j : (a : (↑(S j) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj) : β)
hS : ∀ (x : α), ∃ (i : ι), S i ∈ 𝓝 x
i : ι
h :
  ∀ (a : (↑(S i) : Type u_1)),
    Eq.{u_2 + 1} (α := β) ((restrict (S i) (liftCover S φ hφ hS) : (a : (↑(S i) : Type u_1)) → β) a : β)
      ((φ i : (a : (↑(S i) : Type u_1)) → β) a : β)
⊢ restrict (S i) (liftCover S φ hφ hS) = φ i

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → ContinuousMap.{u_1, u_2} (↑(S i) : Type u_1) β
hφ :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    Eq.{u_2 + 1} (α := β) ((φ i : (a : (↑(S i) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) : β)
      ((φ j : (a : (↑(S j) : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj) : β)
hS : ∀ (x : α), ∃ (i : ι), S i ∈ 𝓝 x
i : ι
a : (↑(S i) : Type u_1)
⊢ Eq.{u_2 + 1} (α := β) ((restrict (S i) (liftCover S φ hφ hS) : (a : (↑(S i) : Type u_1)) → β) a : β)
    ((φ i : (a : (↑(S i) : Type u_1)) → β) a : β)

Tactic:
simp only [restrict_apply, liftCover_coe]

Premises used: ContinuousMap.liftCover_coe, ContinuousMap.restrict_apply
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
A : Set (Set α)
F : (s : Set α) → s ∈ A → ContinuousMap.{u_1, u_2} (↑s : Type u_1) β
hF :
  ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
    Eq.{u_2 + 1} (α := β) ((F s hs : (a : (↑s : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hxi) : β)
      ((F t ht : (a : (↑t : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hxj) : β)
hA : ∀ (x : α), ∃ i ∈ A, i ∈ 𝓝 x
s : Set α
hs : s ∈ A
x : (↑s : Type u_1)
x' : (↑(↑(Subtype.mk (p := fun (x : Set α) ↦ x ∈ A) s hs) : Set α) : Type u_1) := x
delta :
  Eq.{u_2 + 1} (α := β)
    ((let F_1 : (i : (↑A : Type u_1)) → ContinuousMap.{u_1, u_2} (↑(↑i : Set α) : Type u_1) β :=
            fun (i : (↑A : Type u_1)) ↦ F (↑i : Set α) ⋯;
          liftCover (Subtype.val (p := fun (x : Set α) ↦ x ∈ A)) F_1 ⋯ ⋯ :
          (a : α) → β)
        (↑x : α) :
      β)
    ((F s hs : (a : (↑s : Type u_1)) → β) x : β)
⊢ Eq.{u_2 + 1} (α := β) ((liftCover' A F hF hA : (a : α) → β) (↑x : α) : β) ((F s hs : (a : (↑s : Type u_1)) → β) x : β)

Tactic:
delta liftCover'

Premises used: ContinuousMap.liftCover'