awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : IsTopologicalSemiring A
k : R
a : α
rw : (HSMul.hSMul (β := C(α, A)) k 1 : (a : α) → A) a = HSMul.hSMul (β := A) k 1
⊢ (((algebraMap R C(α, A) : (a : R) → C(α, A)) k : C(α, A)) : (a : α) → A) a = HSMul.hSMul (β := A) k 1

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
A : Type u_3
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : IsTopologicalSemiring A
k : R
a : α
⊢ (HSMul.hSMul (β := C(α, A)) k 1 : (a : α) → A) a = HSMul.hSMul (β := A) k 1

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
pos : ∀ (n : x = y), ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y
neg : ∀ (n : ¬x = y), ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y
⊢ ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y

Tactic:
by_cases n : x = y
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : x = y
pos : ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) x = v x
⊢ ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y

Tactic:
subst n
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x : α
⊢ ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) x = v x

Tactic:
⟨_, (v x • (1 : s) : s).prop, mul_one _, mul_one _⟩

Premises used: Subtype.prop, And.intro, Exists.intro, HSMul.hSMul, mul_one, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x : α
⊢ ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) x = v x

Tactic:
exact ⟨_, (v x • (1 : s) : s).prop, mul_one _, mul_one _⟩
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
neg :
  ∀ (f : C(α, 𝕜)) (hf : f ∈ (↑s : Set C(α, 𝕜)))
    (hxy :
      Ne.{u_5 + 1} (α := 𝕜) ((fun (f : C(α, 𝕜)) ↦ ((⇑f : (a : α) → 𝕜) : (a : α) → 𝕜)) f x)
        ((fun (f : C(α, 𝕜)) ↦ ((⇑f : (a : α) → 𝕜) : (a : α) → 𝕜)) f y)),
    ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y
⊢ ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y

Tactic:
obtain ⟨_, ⟨f, hf, rfl⟩, hxy⟩ := h n

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ (↑s : Set C(α, 𝕜))
hxy :
  Ne.{u_5 + 1} (α := 𝕜) ((fun (f : C(α, 𝕜)) ↦ ((⇑f : (a : α) → 𝕜) : (a : α) → 𝕜)) f x)
    ((fun (f : C(α, 𝕜)) ↦ ((⇑f : (a : α) → 𝕜) : (a : α) → 𝕜)) f y)
⊢ HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) ((f : (a : α) → 𝕜) y : 𝕜) ≠ 0

Tactic:
replace hxy : f x - f y ≠ 0 := sub_ne_zero_of_ne hxy
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ (↑s : Set C(α, 𝕜))
hxy : HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) ((f : (a : α) → 𝕜) y : 𝕜) ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : ↥s :=
  HAdd.hAdd (β := ↥s)
    (((b - a) * (HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) ((f : (a : α) → 𝕜) y : 𝕜))⁻¹) •
      HSub.hSub (α := ↥s) ((algebraMap 𝕜 ↥s : (a : 𝕜) → ↥s) ((f : (a : α) → 𝕜) x) : ↥s)
        (Subtype.mk (p := fun (x : C(α, 𝕜)) ↦ x ∈ s) f hf))
    ((algebraMap 𝕜 ↥s : (a : 𝕜) → ↥s) a : ↥s)
⊢ ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y

Tactic:
⟨f', f'.prop, ?_, ?_⟩

Premises used: Subtype.prop, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ (↑s : Set C(α, 𝕜))
hxy : HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) ((f : (a : α) → 𝕜) y : 𝕜) ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : ↥s :=
  HAdd.hAdd (β := ↥s)
    (((b - a) * (HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) ((f : (a : α) → 𝕜) y : 𝕜))⁻¹) •
      HSub.hSub (α := ↥s) ((algebraMap 𝕜 ↥s : (a : 𝕜) → ↥s) ((f : (a : α) → 𝕜) x) : ↥s)
        (Subtype.mk (p := fun (x : C(α, 𝕜)) ↦ x ∈ s) f hf))
    ((algebraMap 𝕜 ↥s : (a : 𝕜) → ↥s) a : ↥s)
neg : ((↑f' : C(α, 𝕜)) : (a : α) → 𝕜) x = v x
neg₁ : ((↑f' : C(α, 𝕜)) : (a : α) → 𝕜) y = v y
⊢ ∃ f ∈ (↑s : Set C(α, 𝕜)), (f : (a : α) → 𝕜) x = v x ∧ (f : (a : α) → 𝕜) y = v y

Tactic:
refine ⟨f', f'.prop, ?_, ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ (↑s : Set C(α, 𝕜))
hxy : HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) ((f : (a : α) → 𝕜) y : 𝕜) ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : ↥s :=
  HAdd.hAdd (β := ↥s)
    (((b - a) * (HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) ((f : (a : α) → 𝕜) y : 𝕜))⁻¹) •
      HSub.hSub (α := ↥s) ((algebraMap 𝕜 ↥s : (a : 𝕜) → ↥s) ((f : (a : α) → 𝕜) x) : ↥s)
        (Subtype.mk (p := fun (x : C(α, 𝕜)) ↦ x ∈ s) f hf))
    ((algebraMap 𝕜 ↥s : (a : 𝕜) → ↥s) a : ↥s)
⊢ ((↑f' : C(α, 𝕜)) : (a : α) → 𝕜) x = v x

Tactic:
simp [a, b, f']
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Field 𝕜
inst_3 : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ (↑s : Set C(α, 𝕜))
hxy : HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) ((f : (a : α) → 𝕜) y : 𝕜) ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : ↥s :=
  HAdd.hAdd (β := ↥s)
    (((b - a) * (HSub.hSub (α := 𝕜) (β := 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) ((f : (a : α) → 𝕜) y : 𝕜))⁻¹) •
      HSub.hSub (α := ↥s) ((algebraMap 𝕜 ↥s : (a : 𝕜) → ↥s) ((f : (a : α) → 𝕜) x) : ↥s)
        (Subtype.mk (p := fun (x : C(α, 𝕜)) ↦ x ∈ s) f hf))
    ((algebraMap 𝕜 ↥s : (a : 𝕜) → ↥s) a : ↥s)
⊢ ((↑f' : C(α, 𝕜)) : (a : α) → 𝕜) y = v y

Tactic:
simp [a, b, f', inv_mul_cancel_right₀ hxy]

Premises used: inv_mul_cancel_right₀
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
inl : IsEmpty α → s₁ = s₂
inr : Nonempty α → s₁ = s₂
⊢ s₁ = s₂

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h : IsEmpty α
⊢ Subsingleton C(α, R)

Tactic:
have : Subsingleton C(α, R) := DFunLike.coe_injective.subsingleton
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h : IsEmpty α
this : Subsingleton C(α, R)
⊢ s₁ = s₂

Tactic:
subsingleton
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h : Nonempty α
inr : ∀ (inhabited_h : Inhabited α), s₁ = s₂
⊢ s₁ = s₂

Tactic:
inhabit α
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h : Nonempty α
inhabited_h : Inhabited α
inr : ∀ (f : C(α, R)), f ∈ s₁ ↔ f ∈ s₂
⊢ s₁ = s₂

Tactic:
ext f
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h_1 : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
h :
  ∀ (x' : α),
    Eq.{u_2 + 1} (α := R) ((f : (a : α) → R) x' : R)
      (((algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default) : (a : α) → R) x' : R)
⊢ f = (algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default)

Tactic:
ext x'
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h_1 : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
x' : α
h : Eq.{u_2 + 1} (α := R) ((f : (a : α) → R) x' : R) ((f : (a : α) → R) default : R)
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : α) → R) x' : R)
    (((algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default) : (a : α) → R) x' : R)

Tactic:
simp only [mul_one, smul_eq_mul, algebraMap_apply]

Premises used: algebraMap_apply, smul_eq_mul, mul_one
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h_1 : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
x' : α
h : x' = default
⊢ Eq.{u_2 + 1} (α := R) ((f : (a : α) → R) x' : R) ((f : (a : α) → R) default : R)

Tactic:
congr
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
x' : α
⊢ x' = default

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
⊢ f = (algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default)

Tactic:
have h : f = algebraMap R C(α, R) (f default) := by
        ext x'
        simp only [mul_one, smul_eq_mul, algebraMap_apply]
        congr
        simp [eq_iff_true_of_subsingleton]
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h_1 : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
h : f = (algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default)
inr :
  (algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default) ∈ s₁ ↔
    (algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default) ∈ s₂
⊢ f ∈ s₁ ↔ f ∈ s₂

Tactic:
rw [h]
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : CommSemiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h_1 : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
h : f = (algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default)
⊢ (algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default) ∈ s₁ ↔
    (algebraMap R C(α, R) : (a : R) → C(α, R)) ((f : (a : α) → R) default) ∈ s₂

Tactic:
simp only [Subalgebra.algebraMap_mem]

Premises used: Subalgebra.algebraMap_mem
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
f : C(α, R)
g : C(α, M)
⊢ (⇑(f • g) : (a : α) → M) = HSMul.hSMul (α := (a : α) → R) (β := (a : α) → M) (⇑f : (a : α) → R) (⇑g : (a : α) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
f : C(α, R)
g : C(α, M)
x : α
⊢ (f • g : (a : α) → M) x =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((f : (a : α) → R) x : R) ((g : (a : α) → M) x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
c₁ c₂ : C(α, R)
f : C(α, M)
h : ∀ (x : α), Eq.{u_3 + 1} (α := M) (((c₁ * c₂) • f : (a : α) → M) x : M) ((c₁ • c₂ • f : (a : α) → M) x : M)
⊢ (c₁ * c₂) • f = c₁ • c₂ • f

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
c₁ c₂ : C(α, R)
f : C(α, M)
x : α
⊢ Eq.{u_3 + 1} (α := M) (((c₁ * c₂) • f : (a : α) → M) x : M) ((c₁ • c₂ • f : (a : α) → M) x : M)

Tactic:
mul_smul (c₁ x) (c₂ x) (f x)

Premises used: DFunLike.coe, SemigroupAction.mul_smul
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
c₁ c₂ : C(α, R)
f : C(α, M)
x : α
⊢ Eq.{u_3 + 1} (α := M) (((c₁ * c₂) • f : (a : α) → M) x : M) ((c₁ • c₂ • f : (a : α) → M) x : M)

Tactic:
exact mul_smul (c₁ x) (c₂ x) (f x)

Premises used: DFunLike.coe, SemigroupAction.mul_smul
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
f : C(α, M)
h : ∀ (x : α), Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (α := C(α, R)) 1 f : (a : α) → M) x : M) ((f : (a : α) → M) x : M)
⊢ HSMul.hSMul (α := C(α, R)) 1 f = f

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
f : C(α, M)
x : α
⊢ Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (α := C(α, R)) 1 f : (a : α) → M) x : M) ((f : (a : α) → M) x : M)

Tactic:
one_smul R (f x)

Premises used: one_smul, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
f : C(α, M)
x : α
⊢ Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (α := C(α, R)) 1 f : (a : α) → M) x : M) ((f : (a : α) → M) x : M)

Tactic:
exact one_smul R (f x)

Premises used: one_smul, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
r : C(α, R)
h : ∀ (x : α), Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (β := C(α, M)) r 0 : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
⊢ HSMul.hSMul (β := C(α, M)) r 0 = 0

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
r : C(α, R)
x : α
⊢ Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (β := C(α, M)) r 0 : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)

Tactic:
smul_zero _

Premises used: smul_zero
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
r : C(α, R)
x : α
⊢ Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (β := C(α, M)) r 0 : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)

Tactic:
exact smul_zero _

Premises used: smul_zero
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
c : C(α, R)
f g : C(α, M)
h : ∀ (x : α), Eq.{u_3 + 1} (α := M) ((c • (f + g) : (a : α) → M) x : M) ((c • f + c • g : (a : α) → M) x : M)
⊢ c • (f + g) = c • f + c • g

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
c : C(α, R)
f g : C(α, M)
x : α
⊢ Eq.{u_3 + 1} (α := M) ((c • (f + g) : (a : α) → M) x : M) ((c • f + c • g : (a : α) → M) x : M)

Tactic:
smul_add (c x) (f x) (g x)

Premises used: DFunLike.coe, smul_add
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
c : C(α, R)
f g : C(α, M)
x : α
⊢ Eq.{u_3 + 1} (α := M) ((c • (f + g) : (a : α) → M) x : M) ((c • f + c • g : (a : α) → M) x : M)

Tactic:
exact smul_add (c x) (f x) (g x)

Premises used: DFunLike.coe, smul_add
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
c₁ c₂ : C(α, R)
f : C(α, M)
h : ∀ (x : α), Eq.{u_3 + 1} (α := M) (((c₁ + c₂) • f : (a : α) → M) x : M) ((c₁ • f + c₂ • f : (a : α) → M) x : M)
⊢ (c₁ + c₂) • f = c₁ • f + c₂ • f

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
c₁ c₂ : C(α, R)
f : C(α, M)
x : α
⊢ Eq.{u_3 + 1} (α := M) (((c₁ + c₂) • f : (a : α) → M) x : M) ((c₁ • f + c₂ • f : (a : α) → M) x : M)

Tactic:
add_smul (c₁ x) (c₂ x) (f x)

Premises used: add_smul, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
c₁ c₂ : C(α, R)
f : C(α, M)
x : α
⊢ Eq.{u_3 + 1} (α := M) (((c₁ + c₂) • f : (a : α) → M) x : M) ((c₁ • f + c₂ • f : (a : α) → M) x : M)

Tactic:
exact add_smul (c₁ x) (c₂ x) (f x)

Premises used: add_smul, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
f : C(α, M)
h : ∀ (x : α), Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (α := C(α, R)) 0 f : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
⊢ HSMul.hSMul (α := C(α, R)) 0 f = 0

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
f : C(α, M)
x : α
⊢ Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (α := C(α, R)) 0 f : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)

Tactic:
zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_2
inst_1 : Semiring R
inst_2 : TopologicalSpace R
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : IsTopologicalSemiring R
inst_8 : ContinuousAdd M
f : C(α, M)
x : α
⊢ Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (α := C(α, R)) 0 f : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)

Tactic:
exact zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : FunLike F α β
inst_3 : ContinuousMapClass F α β
f : F
a : α
⊢ ContinuousAt.{u_2, u_3} (Y := β) (⇑f : (a : α) → β) a

Tactic:
(map_continuous f).continuousAt

Premises used: Continuous.continuousAt, ContinuousMapClass.map_continuous
-- Module: Mathlib.Topology.ContinuousMap.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : FunLike F α β
inst_3 : ContinuousMapClass F α β
f : F
s : Set α
a : α
⊢ ContinuousWithinAt.{u_2, u_3} (Y := β) (⇑f : (a : α) → β) s a

Tactic:
(map_continuous f).continuousWithinAt

Premises used: ContinuousMapClass.map_continuous, Continuous.continuousWithinAt