awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_3
inst : Zero X
inst_1 : Zero R
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace R
⊢ Eq (α := Set C(X, R)) (range (ι := C(X, R)₀) _root_.toContinuousMap)
    {f : C(X, R) | Eq.{u_3 + 1} (α := R) ((f : (a : X) → R) 0 : R) (0 : R)}

Tactic:
Set.ext fun f ↦ ⟨fun ⟨f', hf'⟩ ↦ hf' ▸ map_zero f', fun hf ↦ ⟨⟨f, hf⟩, rfl⟩⟩

Premises used: Set.ext, setOf, Membership.mem, _private.0.ContinuousMapZero.range_toContinuousMap.match_1, Eq.rec, map_zero, Iff.intro, Exists.intro, ContinuousMapZero.mk, OfNat.ofNat, Eq, DFunLike.coe, rfl
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
g : C(Y, R)₀
f : C(X, Y)₀
x : X
⊢ Eq.{u_3 + 1} (α := R) ((g.comp f : (a : X) → R) x : R) ((g : (a : Y) → R) ((f : (a : X) → Y) x : Y) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_3
inst : Zero X
inst_1 : Zero R
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace R
inst_4 : PartialOrder R
f g : C(X, R)₀
⊢ f ≤ g ↔ ∀ (x : X), LE.le.{u_3} (α := R) ((f : (a : X) → R) x : R) ((g : (a : X) → R) x : R)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
inst_6 : T0Space R
⊢ T0Space C(X, R)₀

Tactic:
isEmbedding_toContinuousMap.t0Space

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, Topology.IsEmbedding.t0Space
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
inst_6 : R0Space R
⊢ R0Space C(X, R)₀

Tactic:
isEmbedding_toContinuousMap.r0Space

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, Topology.IsInducing.r0Space, Topology.IsEmbedding.toIsInducing
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
inst_6 : T1Space R
⊢ T1Space C(X, R)₀

Tactic:
isEmbedding_toContinuousMap.t1Space

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, Topology.IsEmbedding.t1Space
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
inst_6 : R1Space R
⊢ R1Space C(X, R)₀

Tactic:
isEmbedding_toContinuousMap.r1Space

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, Topology.IsInducing.r1Space, Topology.IsEmbedding.toIsInducing
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
inst_6 : T2Space R
⊢ T2Space C(X, R)₀

Tactic:
isEmbedding_toContinuousMap.t2Space

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, Topology.IsEmbedding.t2Space
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
inst_6 : RegularSpace R
⊢ RegularSpace C(X, R)₀

Tactic:
isEmbedding_toContinuousMap.regularSpace

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, Topology.IsEmbedding.toIsInducing, Topology.IsInducing.regularSpace
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
inst_6 : T3Space R
⊢ T3Space C(X, R)₀

Tactic:
isEmbedding_toContinuousMap.t3Space

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, Topology.IsEmbedding.t3Space
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
⊢ ContinuousEvalConst C(X, R)₀ X R

Tactic:
.of_continuous_forget isEmbedding_toContinuousMap.continuous

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, ContinuousEvalConst.of_continuous_forget, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
inst_6 : LocallyCompactPair X R
⊢ ContinuousEval C(X, R)₀ X R

Tactic:
.of_continuous_forget isEmbedding_toContinuousMap.continuous

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, ContinuousEval.of_continuous_forget, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_3
inst : Zero X
inst_1 : Zero R
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace R
inst_4 : T1Space R
rw : IsClosed (X := C(X, R)) {f : C(X, R) | Eq.{u_3 + 1} (α := R) ((f : (a : X) → R) 0 : R) (0 : R)}
⊢ IsClosed (X := C(X, R)) (range (ι := C(X, R)₀) _root_.toContinuousMap)

Tactic:
rw [range_toContinuousMap]

Premises used: ContinuousMapZero.range_toContinuousMap
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_3
inst : Zero X
inst_1 : Zero R
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace R
inst_4 : T1Space R
⊢ IsClosed (X := C(X, R)) {f : C(X, R) | Eq.{u_3 + 1} (α := R) ((f : (a : X) → R) 0 : R) (0 : R)}

Tactic:
isClosed_singleton.preimage <| continuous_eval_const 0

Premises used: Set.Mem, setOf, Set.preimage, ContinuousEvalConst.continuous_eval_const, Set.singleton, IsClosed.preimage, OfNat.ofNat, isClosed_singleton
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_3
inst : Zero X
inst_1 : Zero R
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace R
inst_4 : T1Space R
⊢ IsClosed (X := C(X, R)) {f : C(X, R) | Eq.{u_3 + 1} (α := R) ((f : (a : X) → R) 0 : R) (0 : R)}

Tactic:
exact isClosed_singleton.preimage <| continuous_eval_const 0

Premises used: ContinuousEvalConst.continuous_eval_const, IsClosed.preimage, OfNat.ofNat, isClosed_singleton
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
f : C(X, Y)₀
rw :
  Continuous (X := C(Y, R)₀) (Y := C(X, R))
    (Function.comp (β := C(X, R)₀) _root_.toContinuousMap fun (g : C(Y, R)₀) ↦ g.comp f)
⊢ Continuous (Y := C(X, R)₀) fun (g : C(Y, R)₀) ↦ g.comp f

Tactic:
rw [continuous_induced_rng]

Premises used: continuous_induced_rng
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
f : C(X, Y)₀
change : Continuous (Y := C(X, R)) fun (g : C(Y, R)₀) ↦ ContinuousMap.comp (↑g : C(Y, R)) (↑f : C(X, Y))
⊢ Continuous (X := C(Y, R)₀) (Y := C(X, R))
    (Function.comp (β := C(X, R)₀) _root_.toContinuousMap fun (g : C(Y, R)₀) ↦ g.comp f)

Tactic:
change Continuous fun g : C(Y, R)₀ ↦ (g : C(Y, R)).comp (f : C(X, Y))

Premises used: Continuous, ContinuousMap.comp, toContinuousMap
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
f : C(X, Y)₀
⊢ Continuous (Y := C(X, R)) fun (g : C(Y, R)₀) ↦ ContinuousMap.comp (↑g : C(Y, R)) (↑f : C(X, Y))

Tactic:
fun_prop
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
g : C(Y, R)₀
hg : Injective.{u_2 + 1, u_3 + 1} (α := Y) (β := R) (⇑g : (a : Y) → R)
⊢ Injective (α := C(X, Y)₀) g.comp

Tactic:
fun _ _ h ↦ ext fun x ↦ hg congr($h x)

Premises used: ContinuousMapZero.ext, congrArg, id, Function.Injective, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
g : C(Y, R)₀
rw : Continuous (X := C(X, Y)₀) (Y := C(X, R)) (_root_.toContinuousMap ∘ g.comp)
⊢ Continuous (X := C(X, Y)₀) g.comp

Tactic:
rw [ContinuousMapZero.isEmbedding_toContinuousMap.continuous_iff]

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
g : C(Y, R)₀
⊢ Continuous (X := C(X, Y)₀) (Y := C(X, R)) (_root_.toContinuousMap ∘ g.comp)

Tactic:
g.toContinuousMap.continuous_postcomp |>.comp <|
    ContinuousMapZero.isEmbedding_toContinuousMap.continuous

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, ContinuousMap.continuous_postcomp, Continuous.comp, ContinuousMap.comp, ContinuousMapZero.toContinuousMap, toContinuousMap, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
R : Type u_3
inst : Zero X
inst_1 : Zero Y
inst_2 : Zero R
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
g : C(Y, R)₀
⊢ Continuous (X := C(X, Y)₀) (Y := C(X, R)) (_root_.toContinuousMap ∘ g.comp)

Tactic:
exact g.toContinuousMap.continuous_postcomp |>.comp <|
    ContinuousMapZero.isEmbedding_toContinuousMap.continuous

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, ContinuousMap.continuous_postcomp, Continuous.comp, ContinuousMapZero.toContinuousMap, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
R : Type u_3
inst : Zero R
inst_1 : TopologicalSpace R
s : Set R
inst_2 : Fact (0 ∈ s)
⊢ Eq (α := C((↑s : Type u_3), R)) (↑(ContinuousMapZero.id s) : C((↑s : Type u_3), R))
    (ContinuousMap.restrict s (ContinuousMap.id R))

Tactic:
rfl

Premises used: toContinuousMap, rfl, ContinuousMap.restrict
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : Zero X
f : X → R
g : C(X, R)₀
hf : Continuous[inst_1, inst_2] f
hf₀ : f 0 = 0
⊢ mkD f g = { toFun := f, continuous_toFun := hf, map_zero' := hf₀ }

Tactic:
simp only [mkD, And.intro hf hf₀, true_and, ↓reduceDIte]

Premises used: reduceDIte, ContinuousMapZero.mkD, And.intro, true_and
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : Zero X
f : X → R
g : C(X, R)₀
hf : ¬Continuous[inst_1, inst_2] f
⊢ mkD f g = g

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

Premises used: not_and_of_not_left, reduceDIte, ContinuousMapZero.mkD
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : Zero X
f : X → R
g : C(X, R)₀
hf : f 0 ≠ 0
⊢ mkD f g = g

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

Premises used: reduceDIte, not_and_of_not_right, ContinuousMapZero.mkD
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : Zero X
f : X → R
g : C(X, R)₀
x : X
hf : Continuous[inst_1, inst_2] f
hf₀ : f 0 = 0
rw : ({ toFun := f, continuous_toFun := hf, map_zero' := hf₀ : C(X, R)₀ } : (a : X) → R) x = f x
rw₁ : ({ toFun := f, continuous_toFun := hf : C(X, R) } : (a : X) → R) x = f x
rw₂ rw₃ : f x = f x
⊢ (mkD f g : (a : X) → R) x = f x

Tactic:
rw [mkD_of_continuous hf hf₀, coe_mk, ContinuousMap.coe_mk]

Premises used: ContinuousMapZero.coe_mk, ContinuousMap.coe_mk, ContinuousMapZero.mkD_of_continuous
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
s : Set X
inst_3 : Zero (↑s : Type u_1)
f : X → R
g : ContinuousMapZero.{u_1, u_2} (↑s : Type u_1) R
hf : ContinuousOn f s
hf₀ : f (↑0 : X) = 0
⊢ mkD (s.restrict (π := fun (a : X) ↦ R) f) g =
    { toFun := s.restrict (π := fun (a : X) ↦ R) f, continuous_toFun := ⋯, map_zero' := hf₀ }

Tactic:
mkD_of_continuous hf.restrict hf₀

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

Tactic:
rw [continuousOn_iff_continuous_restrict] at hf

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

Tactic:
mkD_of_not_continuous hf

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

Tactic:
exact mkD_of_not_continuous hf

Premises used: ContinuousMapZero.mkD_of_not_continuous
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
s : Set X
inst_3 : Zero (↑s : Type u_1)
f : X → R
g : ContinuousMapZero.{u_1, u_2} (↑s : Type u_1) R
x : (↑s : Type u_1)
hf : ContinuousOn f s
hf₀ : f (↑0 : X) = 0
rw :
  ({ toFun := s.restrict (π := fun (a : X) ↦ R) f, continuous_toFun := ⋯, map_zero' := hf₀ :
          ContinuousMapZero.{u_1, u_2} (↑s : Type u_1) R } :
        (a : (↑s : Type u_1)) → R)
      x =
    f (↑x : X)
rw₁ :
  ({ toFun := s.restrict (π := fun (a : X) ↦ R) f, continuous_toFun := ⋯ :
          ContinuousMap.{u_1, u_2} (↑s : Type u_1) R } :
        (a : (↑s : Type u_1)) → R)
      x =
    f (↑x : X)
rw₂ : s.restrict (π := fun (a : X) ↦ R) f x = f (↑x : X)
rw₃ rw₄ : f (↑x : X) = f (↑x : X)
⊢ (mkD (s.restrict (π := fun (a : X) ↦ R) f) g : (a : (↑s : Type u_1)) → R) x = f (↑x : X)

Tactic:
rw [mkD_of_continuousOn hf hf₀, coe_mk, ContinuousMap.coe_mk, restrict_apply]

Premises used: Set.restrict_apply, ContinuousMapZero.coe_mk, ContinuousMap.coe_mk, ContinuousMapZero.mkD_of_continuousOn
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : Zero X
f : X → R
g : C(X, R)₀
f_zero : f 0 = 0
h :
  ∀ (a : X),
    Eq.{u_2 + 1} (α := R) (((↑(mkD f g) : C(X, R)) : (a : X) → R) a : R)
      ((ContinuousMap.mkD f (↑g : C(X, R)) : (a : X) → R) a : R)
⊢ Eq (α := C(X, R)) (↑(mkD f g) : C(X, R)) (ContinuousMap.mkD f (↑g : C(X, R)))

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : Zero X
f : X → R
g : C(X, R)₀
f_zero : f 0 = 0
a : X
pos :
  ∀ (f_cont : Continuous[inst_1, inst_2] f),
    Eq.{u_2 + 1} (α := R) (((↑(mkD f g) : C(X, R)) : (a : X) → R) a : R)
      ((ContinuousMap.mkD f (↑g : C(X, R)) : (a : X) → R) a : R)
neg :
  ∀ (f_cont : ¬Continuous[inst_1, inst_2] f),
    Eq.{u_2 + 1} (α := R) (((↑(mkD f g) : C(X, R)) : (a : X) → R) a : R)
      ((ContinuousMap.mkD f (↑g : C(X, R)) : (a : X) → R) a : R)
⊢ Eq.{u_2 + 1} (α := R) (((↑(mkD f g) : C(X, R)) : (a : X) → R) a : R)
    ((ContinuousMap.mkD f (↑g : C(X, R)) : (a : X) → R) a : R)

Tactic:
by_cases f_cont : Continuous f

Premises used: Continuous
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : Zero X
f : X → R
g : C(X, R)₀
f_zero : f 0 = 0
a : X
f_cont : Continuous[inst_1, inst_2] f
⊢ Eq.{u_2 + 1} (α := R) (((↑(mkD f g) : C(X, R)) : (a : X) → R) a : R)
    ((ContinuousMap.mkD f (↑g : C(X, R)) : (a : X) → R) a : R)

Tactic:
simp [*, ContinuousMap.mkD_of_continuous, mkD_of_continuous, mkD_of_not_continuous,
      ContinuousMap.mkD_of_not_continuous]

Premises used: ContinuousMap.mkD_of_not_continuous, ContinuousMapZero.mkD_of_not_continuous, ContinuousMapZero.mkD_of_continuous, ContinuousMap.mkD_of_continuous
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : Zero X
f : X → R
g : C(X, R)₀
f_zero : f 0 = 0
a : X
f_cont : ¬Continuous[inst_1, inst_2] f
⊢ Eq.{u_2 + 1} (α := R) (((↑(mkD f g) : C(X, R)) : (a : X) → R) a : R)
    ((ContinuousMap.mkD f (↑g : C(X, R)) : (a : X) → R) a : R)

Tactic:
simp [*, ContinuousMap.mkD_of_continuous, mkD_of_continuous, mkD_of_not_continuous,
      ContinuousMap.mkD_of_not_continuous]

Premises used: ContinuousMap.mkD_of_not_continuous, ContinuousMapZero.mkD_of_not_continuous, ContinuousMapZero.mkD_of_continuous, ContinuousMap.mkD_of_continuous
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : Zero X
f g : C(X, R)₀
⊢ mkD (⇑f : (a : X) → R) g = f

Tactic:
mkD_of_continuous f.continuous (map_zero f)

Premises used: ContinuousMap.continuous, map_zero, ContinuousMapZero.toContinuousMap, ContinuousMapZero.mkD_of_continuous
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : Zero R
⊢ Eq (α := (a : X) → R) (⇑0 : (a : X) → R) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : AddZeroClass R
inst_4 : ContinuousAdd R
f g : C(X, R)₀
⊢ Eq.{u_2 + 1} (α := R) ((HAdd.hAdd (α := C(X, R)) (↑f : C(X, R)) (↑g : C(X, R)) : (a : X) → R) 0 : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : AddZeroClass R
inst_4 : ContinuousAdd R
f g : C(X, R)₀
⊢ (⇑(f + g) : (a : X) → R) = HAdd.hAdd (α := (a : X) → R) (⇑f : (a : X) → R) (⇑g : (a : X) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : NegZeroClass R
inst_4 : ContinuousNeg R
f : C(X, R)₀
⊢ Eq.{u_2 + 1} (α := R) ((-(↑f : C(X, R)) : (a : X) → R) 0 : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : NegZeroClass R
inst_4 : ContinuousNeg R
f : C(X, R)₀
⊢ Eq (α := (a : X) → R) (⇑(-f) : (a : X) → R) (-(⇑f : (a : X) → R))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : SubNegZeroMonoid R
inst_4 : ContinuousSub R
f g : C(X, R)₀
⊢ Eq.{u_2 + 1} (α := R) ((HSub.hSub (α := C(X, R)) (↑f : C(X, R)) (↑g : C(X, R)) : (a : X) → R) 0 : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : SubNegZeroMonoid R
inst_4 : ContinuousSub R
f g : C(X, R)₀
⊢ (⇑(f - g) : (a : X) → R) = HSub.hSub (α := (a : X) → R) (⇑f : (a : X) → R) (⇑g : (a : X) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : MulZeroClass R
inst_4 : ContinuousMul R
f g : C(X, R)₀
⊢ Eq.{u_2 + 1} (α := R) ((HMul.hMul (α := C(X, R)) (↑f : C(X, R)) (↑g : C(X, R)) : (a : X) → R) 0 : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : MulZeroClass R
inst_4 : ContinuousMul R
f g : C(X, R)₀
⊢ (⇑(f * g) : (a : X) → R) = HMul.hMul (α := (a : X) → R) (⇑f : (a : X) → R) (⇑g : (a : X) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : Zero R
inst_4 : SMulZeroClass M R
inst_5 : ContinuousConstSMul M R
m : M
f : C(X, R)₀
⊢ Eq.{u_2 + 1} (α := R) ((HSMul.hSMul (β := C(X, R)) m (↑f : C(X, R)) : (a : X) → R) 0 : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : Zero R
inst_4 : SMulZeroClass M R
inst_5 : ContinuousConstSMul M R
m : M
f : C(X, R)₀
⊢ (⇑(m • f) : (a : X) → R) = HSMul.hSMul (β := (a : X) → R) m (⇑f : (a : X) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : IsTopologicalSemiring R
inst_5 : StarRing R
inst_6 : ContinuousStar R
f : C(X, R)₀
⊢ Eq.{u_2 + 1} (α := R) ((star (↑f : C(X, R)) : (a : X) → R) 0 : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : IsTopologicalSemiring R
inst_5 : StarRing R
inst_6 : ContinuousStar R
f : C(X, R)₀
⊢ Eq (α := (a : X) → R) (⇑(star f) : (a : X) → R) (star (⇑f : (a : X) → R))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : IsTopologicalSemiring R
inst_5 : StarRing R
inst_6 : ContinuousStar R
⊢ Eq (α := (a : C(X, R)₀) → C(X, R)) (⇑toContinuousMapHom : (a : C(X, R)₀) → C(X, R)) _root_.toContinuousMap

Tactic:
rfl

Premises used: toContinuousMap, rfl