awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α →C_c ℝ≥0
h : ∀ (x : α), (↑(((-f.toReal).nnrealPart : (a : α) → ℝ≥0) x) : ℝ) = (↑(((0 : α →C_c ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ)
⊢ (-f.toReal).nnrealPart = 0

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) : ℝ) = (↑(((0 : α →C_c ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
Λ : (α →C_c ℝ) →ₚ[ℝ] ℝ
f : α →C_c ℝ≥0
⊢ LE.le (α := α →C_c ℝ) (0 : α →C_c ℝ) ((toRealLinearMap : (a : α →C_c ℝ≥0) → α →C_c ℝ) f : α →C_c ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
Λ : (α →C_c ℝ) →ₚ[ℝ] ℝ
f g : α →C_c ℝ≥0
simp :
  NNReal.mk
      (HAdd.hAdd (α := ℝ) (β := ℝ) ((Λ : (a : α →C_c ℝ) → ℝ) f.toReal : ℝ) ((Λ : (a : α →C_c ℝ) → ℝ) g.toReal : ℝ)) ⋯ =
    NNReal.mk ((Λ : (a : α →C_c ℝ) → ℝ) f.toReal) ⋯ + NNReal.mk ((Λ : (a : α →C_c ℝ) → ℝ) g.toReal) ⋯
⊢ 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 ℝ)) ⋯

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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
      (HAdd.hAdd (α := ℝ) (β := ℝ) ((Λ : (a : α →C_c ℝ) → ℝ) f.toReal : ℝ) ((Λ : (a : α →C_c ℝ) → ℝ) g.toReal : ℝ)) ⋯ =
    NNReal.mk ((Λ : (a : α →C_c ℝ) → ℝ) f.toReal) ⋯ + NNReal.mk ((Λ : (a : α →C_c ℝ) → ℝ) g.toReal) ⋯

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
Λ : (α →C_c ℝ) →ₚ[ℝ] ℝ
a : ℝ≥0
f : α →C_c ℝ≥0
simp :
  NNReal.mk (HMul.hMul (β := ℝ) (↑a : ℝ) ((Λ : (a : α →C_c ℝ) → ℝ) f.toReal : ℝ)) ⋯ =
    a * NNReal.mk ((Λ : (a : α →C_c ℝ) → ℝ) f.toReal) ⋯
⊢ 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 ℝ)) ⋯)

Tactic:
simp [NNReal.smul_def]

Premises used: NNReal.smul_def
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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 (HMul.hMul (β := ℝ) (↑a : ℝ) ((Λ : (a : α →C_c ℝ) → ℝ) f.toReal : ℝ)) ⋯ =
    a * NNReal.mk ((Λ : (a : α →C_c ℝ) → ℝ) f.toReal) ⋯

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ : (α →C_c ℝ) →ₚ[ℝ] ℝ
f : α →C_c ℝ≥0
⊢ (↑((toNNRealLinear Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f) : ℝ) = (Λ : (a : α →C_c ℝ) → ℝ) f.toReal

Tactic:
rfl

Premises used: CompactlySupportedContinuousMap.toReal, CompactlySupportedContinuousMap.compLeft, NNReal.toReal, rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
h : Λ₁ = Λ₂
rw rw₁ : toNNRealLinear Λ₂ = toNNRealLinear Λ₂
⊢ toNNRealLinear Λ₁ = toNNRealLinear Λ₂

Tactic:
rw [h]
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
refine : ∀ (h : toNNRealLinear Λ₁ = toNNRealLinear Λ₂), Λ₁ = Λ₂
⊢ toNNRealLinear Λ₁ = toNNRealLinear Λ₂ ↔ Λ₁ = Λ₂

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
h : toNNRealLinear Λ₁ = toNNRealLinear Λ₂
h₁ : ∀ (f : α →C_c ℝ), Eq (α := ℝ) ((Λ₁ : (a : α →C_c ℝ) → ℝ) f : ℝ) ((Λ₂ : (a : α →C_c ℝ) → ℝ) f : ℝ)
⊢ Λ₁ = Λ₂

Tactic:
ext f
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
h : toNNRealLinear Λ₁ = toNNRealLinear Λ₂
f : α →C_c ℝ
h₁ :
  Eq (α := ℝ) ((Λ₁ : (a : α →C_c ℝ) → ℝ) (f.nnrealPart.toReal - (-f).nnrealPart.toReal) : ℝ)
    ((Λ₂ : (a : α →C_c ℝ) → ℝ) (f.nnrealPart.toReal - (-f).nnrealPart.toReal) : ℝ)
⊢ Eq (α := ℝ) ((Λ₁ : (a : α →C_c ℝ) → ℝ) f : ℝ) ((Λ₂ : (a : α →C_c ℝ) → ℝ) f : ℝ)

Tactic:
rw [← nnrealPart_sub_nnrealPart_neg f]

Premises used: CompactlySupportedContinuousMap.nnrealPart_sub_nnrealPart_neg
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ₁ Λ₂ : (α →C_c ℝ) →ₚ[ℝ] ℝ
h : toNNRealLinear Λ₁ = toNNRealLinear Λ₂
f : α →C_c ℝ
⊢ ∀ (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

Premises used: NNReal.eq_iff, LinearMap.ext_iff, CompactlySupportedContinuousMap.toNNRealLinear_apply
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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 : ℝ)
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 : ℝ)
⊢ Eq (α := ℝ) ((Λ₁ : (a : α →C_c ℝ) → ℝ) (f.nnrealPart.toReal - (-f).nnrealPart.toReal) : ℝ)
    ((Λ₂ : (a : α →C_c ℝ) → ℝ) (f.nnrealPart.toReal - (-f).nnrealPart.toReal) : ℝ)

Tactic:
simp_rw [map_sub, h]

Premises used: map_sub
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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 ℝ
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) : ℝ))
⊢ (↑((Λ : (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) : ℝ))

Tactic:
simp only [neg_add_rev]

Premises used: neg_add_rev
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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 ℝ
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) : ℝ))
⊢ (↑((Λ : (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

Premises used: CompactlySupportedContinuousMap.exists_add_nnrealPart_add_eq
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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
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) : ℝ))
⊢ (↑((Λ : (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:
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]

Premises used: NNReal.coe_add, sub_self, HSub.hSub, map_add, sub_add_sub_comm, add_comm, And.right, And.left, HAdd.hAdd, CompactlySupportedContinuousMap.nnrealPart, add_zero, DFunLike.coe, NNReal.toReal, Neg.neg
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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
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) : ℝ))
⊢ (↑((Λ : (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:
simp only [map_add, NNReal.coe_add]

Premises used: NNReal.coe_add, map_add
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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) : ℝ) + (↑((Λ : (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:
ring
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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) : ℝ))
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) : ℝ))
⊢ (↑((Λ : (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

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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
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) : ℝ))
⊢ (↑((Λ : (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:
rw [RingHom.id_apply, smul_eq_mul, ← (smul_neg a f), nnrealPart_smul_pos f ha,
            nnrealPart_smul_pos (-f) ha]

Premises used: RingHom.id_apply, smul_neg, CompactlySupportedContinuousMap.nnrealPart_smul_pos, smul_eq_mul, Neg.neg
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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.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:
simp [sup_of_le_left ha, mul_sub]

Premises used: mul_sub, sup_of_le_left
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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
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) : ℝ))
⊢ (↑((Λ : (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:
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)]

Premises used: Iff.mpr, CompactlySupportedContinuousMap.nnrealPart_smul_neg, RingHom.id_apply, Real.coe_toNNReal', neg_neg, smul_neg, neg_nonneg, NNReal.coe_mul, smul_eq_mul, sup_of_le_left, Neg.neg, map_smul
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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 * (↑((Λ : (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:
ring
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
g : α →C_c ℝ
hg : 0 ≤ g
⊢ LE.le (α := ℝ) (0 : ℝ)
    (({
            toFun := fun (f : α →C_c ℝ) ↦
              (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) -
                (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ),
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : α →C_c ℝ) → ℝ)
        g :
      ℝ)

Tactic:
simp [nnrealPart_neg_eq_zero_of_nonneg hg]

Premises used: CompactlySupportedContinuousMap.nnrealPart_neg_eq_zero_of_nonneg
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : α →C_c ℝ
⊢ (toRealPositiveLinear Λ : (a : α →C_c ℝ) → ℝ) f =
    (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f.nnrealPart) : ℝ) - (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) (-f).nnrealPart) : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : α →C_c ℝ≥0
⊢ (toRealPositiveLinear Λ : (a : α →C_c ℝ) → ℝ) f.toReal = (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f) : ℝ)

Tactic:
simp [toRealPositiveLinear_apply]

Premises used: CompactlySupportedContinuousMap.toRealPositiveLinear_apply
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
h :
  ∀ (f : α →C_c ℝ≥0),
    (↑((toNNRealLinear (toRealPositiveLinear Λ) : (a : α →C_c ℝ≥0) → ℝ≥0) f) : ℝ) =
      (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f) : ℝ)
⊢ toNNRealLinear (toRealPositiveLinear Λ) = Λ

Tactic:
ext f
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : α →C_c ℝ≥0
⊢ (↑((toNNRealLinear (toRealPositiveLinear Λ) : (a : α →C_c ℝ≥0) → ℝ≥0) f) : ℝ) =
    (↑((Λ : (a : α →C_c ℝ≥0) → ℝ≥0) f) : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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 : β
⊢ Continuous.{u_2, u_4} (Y := γ) fun (a : α) ↦ (f : (a : β) → γ) (HMul.hMul (β := β) b ((φ : (a : α) → β) a : β))

Tactic:
fun_prop
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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 : β
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 : β))
⊢ 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

Premises used: Iff.mpr, CompactlySupportedContinuousMap.hasCompactSupport, exists_compact_iff_hasCompactSupport
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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 : β))

Tactic:
exists_compact_iff_hasCompactSupport.mp ⟨φ ⁻¹' (b⁻¹ • K),
      hφ.isCompact_preimage (hK.smul b⁻¹), fun x hx ↦ hf _ ?_⟩

Premises used: HMul.hMul, exists_compact_iff_hasCompactSupport, Inv.inv, Set.preimage, And.intro, Topology.IsClosedEmbedding.isCompact_preimage, Exists.intro, Iff.mp, HSMul.hSMul, IsCompact.smul, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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 : γ)
refine : ∀ (x : α) (hx : x ∉ (⇑φ : (a : α) → β) ⁻¹' (b⁻¹ • K)), HMul.hMul (β := β) b ((φ : (a : α) → β) x : β) ∉ K
⊢ HasCompactSupport.{u_2, u_4} (β := γ) fun (a : α) ↦ (f : (a : β) → γ) (HMul.hMul (β := β) b ((φ : (a : α) → β) a : β))

Tactic:
refine exists_compact_iff_hasCompactSupport.mp ⟨φ ⁻¹' (b⁻¹ • K),
      hφ.isCompact_preimage (hK.smul b⁻¹), fun x hx ↦ hf _ ?_⟩

Premises used: exists_compact_iff_hasCompactSupport, Inv.inv, Set.preimage, And.intro, Topology.IsClosedEmbedding.isCompact_preimage, Exists.intro, Iff.mp, HSMul.hSMul, IsCompact.smul, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
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 : γ)
x : α
hx : x ∉ (⇑φ : (a : α) → β) ⁻¹' (b⁻¹ • K)
⊢ HMul.hMul (β := β) b ((φ : (a : α) → β) x : β) ∉ K

Tactic:
simpa [Set.mem_smul_set_iff_inv_smul_mem] using hx

Premises used: Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : 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 : β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((pullback_monoidHom hφ f b : (a : α) → γ) a : γ)
    ((f : (a : β) → γ) (HMul.hMul (β := β) b ((φ : (a : α) → β) a : β)) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_3
inst : Zero X
inst_1 : Zero R
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace R
f g : C(X, R)₀
h : ∀ (x : X), Eq.{u_3 + 1} (α := R) ((f : (a : X) → R) x : R) ((g : (a : X) → R) x : R)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_3
inst : Zero X
inst_1 : Zero R
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace R
f : C(X, R)
h0 : Eq.{u_3 + 1} (α := R) ((f : (a : X) → R) 0 : R) (0 : R)
⊢ Eq (α := (a : X) → R) (⇑{ toContinuousMap := f, map_zero' := h0 : C(X, R)₀ } : (a : X) → R) (⇑f : (a : X) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero
Goal:
X : Type u_1
R : Type u_3
inst : Zero X
inst_1 : Zero R
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace R
⊢ Injective (α := C(X, R)₀) (β := C(X, R)) _root_.toContinuousMap

Tactic:
fun _ _ h ↦ congr(.mk $(h) _)

Premises used: HEq.refl, Eq.casesOn, id, toContinuousMap, ContinuousMapZero.map_zero', eq_of_heq, Eq.ndrec, Eq.refl, ContinuousMapZero.mk, Function.Injective, Eq.symm