awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
⊢ (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (a • f).nnrealPart) : ℝ) -
      (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-(a • f)).nnrealPart) : ℝ) =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) a : ℝ)
      ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ))
have inl : ∀ (ha : 0 ≤ a),
  (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (a • f).nnrealPart) : ℝ) -
      (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-(a • f)).nnrealPart) : ℝ) =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) a : ℝ)
      ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ))
Tactic: rcases le_total 0 a with ha | ha
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
inl :
  ∀ (ha : 0 ≤ a),
    (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (a • f).nnrealPart) : ℝ) -
        (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-(a • f)).nnrealPart) : ℝ) =
      HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) a : ℝ)
        ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ))
⊢ (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (a • f).nnrealPart) : ℝ) -
      (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-(a • f)).nnrealPart) : ℝ) =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) a : ℝ)
      ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ))
have inr : ∀ (ha : a ≤ 0),
  (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (a • f).nnrealPart) : ℝ) -
      (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-(a • f)).nnrealPart) : ℝ) =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) a : ℝ)
      ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ))
Tactic: rcases le_total 0 a with ha | ha
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
ha : 0 ≤ a
⊢ (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (a • f).nnrealPart) : ℝ) -
      (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-(a • f)).nnrealPart) : ℝ) =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) a : ℝ)
      ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ))
have inl : (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (a.toNNReal • f.nnrealPart)) : ℝ) -
    (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (a.toNNReal • (-f).nnrealPart)) : ℝ) =
  a * ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ))
Tactic: rw [RingHom.id_apply, smul_eq_mul, ← (smul_neg a f), nnrealPart_smul_pos f ha,
            nnrealPart_smul_pos (-f) ha]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
ha : a ≤ 0
⊢ (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (a • f).nnrealPart) : ℝ) -
      (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-(a • f)).nnrealPart) : ℝ) =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) a : ℝ)
      ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ))
have inr : -a * (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ) - -a * (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) =
  a * ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ))
Tactic: simp only [RingHom.id_apply, smul_eq_mul, ← (smul_neg a f),
            nnrealPart_smul_neg f ha, nnrealPart_smul_neg (-f) ha, map_smul,
            NNReal.coe_mul, Real.coe_toNNReal', neg_neg, sup_of_le_left (neg_nonneg.mpr ha)]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
⊢ toNNRealLinear (toRealPositiveLinear Λ) = Λ
have h : ∀ (f : α →C_c ℝ≥0),
  (↑((toNNRealLinear (toRealPositiveLinear Λ) : (a : α →C_c ℝ≥0) → ℝ≥0) f) : ℝ) =
    (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f) : ℝ)
Tactic: ext f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : R1Space α
inst_2 : Group α
inst_3 : TopologicalSpace β
inst_4 : R1Space β
inst_5 : Group β
inst_6 : ContinuousMul β
inst_7 : NormedAddCommGroup γ
φ : α →* β
hφ : Topology.IsClosedEmbedding.{u_2, u_3} (X := α) (Y := β) (⇑φ : (a : α) → β)
f : β →C_c γ
b : β
⊢ HasCompactSupport.{u_2, u_4} (β := γ) fun (a : α) ↦ (f : (a : β) → γ) (HMul.hMul (β := β) b ((φ : (a : α) → β) a : β))
have obtain : ∀ (K : Set β) (hK : IsCompact K) (hf : ∀ x ∉ K, Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) x : γ) (0 : γ)),
  HasCompactSupport.{u_2, u_4} (β := γ) fun (a : α) ↦ (f : (a : β) → γ) (HMul.hMul (β := β) b ((φ : (a : α) → β) a : β))
Tactic: obtain ⟨K, hK, hf⟩ := exists_compact_iff_hasCompactSupport.mpr f.hasCompactSupport
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : R1Space α
inst_2 : Group α
inst_3 : TopologicalSpace β
inst_4 : R1Space β
inst_5 : Group β
inst_6 : ContinuousMul β
inst_7 : NormedAddCommGroup γ
φ : α →* β
hφ : Topology.IsClosedEmbedding.{u_2, u_3} (X := α) (Y := β) (⇑φ : (a : α) → β)
f : β →C_c γ
b : β
K : Set β
hK : IsCompact K
hf : ∀ x ∉ K, Eq.{u_4 + 1} (α := γ) ((f : (a : β) → γ) x : γ) (0 : γ)
⊢ HasCompactSupport.{u_2, u_4} (β := γ) fun (a : α) ↦ (f : (a : β) → γ) (HMul.hMul (β := β) b ((φ : (a : α) → β) a : β))
have refine : ∀ (x : α) (hx : x ∉ (⇑φ : (a : α) → β) ⁻¹' (b⁻¹ • K)), HMul.hMul (β := β) b ((φ : (a : α) → β) x : β) ∉ K
Tactic: refine exists_compact_iff_hasCompactSupport.mp ⟨φ ⁻¹' (b⁻¹ • K),
      hφ.isCompact_preimage (hK.smul b⁻¹), fun x hx ↦ hf _ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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)) (range (ι := C(X, R)₀) _root_.toContinuousMap)
have rw : IsClosed (X := C(X, R)) {f : C(X, R) | Eq.{u_3 + 1} (α := R) ((f : (a : X) → R) 0 : R) (0 : R)}
Tactic: rw [range_toContinuousMap]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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)₀) ↦ g.comp f
have 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)
Tactic: rw [continuous_induced_rng]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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 (X := C(Y, R)₀) (Y := C(X, R))
    (Function.comp (β := C(X, R)₀) _root_.toContinuousMap fun (g : C(Y, R)₀) ↦ g.comp f)
have change : Continuous (Y := C(X, R)) fun (g : C(Y, R)₀) ↦ ContinuousMap.comp (↑g : C(Y, R)) (↑f : C(X, Y))
Tactic: change Continuous fun g : C(Y, R)₀ ↦ (g : C(Y, R)).comp (f : C(X, Y))
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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)₀) g.comp
have rw : Continuous (X := C(X, Y)₀) (Y := C(X, R)) (_root_.toContinuousMap ∘ g.comp)
Tactic: rw [ContinuousMapZero.isEmbedding_toContinuousMap.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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
⊢ (mkD f g : (a : X) → R) x = f x
have rw : ({ toFun := f, continuous_toFun := hf, map_zero' := hf₀ : C(X, R)₀ } : (a : X) → R) x = f x
Tactic: rw [mkD_of_continuous hf hf₀, coe_mk, ContinuousMap.coe_mk]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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
⊢ (mkD f g : (a : X) → R) x = f x
have rw₁ : ({ toFun := f, continuous_toFun := hf : C(X, R) } : (a : X) → R) x = f x
Tactic: rw [mkD_of_continuous hf hf₀, coe_mk, ContinuousMap.coe_mk]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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
⊢ (mkD f g : (a : X) → R) x = f x
have rw₂ : f x = f x
Tactic: rw [mkD_of_continuous hf hf₀, coe_mk, ContinuousMap.coe_mk]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (hypothesis)
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
⊢ mkD (s.restrict (π := fun (a : X) ↦ R) f) g = g
have hf₁ : ¬Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ R) f)
Tactic: rw [continuousOn_iff_continuous_restrict] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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
⊢ (mkD (s.restrict (π := fun (a : X) ↦ R) f) g : (a : (↑s : Type u_1)) → R) x = f (↑x : X)
have rw : ({ toFun := s.restrict (π := fun (a : X) ↦ R) f, continuous_toFun := sorry, map_zero' := hf₀ :
        ContinuousMapZero.{u_1, u_2} (↑s : Type u_1) R } :
      (a : (↑s : Type u_1)) → R)
    x =
  f (↑x : X)
Tactic: rw [mkD_of_continuousOn hf hf₀, coe_mk, ContinuousMap.coe_mk, restrict_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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)
⊢ (mkD (s.restrict (π := fun (a : X) ↦ R) f) g : (a : (↑s : Type u_1)) → R) x = f (↑x : X)
have rw₁ : ({ toFun := s.restrict (π := fun (a : X) ↦ R) f, continuous_toFun := sorry : ContinuousMap.{u_1, u_2} (↑s : Type u_1) R } :
      (a : (↑s : Type u_1)) → R)
    x =
  f (↑x : X)
Tactic: rw [mkD_of_continuousOn hf hf₀, coe_mk, ContinuousMap.coe_mk, restrict_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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)
⊢ (mkD (s.restrict (π := fun (a : X) ↦ R) f) g : (a : (↑s : Type u_1)) → R) x = f (↑x : X)
have rw₂ : s.restrict (π := fun (a : X) ↦ R) f x = f (↑x : X)
Tactic: rw [mkD_of_continuousOn hf hf₀, coe_mk, ContinuousMap.coe_mk, restrict_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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)
⊢ (mkD (s.restrict (π := fun (a : X) ↦ R) f) g : (a : (↑s : Type u_1)) → R) x = f (↑x : X)
have rw₃ : f (↑x : X) = f (↑x : X)
Tactic: rw [mkD_of_continuousOn hf hf₀, coe_mk, ContinuousMap.coe_mk, restrict_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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
⊢ Eq (α := C(X, R)) (↑(mkD f g) : C(X, R)) (ContinuousMap.mkD f (↑g : C(X, R)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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
⊢ 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)
have 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)
Tactic: by_cases f_cont : Continuous f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases f_cont : Continuous f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousMapZero (goal)
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 (Y := C(X, R)₀) fun (a : C(X, R)₀) ↦ -a
have rw : Continuous (X := C(X, R)₀) (Y := C(X, R)) (Function.comp (β := C(X, R)₀) _root_.toContinuousMap fun (a : C(X, R)₀) ↦ -a)
Tactic: rw [continuous_induced_rng]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousSqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x : 𝕜 × 𝕜
hx : x.1 ≤ x.2
⊢ 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)
have simp : x.2 = x.1 + HMul.hMul (α := 𝕜) (↑√((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜) (↑√((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜)
Tactic: simp only [Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousSqrt (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x : 𝕜 × 𝕜
hx : x.1 ≤ x.2
⊢ x.2 = x.1 + HMul.hMul (α := 𝕜) (↑√((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜) (↑√((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜)
have hx₁ : 0 ≤ x.2 - x.1
Tactic: rw [← sub_nonneg] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousSqrt (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x : 𝕜 × 𝕜
hx : 0 ≤ x.2 - x.1
⊢ x.2 = x.1 + HMul.hMul (α := 𝕜) (↑√((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜) (↑√((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜)
have hx' : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (x.2 - x.1) : ℝ) (0 : ℝ)
Tactic: obtain hx' := nonneg_iff.mp hx |>.right
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousSqrt (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x : 𝕜 × 𝕜
hx : 0 ≤ x.2 - x.1
hx' : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (x.2 - x.1) : ℝ) (0 : ℝ)
⊢ x.2 = x.1 + HMul.hMul (α := 𝕜) (↑√((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜) (↑√((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜)
have hx'₁ : (↑((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜) = x.2 - x.1
Tactic: rw [← conj_eq_iff_im, conj_eq_iff_re] at hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.ContinuousSqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x : 𝕜 × 𝕜
hx : 0 ≤ x.2 - x.1
hx' : (↑((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜) = x.2 - x.1
⊢ x.2 = x.1 + HMul.hMul (α := 𝕜) (↑√((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜) (↑√((re : (a : 𝕜) → ℝ) (x.2 - x.1)) : 𝕜)
have rw : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) (x.2 - x.1) : ℝ)
Tactic: rw [← ofReal_mul, Real.mul_self_sqrt, hx', add_sub_cancel]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Defs (goal)
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
⊢ f = g
have 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
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Defs (goal)
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
⊢ { toFun := toFun, continuous_toFun := continuous_toFun : C(X, Y) } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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 (↑(idealOfSet R s) : Set C(X, R))
have simp : IsClosed
  (↑{ carrier := ⋂ i ∈ sᶜ, {x : C(X, R) | Eq.{u_2 + 1} (α := R) ((x : (a : X) → R) i : R) (0 : R)}, add_mem' := sorry,
        zero_mem' := sorry : AddSubmonoid C(X, R) } :
    Set C(X, R))
Tactic: simp only [idealOfSet, Submodule.coe_set_mk, Set.setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
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)
⊢ (¬∀ ⦃x : X⦄, x ∈ sᶜ → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)) ↔
    ∃ x ∈ sᶜ, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
have push : (∃ x ∈ sᶜ, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)) ↔
  ∃ x ∈ sᶜ, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
Tactic: push Not
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ x ∉ setOfIdeal I ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
have rw : x ∈ (setOfIdeal I)ᶜ ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
Tactic: rw [← Set.mem_compl_iff, setOfIdeal, compl_compl, Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
rw : x ∈ (setOfIdeal I)ᶜ ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
⊢ x ∉ setOfIdeal I ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
have rw₁ : Membership.mem (γ := Set X) {x : X | ∀ f ∈ I, Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)}ᶜᶜ x ↔
  ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
Tactic: rw [← Set.mem_compl_iff, setOfIdeal, compl_compl, Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
rw : x ∈ (setOfIdeal I)ᶜ ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
rw₁ :
  Membership.mem (γ := Set X) {x : X | ∀ f ∈ I, Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)}ᶜᶜ x ↔
    ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
⊢ x ∉ setOfIdeal I ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
have rw₂ : Membership.mem (γ := Set X) {x : X | ∀ f ∈ I, Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)} x ↔
  ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
Tactic: rw [← Set.mem_compl_iff, setOfIdeal, compl_compl, Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Ideals (goal)
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
rw : x ∈ (setOfIdeal I)ᶜ ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
rw₁ :
  Membership.mem (γ := Set X) {x : X | ∀ f ∈ I, Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)}ᶜᶜ x ↔
    ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
rw₂ :
  Membership.mem (γ := Set X) {x : X | ∀ f ∈ I, Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)} x ↔
    ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
⊢ x ∉ setOfIdeal I ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
have rw₃ : (∀ f ∈ I, Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)) ↔
  ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
Tactic: rw [← Set.mem_compl_iff, setOfIdeal, compl_compl, Set.mem_setOf]