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 α
δ : 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 : γ)
⊢ (o ∩ Function.support f.toFun).Nonempty
have obtain : ∀ (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: obtain ⟨y, hy⟩ := hx (g ⁻¹' o) (IsOpen.preimage g.1.2 ho) hgxo
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ ∃ (g : α →C_c ℝ≥0), f₁ + g = f₂
have refine_1 : HasCompactSupport (f₂.toContinuousMap - f₁.toContinuousMap).toFun
Tactic: refine ⟨⟨f₂.1 - f₁.1, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
refine_1 : HasCompactSupport (f₂.toContinuousMap - f₁.toContinuousMap).toFun
⊢ ∃ (g : α →C_c ℝ≥0), f₁ + g = f₂
have refine_2 : f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := sorry : α →C_c ℝ≥0 } = f₂
Tactic: refine ⟨⟨f₂.1 - f₁.1, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ HasCompactSupport (f₂.toContinuousMap - f₁.toContinuousMap).toFun
have refine_1 : closure (Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun) ⊆ tsupport f₁.toFun ∪ tsupport f₂.toFun
Tactic: apply (f₁.hasCompactSupport'.union f₂.hasCompactSupport').of_isClosed_subset isClosed_closure
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : 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
have refine_1 : closure (Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun) ⊆
  closure (Function.support f₁.toFun ∪ Function.support f₂.toFun)
Tactic: rw [tsupport, tsupport, ← closure_union]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : 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)
have refine_1 : Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun ⊆ Function.support f₁.toFun ∪ Function.support f₂.toFun
Tactic: apply closure_mono
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : 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
have refine_1 : ∀ (hx : x ∉ Function.support f₁.toFun ∪ Function.support f₂.toFun),
  x ∉ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
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
⊢ x ∉ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun
have 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
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 ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ⋯ : α →C_c ℝ≥0 } = f₂
have refine_2 : ∀ (x : α),
  (↑((f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := sorry : α →C_c ℝ≥0 } :
            (a : α) → ℝ≥0)
          x) :
      ℝ) =
    (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
hf : 0 ≤ f
⊢ (-f).nnrealPart = 0
have h : ∀ (x : α), (↑(((-f).nnrealPart : (a : α) → ℝ≥0) x) : ℝ) = (↑(((0 : α →C_c ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
⊢ (a • f).nnrealPart = a.toNNReal • f.nnrealPart
have h : ∀ (x : α), (↑(((a • f).nnrealPart : (a : α) → ℝ≥0) x) : ℝ) = (↑((a.toNNReal • f.nnrealPart : (a : α) → ℝ≥0) x) : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
⊢ (↑(((a • f).nnrealPart : (a : α) → ℝ≥0) x) : ℝ) = (↑((a.toNNReal • f.nnrealPart : (a : α) → ℝ≥0) x) : ℝ)
have h : max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 = HMul.hMul (β := ℝ) a (max ((f : (a : α) → ℝ) x) 0 : ℝ)
Tactic: simp only [nnrealPart_apply, coe_smul, Pi.smul_apply, Real.coe_toNNReal', smul_eq_mul,
    NNReal.coe_mul, ha, sup_of_le_left]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
⊢ max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 = HMul.hMul (β := ℝ) a (max ((f : (a : α) → ℝ) x) 0 : ℝ)
have h : ∀ (hfx : LE.le (α := ℝ) (0 : ℝ) ((f : (a : α) → ℝ) x : ℝ)),
  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
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
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 : ℝ)
⊢ max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 = HMul.hMul (β := ℝ) a (max ((f : (a : α) → ℝ) x) 0 : ℝ)
have h₁ : ∀ (hfx : LE.le (α := ℝ) ((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
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
⊢ (a • f).nnrealPart = (-a).toNNReal • (-f).nnrealPart
have h : ∀ (x : α),
  (↑(((a • f).nnrealPart : (a : α) → ℝ≥0) x) : ℝ) = (↑(((-a).toNNReal • (-f).nnrealPart : (a : α) → ℝ≥0) x) : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
⊢ max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 =
    HMul.hMul (β := ℝ) (max (-a) 0) (max (-(f : (a : α) → ℝ) x) 0 : ℝ)
have 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 : ℝ)
Tactic: rcases le_total 0 (f x) with hfx | hfx
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
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 : ℝ)
⊢ max (HMul.hMul (β := ℝ) a ((f : (a : α) → ℝ) x : ℝ)) 0 =
    HMul.hMul (β := ℝ) (max (-a) 0) (max (-(f : (a : α) → ℝ) x) 0 : ℝ)
have 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 : ℝ)
Tactic: rcases le_total 0 (f x) with hfx | hfx
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f g : α →C_c ℝ
⊢ ∃ (h : α →C_c ℝ≥0),
    (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart
have 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
Tactic: obtain ⟨h, hh⟩ := CompactlySupportedContinuousMap.exists_add_of_le
    (nnrealPart_add_le_add_nnrealPart f g)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f g : α →C_c ℝ
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
have h₁ : (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧ (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart
Tactic: use h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
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
have h₁ : (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart
Tactic: refine ⟨hh, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
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
have h₁ : ∀ (x : α),
  (↑(((-f + -g).nnrealPart + h : (a : α) → ℝ≥0) x) : ℝ) = (↑(((-f).nnrealPart + (-g).nnrealPart : (a : α) → ℝ≥0) x) : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (hypothesis)
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) : ℝ)
have hhx : (↑(((f + g).nnrealPart + h : (a : α) → ℝ≥0) x) : ℝ) = (↑((f.nnrealPart + g.nnrealPart : (a : α) → ℝ≥0) x) : ℝ)
Tactic: have hhx := congr(($hh x : ℝ))
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
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) : ℝ)
⊢ (↑(((-f + -g).nnrealPart + h : (a : α) → ℝ≥0) x) : ℝ) = (↑(((-f).nnrealPart + (-g).nnrealPart : (a : α) → ℝ≥0) x) : ℝ)
have 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 : ℝ)
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 ⊢
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f g : α →C_c ℝ≥0
⊢ (f + g).toReal = f.toReal + g.toReal
have h : ∀ (x : α), Eq (α := ℝ) (((f + g).toReal : (a : α) → ℝ) x : ℝ) ((f.toReal + g.toReal : (a : α) → ℝ) x : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
r : ℝ≥0
f : α →C_c ℝ≥0
⊢ (r • f).toReal = r • f.toReal
have h : ∀ (x : α), Eq (α := ℝ) (((r • f).toReal : (a : α) → ℝ) x : ℝ) ((r • f.toReal : (a : α) → ℝ) x : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ
⊢ f.nnrealPart.toReal - (-f).nnrealPart.toReal = f
have h : ∀ (x : α), Eq (α := ℝ) ((f.nnrealPart.toReal - (-f).nnrealPart.toReal : (a : α) → ℝ) x : ℝ) ((f : (a : α) → ℝ) x : ℝ)
Tactic: ext x
-- 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 α
f g : α →C_c ℝ≥0
⊢ (f + g).toReal = f.toReal + g.toReal
have h : ∀ (x : α), Eq (α := ℝ) (((f + g).toReal : (a : α) → ℝ) x : ℝ) ((f.toReal + g.toReal : (a : α) → ℝ) x : ℝ)
Tactic: ext x
-- 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 α
a : ℝ≥0
f : α →C_c ℝ≥0
⊢ (a • f).toReal = HSMul.hSMul (α := ℝ≥0) ((RingHom.id ℝ≥0 : (a : ℝ≥0) → ℝ≥0) a : ℝ≥0) f.toReal
have h : ∀ (x : α),
  Eq (α := ℝ) (((a • f).toReal : (a : α) → ℝ) x : ℝ)
    ((HSMul.hSMul (α := ℝ≥0) ((RingHom.id ℝ≥0 : (a : ℝ≥0) → ℝ≥0) a : ℝ≥0) f.toReal : (a : α) → ℝ) x : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ≥0
⊢ f.toReal.nnrealPart = f
have h : ∀ (x : α), (↑((f.toReal.nnrealPart : (a : α) → ℝ≥0) x) : ℝ) = (↑((f : (a : α) → ℝ≥0) x) : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ≥0
⊢ (-f.toReal).nnrealPart = 0
have h : ∀ (x : α), (↑(((-f.toReal).nnrealPart : (a : α) → ℝ≥0) x) : ℝ) = (↑(((0 : α →C_c ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ)
Tactic: ext x
-- 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 ℝ) →ₚ[ℝ] ℝ
f g : α →C_c ℝ≥0
⊢ NNReal.mk ((Λ : (a : α →C_c ℝ) → ℝ) ((toRealLinearMap : (a : α →C_c ℝ≥0) → α →C_c ℝ) (f + g) : α →C_c ℝ)) ⋯ =
    NNReal.mk ((Λ : (a : α →C_c ℝ) → ℝ) ((toRealLinearMap : (a : α →C_c ℝ≥0) → α →C_c ℝ) f : α →C_c ℝ)) ⋯ +
      NNReal.mk ((Λ : (a : α →C_c ℝ) → ℝ) ((toRealLinearMap : (a : α →C_c ℝ≥0) → α →C_c ℝ) g : α →C_c ℝ)) ⋯
have simp : NNReal.mk (HAdd.hAdd (α := ℝ) (β := ℝ) ((Λ : (a : α →C_c ℝ) → ℝ) f.toReal : ℝ) ((Λ : (a : α →C_c ℝ) → ℝ) g.toReal : ℝ))
    sorry =
  NNReal.mk ((Λ : (a : α →C_c ℝ) → ℝ) f.toReal) sorry + NNReal.mk ((Λ : (a : α →C_c ℝ) → ℝ) g.toReal) sorry
Tactic: simp
-- 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 ℝ) →ₚ[ℝ] ℝ
a : ℝ≥0
f : α →C_c ℝ≥0
⊢ NNReal.mk ((Λ : (a : α →C_c ℝ) → ℝ) ((toRealLinearMap : (a : α →C_c ℝ≥0) → α →C_c ℝ) (a • f) : α →C_c ℝ)) ⋯ =
    HSMul.hSMul (α := ℝ≥0) ((RingHom.id ℝ≥0 : (a : ℝ≥0) → ℝ≥0) a : ℝ≥0)
      (NNReal.mk ((Λ : (a : α →C_c ℝ) → ℝ) ((toRealLinearMap : (a : α →C_c ℝ≥0) → α →C_c ℝ) f : α →C_c ℝ)) ⋯)
have simp : NNReal.mk (HMul.hMul (β := ℝ) (↑a : ℝ) ((Λ : (a : α →C_c ℝ) → ℝ) f.toReal : ℝ)) sorry =
  a * NNReal.mk ((Λ : (a : α →C_c ℝ) → ℝ) f.toReal) sorry
Tactic: simp [NNReal.smul_def]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
h : Λ₁ = Λ₂
⊢ toNNRealLinear Λ₁ = toNNRealLinear Λ₂
have rw : toNNRealLinear Λ₂ = toNNRealLinear Λ₂
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
⊢ toNNRealLinear Λ₁ = toNNRealLinear Λ₂ ↔ Λ₁ = Λ₂
have refine : ∀ (h : toNNRealLinear Λ₁ = toNNRealLinear Λ₂), Λ₁ = Λ₂
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
h : toNNRealLinear Λ₁ = toNNRealLinear Λ₂
⊢ Λ₁ = Λ₂
have h₁ : ∀ (f : α →C_c ℝ), Eq (α := ℝ) ((Λ₁ : (a : α →C_c ℝ) → ℝ) f : ℝ) ((Λ₂ : (a : α →C_c ℝ) → ℝ) f : ℝ)
Tactic: ext f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
h : toNNRealLinear Λ₁ = toNNRealLinear Λ₂
f : α →C_c ℝ
⊢ Eq (α := ℝ) ((Λ₁ : (a : α →C_c ℝ) → ℝ) f : ℝ) ((Λ₂ : (a : α →C_c ℝ) → ℝ) f : ℝ)
have h₁ : Eq (α := ℝ) ((Λ₁ : (a : α →C_c ℝ) → ℝ) (f.nnrealPart.toReal - (-f).nnrealPart.toReal) : ℝ)
  ((Λ₂ : (a : α →C_c ℝ) → ℝ) (f.nnrealPart.toReal - (-f).nnrealPart.toReal) : ℝ)
Tactic: rw [← nnrealPart_sub_nnrealPart_neg f]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (hypothesis)
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
h : toNNRealLinear Λ₁ = toNNRealLinear Λ₂
f : α →C_c ℝ
⊢ Eq (α := ℝ) ((Λ₁ : (a : α →C_c ℝ) → ℝ) (f.nnrealPart.toReal - (-f).nnrealPart.toReal) : ℝ)
    ((Λ₂ : (a : α →C_c ℝ) → ℝ) (f.nnrealPart.toReal - (-f).nnrealPart.toReal) : ℝ)
have h₁ : ∀ (x : α →C_c ℝ≥0), Eq (α := ℝ) ((Λ₁ : (a : α →C_c ℝ) → ℝ) x.toReal : ℝ) ((Λ₂ : (a : α →C_c ℝ) → ℝ) x.toReal : ℝ)
Tactic: simp only [LinearMap.ext_iff, NNReal.eq_iff, toNNRealLinear_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
f : α →C_c ℝ
h : ∀ (x : α →C_c ℝ≥0), Eq (α := ℝ) ((Λ₁ : (a : α →C_c ℝ) → ℝ) x.toReal : ℝ) ((Λ₂ : (a : α →C_c ℝ) → ℝ) x.toReal : ℝ)
⊢ Eq (α := ℝ) ((Λ₁ : (a : α →C_c ℝ) → ℝ) (f.nnrealPart.toReal - (-f).nnrealPart.toReal) : ℝ)
    ((Λ₂ : (a : α →C_c ℝ) → ℝ) (f.nnrealPart.toReal - (-f).nnrealPart.toReal) : ℝ)
have h₁ : HSub.hSub (α := ℝ) (β := ℝ) ((Λ₁ : (a : α →C_c ℝ) → ℝ) f.nnrealPart.toReal : ℝ)
    ((Λ₁ : (a : α →C_c ℝ) → ℝ) (-f).nnrealPart.toReal : ℝ) =
  HSub.hSub (α := ℝ) (β := ℝ) ((Λ₂ : (a : α →C_c ℝ) → ℝ) f.nnrealPart.toReal : ℝ)
    ((Λ₂ : (a : α →C_c ℝ) → ℝ) (-f).nnrealPart.toReal : ℝ)
Tactic: simp_rw [map_sub, h]
-- 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
f g : α →C_c ℝ
⊢ (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (f + g).nnrealPart) : ℝ) -
      (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-(f + g)).nnrealPart) : ℝ) =
    (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ) +
      ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) g.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-g).nnrealPart) : ℝ))
have simp : (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (f + g).nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-g + -f).nnrealPart) : ℝ) =
  (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ) +
    ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) g.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-g).nnrealPart) : ℝ))
Tactic: simp only [neg_add_rev]
-- 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
f g : α →C_c ℝ
⊢ (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (f + g).nnrealPart) : ℝ) -
      (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-g + -f).nnrealPart) : ℝ) =
    (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ) +
      ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) g.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-g).nnrealPart) : ℝ))
have obtain : ∀ (h : α →C_c ℝ≥0)
  (hh :
    (f + g).nnrealPart + h = f.nnrealPart + g.nnrealPart ∧
      (-f + -g).nnrealPart + h = (-f).nnrealPart + (-g).nnrealPart),
  (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (f + g).nnrealPart) : ℝ) -
      (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-g + -f).nnrealPart) : ℝ) =
    (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ) +
      ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) g.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-g).nnrealPart) : ℝ))
Tactic: obtain ⟨h, hh⟩ := exists_add_nnrealPart_add_eq f g
-- 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
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
⊢ (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (f + g).nnrealPart) : ℝ) -
      (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-g + -f).nnrealPart) : ℝ) =
    (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ) +
      ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) g.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-g).nnrealPart) : ℝ))
have rw : (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (f.nnrealPart + g.nnrealPart)) : ℝ) -
    (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) ((-f).nnrealPart + (-g).nnrealPart)) : ℝ) =
  (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ) +
    ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) g.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-g).nnrealPart) : ℝ))
Tactic: rw [← add_zero ((Λ (f + g).nnrealPart).toReal - (Λ (-g + -f).nnrealPart).toReal),
          ← sub_self (Λ h).toReal, sub_add_sub_comm, ← NNReal.coe_add, ← NNReal.coe_add,
          ← map_add, ← map_add, hh.1, add_comm (-g) (-f), hh.2]
-- 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
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
⊢ (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (f.nnrealPart + g.nnrealPart)) : ℝ) -
      (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) ((-f).nnrealPart + (-g).nnrealPart)) : ℝ) =
    (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ) +
      ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) g.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-g).nnrealPart) : ℝ))
have simp : (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) + (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) g.nnrealPart) : ℝ) -
    ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ) + (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-g).nnrealPart) : ℝ)) =
  (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ) +
    ((↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) g.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-g).nnrealPart) : ℝ))
Tactic: simp only [map_add, NNReal.coe_add]