awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
δ : Type u_5
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
inst_4 : Zero δ
f : γ →C_c δ
g : β →co γ
x : β
hx :
  ∀ (o : Set β),
    IsOpen o →
      x ∈ o →
        (o ∩
            Function.support.{u_3, u_5} (M := δ)
              (Function.comp.{u_3 + 1, u_4 + 1, u_5 + 1} (β := γ) (⇑f : (a : γ) → δ) (⇑g : (a : β) → γ))).Nonempty
o : Set γ
ho : IsOpen o
hgxo : Membership.mem (α := γ) o ((g : (a : β) → γ) x : γ)
y : β
hy :
  Membership.mem (γ := Set β)
    ((⇑g : (a : β) → γ) ⁻¹' o ∩
      Function.support.{u_3, u_5} (M := δ)
        (Function.comp.{u_3 + 1, u_4 + 1, u_5 + 1} (β := γ) (⇑f : (a : γ) → δ) (⇑g : (a : β) → γ)))
    y
⊢ (o ∩ Function.support f.toFun).Nonempty

Tactic:
exact ⟨g y, hy⟩
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
inst_2 : TopologicalSpace δ
inst_3 : Zero δ
f : γ →C_c δ
g : β →co γ
⊢ Eq (α := (a : β) → δ) (⇑(f.comp g) : (a : β) → δ)
    (Function.comp.{u_3 + 1, u_4 + 1, u_5 + 1} (β := γ) (⇑f : (a : γ) → δ) (⇑g : (a : β) → γ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace γ
inst_1 : TopologicalSpace δ
inst_2 : Zero δ
f : γ →C_c δ
⊢ f.comp (CocompactMap.id γ) = f

Tactic:
ext fun _ => rfl

Premises used: CompactlySupportedContinuousMap.ext, rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
δ : Type u_5
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
inst_4 : Zero δ
f : γ →C_c δ
g : β →co γ
h : α →co β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: CompactlySupportedContinuousMap.comp, ContinuousMap.comp, toContinuousMap, rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
inst_2 : TopologicalSpace δ
inst_3 : Zero δ
g : β →co γ
⊢ Eq (α := β →C_c δ) (comp 0 g) 0

Tactic:
rfl

Premises used: CompactlySupportedContinuousMap.comp, ContinuousMap.comp, rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Zero β
inst_2 : TopologicalSpace β
G : Type u_5
inst_3 : FunLike G α β
inst_4 : ContinuousMapClass G α β
inst_5 : CompactSpace α
f : G
⊢ HasCompactSupport.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
HasCompactSupport.of_compactSpace f

Premises used: HasCompactSupport.of_compactSpace, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : Zero β
inst_2 : TopologicalSpace β
G : Type u_5
inst_3 : FunLike G α β
inst_4 : ContinuousMapClass G α β
inst_5 : CompactSpace α
f : G
⊢ HasCompactSupport.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
exact HasCompactSupport.of_compactSpace f

Premises used: HasCompactSupport.of_compactSpace, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
β : Type u_3
γ : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
inst_2 : Zero γ
inst_3 : FunLike F β γ
inst_4 : CompactlySupportedContinuousMapClass F β γ
f : F
⊢ UniformContinuous.{u_3, u_4} (α := β) (β := γ) (⇑f : (a : β) → γ)

Tactic:
(map_continuous f).uniformContinuous_of_tendsto_cocompact
  (HasCompactSupport.is_zero_at_infty (hasCompactSupport f))

Premises used: CompactlySupportedContinuousMapClass.hasCompactSupport, ContinuousMapClass.map_continuous, HasCompactSupport.is_zero_at_infty, Continuous.uniformContinuous_of_tendsto_cocompact
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ ∃ (g : α →C_c ℝ≥0), f₁ + g = f₂

Tactic:
⟨⟨f₂.1 - f₁.1, ?_⟩, ?_⟩

Premises used: HSub.hSub, CompactlySupportedContinuousMap.toContinuousMap, Exists.intro, CompactlySupportedContinuousMap.mk
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
refine_1 : HasCompactSupport (f₂.toContinuousMap - f₁.toContinuousMap).toFun
refine_2 :
  f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ⋯ : α →C_c ℝ≥0 } = f₂
⊢ ∃ (g : α →C_c ℝ≥0), f₁ + g = f₂

Tactic:
refine ⟨⟨f₂.1 - f₁.1, ?_⟩, ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
refine_1 :
  closure (Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun) ⊆ tsupport f₁.toFun ∪ tsupport f₂.toFun
⊢ HasCompactSupport (f₂.toContinuousMap - f₁.toContinuousMap).toFun

Tactic:
apply (f₁.hasCompactSupport'.union f₂.hasCompactSupport').of_isClosed_subset isClosed_closure

Premises used: IsCompact.of_isClosed_subset, CompactlySupportedContinuousMap.hasCompactSupport', IsCompact.union, isClosed_closure
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
refine_1 :
  closure (Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun) ⊆
    closure (Function.support f₁.toFun ∪ Function.support f₂.toFun)
⊢ closure (Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun) ⊆ tsupport f₁.toFun ∪ tsupport f₂.toFun

Tactic:
rw [tsupport, tsupport, ← closure_union]

Premises used: tsupport, closure_union
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
refine_1 :
  Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun ⊆
    Function.support f₁.toFun ∪ Function.support f₂.toFun
⊢ closure (Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun) ⊆
    closure (Function.support f₁.toFun ∪ Function.support f₂.toFun)

Tactic:
apply closure_mono

Premises used: closure_mono
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
hx : x ∈ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun
refine_1 :
  ∀ (hx : x ∉ Function.support f₁.toFun ∪ Function.support f₂.toFun),
    x ∉ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun
⊢ x ∈ Function.support f₁.toFun ∪ Function.support f₂.toFun

Tactic:
contrapose hx
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
hx : x ∉ Function.support f₁.toFun ∪ Function.support f₂.toFun
refine_1 :
  ∀
    (hx :
      Eq (α := ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0) ∧ Eq (α := ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)),
    HSub.hSub (α := ℝ≥0) (β := ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0) = 0
⊢ x ∉ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun

Tactic:
simp only [ContinuousMap.toFun_eq_coe, coe_toContinuousMap, Set.mem_union, Function.mem_support,
      ne_eq, not_or, Decidable.not_not, ContinuousMap.coe_sub, Pi.sub_apply] at hx ⊢

Premises used: Set.mem_union, ContinuousMap.coe_sub, ne_eq, not_or, CompactlySupportedContinuousMap.coe_toContinuousMap, Function.mem_support, Decidable.not_not, ContinuousMap.toFun_eq_coe, Pi.sub_apply
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
hx : Eq (α := ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0) ∧ Eq (α := ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
⊢ HSub.hSub (α := ℝ≥0) (β := ℝ≥0) ((f₂ : (a : α) → ℝ≥0) x : ℝ≥0) ((f₁ : (a : α) → ℝ≥0) x : ℝ≥0) = 0

Tactic:
simp [hx.1, hx.2]

Premises used: And.right, And.left
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
refine_2 :
  ∀ (x : α),
    (↑((f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ⋯ : α →C_c ℝ≥0 } :
              (a : α) → ℝ≥0)
            x) :
        ℝ) =
      (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ)
⊢ f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ⋯ : α →C_c ℝ≥0 } = f₂

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
⊢ (↑((f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ⋯ : α →C_c ℝ≥0 } :
            (a : α) → ℝ≥0)
          x) :
      ℝ) =
    (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ)

Tactic:
simpa [← NNReal.coe_add] using add_tsub_cancel_of_le (h x)

Premises used: NNReal.coe_add, add_tsub_cancel_of_le
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
x : α
⊢ (f.nnrealPart : (a : α) → ℝ≥0) x = Real.toNNReal ((f : (a : α) → ℝ) x)

Tactic:
rfl

Premises used: NNReal.mk, rfl, Real.toNNReal
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
hf : 0 ≤ f
h : ∀ (x : α), (↑(((-f).nnrealPart : (a : α) → ℝ≥0) x) : ℝ) = (↑(((0 : α →C_c ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ)
⊢ (-f).nnrealPart = 0

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
hf : 0 ≤ f
x : α
⊢ (↑(((-f).nnrealPart : (a : α) → ℝ≥0) x) : ℝ) = (↑(((0 : α →C_c ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ)

Tactic:
simpa using hf x
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
h : ∀ (x : α), (↑(((a • f).nnrealPart : (a : α) → ℝ≥0) x) : ℝ) = (↑((a.toNNReal • f.nnrealPart : (a : α) → ℝ≥0) x) : ℝ)
⊢ (a • f).nnrealPart = a.toNNReal • f.nnrealPart

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
h : max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 = HMul.hMul (β := ℝ) a (max ((f : (a : α) → ℝ) x) 0 : ℝ)
⊢ (↑(((a • f).nnrealPart : (a : α) → ℝ≥0) x) : ℝ) = (↑((a.toNNReal • f.nnrealPart : (a : α) → ℝ≥0) x) : ℝ)

Tactic:
simp only [nnrealPart_apply, coe_smul, Pi.smul_apply, Real.coe_toNNReal', smul_eq_mul,
    NNReal.coe_mul, ha, sup_of_le_left]

Premises used: Real.coe_toNNReal', CompactlySupportedContinuousMap.coe_smul, CompactlySupportedContinuousMap.nnrealPart_apply, NNReal.coe_mul, smul_eq_mul, sup_of_le_left, Pi.smul_apply
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
h :
  ∀ (hfx : LE.le (α := ℝ) (0 : ℝ) ((f : (a : α) → ℝ) x : ℝ)),
    max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 = HMul.hMul (β := ℝ) a (max ((f : (a : α) → ℝ) x) 0 : ℝ)
h₁ :
  ∀ (hfx : LE.le (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) (0 : ℝ)),
    max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 = HMul.hMul (β := ℝ) a (max ((f : (a : α) → ℝ) x) 0 : ℝ)
⊢ max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 = HMul.hMul (β := ℝ) a (max ((f : (a : α) → ℝ) x) 0 : ℝ)

Tactic:
rcases le_total 0 (f x) with hfx | hfx

Premises used: le_total, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
hfx : LE.le (α := ℝ) (0 : ℝ) ((f : (a : α) → ℝ) x : ℝ)
⊢ max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 = HMul.hMul (β := ℝ) a (max ((f : (a : α) → ℝ) x) 0 : ℝ)

Tactic:
simp [ha, hfx, mul_nonneg]

Premises used: mul_nonneg
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
hfx : LE.le (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) (0 : ℝ)
⊢ max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 = HMul.hMul (β := ℝ) a (max ((f : (a : α) → ℝ) x) 0 : ℝ)

Tactic:
simp [mul_nonpos_iff, ha, hfx]

Premises used: mul_nonpos_iff
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
h :
  ∀ (x : α),
    (↑(((a • f).nnrealPart : (a : α) → ℝ≥0) x) : ℝ) = (↑(((-a).toNNReal • (-f).nnrealPart : (a : α) → ℝ≥0) x) : ℝ)
⊢ (a • f).nnrealPart = (-a).toNNReal • (-f).nnrealPart

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
h :
  ∀ (hfx : LE.le (α := ℝ) (0 : ℝ) ((f : (a : α) → ℝ) x : ℝ)),
    max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 =
      HMul.hMul (β := ℝ) (max (-a) 0) (max (-(f : (a : α) → ℝ) x) 0 : ℝ)
h₁ :
  ∀ (hfx : LE.le (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) (0 : ℝ)),
    max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 =
      HMul.hMul (β := ℝ) (max (-a) 0) (max (-(f : (a : α) → ℝ) x) 0 : ℝ)
⊢ max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 =
    HMul.hMul (β := ℝ) (max (-a) 0) (max (-(f : (a : α) → ℝ) x) 0 : ℝ)

Tactic:
rcases le_total 0 (f x) with hfx | hfx

Premises used: le_total, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
hfx : LE.le (α := ℝ) (0 : ℝ) ((f : (a : α) → ℝ) x : ℝ)
⊢ max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 =
    HMul.hMul (β := ℝ) (max (-a) 0) (max (-(f : (a : α) → ℝ) x) 0 : ℝ)

Tactic:
simp [mul_nonpos_iff, ha, hfx]

Premises used: mul_nonpos_iff
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
hfx : LE.le (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) (0 : ℝ)
⊢ max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 =
    HMul.hMul (β := ℝ) (max (-a) 0) (max (-(f : (a : α) → ℝ) x) 0 : ℝ)

Tactic:
simp [ha, hfx, mul_nonneg_of_nonpos_of_nonpos]

Premises used: mul_nonneg_of_nonpos_of_nonpos
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f g : α →C_c ℝ
x : α
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0) x) (((f + g).nnrealPart : (a : α) → ℝ≥0) x : ℝ≥0)
    ((f.nnrealPart + g.nnrealPart : (a : α) → ℝ≥0) x : ℝ≥0)

Tactic:
simpa using Real.toNNReal_add_le

Premises used: Real.toNNReal_add_le
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f g : α →C_c ℝ
obtain :
  ∀ (h : α →C_c ℝ≥0) (hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart),
    ∃ (h : α →C_c ℝ≥0),
      (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧
        (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart
⊢ ∃ (h : α →C_c ℝ≥0),
    (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart

Tactic:
obtain ⟨h, hh⟩ := CompactlySupportedContinuousMap.exists_add_of_le
    (nnrealPart_add_le_add_nnrealPart f g)

Premises used: CompactlySupportedContinuousMap.exists_add_of_le, CompactlySupportedContinuousMap.nnrealPart_add_le_add_nnrealPart
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart
h₁ : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart
⊢ ∃ (h : α →C_c ℝ≥0),
    (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart

Tactic:
use h
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart
⊢ (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart

Tactic:
⟨hh, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart
h₁ : (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart
⊢ (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart

Tactic:
refine ⟨hh, ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart
h₁ :
  ∀ (x : α),
    (↑(((-f + -g).nnrealPart + h : (a : α) → ℝ≥0) x) : ℝ) =
      (↑(((-f).nnrealPart + (-g).nnrealPart : (a : α) → ℝ≥0) x) : ℝ)
⊢ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart
x : α
⊢ (↑(((f + g).nnrealPart + h : (a : α) → ℝ≥0) x) : ℝ) = (↑((f.nnrealPart + g.nnrealPart : (a : α) → ℝ≥0) x) : ℝ)

Tactic:
have hhx := congr(($hh x : ℝ))
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart
x : α
hhx : (↑(((f + g).nnrealPart + h : (a : α) → ℝ≥0) x) : ℝ) = (↑((f.nnrealPart + g.nnrealPart : (a : α) → ℝ≥0) x) : ℝ)
h₁ :
  -HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : α) → ℝ) x : ℝ) ((g : (a : α) → ℝ) x : ℝ) +
        max (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : α) → ℝ) x : ℝ) ((g : (a : α) → ℝ) x : ℝ)) 0 +
      (↑((h : (a : α) → ℝ≥0) x) : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) (-(f : (a : α) → ℝ) x : ℝ) (max ((f : (a : α) → ℝ) x) 0 : ℝ) +
      HAdd.hAdd (α := ℝ) (β := ℝ) (-(g : (a : α) → ℝ) x : ℝ) (max ((g : (a : α) → ℝ) x) 0 : ℝ)
⊢ (↑(((-f + -g).nnrealPart + h : (a : α) → ℝ≥0) x) : ℝ) = (↑(((-f).nnrealPart + (-g).nnrealPart : (a : α) → ℝ≥0) x) : ℝ)

Tactic:
simp only [coe_add, Pi.add_apply, nnrealPart_apply, coe_neg, Pi.neg_apply, NNReal.coe_add,
    Real.coe_toNNReal', ← neg_add, max_neg_zero] at hhx ⊢

Premises used: NNReal.coe_add, Real.coe_toNNReal', neg_add, Pi.add_apply, CompactlySupportedContinuousMap.nnrealPart_apply, CompactlySupportedContinuousMap.coe_neg, CompactlySupportedContinuousMap.coe_add, max_neg_zero, Pi.neg_apply
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f g : α →C_c ℝ
h : α →C_c ℝ≥0
hh : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart
x : α
hhx :
  max (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : α) → ℝ) x : ℝ) ((g : (a : α) → ℝ) x : ℝ)) 0 +
      (↑((h : (a : α) → ℝ≥0) x) : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) (max ((f : (a : α) → ℝ) x) 0 : ℝ) (max ((g : (a : α) → ℝ) x) 0 : ℝ)
⊢ -HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : α) → ℝ) x : ℝ) ((g : (a : α) → ℝ) x : ℝ) +
        max (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : α) → ℝ) x : ℝ) ((g : (a : α) → ℝ) x : ℝ)) 0 +
      (↑((h : (a : α) → ℝ≥0) x) : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) (-(f : (a : α) → ℝ) x : ℝ) (max ((f : (a : α) → ℝ) x) 0 : ℝ) +
      HAdd.hAdd (α := ℝ) (β := ℝ) (-(g : (a : α) → ℝ) x : ℝ) (max ((g : (a : α) → ℝ) x) 0 : ℝ)

Tactic:
linear_combination hhx
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ≥0
x : α
⊢ (f.toReal : (a : α) → ℝ) x = (↑((f : (a : α) → ℝ≥0) x) : ℝ)

Tactic:
compLeft_apply rfl _ _

Premises used: CompactlySupportedContinuousMap.compLeft_apply, NNReal.toReal
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ≥0
x : α
⊢ LE.le (α := (fun (a : α) ↦ ℝ) x) ((0 : (a : α) → ℝ) x : ℝ) ((f.toReal : (a : α) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f g : α →C_c ℝ≥0
h : ∀ (x : α), Eq (α := ℝ) (((f + g).toReal : (a : α) → ℝ) x : ℝ) ((f.toReal + g.toReal : (a : α) → ℝ) x : ℝ)
⊢ (f + g).toReal = f.toReal + g.toReal

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f g : α →C_c ℝ≥0
x : α
⊢ Eq (α := ℝ) (((f + g).toReal : (a : α) → ℝ) x : ℝ) ((f.toReal + g.toReal : (a : α) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
r : ℝ≥0
f : α →C_c ℝ≥0
h : ∀ (x : α), Eq (α := ℝ) (((r • f).toReal : (a : α) → ℝ) x : ℝ) ((r • f.toReal : (a : α) → ℝ) x : ℝ)
⊢ (r • f).toReal = r • f.toReal

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
r : ℝ≥0
f : α →C_c ℝ≥0
x : α
⊢ Eq (α := ℝ) (((r • f).toReal : (a : α) → ℝ) x : ℝ) ((r • f.toReal : (a : α) → ℝ) x : ℝ)

Tactic:
simp [NNReal.smul_def]

Premises used: NNReal.smul_def
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
h :
  ∀ (x : α), Eq (α := ℝ) ((f.nnrealPart.toReal - (-f).nnrealPart.toReal : (a : α) → ℝ) x : ℝ) ((f : (a : α) → ℝ) x : ℝ)
⊢ f.nnrealPart.toReal - (-f).nnrealPart.toReal = f

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
x : α
⊢ Eq (α := ℝ) ((f.nnrealPart.toReal - (-f).nnrealPart.toReal : (a : α) → ℝ) x : ℝ) ((f : (a : α) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
f g : α →C_c ℝ≥0
h : ∀ (x : α), Eq (α := ℝ) (((f + g).toReal : (a : α) → ℝ) x : ℝ) ((f.toReal + g.toReal : (a : α) → ℝ) x : ℝ)
⊢ (f + g).toReal = f.toReal + g.toReal

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
f g : α →C_c ℝ≥0
x : α
⊢ Eq (α := ℝ) (((f + g).toReal : (a : α) → ℝ) x : ℝ) ((f.toReal + g.toReal : (a : α) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
a : ℝ≥0
f : α →C_c ℝ≥0
h :
  ∀ (x : α),
    Eq (α := ℝ) (((a • f).toReal : (a : α) → ℝ) x : ℝ)
      ((HSMul.hSMul (α := ℝ≥0) ((RingHom.id ℝ≥0 : (a : ℝ≥0) → ℝ≥0) a : ℝ≥0) f.toReal : (a : α) → ℝ) x : ℝ)
⊢ (a • f).toReal = HSMul.hSMul (α := ℝ≥0) ((RingHom.id ℝ≥0 : (a : ℝ≥0) → ℝ≥0) a : ℝ≥0) f.toReal

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
a : ℝ≥0
f : α →C_c ℝ≥0
x : α
⊢ Eq (α := ℝ) (((a • f).toReal : (a : α) → ℝ) x : ℝ)
    ((HSMul.hSMul (α := ℝ≥0) ((RingHom.id ℝ≥0 : (a : ℝ≥0) → ℝ≥0) a : ℝ≥0) f.toReal : (a : α) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ Eq.{u_2 + 1} (α := (a : α →C_c ℝ≥0) → α →C_c ℝ) (⇑toRealLinearMap : (a : α →C_c ℝ≥0) → α →C_c ℝ) toReal

Tactic:
rfl

Premises used: CompactlySupportedContinuousMap.toReal, CompactlySupportedContinuousMap.compLeft, rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ≥0
⊢ (toRealLinearMap : (a : α →C_c ℝ≥0) → α →C_c ℝ) f = f.toReal

Tactic:
rfl

Premises used: CompactlySupportedContinuousMap.toReal, CompactlySupportedContinuousMap.compLeft, rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ≥0
x : α
⊢ (((toRealLinearMap : (a : α →C_c ℝ≥0) → α →C_c ℝ) f : α →C_c ℝ) : (a : α) → ℝ) x = (↑((f : (a : α) → ℝ≥0) x) : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ≥0
h : ∀ (x : α), (↑((f.toReal.nnrealPart : (a : α) → ℝ≥0) x) : ℝ) = (↑((f : (a : α) → ℝ≥0) x) : ℝ)
⊢ f.toReal.nnrealPart = f

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ≥0
x : α
⊢ (↑((f.toReal.nnrealPart : (a : α) → ℝ≥0) x) : ℝ) = (↑((f : (a : α) → ℝ≥0) x) : ℝ)

Tactic:
simp