-- Mathlib/Topology/ContinuousMap/CompactlySupported.lean
protected lemma exists_add_of_le {f₁ f₂ : C_c(α, ℝ≥0)} (h : f₁ ≤ f₂) : ∃ (g : C_c(α, ℝ≥0)),
    f₁ + g = f₂

Proof state:
case refine_1.h
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
hx : x ∉ Function.support f₁.toFun ∪ Function.support f₂.toFun
⊢ 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 ⊢

Result:
case refine_1.h
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
hx : f₁ x = 0 ∧ f₂ x = 0
⊢ f₂ x - f₁ x = 0

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ ∃ g, f₁ + g = f₂

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

Result:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ HasCompactSupport (f₂.toContinuousMap - f₁.toContinuousMap).toFun

case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ?refine_1 } = f₂

Proof state:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ closure (Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun) ⊆ tsupport f₁.toFun ∪ tsupport f₂.toFun

Tactic:
rw [tsupport, tsupport, ← closure_union]

Result:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ closure (Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun) ⊆
    closure (Function.support f₁.toFun ∪ Function.support f₂.toFun)

Proof state:
case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ⋯ } = f₂

Tactic:
ext x

Result:
case refine_2.h.a
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
⊢ ↑((f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ⋯ }) x) = ↑(f₂ x)

Proof state:
case refine_1.h
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
hx : f₁ x = 0 ∧ f₂ x = 0
⊢ f₂ x - f₁ x = 0

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

Result:
no goals

Proof state:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ HasCompactSupport (f₂.toContinuousMap - f₁.toContinuousMap).toFun

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

Result:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ closure (Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun) ⊆ tsupport f₁.toFun ∪ tsupport f₂.toFun

Proof state:
case refine_1.h
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
hx : x ∈ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun
⊢ x ∈ Function.support f₁.toFun ∪ Function.support f₂.toFun

Tactic:
contrapose! hx

Result:
case refine_1.h
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
hx : x ∉ Function.support f₁.toFun ∪ Function.support f₂.toFun
⊢ x ∉ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun

Proof state:
case refine_1.h
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun ⊆
    Function.support f₁.toFun ∪ Function.support f₂.toFun

Tactic:
intro x hx

Result:
case refine_1.h
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
hx : x ∈ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun
⊢ x ∈ Function.support f₁.toFun ∪ Function.support f₂.toFun

Proof state:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ closure (Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun) ⊆
    closure (Function.support f₁.toFun ∪ Function.support f₂.toFun)

Tactic:
apply closure_mono

Result:
case refine_1.h
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun ⊆
    Function.support f₁.toFun ∪ Function.support f₂.toFun

Proof state:
case refine_2.h.a
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
⊢ ↑((f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ⋯ }) x) = ↑(f₂ x)

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

Result:
no goals