awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
𝕜 : Type u_3
inst_5 : Semiring 𝕜
inst_6 : Module 𝕜 R
inst_7 : ContinuousConstSMul 𝕜 R
x : X
f : C(X, R)₀
⊢ Eq.{u_2 + 1} (α := R) (((evalCLM 𝕜 x : C(X, R)₀ →L[𝕜] R) : (a : C(X, R)₀) → R) f : R) ((f : (a : X) → R) 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
f g : C(X, R)₀
⊢ (⇑(f + g) : (a : X) → R) = HAdd.hAdd (α := X → R) (⇑f : (a : X) → R) (⇑g : (a : X) → 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
f : C(X, R)₀
⊢ Eq (α := X → R) (((coeFnAddMonoidHom : C(X, R)₀ →+ X → R) : (a : C(X, R)₀) → X → R) f : X → R)
    ((⇑f : (a : X) → R) : (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
ι : Type u_3
s : Finset ι
f : ι → C(X, R)₀
⊢ Eq (α := (a : X) → R) (⇑(s.sum f) : (a : X) → R) (∑ i ∈ s, (⇑(f i) : (a : X) → R))

Tactic:
map_sum coeFnAddMonoidHom f s

Premises used: map_sum, ContinuousMapZero.coeFnAddMonoidHom
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X_1 : Type u_1
R_1 : Type u_2
inst : Zero X_1
inst_1 : TopologicalSpace X_1
inst_2 : TopologicalSpace R_1
X : Type u_3
R : Type u_4
inst_3 : Zero X
inst_4 : TopologicalSpace X
inst_5 : CommRing R
inst_6 : TopologicalSpace R
inst_7 : IsTopologicalRing R
rw :
  Continuous (X := C(X, R)₀) (Y := C(X, R))
    (Function.comp (β := C(X, R)₀) _root_.toContinuousMap fun (a : C(X, R)₀) ↦ -a)
⊢ Continuous (Y := C(X, R)₀) fun (a : C(X, R)₀) ↦ -a

Tactic:
rw [continuous_induced_rng]

Premises used: continuous_induced_rng
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X_1 : Type u_1
R_1 : Type u_2
inst : Zero X_1
inst_1 : TopologicalSpace X_1
inst_2 : TopologicalSpace R_1
X : Type u_3
R : Type u_4
inst_3 : Zero X
inst_4 : TopologicalSpace X
inst_5 : CommRing R
inst_6 : TopologicalSpace R
inst_7 : IsTopologicalRing R
⊢ Continuous (X := C(X, R)₀) (Y := C(X, R))
    (Function.comp (β := C(X, R)₀) _root_.toContinuousMap fun (a : C(X, R)₀) ↦ -a)

Tactic:
continuous_neg.comp continuous_induced_dom

Premises used: ContinuousNeg.continuous_neg, Continuous.comp, toContinuousMap, continuous_induced_dom
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X_1 : Type u_1
R_1 : Type u_2
inst : Zero X_1
inst_1 : TopologicalSpace X_1
inst_2 : TopologicalSpace R_1
X : Type u_3
R : Type u_4
inst_3 : Zero X
inst_4 : TopologicalSpace X
inst_5 : CommRing R
inst_6 : TopologicalSpace R
inst_7 : IsTopologicalRing R
⊢ Continuous (X := C(X, R)₀) (Y := C(X, R))
    (Function.comp (β := C(X, R)₀) _root_.toContinuousMap fun (a : C(X, R)₀) ↦ -a)

Tactic:
exact continuous_neg.comp continuous_induced_dom

Premises used: ContinuousNeg.continuous_neg, Continuous.comp, continuous_induced_dom
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : Zero R
inst_3 : UniformSpace R
inst_4 : T1Space R
inst_5 : CompleteSpace C(X, R)
⊢ CompleteSpace C(X, R)₀

Tactic:
completeSpace_iff_isComplete_range isUniformEmbedding_toContinuousMap.isUniformInducing
    |>.mpr isClosedEmbedding_toContinuousMap.isClosed_range.isComplete

Premises used: Iff.mpr, IsUniformEmbedding.isUniformInducing, ContinuousMapZero.isUniformEmbedding_toContinuousMap, IsClosed.isComplete, completeSpace_iff_isComplete_range
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_2
inst : Zero X
inst_1 : TopologicalSpace X
inst_2 : Zero R
inst_3 : UniformSpace R
Y : Type u_3
inst_4 : UniformSpace Y
inst_5 : Zero Y
g : C(Y, R)₀
hg : IsUniformEmbedding.{u_3, u_2} (α := Y) (β := R) (⇑g : (a : Y) → R)
⊢ IsUniformEmbedding (β := C(X, R)₀) fun (x : C(X, Y)₀) ↦ g.comp x

Tactic:
isUniformEmbedding_toContinuousMap.of_comp_iff.mp <|
    ContinuousMap.isUniformEmbedding_comp g.toContinuousMap hg |>.comp
      isUniformEmbedding_toContinuousMap

Premises used: IsUniformEmbedding.comp, ContinuousMapZero.toContinuousMap, ContinuousMap.isUniformEmbedding_comp, IsUniformEmbedding.of_comp_iff, Iff.mp, ContinuousMapZero.isUniformEmbedding_toContinuousMap
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
M : Type u_3
R : Type u_4
S : Type u_5
inst : Zero X
inst_1 : Zero Y
inst_2 : CommSemiring M
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace S
inst_7 : CommSemiring R
inst_8 : StarRing R
inst_9 : IsTopologicalSemiring R
inst_10 : ContinuousStar R
inst_11 : CommSemiring S
inst_12 : StarRing S
inst_13 : IsTopologicalSemiring S
inst_14 : ContinuousStar S
inst_15 : Module M R
inst_16 : Module M S
inst_17 : ContinuousConstSMul M R
inst_18 : ContinuousConstSMul M S
φ : R →⋆ₙₐ[M] S
hφ : Continuous[inst_5, inst_6] (⇑φ : (a : R) → S)
⊢ Eq.{u_5 + 1} (α := S) (({ toFun := (⇑φ : (a : R) → S), continuous_toFun := hφ : C(R, S) } : (a : R) → S) 0 : S)
    (0 : S)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
M : Type u_3
R : Type u_4
S : Type u_5
inst : Zero X
inst_1 : Zero Y
inst_2 : CommSemiring M
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace S
inst_7 : CommSemiring R
inst_8 : StarRing R
inst_9 : IsTopologicalSemiring R
inst_10 : ContinuousStar R
inst_11 : CommSemiring S
inst_12 : StarRing S
inst_13 : IsTopologicalSemiring S
inst_14 : ContinuousStar S
inst_15 : Module M R
inst_16 : Module M S
inst_17 : ContinuousConstSMul M R
inst_18 : ContinuousConstSMul M S
φ : R →⋆ₙₐ[M] S
hφ : Continuous[inst_5, inst_6] (⇑φ : (a : R) → S)
r : M
f : C(X, R)₀
⊢ ∀ (x : X),
    Eq.{u_5 + 1} (α := S)
      (({ toFun := (⇑φ : (a : R) → S), continuous_toFun := hφ, map_zero' := ⋯ : C(R, S)₀ }.comp (r • f) : (a : X) → S)
          x :
        S)
      ((HSMul.hSMul (α := M) ((MonoidHom.id M : (a : M) → M) r : M)
              ({ toFun := (⇑φ : (a : R) → S), continuous_toFun := hφ, map_zero' := ⋯ : C(R, S)₀ }.comp f) :
            (a : X) → S)
          x :
        S)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
M : Type u_3
R : Type u_4
S : Type u_5
inst : Zero X
inst_1 : Zero Y
inst_2 : CommSemiring M
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace S
inst_7 : CommSemiring R
inst_8 : StarRing R
inst_9 : IsTopologicalSemiring R
inst_10 : ContinuousStar R
inst_11 : CommSemiring S
inst_12 : StarRing S
inst_13 : IsTopologicalSemiring S
inst_14 : ContinuousStar S
inst_15 : Module M R
inst_16 : Module M S
inst_17 : ContinuousConstSMul M R
inst_18 : ContinuousConstSMul M S
φ : R →⋆ₙₐ[M] S
hφ : Continuous[inst_5, inst_6] (⇑φ : (a : R) → S)
⊢ ∀ (x : X),
    Eq.{u_5 + 1} (α := S)
      (({ toFun := (⇑φ : (a : R) → S), continuous_toFun := hφ, map_zero' := ⋯ : C(R, S)₀ }.comp 0 : (a : X) → S) x : S)
      ((0 : (a : X) → S) x : S)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
M : Type u_3
R : Type u_4
S : Type u_5
inst : Zero X
inst_1 : Zero Y
inst_2 : CommSemiring M
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace S
inst_7 : CommSemiring R
inst_8 : StarRing R
inst_9 : IsTopologicalSemiring R
inst_10 : ContinuousStar R
inst_11 : CommSemiring S
inst_12 : StarRing S
inst_13 : IsTopologicalSemiring S
inst_14 : ContinuousStar S
inst_15 : Module M R
inst_16 : Module M S
inst_17 : ContinuousConstSMul M R
inst_18 : ContinuousConstSMul M S
φ : R →⋆ₙₐ[M] S
hφ : Continuous[inst_5, inst_6] (⇑φ : (a : R) → S)
x x_1 : C(X, R)₀
⊢ ∀ (x_2 : X),
    Eq.{u_5 + 1} (α := S)
      (({ toFun := (⇑φ : (a : R) → S), continuous_toFun := hφ, map_zero' := ⋯ : C(R, S)₀ }.comp (x + x_1) : (a : X) → S)
          x_2 :
        S)
      (({ toFun := (⇑φ : (a : R) → S), continuous_toFun := hφ, map_zero' := ⋯ : C(R, S)₀ }.comp x +
              { toFun := (⇑φ : (a : R) → S), continuous_toFun := hφ, map_zero' := ⋯ : C(R, S)₀ }.comp x_1 :
            (a : X) → S)
          x_2 :
        S)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
M : Type u_3
R : Type u_4
S : Type u_5
inst : Zero X
inst_1 : Zero Y
inst_2 : CommSemiring M
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace S
inst_7 : CommSemiring R
inst_8 : StarRing R
inst_9 : IsTopologicalSemiring R
inst_10 : ContinuousStar R
inst_11 : CommSemiring S
inst_12 : StarRing S
inst_13 : IsTopologicalSemiring S
inst_14 : ContinuousStar S
inst_15 : Module M R
inst_16 : Module M S
inst_17 : ContinuousConstSMul M R
inst_18 : ContinuousConstSMul M S
φ : R →⋆ₙₐ[M] S
hφ : Continuous[inst_5, inst_6] (⇑φ : (a : R) → S)
x x_1 : C(X, R)₀
⊢ ∀ (x_2 : X),
    Eq.{u_5 + 1} (α := S)
      (({ toFun := (⇑φ : (a : R) → S), continuous_toFun := hφ, map_zero' := ⋯ : C(R, S)₀ }.comp (x * x_1) : (a : X) → S)
          x_2 :
        S)
      (({ toFun := (⇑φ : (a : R) → S), continuous_toFun := hφ, map_zero' := ⋯ : C(R, S)₀ }.comp x *
              { toFun := (⇑φ : (a : R) → S), continuous_toFun := hφ, map_zero' := ⋯ : C(R, S)₀ }.comp x_1 :
            (a : X) → S)
          x_2 :
        S)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
Y : Type u_2
M : Type u_3
R : Type u_4
S : Type u_5
inst : Zero X
inst_1 : Zero Y
inst_2 : CommSemiring M
inst_3 : TopologicalSpace X
inst_4 : TopologicalSpace Y
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace S
inst_7 : CommSemiring R
inst_8 : StarRing R
inst_9 : IsTopologicalSemiring R
inst_10 : ContinuousStar R
inst_11 : CommSemiring S
inst_12 : StarRing S
inst_13 : IsTopologicalSemiring S
inst_14 : ContinuousStar S
inst_15 : Module M R
inst_16 : Module M S
inst_17 : ContinuousConstSMul M R
inst_18 : ContinuousConstSMul M S
φ : R →⋆ₙₐ[M] S
hφ : Continuous[inst_5, inst_6] (⇑φ : (a : R) → S)
x : C(X, R)₀
⊢ ∀ (x_1 : X),
    Eq.{u_5 + 1} (α := S)
      (({ toFun := (⇑φ : (a : R) → S), continuous_toFun := hφ, map_zero' := ⋯ : C(R, S)₀ }.comp (star x) : (a : X) → S)
          x_1 :
        S)
      ((star ({ toFun := (⇑φ : (a : R) → S), continuous_toFun := hφ, map_zero' := ⋯ : C(R, S)₀ }.comp x) : (a : X) → S)
          x_1 :
        S)

Tactic:
simp [map_star]

Premises used: StarHomClass.map_star
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
α : Type u_1
R : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : Zero α
inst_3 : MetricSpace R
inst_4 : Zero R
⊢ Isometry (α := C(α, R)₀) toContinuousMap

Tactic:
fun _ _ ↦ rfl

Premises used: setOf, rfl, Isometry
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
α : Type u_1
R : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : Zero α
inst_3 : NormedAddCommGroup R
f : C(α, R)₀
⊢ ‖f‖ = norm (E := C(α, R)) (↑f : C(α, R))

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Topology.ContinuousMap.ContinuousSqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ ContinuousOn.{u_1, u_1} (X := 𝕜 × 𝕜) (Y := 𝕜)
    (ofReal ∘ (fun (x : ℝ) ↦ √x) ∘ Function.comp (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) fun (z : 𝕜 × 𝕜) ↦ z.2 - z.1)
    {x : 𝕜 × 𝕜 | x.1 ≤ x.2}

Tactic:
fun_prop
-- Module: Mathlib.Topology.ContinuousMap.ContinuousSqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x : 𝕜 × 𝕜
h : x.1 ≤ x.2
⊢ LE.le (α := 𝕜) 0
    ((ofReal ∘ (fun (x : ℝ) ↦ √x) ∘ Function.comp (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) fun (z : 𝕜 × 𝕜) ↦ z.2 - z.1) x)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousSqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x : 𝕜 × 𝕜
hx : x.1 ≤ x.2
simp : x.2 = x.1 + HMul.hMul (α := 𝕜) (↑√((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜) (↑√((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜)
⊢ x.2 =
    x.1 +
      HMul.hMul (α := 𝕜)
        ((ofReal ∘ (fun (x : ℝ) ↦ √x) ∘ Function.comp (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) fun (z : 𝕜 × 𝕜) ↦ z.2 - z.1) x)
        ((ofReal ∘ (fun (x : ℝ) ↦ √x) ∘ Function.comp (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) fun (z : 𝕜 × 𝕜) ↦ z.2 - z.1) x)

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Topology.ContinuousMap.ContinuousSqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x : 𝕜 × 𝕜
hx : x.1 ≤ x.2
⊢ 0 ≤ x.2 - x.1

Tactic:
rw [← sub_nonneg] at hx

Premises used: sub_nonneg
-- Module: Mathlib.Topology.ContinuousMap.ContinuousSqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x : 𝕜 × 𝕜
hx : 0 ≤ x.2 - x.1
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (x.2 - x.1) : ℝ) (0 : ℝ)

Tactic:
obtain hx' := nonneg_iff.mp hx |>.right

Premises used: RCLike.nonneg_iff, And.right, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousSqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x : 𝕜 × 𝕜
hx : 0 ≤ x.2 - x.1
hx' : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (x.2 - x.1) : ℝ) (0 : ℝ)
⊢ (↑((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜) = x.2 - x.1

Tactic:
rw [← conj_eq_iff_im, conj_eq_iff_re] at hx'

Premises used: RCLike.conj_eq_iff_re, RCLike.conj_eq_iff_im
-- Module: Mathlib.Topology.ContinuousMap.ContinuousSqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x : 𝕜 × 𝕜
hx : 0 ≤ x.2 - x.1
hx' : (↑((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜) = x.2 - x.1
rw : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) (x.2 - x.1) : ℝ)
⊢ x.2 = x.1 + HMul.hMul (α := 𝕜) (↑√((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜) (↑√((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜)

Tactic:
rw [← ofReal_mul, Real.mul_self_sqrt, hx', add_sub_cancel]

Premises used: RCLike.ofReal_mul, Real.mul_self_sqrt, add_sub_cancel
-- Module: Mathlib.Topology.ContinuousMap.ContinuousSqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x : 𝕜 × 𝕜
hx : 0 ≤ x.2 - x.1
hx' : (↑((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜) = x.2 - x.1
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) (x.2 - x.1) : ℝ)

Tactic:
simpa using nonneg_iff.mp hx |>.left

Premises used: RCLike.nonneg_iff, And.left, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousSqrt
Goal:
⊢ ContinuousOn (X := ℝ≥0 × ℝ≥0) (Y := ℝ≥0)
    (Function.comp (β := ℝ≥0) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0 × ℝ≥0) ↦ x.2 - x.1)
    {x : ℝ≥0 × ℝ≥0 | x.1 ≤ x.2}

Tactic:
fun_prop
-- Module: Mathlib.Topology.ContinuousMap.ContinuousSqrt
Goal:
⊢ ∀ (x : ℝ≥0 × ℝ≥0),
    x.1 ≤ x.2 →
      LE.le (α := ℝ≥0) 0 (Function.comp (β := ℝ≥0) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0 × ℝ≥0) ↦ x.2 - x.1) x)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.ContinuousSqrt
Goal:
⊢ ∀ (x : ℝ≥0 × ℝ≥0),
    x.1 ≤ x.2 →
      x.2 =
        x.1 +
          HMul.hMul (α := ℝ≥0)
            (Function.comp (β := ℝ≥0) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0 × ℝ≥0) ↦ x.2 - x.1) x)
            (Function.comp (β := ℝ≥0) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (fun (x : ℝ≥0 × ℝ≥0) ↦ x.2 - x.1) x)

Tactic:
simpa using fun _ _ h ↦ Eq.symm <| add_tsub_cancel_of_le h

Premises used: Eq.symm, add_tsub_cancel_of_le
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
h : f.toFun = g.toFun
mk :
  ∀ (toFun : X → Y) (continuous_toFun : Continuous[inst, inst_1] toFun)
    (h : { toFun := toFun, continuous_toFun := continuous_toFun : C(X, Y) }.toFun = g.toFun),
    { toFun := toFun, continuous_toFun := continuous_toFun : C(X, Y) } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : C(X, Y)
toFun : X → Y
continuous_toFun : Continuous[inst, inst_1] toFun
h : { toFun := toFun, continuous_toFun := continuous_toFun : C(X, Y) }.toFun = g.toFun
mk :
  ∀ (toFun_1 : X → Y) (continuous_toFun_1 : Continuous[inst, inst_1] toFun_1)
    (h :
      { toFun := toFun, continuous_toFun := continuous_toFun : C(X, Y) }.toFun =
        { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(X, Y) }.toFun),
    { toFun := toFun, continuous_toFun := continuous_toFun : C(X, Y) } =
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1 }
⊢ { toFun := toFun, continuous_toFun := continuous_toFun : C(X, Y) } = g

Tactic:
cases g
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
toFun : X → Y
continuous_toFun : Continuous[inst, inst_1] toFun
toFun_1 : X → Y
continuous_toFun_1 : Continuous[inst, inst_1] toFun_1
h :
  { toFun := toFun, continuous_toFun := continuous_toFun : C(X, Y) }.toFun =
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(X, Y) }.toFun
⊢ { toFun := toFun, continuous_toFun := continuous_toFun : C(X, Y) } =
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1 }

Tactic:
congr
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
⊢ f.toFun = (⇑f : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ CanLift (X → Y) C(X, Y) (DFunLike.coe (β := fun (a : X) ↦ Y)) Continuous[inst, inst_1]

Tactic:
⟨fun f hf ↦ ⟨⟨f, hf⟩, rfl⟩⟩

Premises used: ContinuousMap.mk, Exists.intro, CanLift.mk, rfl
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Type u_3
inst_2 : FunLike F X Y
inst_3 : ContinuousMapClass F X Y
f : F
⊢ Eq (α := (a : X) → Y) (⇑(↑f : C(X, Y)) : (a : X) → Y) (⇑f : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Type u_3
inst_2 : FunLike F X Y
inst_3 : ContinuousMapClass F X Y
f : F
x : X
⊢ Eq.{u_2 + 1} (α := Y) (((↑f : C(X, Y)) : (a : X) → Y) x : Y) ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Type u_3
inst_2 : FunLike F X Y
inst_3 : ContinuousMapClass F X Y
⊢ Injective (α := F) (β := C(X, Y)) toContinuousMap

Tactic:
.of_comp (f := DFunLike.coe) DFunLike.coe_injective

Premises used: DFunLike.coe_injective, Function.Injective.of_comp
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
h : ∀ (a : X), Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) a : Y) ((g : (a : X) → Y) a : Y)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
f' : X → Y
h : f' = (⇑f : (a : X) → Y)
⊢ (⇑(f.copy f' h) : (a : X) → Y) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
f' : X → Y
h : f' = (⇑f : (a : X) → Y)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
⊢ Continuous[inst, inst_1] (⇑f : (a : X) → Y)

Tactic:
f.continuous_toFun

Premises used: ContinuousMap.continuous_toFun
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
H : f = g
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((g : (a : X) → Y) x : Y)

Tactic:
H ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
x y : X
h : x = y
⊢ Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f : (a : X) → Y) y : Y)

Tactic:
h ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Injective (α := C(X, Y)) (β := (a : X) → Y) (DFunLike.coe (β := fun (a : X) ↦ Y))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f
⊢ (⇑{ toFun := f, continuous_toFun := h : C(X, Y) } : (a : X) → Y) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Subsingleton Y
⊢ Subsingleton C(X, Y)

Tactic:
DFunLike.subsingleton_cod

Premises used: DFunLike.subsingleton_cod
-- Module: Mathlib.Topology.ContinuousMap.Defs
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : IsEmpty X
⊢ Subsingleton C(X, Y)

Tactic:
DFunLike.subsingleton_dom

Premises used: DFunLike.subsingleton_dom
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
s : Set X
f g : C(X, R)
hf :
  Membership.mem (γ := Set C(X, R)) {f : C(X, R) | ∀ x ∈ sᶜ, Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)} f
hg :
  Membership.mem (γ := Set C(X, R)) {f : C(X, R) | ∀ x ∈ sᶜ, Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)} g
x : X
hx : x ∈ sᶜ
⊢ Eq.{u_2 + 1} (α := R) ((f + g : (a : X) → R) x : R) (0 : R)

Tactic:
simp [hf x hx, hg x hx, add_zero]

Premises used: add_zero
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : T2Space R
s : Set X
simp :
  IsClosed
    (↑{ carrier := ⋂ i ∈ sᶜ, {x : C(X, R) | Eq.{u_2 + 1} (α := R) ((x : (a : X) → R) i : R) (0 : R)}, add_mem' := ⋯,
          zero_mem' := ⋯ : AddSubmonoid C(X, R) } :
      Set C(X, R))
⊢ IsClosed (↑(idealOfSet R s) : Set C(X, R))

Tactic:
simp only [idealOfSet, Submodule.coe_set_mk, Set.setOf_forall]

Premises used: ContinuousMap.idealOfSet, Submodule.coe_set_mk, Set.setOf_forall
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : T2Space R
s : Set X
⊢ IsClosed
    (↑{ carrier := ⋂ i ∈ sᶜ, {x : C(X, R) | Eq.{u_2 + 1} (α := R) ((x : (a : X) → R) i : R) (0 : R)}, add_mem' := ⋯,
          zero_mem' := ⋯ : AddSubmonoid C(X, R) } :
      Set C(X, R))

Tactic:
isClosed_iInter fun x => isClosed_iInter fun _ =>
    isClosed_eq (continuous_eval_const x) continuous_const

Premises used: iInf, Set.iInter, continuous_const, setOf, isClosed_eq, ContinuousEvalConst.continuous_eval_const, isClosed_iInter
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : T2Space R
s : Set X
⊢ IsClosed
    (↑{ carrier := ⋂ i ∈ sᶜ, {x : C(X, R) | Eq.{u_2 + 1} (α := R) ((x : (a : X) → R) i : R) (0 : R)}, add_mem' := ⋯,
          zero_mem' := ⋯ : AddSubmonoid C(X, R) } :
      Set C(X, R))

Tactic:
exact isClosed_iInter fun x => isClosed_iInter fun _ =>
    isClosed_eq (continuous_eval_const x) continuous_const

Premises used: continuous_const, isClosed_eq, ContinuousEvalConst.continuous_eval_const, isClosed_iInter
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ Membership.mem (γ := Ideal C(X, R)) (idealOfSet R s) f ↔ Membership.mem (γ := Ideal C(X, R)) (idealOfSet R s) f

Tactic:
Iff.rfl

Premises used: Iff.rfl