awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.LocallyConstant
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
R : Type u_3
inst_2 : CommSemiring R
inst_3 : Semiring Y
inst_4 : Algebra R Y
inst_5 : IsTopologicalSemiring Y
r : R
x : X
⊢ Eq.{u_2 + 1} (α := Y)
    (((↑((algebraMap R (LocallyConstant X Y) : (a : R) → LocallyConstant X Y) r) : C(X, Y)) : (a : X) → Y) x : Y)
    ((((algebraMap R C(X, Y) : (a : R) → C(X, Y)) r : C(X, Y)) : (a : X) → Y) x : Y)

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Topology.ContinuousMap.LocallyConstant
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
R : Type u_3
inst_2 : CommSemiring R
inst_3 : Semiring Y
inst_4 : Algebra R Y
inst_5 : IsTopologicalSemiring Y
⊢ Eq (α := LocallyConstant X Y →ₗ[R] C(X, Y)) (AlgHom.toLinearMap (toContinuousMapAlgHom R))
    (toContinuousMapLinearMap R)

Tactic:
rfl

Premises used: AlgHom.toLinearMap, LocallyConstant.toContinuousMap, rfl, LocallyConstant.toContinuousMapLinearMap
-- Module: Mathlib.Topology.ContinuousMap.LocallyConstant
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
R : Type u_3
inst_2 : CommSemiring R
inst_3 : TotallySeparatedSpace X
inst_4 : Semiring Y
inst_5 : Algebra R Y
inst_6 : IsTopologicalSemiring Y
inst_7 : Nontrivial Y
x x_1 : X
hxy : x ≠ x_1
w : Set X
hU : IsClopen w
left : x ∈ w
right : x_1 ∈ wᶜ
⊢ Membership.mem (γ := Set (X → Y))
      ((fun (f : C(X, Y)) ↦ (⇑f : (a : X) → Y)) '' (↑(AlgHom.range (toContinuousMapAlgHom R)) : Set C(X, Y)))
      (⇑(charFn Y (U := w) hU) : (a : X) → Y) ∧
    Ne.{u_2 + 1} (α := Y) ((charFn Y (U := w) hU : (a : X) → Y) x : Y) ((charFn Y (U := w) hU : (a : X) → Y) x_1 : Y)

Tactic:
simp_all [charFn]

Premises used: LocallyConstant.charFn
-- Module: Mathlib.Topology.ContinuousMap.LocallyConvex
Goal:
X : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : TopologicalSpace X
inst_1 : Semiring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : LocallyConvexSpace 𝕜 E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
K : Set X
U : Set E
hK : IsCompact (K, U).1
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) (K, U).2
hUc : Convex 𝕜 (K, U).2
f : C(X, E)
hf : Membership.mem (γ := Set C(X, E)) {f : C(X, E) | Set.MapsTo (⇑f : (a : X) → E) (K, U).1 (id (K, U).2)} f
g : C(X, E)
hg : Membership.mem (γ := Set C(X, E)) {f : C(X, E) | Set.MapsTo (⇑f : (a : X) → E) (K, U).1 (id (K, U).2)} g
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x : X
hx : x ∈ (K, U).1
⊢ Membership.mem (α := E) (id (K, U).2) ((a • f + b • g : (a : X) → E) x : E)

Tactic:
hUc (hf hx) (hg hx) ha hb hab

Premises used: Set.Mem
-- Module: Mathlib.Topology.ContinuousMap.LocallyConvex
Goal:
X : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : TopologicalSpace X
inst_1 : Semiring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : LocallyConvexSpace 𝕜 E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousConstSMul 𝕜 E
K : Set X
U : Set E
hK : IsCompact (K, U).1
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) (K, U).2
hUc : Convex 𝕜 (K, U).2
f : C(X, E)
hf : Membership.mem (γ := Set C(X, E)) {f : C(X, E) | Set.MapsTo (⇑f : (a : X) → E) (K, U).1 (id (K, U).2)} f
g : C(X, E)
hg : Membership.mem (γ := Set C(X, E)) {f : C(X, E) | Set.MapsTo (⇑f : (a : X) → E) (K, U).1 (id (K, U).2)} g
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x : X
hx : x ∈ (K, U).1
⊢ Membership.mem (α := E) (id (K, U).2) ((a • f + b • g : (a : X) → E) x : E)

Tactic:
exact hUc (hf hx) (hg hx) ha hb hab
-- Module: Mathlib.Topology.ContinuousMap.Ordered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : PartialOrder β
f g : C(α, β)
h : Eq (α := α → β) ((fun (f : C(α, β)) ↦ f.toFun) f) ((fun (f : C(α, β)) ↦ f.toFun) g)
⊢ f = g

Tactic:
aesop
-- Module: Mathlib.Topology.ContinuousMap.Ordered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : PartialOrder β
f g : C(α, β)
⊢ f ≤ g ↔ ∀ (a : α), LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)

Tactic:
Pi.le_def

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

Tactic:
Pi.lt_def

Premises used: Pi.lt_def
-- Module: Mathlib.Topology.ContinuousMap.Ordered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : C(α, β)
⊢ Eq (α := (a : α) → β) (⇑(f ⊔ g) : (a : α) → β) ((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Ordered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
f g : C(α, β)
a : α
⊢ Eq.{u_2 + 1} (α := β) ((f ⊔ g : (a : α) → β) a : β) ((f : (a : α) → β) a ⊔ (g : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Ordered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
a : α
⊢ Eq.{u_2 + 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(α, β) ↦ g a) fun _ _ ↦ rfl

Premises used: Finset.comp_sup'_eq_sup'_comp, DFunLike.coe, rfl
-- Module: Mathlib.Topology.ContinuousMap.Ordered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
h :
  ∀ (x : α),
    Eq.{u_2 + 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.Ordered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
x : α
⊢ Eq.{u_2 + 1} (α := β) ((s.sup' H f : (a : α) → β) x : β) (s.sup' H (fun (i : ι) ↦ (⇑(f i) : (a : α) → β)) x : β)

Tactic:
simp [sup'_apply]

Premises used: ContinuousMap.sup'_apply
-- Module: Mathlib.Topology.ContinuousMap.Ordered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : C(α, β)
⊢ Eq (α := (a : α) → β) (⇑(f ⊓ g) : (a : α) → β) ((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Ordered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
f g : C(α, β)
a : α
⊢ Eq.{u_2 + 1} (α := β) ((f ⊓ g : (a : α) → β) a : β) ((f : (a : α) → β) a ⊓ (g : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Ordered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
a : α
⊢ Eq.{u_2 + 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(α, β) ↦ g a) fun _ _ ↦ rfl

Premises used: Finset.comp_inf'_eq_inf'_comp, DFunLike.coe, rfl
-- Module: Mathlib.Topology.ContinuousMap.Ordered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
h :
  ∀ (x : α),
    Eq.{u_2 + 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.Ordered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SemilatticeInf β
inst_3 : ContinuousInf β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
x : α
⊢ Eq.{u_2 + 1} (α := β) ((s.inf' H f : (a : α) → β) x : β) (s.inf' H (fun (i : ι) ↦ (⇑(f i) : (a : α) → β)) x : β)

Tactic:
simp [inf'_apply]

Premises used: ContinuousMap.inf'_apply
-- Module: Mathlib.Topology.ContinuousMap.Ordered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : LinearOrder α
inst_3 : OrderTopology α
a b : α
h : a ≤ b
f : ContinuousMap.{u_1, u_2} (↑(Set.Icc a b) : Type u_1) β
⊢ Eq (α := (a : α) → β) (⇑(IccExtend h f) : (a : α) → β) (Set.IccExtend h (⇑f : (a : (↑(Set.Icc a b) : Type u_1)) → β))

Tactic:
rfl

Premises used: Set.IccExtend, rfl
-- Module: Mathlib.Topology.ContinuousMap.Periodic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : AddCommGroup X
inst_3 : ContinuousAdd X
inst_4 : AddCommMonoid Y
inst_5 : ContinuousAdd Y
inst_6 : T2Space Y
f : C(X, Y)
p x : X
pos :
  ∀ (h : Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))),
    Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
      ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) x : Y)
neg :
  ∀ (h : ¬Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))),
    Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
      ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) x : Y)
⊢ Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
    ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) x : Y)

Tactic:
by_cases h : Summable fun n : ℤ => f.comp (ContinuousMap.addRight (n • p))

Premises used: ContinuousMap.comp, HSMul.hSMul, Summable, SummationFilter.unconditional, ContinuousMap.addRight
-- Module: Mathlib.Topology.ContinuousMap.Periodic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : AddCommGroup X
inst_3 : ContinuousAdd X
inst_4 : AddCommMonoid Y
inst_5 : ContinuousAdd Y
inst_6 : T2Space Y
f : C(X, Y)
p x : X
h : Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ Eq.{u_2 + 1} (α := Y)
    ((fun (f : C(X, Y)) ↦ ((f : (a : X) → Y) x : Y))
      (∑' (c : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (α := ℤ) ((Equiv.addRight 1 : (a : ℤ) → ℤ) c : ℤ) p))))
    ((fun (f : C(X, Y)) ↦ ((f : (a : X) → Y) x : Y)) (∑' (b : ℤ), f.comp (ContinuousMap.addRight (b • p))))

Tactic:
congr_arg (fun f : C(X, Y) => f x) ((Equiv.addRight (1 : ℤ)).tsum_eq _)

Premises used: Equiv.addRight, Equiv.tsum_eq, congr_arg, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Periodic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : AddCommGroup X
inst_3 : ContinuousAdd X
inst_4 : AddCommMonoid Y
inst_5 : ContinuousAdd Y
inst_6 : T2Space Y
f : C(X, Y)
p x : X
h : Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))
h₁ :
  Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
    ((∑' (c : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (α := ℤ) ((Equiv.addRight 1 : (a : ℤ) → ℤ) c : ℤ) p)) :
          (a : X) → Y)
        x :
      Y)
⊢ Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
    ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) x : Y)

Tactic:
convert! congr_arg (fun f : C(X, Y) => f x) ((Equiv.addRight (1 : ℤ)).tsum_eq _) using 1

Premises used: Equiv.addRight, Equiv.tsum_eq, congr_arg, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Periodic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : AddCommGroup X
inst_3 : ContinuousAdd X
inst_4 : AddCommMonoid Y
inst_5 : ContinuousAdd Y
inst_6 : T2Space Y
f : C(X, Y)
p x : X
h : Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ Summable (α := C(X, Y)) fun (c : ℤ) ↦
    f.comp (ContinuousMap.addRight (HSMul.hSMul (α := ℤ) ((Equiv.addRight 1 : (a : ℤ) → ℤ) c : ℤ) p))

Tactic:
have : Summable fun (c : ℤ) => f.comp (ContinuousMap.addRight (Equiv.addRight 1 c • p)) :=
      (Equiv.addRight (1 : ℤ)).summable_iff.mpr h
-- Module: Mathlib.Topology.ContinuousMap.Periodic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : AddCommGroup X
inst_3 : ContinuousAdd X
inst_4 : AddCommMonoid Y
inst_5 : ContinuousAdd Y
inst_6 : T2Space Y
f : C(X, Y)
p x : X
h : Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))
this :
  Summable (α := C(X, Y)) fun (c : ℤ) ↦
    f.comp (ContinuousMap.addRight (HSMul.hSMul (α := ℤ) ((Equiv.addRight 1 : (a : ℤ) → ℤ) c : ℤ) p))
h₁ :
  Eq.{u_2 + 1} (α := Y) (∑' (i : ℤ), (f.comp (ContinuousMap.addRight (i • p)) : (a : X) → Y) (x + p))
    (∑' (i : ℤ),
      (f.comp (ContinuousMap.addRight (HSMul.hSMul (α := ℤ) ((Equiv.addRight 1 : (a : ℤ) → ℤ) i : ℤ) p)) : (a : X) → Y)
        x)
⊢ Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
    ((∑' (c : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (α := ℤ) ((Equiv.addRight 1 : (a : ℤ) → ℤ) c : ℤ) p)) :
          (a : X) → Y)
        x :
      Y)

Tactic:
simp_rw [← tsum_apply h, ← tsum_apply this]

Premises used: ContinuousMap.tsum_apply
-- Module: Mathlib.Topology.ContinuousMap.Periodic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : AddCommGroup X
inst_3 : ContinuousAdd X
inst_4 : AddCommMonoid Y
inst_5 : ContinuousAdd Y
inst_6 : T2Space Y
f : C(X, Y)
p x : X
h : Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))
this :
  Summable (α := C(X, Y)) fun (c : ℤ) ↦
    f.comp (ContinuousMap.addRight (HSMul.hSMul (α := ℤ) ((Equiv.addRight 1 : (a : ℤ) → ℤ) c : ℤ) p))
⊢ Eq.{u_2 + 1} (α := Y) (∑' (i : ℤ), (f.comp (ContinuousMap.addRight (i • p)) : (a : X) → Y) (x + p))
    (∑' (i : ℤ),
      (f.comp (ContinuousMap.addRight (HSMul.hSMul (α := ℤ) ((Equiv.addRight 1 : (a : ℤ) → ℤ) i : ℤ) p)) : (a : X) → Y)
        x)

Tactic:
simp [Equiv.coe_addRight, comp_apply, add_one_zsmul, add_comm (_ • p) p, ← add_assoc]

Premises used: add_assoc, ContinuousMap.comp_apply, Equiv.coe_addRight, add_one_zsmul, add_comm, HSMul.hSMul
-- Module: Mathlib.Topology.ContinuousMap.Periodic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : AddCommGroup X
inst_3 : ContinuousAdd X
inst_4 : AddCommMonoid Y
inst_5 : ContinuousAdd Y
inst_6 : T2Space Y
f : C(X, Y)
p x : X
h : ¬Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))
neg : Eq.{u_2 + 1} (α := Y) ((0 : (a : X) → Y) (x + p) : Y) ((0 : (a : X) → Y) x : Y)
⊢ Eq.{u_2 + 1} (α := Y) ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) (x + p) : Y)
    ((∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)) : (a : X) → Y) x : Y)

Tactic:
rw [tsum_eq_zero_of_not_summable h]

Premises used: tsum_eq_zero_of_not_summable
-- Module: Mathlib.Topology.ContinuousMap.Periodic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : AddCommGroup X
inst_3 : ContinuousAdd X
inst_4 : AddCommMonoid Y
inst_5 : ContinuousAdd Y
inst_6 : T2Space Y
f : C(X, Y)
p x : X
h : ¬Summable (α := C(X, Y)) fun (n : ℤ) ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ Eq.{u_2 + 1} (α := Y) ((0 : (a : X) → Y) (x + p) : Y) ((0 : (a : X) → Y) x : Y)

Tactic:
simp only [coe_zero, Pi.zero_apply]

Premises used: Pi.zero_apply, ContinuousMap.coe_zero
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
p : R[X]
⊢ Continuous (Y := R) fun (x : R) ↦ eval x p

Tactic:
fun_prop
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
h : ∀ (a : R), Eq (α := R) ((toContinuousMap X : (a : R) → R) a : R) ((ContinuousMap.id R : (a : R) → R) a : R)
⊢ Eq (α := C(R, R)) (toContinuousMap X) (ContinuousMap.id R)

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
a : R
⊢ Eq (α := R) ((toContinuousMap X : (a : R) → R) a : R) ((ContinuousMap.id R : (a : R) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
p : R[X]
X : Set R
⊢ Continuous (Y := R) fun (x : (↑X : Type u_1)) ↦ (p.toContinuousMap : (a : R) → R) (↑x : R)

Tactic:
fun_prop
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
h :
  ∀ (a : (↑s : Type u_1)),
    Eq (α := R) ((toContinuousMapOn X s : (a : (↑s : Type u_1)) → R) a : R)
      ((restrict s (ContinuousMap.id R) : (a : (↑s : Type u_1)) → R) a : R)
⊢ Eq (α := C((↑s : Type u_1), R)) (toContinuousMapOn X s) (restrict s (ContinuousMap.id R))

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
s : Set R
a : (↑s : Type u_1)
⊢ Eq (α := R) ((toContinuousMapOn X s : (a : (↑s : Type u_1)) → R) a : R)
    ((restrict s (ContinuousMap.id R) : (a : (↑s : Type u_1)) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
⊢ Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) g : C(α, R)) : (a : α) → R) x : R)
    (eval ((f : (a : α) → R) x) g : R)

Tactic:
Polynomial.induction_on' g ?_ ?_

Premises used: Polynomial.induction_on'
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
refine_1 :
  ∀ (p q : R[X]),
    Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) p : C(α, R)) : (a : α) → R) x : R)
        (eval ((f : (a : α) → R) x) p : R) →
      Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) q : C(α, R)) : (a : α) → R) x : R)
          (eval ((f : (a : α) → R) x) q : R) →
        Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) (p + q) : C(α, R)) : (a : α) → R) x : R)
          (eval ((f : (a : α) → R) x) (p + q) : R)
refine_2 :
  ∀ (n : ℕ) (a : R),
    Eq.{u_1 + 1} (α := R)
      ((((aeval f : (a : R[X]) → C(α, R)) ((monomial n : (a : R) → R[X]) a) : C(α, R)) : (a : α) → R) x : R)
      (eval ((f : (a : α) → R) x) ((monomial n : (a : R) → R[X]) a) : R)
⊢ Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) g : C(α, R)) : (a : α) → R) x : R)
    (eval ((f : (a : α) → R) x) g : R)

Tactic:
refine Polynomial.induction_on' g ?_ ?_
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
p q : R[X]
hp :
  Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) p : C(α, R)) : (a : α) → R) x : R)
    (eval ((f : (a : α) → R) x) p : R)
hq :
  Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) q : C(α, R)) : (a : α) → R) x : R)
    (eval ((f : (a : α) → R) x) q : R)
⊢ Eq.{u_1 + 1} (α := R) ((((aeval f : (a : R[X]) → C(α, R)) (p + q) : C(α, R)) : (a : α) → R) x : R)
    (eval ((f : (a : α) → R) x) (p + q) : R)

Tactic:
simp [hp, hq]
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
g : R[X]
f : C(α, R)
x : α
n : ℕ
a : R
⊢ Eq.{u_1 + 1} (α := R)
    ((((aeval f : (a : R[X]) → C(α, R)) ((monomial n : (a : R) → R[X]) a) : C(α, R)) : (a : α) → R) x : R)
    (eval ((f : (a : α) → R) x) ((monomial n : (a : R) → R[X]) a) : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
h : ∀ (a : R), Eq (α := R) ((toContinuousMap 1 : (a : R) → R) a : R) ((1 : (a : R) → R) a : R)
⊢ Eq.{u_1 + 1} (α := C(R, R)) (toContinuousMap 1) 1

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
a : R
⊢ Eq (α := R) ((toContinuousMap 1 : (a : R) → R) a : R) ((1 : (a : R) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
x x_1 : R[X]
h :
  ∀ (a : R),
    Eq (α := R) (((x * x_1).toContinuousMap : (a : R) → R) a : R)
      ((HMul.hMul (α := C(R, R)) x.toContinuousMap x_1.toContinuousMap : (a : R) → R) a : R)
⊢ (x * x_1).toContinuousMap = HMul.hMul (α := C(R, R)) x.toContinuousMap x_1.toContinuousMap

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
x x_1 : R[X]
a : R
⊢ Eq (α := R) (((x * x_1).toContinuousMap : (a : R) → R) a : R)
    ((HMul.hMul (α := C(R, R)) x.toContinuousMap x_1.toContinuousMap : (a : R) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
h : ∀ (a : R), Eq (α := R) ((toContinuousMap 0 : (a : R) → R) a : R) ((0 : (a : R) → R) a : R)
⊢ Eq.{u_1 + 1} (α := C(R, R)) (toContinuousMap 0) 0

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
a : R
⊢ Eq (α := R) ((toContinuousMap 0 : (a : R) → R) a : R) ((0 : (a : R) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
x x_1 : R[X]
h :
  ∀ (a : R),
    Eq (α := R) (((x + x_1).toContinuousMap : (a : R) → R) a : R)
      ((HAdd.hAdd (α := C(R, R)) x.toContinuousMap x_1.toContinuousMap : (a : R) → R) a : R)
⊢ (x + x_1).toContinuousMap = HAdd.hAdd (α := C(R, R)) x.toContinuousMap x_1.toContinuousMap

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
x x_1 : R[X]
a : R
⊢ Eq (α := R) (((x + x_1).toContinuousMap : (a : R) → R) a : R)
    ((HAdd.hAdd (α := C(R, R)) x.toContinuousMap x_1.toContinuousMap : (a : R) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
x : R
h :
  ∀ (a : R),
    Eq (α := R) ((toContinuousMap ((algebraMap R R[X] : (a : R) → R[X]) x) : (a : R) → R) a : R)
      ((((algebraMap R C(R, R) : (a : R) → C(R, R)) x : C(R, R)) : (a : R) → R) a : R)
⊢ Eq.{u_1 + 1} (α := C(R, R)) (toContinuousMap ((algebraMap R R[X] : (a : R) → R[X]) x))
    ((algebraMap R C(R, R) : (a : R) → C(R, R)) x)

Tactic:
ext