awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : NonUnitalNormedRing β
inst_3 : StarRing β
inst_4 : CStarRing β
f : C(α, β)
rw : ∀ (x : α), norm.{u_2} (E := β) ((f : (a : α) → β) x : β) ≤ √‖star f * f‖
⊢ ‖f‖ * ‖f‖ ≤ ‖star f * f‖

Tactic:
rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _),
      ContinuousMap.norm_le _ (Real.sqrt_nonneg _)]

Premises used: ContinuousMap.norm_le, Real.le_sqrt, sq, Real.sqrt_nonneg, norm_nonneg
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : NonUnitalNormedRing β
inst_3 : StarRing β
inst_4 : CStarRing β
f : C(α, β)
x : α
rw : ‖HMul.hMul (α := β) (β := β) (star ((f : (a : α) → β) x) : β) ((f : (a : α) → β) x : β)‖ ≤ ‖star f * f‖
⊢ norm.{u_2} (E := β) ((f : (a : α) → β) x : β) ≤ √‖star f * f‖

Tactic:
rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self]

Premises used: Real.le_sqrt, sq, CStarRing.norm_star_mul_self, norm_nonneg
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : NonUnitalNormedRing β
inst_3 : StarRing β
inst_4 : CStarRing β
f : C(α, β)
x : α
⊢ ‖HMul.hMul (α := β) (β := β) (star ((f : (a : α) → β) x) : β) ((f : (a : α) → β) x : β)‖ ≤ ‖star f * f‖

Tactic:
ContinuousMap.norm_coe_le_norm (star f * f) x

Premises used: ContinuousMap.norm_coe_le_norm, HMul.hMul, setOf, Star.star
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : NonUnitalNormedRing β
inst_3 : StarRing β
inst_4 : CStarRing β
f : C(α, β)
x : α
⊢ ‖HMul.hMul (α := β) (β := β) (star ((f : (a : α) → β) x) : β) ((f : (a : α) → β) x : β)‖ ≤ ‖star f * f‖

Tactic:
exact ContinuousMap.norm_coe_le_norm (star f * f) x

Premises used: ContinuousMap.norm_coe_le_norm, HMul.hMul, Star.star
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f g : α →C_c β
h : Eq (α := (a : α) → β) ((fun (f : α →C_c β) ↦ f.toFun) f) ((fun (f : α →C_c β) ↦ f.toFun) g)
obtain :
  ∀ (toFun : α → β) (continuous_toFun : Continuous toFun)
    (hasCompactSupport' : HasCompactSupport { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →C_c β) ↦ f.toFun)
          { toFun := toFun, continuous_toFun := continuous_toFun, hasCompactSupport' := hasCompactSupport' })
        ((fun (f : α →C_c β) ↦ f.toFun) g)),
    { toFun := toFun, continuous_toFun := continuous_toFun, hasCompactSupport' := hasCompactSupport' : α →C_c β } = g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
g : α →C_c β
toFun : α → β
continuous_toFun : Continuous toFun
hasCompactSupport' : HasCompactSupport { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →C_c β) ↦ f.toFun)
      { toFun := toFun, continuous_toFun := continuous_toFun, hasCompactSupport' := hasCompactSupport' })
    ((fun (f : α →C_c β) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : α → β) (continuous_toFun_1 : Continuous toFun_1)
    (hasCompactSupport'_1 :
      HasCompactSupport { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(α, β) }.toFun)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →C_c β) ↦ f.toFun)
          { toFun := toFun, continuous_toFun := continuous_toFun, hasCompactSupport' := hasCompactSupport' })
        ((fun (f : α →C_c β) ↦ f.toFun)
          { toFun := toFun_1, continuous_toFun := continuous_toFun_1, hasCompactSupport' := hasCompactSupport'_1 })),
    { toFun := toFun, continuous_toFun := continuous_toFun, hasCompactSupport' := hasCompactSupport' : α →C_c β } =
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1, hasCompactSupport' := hasCompactSupport'_1 }
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, hasCompactSupport' := hasCompactSupport' : α →C_c β } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
toFun : α → β
continuous_toFun : Continuous toFun
hasCompactSupport' : HasCompactSupport { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun
toFun_1 : α → β
continuous_toFun_1 : Continuous toFun_1
hasCompactSupport'_1 : HasCompactSupport { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(α, β) }.toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →C_c β) ↦ f.toFun)
      { toFun := toFun, continuous_toFun := continuous_toFun, hasCompactSupport' := hasCompactSupport' })
    ((fun (f : α →C_c β) ↦ f.toFun)
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1, hasCompactSupport' := hasCompactSupport'_1 })
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, hasCompactSupport' := hasCompactSupport' : α →C_c β } =
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1, hasCompactSupport' := hasCompactSupport'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C_c β
⊢ HasCompactSupport.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
f.hasCompactSupport'

Premises used: CompactlySupportedContinuousMap.hasCompactSupport'
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C_c β
⊢ Eq (α := (a : α) → β) (⇑f.toContinuousMap : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f g : α →C_c β
h : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : C(α, β)
h : HasCompactSupport.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Eq (α := (a : α) → β) (⇑{ toContinuousMap := f, hasCompactSupport' := h : α →C_c β } : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C_c β
f' : α → β
h : f' = (⇑f : (a : α) → β)
rw : Continuous.{u_2, u_3} (X := α) (Y := β) (⇑f : (a : α) → β)
⊢ Continuous f'

Tactic:
rw [h]
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C_c β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Continuous.{u_2, u_3} (X := α) (Y := β) (⇑f : (a : α) → β)

Tactic:
f.continuous_toFun

Premises used: CompactlySupportedContinuousMap.toContinuousMap, ContinuousMap.continuous_toFun
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C_c β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Continuous.{u_2, u_3} (X := α) (Y := β) (⇑f : (a : α) → β)

Tactic:
exact f.continuous_toFun

Premises used: CompactlySupportedContinuousMap.toContinuousMap, ContinuousMap.continuous_toFun
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C_c β
f' : α → β
h : f' = (⇑f : (a : α) → β)
simp_rw : HasCompactSupport.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ HasCompactSupport f'

Tactic:
simp_rw [h]
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C_c β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ HasCompactSupport.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
f.hasCompactSupport'

Premises used: CompactlySupportedContinuousMap.hasCompactSupport'
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C_c β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ HasCompactSupport.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
exact f.hasCompactSupport'

Premises used: CompactlySupportedContinuousMap.hasCompactSupport'
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C_c β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C_c β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : IsEmpty α
f g : α →C_c β
⊢ f = g

Tactic:
ext <| IsEmpty.elim ‹_›

Premises used: IsEmpty.elim, CompactlySupportedContinuousMap.ext
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
g : C(β, γ)
f : α →C_c β
⊢ C(α, γ)

Tactic:
exact if g 0 = 0 then g.comp f else 0

Premises used: ContinuousMap.comp, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
g : C(β, γ)
f : α →C_c β
⊢ C(α, γ)

Tactic:
classical exact if g 0 = 0 then g.comp f else 0

Premises used: ContinuousMap.comp, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
g : C(β, γ)
f : α →C_c β
pos :
  ∀ (hg : Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ)),
    HasCompactSupport (ContinuousMap.toFun (g.comp (↑f : C(α, β))))
neg :
  ∀ (hg : ¬Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ)),
    HasCompactSupport.{u_2, u_5} (α := α) (β := γ) (ContinuousMap.toFun 0)
⊢ HasCompactSupport
    (ContinuousMap.toFun (if Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ) then g.comp (↑f : C(α, β)) else 0))

Tactic:
split_ifs with hg
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
g : C(β, γ)
f : α →C_c β
hg : Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ)
⊢ HasCompactSupport (ContinuousMap.toFun (g.comp (↑f : C(α, β))))

Tactic:
f.hasCompactSupport'.comp_left hg

Premises used: CompactlySupportedContinuousMap.hasCompactSupport', HasCompactSupport.comp_left
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
g : C(β, γ)
f : α →C_c β
hg : Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ)
⊢ HasCompactSupport (ContinuousMap.toFun (g.comp (↑f : C(α, β))))

Tactic:
exact f.hasCompactSupport'.comp_left hg

Premises used: CompactlySupportedContinuousMap.hasCompactSupport', HasCompactSupport.comp_left
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
g : C(β, γ)
f : α →C_c β
hg : ¬Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ)
⊢ HasCompactSupport.{u_2, u_5} (α := α) (β := γ) (ContinuousMap.toFun 0)

Tactic:
.zero

Premises used: HasCompactSupport.zero
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
g : C(β, γ)
f : α →C_c β
hg : ¬Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ)
⊢ HasCompactSupport.{u_2, u_5} (α := α) (β := γ) (ContinuousMap.toFun 0)

Tactic:
exact .zero
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
g : C(β, γ)
hg : Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ)
f : α →C_c β
⊢ toContinuousMap (compLeft g f) = g.comp (↑f : C(α, β))

Tactic:
if_pos hg

Premises used: if_pos, ite
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
g : C(β, γ)
hg : Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ)
f : α →C_c β
⊢ Eq (α := (a : α) → γ) (⇑(compLeft g f) : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β))

Tactic:
simp [compLeft, if_pos hg]

Premises used: if_pos, CompactlySupportedContinuousMap.compLeft
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
g : C(β, γ)
hg : Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ)
f : α →C_c β
a : α
⊢ Eq.{u_5 + 1} (α := γ) ((compLeft g f : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)

Tactic:
simp [coe_compLeft hg f]

Premises used: CompactlySupportedContinuousMap.coe_compLeft
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β_1
inst_2 : Zero β_1
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
β : Type u_6
inst_5 : PseudoMetricSpace β
inst_6 : Zero β
f : α →C_c β
⊢ IsCompact.{u_6} (X := β) (Set.range.{u_6, u_2 + 1} (ι := α) (⇑f : (a : α) → β))

Tactic:
have : IsCompact (Set.range f) := f.hasCompactSupport.isCompact_range f.continuous
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β_1
inst_2 : Zero β_1
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
β : Type u_6
inst_5 : PseudoMetricSpace β
inst_6 : Zero β
f : α →C_c β
this : IsCompact.{u_6} (X := β) (Set.range.{u_6, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
rcases :
  ∀ (C : ℝ)
    (hC :
      ∀ ⦃x : β⦄,
        Membership.mem (γ := Set β) (Set.range.{u_6, u_2 + 1} (ι := α) (⇑f : (a : α) → β)) x →
          ∀ ⦃y : β⦄,
            Membership.mem (γ := Set β) (Set.range.{u_6, u_2 + 1} (ι := α) (⇑f : (a : α) → β)) y → dist x y ≤ C),
    ∃ (C : ℝ), ∀ (x y : α), dist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : α), dist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C

Tactic:
rcases Metric.isBounded_iff.1 this.isBounded with ⟨C, hC⟩

Premises used: IsCompact.isBounded, Metric.isBounded_iff, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β_1
inst_2 : Zero β_1
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
β : Type u_6
inst_5 : PseudoMetricSpace β
inst_6 : Zero β
f : α →C_c β
this : IsCompact.{u_6} (X := β) (Set.range.{u_6, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
C : ℝ
hC :
  ∀ ⦃x : β⦄,
    Membership.mem (γ := Set β) (Set.range.{u_6, u_2 + 1} (ι := α) (⇑f : (a : α) → β)) x →
      ∀ ⦃y : β⦄, Membership.mem (γ := Set β) (Set.range.{u_6, u_2 + 1} (ι := α) (⇑f : (a : α) → β)) y → dist x y ≤ C
⊢ ∀ (x y : α), dist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C

Tactic:
grind
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β_1
inst_2 : Zero β_1
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
β : Type u_6
inst_5 : PseudoMetricSpace β
inst_6 : Zero β
f : α →C_c β
this : IsCompact.{u_6} (X := β) (Set.range.{u_6, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
C : ℝ
hC :
  ∀ ⦃x : β⦄,
    Membership.mem (γ := Set β) (Set.range.{u_6, u_2 + 1} (ι := α) (⇑f : (a : α) → β)) x →
      ∀ ⦃y : β⦄, Membership.mem (γ := Set β) (Set.range.{u_6, u_2 + 1} (ι := α) (⇑f : (a : α) → β)) y → dist x y ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : α), dist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C

Tactic:
exact ⟨C, by grind⟩
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : Zero β
⊢ HasCompactSupport.{u_2, u_3} (α := α) (β := β) (⇑0 : (a : α) → β)

Tactic:
simp [HasCompactSupport, tsupport]

Premises used: tsupport, HasCompactSupport
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
⊢ Eq (α := (a : α) → β) (⇑0 : (a : α) → β) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : Zero β
⊢ Eq.{u_3 + 1} (α := β) ((0 : (a : α) → β) x : β) (0 : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : MulZeroClass β
inst_3 : ContinuousMul β
f g : α →C_c β
⊢ (⇑(f * g) : (a : α) → β) = HMul.hMul (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : MulZeroClass β
inst_3 : ContinuousMul β
f g : α →C_c β
⊢ (f * g : (a : α) → β) x = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : TopologicalSpace γ
inst_4 : SMulZeroClass γ β
inst_5 : ContinuousSMul γ β
F : Type u_5
inst_6 : FunLike F α γ
inst_7 : ContinuousMapClass F α γ
f : F
g : α →C_c β
⊢ Eq (α := (a : α) → β) (⇑(f • g) : (a : α) → β) fun (x : α) ↦
    HSMul.hSMul.{u_4, u_3, u_3} (α := γ) (β := β) ((f : (a : α) → γ) x : γ) ((g : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : TopologicalSpace γ
inst_4 : SMulZeroClass γ β
inst_5 : ContinuousSMul γ β
F : Type u_5
inst_6 : FunLike F α γ
inst_7 : ContinuousMapClass F α γ
f : F
g : α →C_c β
x : α
⊢ (f • g : (a : α) → β) x =
    HSMul.hSMul.{u_4, u_3, u_3} (α := γ) (β := β) ((f : (a : α) → γ) x : γ) ((g : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AddZeroClass β
inst_3 : ContinuousAdd β
f g : α →C_c β
⊢ (⇑(f + g) : (a : α) → β) = HAdd.hAdd (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : AddZeroClass β
inst_3 : ContinuousAdd β
f g : α →C_c β
⊢ (f + g : (a : α) → β) x = HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
R : Type u_5
inst_3 : SMulZeroClass R β
inst_4 : ContinuousConstSMul R β
r : R
f : α →C_c β
⊢ (⇑(r • f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) r (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
R : Type u_5
inst_3 : SMulZeroClass R β
inst_4 : ContinuousConstSMul R β
r : R
f : α →C_c β
x : α
⊢ (r • f : (a : α) → β) x = HSMul.hSMul (β := β) r ((f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AddCommMonoid β
inst_3 : ContinuousAdd β
ι : Type u_5
s : Finset ι
f : ι → α →C_c β
⊢ Eq (α := (a : α) → β) (⇑(∑ i ∈ s, f i) : (a : α) → β) (∑ i ∈ s, (⇑(f i) : (a : α) → β))

Tactic:
map_sum coeFnMonoidHom f s

Premises used: map_sum, CompactlySupportedContinuousMap.coeFnMonoidHom
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AddCommMonoid β
inst_3 : ContinuousAdd β
ι : Type u_5
s : Finset ι
f : ι → α →C_c β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((∑ i ∈ s, f i : (a : α) → β) a : β) (∑ i ∈ s, (f i : (a : α) → β) a : β)

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 : TopologicalSpace β
x : α
inst_2 : AddGroup β
inst_3 : IsTopologicalAddGroup β
f_1 g f : α →C_c β
⊢ HasCompactSupport.{u_2, u_3} (α := α) (β := β) (-(⇑f.toContinuousMap : (a : α) → β))

Tactic:
simpa [HasCompactSupport, tsupport] using f.2

Premises used: tsupport, CompactlySupportedContinuousMap.hasCompactSupport', HasCompactSupport
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AddGroup β
inst_3 : IsTopologicalAddGroup β
f : α →C_c β
⊢ Eq (α := (a : α) → β) (⇑(-f) : (a : α) → β) (-(⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
inst_2 : AddGroup β
inst_3 : IsTopologicalAddGroup β
f : α →C_c β
⊢ Eq.{u_3 + 1} (α := β) ((-f : (a : α) → β) x : β) (-(f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl