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 α
inst_1 : TopologicalSpace β
x : α
inst_2 : AddGroup β
inst_3 : IsTopologicalAddGroup β
f_1 g_1 f g : α →C_c β
⊢ HasCompactSupport (HSub.hSub (α := (a : α) → β) (⇑f.toContinuousMap : (a : α) → β) (⇑g.toContinuousMap : (a : α) → β))

Tactic:
simpa [sub_eq_add_neg] using HasCompactSupport.add f.2 (-g).2

Premises used: sub_eq_add_neg, HasCompactSupport.add, CompactlySupportedContinuousMap.hasCompactSupport', Neg.neg
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AddGroup β
inst_3 : IsTopologicalAddGroup β
f g : α →C_c β
⊢ (⇑(f - g) : (a : α) → β) = HSub.hSub (α := (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 : AddGroup β
inst_3 : IsTopologicalAddGroup β
f g : α →C_c β
⊢ (f - g : (a : α) → β) x = HSub.hSub (α := β) (β := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

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 β
x : α
inst_2 : Zero β
R : Type u_5
inst_3 : Zero R
inst_4 : SMulWithZero R β
inst_5 : SMulWithZero.{u_5, u_3} Rᵐᵒᵖ β
inst_6 : ContinuousConstSMul R β
inst_7 : IsCentralScalar R β
⊢ IsCentralScalar R (α →C_c β)

Tactic:
⟨fun _ _ => ext fun _ => op_smul_eq_smul _ _⟩

Premises used: CompactlySupportedContinuousMap.ext, IsCentralScalar.mk, DFunLike.coe, IsCentralScalar.op_smul_eq_smul
-- 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 : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C_c β
h : ∀ (x : α), Eq.{u_3 + 1} (α := β) (((r • f) • g : (a : α) → β) x : β) ((r • f • g : (a : α) → β) x : β)
⊢ (r • f) • g = r • f • g

Tactic:
ext
-- 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 : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C_c β
x_1 : α
h :
  HMul.hMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
⊢ Eq.{u_3 + 1} (α := β) (((r • f) • g : (a : α) → β) x_1 : β) ((r • f • g : (a : α) → β) x_1 : β)

Tactic:
simp only [smul_eq_mul, coe_mul, coe_smul, Pi.mul_apply, Pi.smul_apply]

Premises used: CompactlySupportedContinuousMap.coe_mul, Pi.mul_apply, CompactlySupportedContinuousMap.coe_smul, smul_eq_mul, Pi.smul_apply
-- 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 : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C_c β
x_1 : α
h :
  HSMul.hSMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
h₁ :
  HSMul.hSMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
h₂ h₃ :
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
⊢ HMul.hMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)

Tactic:
rw [← smul_eq_mul, ← smul_eq_mul, smul_assoc]

Premises used: smul_assoc, smul_eq_mul
-- 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 : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C_c β
h : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((r • f • g : (a : α) → β) x : β) ((f • r • g : (a : α) → β) x : β)
⊢ r • f • g = f • r • g

Tactic:
ext
-- 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 : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C_c β
x_1 : α
h :
  r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
⊢ Eq.{u_3 + 1} (α := β) ((r • f • g : (a : α) → β) x_1 : β) ((f • r • g : (a : α) → β) x_1 : β)

Tactic:
simp only [smul_eq_mul, coe_smul, coe_mul, Pi.smul_apply, Pi.mul_apply]

Premises used: CompactlySupportedContinuousMap.coe_mul, Pi.mul_apply, CompactlySupportedContinuousMap.coe_smul, smul_eq_mul, Pi.smul_apply
-- 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 : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C_c β
x_1 : α
h :
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
h₁ :
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HSMul.hSMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
h₂ h₃ :
  HSMul.hSMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β)) =
    HSMul.hSMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
⊢ r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))

Tactic:
rw [← smul_eq_mul, ← smul_eq_mul, smul_comm]

Premises used: smul_eq_mul, SMulCommClass.smul_comm
-- 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 : AddMonoid β
inst_3 : StarAddMonoid β
inst_4 : ContinuousStar β
f : α →C_c β
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (Function.support.{u_2, u_3} (M := β) fun (x : α) ↦ star ((f : (a : α) → β) x)) x ↔
      Membership.mem (γ := Set α) (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β)) x
⊢ Eq.{u_2 + 1} (α := Set α) (Function.support.{u_2, u_3} (M := β) fun (x : α) ↦ star ((f : (a : α) → β) x))
    (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β))

Tactic:
ext x
-- 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 : AddMonoid β
inst_3 : StarAddMonoid β
inst_4 : ContinuousStar β
f : α →C_c β
x : α
⊢ Membership.mem (γ := Set α) (Function.support.{u_2, u_3} (M := β) fun (x : α) ↦ star ((f : (a : α) → β) x)) x ↔
    Membership.mem (γ := Set α) (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β)) x

Tactic:
simp only [Function.mem_support, ne_eq, star_eq_zero]

Premises used: star_eq_zero, ne_eq, Function.mem_support
-- 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 : AddMonoid β
inst_3 : StarAddMonoid β
inst_4 : ContinuousStar β
f : α →C_c β
⊢ Eq.{u_2 + 1} (α := Set α) (Function.support.{u_2, u_3} (M := β) fun (x : α) ↦ star ((f : (a : α) → β) x))
    (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β))

Tactic:
have support_star : (Function.support fun (x : α) => star (f x)) = Function.support f := by
          ext x
          simp only [Function.mem_support, ne_eq, star_eq_zero]
-- 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 : AddMonoid β
inst_3 : StarAddMonoid β
inst_4 : ContinuousStar β
f : α →C_c β
support_star :
  Eq.{u_2 + 1} (α := Set α) (Function.support.{u_2, u_3} (M := β) fun (x : α) ↦ star ((f : (a : α) → β) x))
    (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β))
rw : IsCompact.{u_2} (X := α) (closure (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β)))
⊢ IsCompact.{u_2} (X := α) (closure (Function.support.{u_2, u_3} (M := β) fun (x : α) ↦ star ((f : (a : α) → β) x)))

Tactic:
rw [support_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 : AddMonoid β
inst_3 : StarAddMonoid β
inst_4 : ContinuousStar β
f : α →C_c β
support_star :
  Eq.{u_2 + 1} (α := Set α) (Function.support.{u_2, u_3} (M := β) fun (x : α) ↦ star ((f : (a : α) → β) x))
    (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β))
⊢ IsCompact.{u_2} (X := α) (closure (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β)))

Tactic:
f.2

Premises used: tsupport, CompactlySupportedContinuousMap.hasCompactSupport', 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 : AddMonoid β
inst_3 : StarAddMonoid β
inst_4 : ContinuousStar β
f : α →C_c β
support_star :
  Eq.{u_2 + 1} (α := Set α) (Function.support.{u_2, u_3} (M := β) fun (x : α) ↦ star ((f : (a : α) → β) x))
    (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β))
⊢ IsCompact.{u_2} (X := α) (closure (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β)))

Tactic:
exact f.2

Premises used: CompactlySupportedContinuousMap.hasCompactSupport'
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AddMonoid β
inst_3 : StarAddMonoid β
inst_4 : ContinuousStar β
f : α →C_c β
⊢ Eq (α := (a : α) → β) (⇑(star f) : (a : α) → β) (star (⇑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 : AddMonoid β
inst_3 : StarAddMonoid β
inst_4 : ContinuousStar β
f : α →C_c β
x : α
⊢ Eq.{u_3 + 1} (α := β) ((star f : (a : α) → β) x : β) (star ((f : (a : α) → β) x) : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
β : Type u_5
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : PartialOrder β
f g : α →C_c β
⊢ f ≤ g ↔ ∀ (a : α), LE.le.{u_5} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)

Tactic:
Pi.le_def

Premises used: Pi.le_def
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
inst : TopologicalSpace α
β : Type u_5
inst_1 : TopologicalSpace β
inst_2 : Zero β
inst_3 : PartialOrder β
f g : α →C_c β
⊢ f < g ↔
    (∀ (a : α), LE.le.{u_5} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)) ∧
      ∃ (a : α), LT.lt.{u_5} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)

Tactic:
Pi.lt_def

Premises used: Pi.lt_def
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SemilatticeSup β
inst_2 : Zero β
inst_3 : TopologicalSpace β
inst_4 : ContinuousSup β
f g : α →C_c β
⊢ Eq (α := (a : α) → β) (⇑(f ⊔ g) : (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 : SemilatticeSup β
inst_2 : Zero β
inst_3 : TopologicalSpace β
inst_4 : ContinuousSup β
f g : α →C_c β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((f ⊔ g : (a : α) → β) a : β) ((f : (a : α) → β) a ⊔ (g : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SemilatticeSup β
inst_2 : Zero β
inst_3 : TopologicalSpace β
inst_4 : ContinuousSup β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((s.sup' H f : (a : α) → β) a : β) (s.sup' H fun (i : ι) ↦ (f i : (a : α) → β) a : β)

Tactic:
Finset.comp_sup'_eq_sup'_comp H (fun g : C_c(α, β) ↦ g a) fun _ _ ↦ rfl

Premises used: Finset.comp_sup'_eq_sup'_comp, DFunLike.coe, rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SemilatticeSup β
inst_2 : Zero β
inst_3 : TopologicalSpace β
inst_4 : ContinuousSup β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
h :
  ∀ (x : α),
    Eq.{u_3 + 1} (α := β) ((s.sup' H f : (a : α) → β) x : β) (s.sup' H (fun (i : ι) ↦ (⇑(f i) : (a : α) → β)) x : β)
⊢ Eq (α := (a : α) → β) (⇑(s.sup' H f) : (a : α) → β) (s.sup' H fun (i : ι) ↦ (⇑(f i) : (a : α) → β))

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SemilatticeSup β
inst_2 : Zero β
inst_3 : TopologicalSpace β
inst_4 : ContinuousSup β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
x : α
⊢ Eq.{u_3 + 1} (α := β) ((s.sup' H f : (a : α) → β) x : β) (s.sup' H (fun (i : ι) ↦ (⇑(f i) : (a : α) → β)) x : β)

Tactic:
simp [finsetSup'_apply]

Premises used: CompactlySupportedContinuousMap.finsetSup'_apply
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SemilatticeInf β
inst_2 : Zero β
inst_3 : TopologicalSpace β
inst_4 : ContinuousInf β
f g : α →C_c β
⊢ Eq (α := (a : α) → β) (⇑(f ⊓ g) : (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 : SemilatticeInf β
inst_2 : Zero β
inst_3 : TopologicalSpace β
inst_4 : ContinuousInf β
f g : α →C_c β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((f ⊓ g : (a : α) → β) a : β) ((f : (a : α) → β) a ⊓ (g : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SemilatticeInf β
inst_2 : Zero β
inst_3 : TopologicalSpace β
inst_4 : ContinuousInf β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
a : α
⊢ Eq.{u_3 + 1} (α := β) ((s.inf' H f : (a : α) → β) a : β) (s.inf' H fun (i : ι) ↦ (f i : (a : α) → β) a : β)

Tactic:
Finset.comp_inf'_eq_inf'_comp H (fun g : C_c(α, β) ↦ g a) fun _ _ ↦ rfl

Premises used: Finset.comp_inf'_eq_inf'_comp, DFunLike.coe, rfl
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SemilatticeInf β
inst_2 : Zero β
inst_3 : TopologicalSpace β
inst_4 : ContinuousInf β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
h :
  ∀ (x : α),
    Eq.{u_3 + 1} (α := β) ((s.inf' H f : (a : α) → β) x : β) (s.inf' H (fun (i : ι) ↦ (⇑(f i) : (a : α) → β)) x : β)
⊢ Eq (α := (a : α) → β) (⇑(s.inf' H f) : (a : α) → β) (s.inf' H fun (i : ι) ↦ (⇑(f i) : (a : α) → β))

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.CompactlySupported
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SemilatticeInf β
inst_2 : Zero β
inst_3 : TopologicalSpace β
inst_4 : ContinuousInf β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
x : α
⊢ Eq.{u_3 + 1} (α := β) ((s.inf' H f : (a : α) → β) x : β) (s.inf' H (fun (i : ι) ↦ (⇑(f i) : (a : α) → β)) x : β)

Tactic:
simp [finsetInf'_apply]

Premises used: CompactlySupportedContinuousMap.finsetInf'_apply
-- 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 : PartialOrder β
inst_3 : MulZeroClass β
inst_4 : ContinuousMul β
inst_5 : MulLeftMono β
⊢ MulLeftMono (α →C_c β)

Tactic:
⟨fun _ _ _ hg₁₂ x => mul_le_mul_right (hg₁₂ x) _⟩

Premises used: CovariantClass.mk, mul_le_mul_right, toContinuousMap, 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 : TopologicalSpace β
inst_2 : PartialOrder β
inst_3 : MulZeroClass β
inst_4 : ContinuousMul β
inst_5 : MulRightMono β
⊢ MulRightMono (α →C_c β)

Tactic:
⟨fun _ _ _ hg₁₂ x => mul_le_mul_left (hg₁₂ x) _⟩

Premises used: CovariantClass.mk, toContinuousMap, mul_le_mul_left, 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 : TopologicalSpace β
inst_2 : PartialOrder β
inst_3 : AddZeroClass β
inst_4 : ContinuousAdd β
inst_5 : AddLeftMono β
⊢ AddLeftMono (α →C_c β)

Tactic:
⟨fun _ _ _ hg₁₂ x => add_le_add_right (hg₁₂ x) _⟩

Premises used: CovariantClass.mk, add_le_add_right, toContinuousMap, 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 : TopologicalSpace β
inst_2 : PartialOrder β
inst_3 : AddZeroClass β
inst_4 : ContinuousAdd β
inst_5 : AddRightMono β
⊢ AddRightMono (α →C_c β)

Tactic:
⟨fun _ _ _ hg₁₂ x => add_le_add_left (hg₁₂ x) _⟩

Premises used: CovariantClass.mk, add_le_add_left, toContinuousMap, DFunLike.coe
-- 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 γ
apply :
  Subset.{u_3} (α := Set β)
    (tsupport.{u_3, u_5} (α := δ)
      (Function.comp.{u_3 + 1, u_4 + 1, u_5 + 1} (β := γ) (⇑f : (a : γ) → δ) (⇑g : (a : β) → γ)))
    ((⇑g : (a : β) → γ) ⁻¹' tsupport f.toFun)
⊢ HasCompactSupport (ContinuousMap.toFun (ContinuousMap.comp (↑f : C(γ, δ)) (↑g : C(β, γ))))

Tactic:
apply IsCompact.of_isClosed_subset (g.isCompact_preimage_of_isClosed f.2 (isClosed_tsupport _))
      (isClosed_tsupport (f ∘ g))

Premises used: CocompactMap.isCompact_preimage_of_isClosed, Function.comp, isClosed_tsupport, IsCompact.of_isClosed_subset, CompactlySupportedContinuousMap.hasCompactSupport', DFunLike.coe
-- 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 :
  Membership.mem (γ := Set β)
    (tsupport.{u_3, u_5} (α := δ)
      (Function.comp.{u_3 + 1, u_4 + 1, u_5 + 1} (β := γ) (⇑f : (a : γ) → δ) (⇑g : (a : β) → γ)))
    x
rw :
  ∀ (o : Set γ),
    IsOpen o → Membership.mem (α := γ) o ((g : (a : β) → γ) x : γ) → (o ∩ Function.support f.toFun).Nonempty
⊢ Membership.mem (γ := Set β) ((⇑g : (a : β) → γ) ⁻¹' tsupport f.toFun) x

Tactic:
rw [tsupport, Set.mem_preimage, _root_.mem_closure_iff]

Premises used: mem_closure_iff, tsupport, Set.mem_preimage
-- 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 :
  Membership.mem (γ := Set β)
    (tsupport.{u_3, u_5} (α := δ)
      (Function.comp.{u_3 + 1, u_4 + 1, u_5 + 1} (β := γ) (⇑f : (a : γ) → δ) (⇑g : (a : β) → γ)))
    x
o : Set γ
ho : IsOpen o
hgxo : Membership.mem (α := γ) o ((g : (a : β) → γ) x : γ)
rw :
  ∀
    (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
⊢ (o ∩ Function.support f.toFun).Nonempty

Tactic:
rw [tsupport, _root_.mem_closure_iff] at hx

Premises used: mem_closure_iff, tsupport
-- 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 : γ)
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
⊢ (o ∩ Function.support f.toFun).Nonempty

Tactic:
obtain ⟨y, hy⟩ := hx (g ⁻¹' o) (IsOpen.preimage g.1.2 ho) hgxo

Premises used: Set.preimage, ContinuousMap.continuous_toFun, CocompactMap.toContinuousMap, IsOpen.preimage, DFunLike.coe
-- 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:
⟨g y, hy⟩

Premises used: Set.Nonempty, Exists.intro, DFunLike.coe