awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this_1 : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
f : C(α, β)
rw :
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn (β := β) (fun (i : C(α, β)) (a : α) ↦ (i⁻¹ : (a : α) → β) a) (⇑f⁻¹ : (a : α) → β) (nhds f) K
⊢ ContinuousAt (Y := C(α, β)) (fun (a : C(α, β)) ↦ a⁻¹) f

Tactic:
rw [ContinuousAt, tendsto_iff_forall_isCompact_tendstoUniformlyOn]

Premises used: ContinuousAt, ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this_1 : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
f : C(α, β)
⊢ ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn (β := β) (fun (i : C(α, β)) (a : α) ↦ (i⁻¹ : (a : α) → β) a) (⇑f⁻¹ : (a : α) → β) (nhds f) K

Tactic:
fun K hK =>
      uniformContinuous_inv.comp_tendstoUniformlyOn
        (tendsto_iff_forall_isCompact_tendstoUniformlyOn.mp Filter.tendsto_id K hK)

Premises used: Filter.tendsto_id, UniformContinuous.comp_tendstoUniformlyOn, ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn, Iff.mp, uniformContinuous_inv
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommGroup β
inst_3 : IsTopologicalGroup β
this_1 : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
f : C(α, β)
⊢ ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn (β := β) (fun (i : C(α, β)) (a : α) ↦ (i⁻¹ : (a : α) → β) a) (⇑f⁻¹ : (a : α) → β) (nhds f) K

Tactic:
exact fun K hK =>
      uniformContinuous_inv.comp_tendstoUniformlyOn
        (tendsto_iff_forall_isCompact_tendstoUniformlyOn.mp Filter.tendsto_id K hK)

Premises used: Filter.tendsto_id, UniformContinuous.comp_tendstoUniformlyOn, ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn, Iff.mp, uniformContinuous_inv
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
γ : Type u_3
inst_2 : CommMonoid β
inst_3 : ContinuousMul β
f : γ → C(α, β)
g : C(α, β)
L : SummationFilter γ
hf : HasProd f g L
x : α
ev : C(α, β) →* β := MonoidHom.comp (Pi.evalMonoidHom (fun (a : α) ↦ β) x) coeFnMonoidHom
⊢ HasProd.{u_2, u_3} (α := β) (fun (i : γ) ↦ ((f i : (a : α) → β) x : β)) ((g : (a : α) → β) x : β) L

Tactic:
hf.map ev (continuous_eval_const x)

Premises used: HasProd.map, ContinuousEvalConst.continuous_eval_const
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
γ : Type u_3
inst_2 : CommMonoid β
inst_3 : ContinuousMul β
f : γ → C(α, β)
g : C(α, β)
L : SummationFilter γ
hf : HasProd f g L
x : α
ev : C(α, β) →* β := MonoidHom.comp (Pi.evalMonoidHom (fun (a : α) ↦ β) x) coeFnMonoidHom
⊢ HasProd.{u_2, u_3} (α := β) (fun (i : γ) ↦ ((f i : (a : α) → β) x : β)) ((g : (a : α) → β) x : β) L

Tactic:
exact hf.map ev (continuous_eval_const x)

Premises used: HasProd.map, ContinuousEvalConst.continuous_eval_const
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : CommMonoid β
inst_3 : ContinuousMul β
γ : Type u_3
f : γ → C(α, β)
L : SummationFilter γ
hf : Multipliable f L
x : α
⊢ Multipliable.{u_2, u_3} (α := β) (fun (i : γ) ↦ (f i : (a : α) → β) x) L

Tactic:
(hasProd_apply hf.hasProd x).multipliable

Premises used: Multipliable.hasProd, HasProd.multipliable, ContinuousMap.hasProd_apply
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : T2Space β
inst_3 : CommMonoid β
inst_4 : ContinuousMul β
γ : Type u_3
f : γ → C(α, β)
L : SummationFilter γ
hf : Multipliable f L
inst_5 : L.NeBot
x : α
⊢ Eq.{u_2 + 1} (α := β) (∏'[L] (i : γ), (f i : (a : α) → β) x : β) ((∏'[L] (i : γ), f i : (a : α) → β) x : β)

Tactic:
(hasProd_apply hf.hasProd x).tprod_eq

Premises used: HasProd.tprod_eq, Multipliable.hasProd, ContinuousMap.hasProd_apply
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
R : Type u_3
R₁ : Type u_4
M : Type u_5
inst_2 : TopologicalSpace M
M₂ : Type u_6
inst_3 : TopologicalSpace M₂
inst_4 : TopologicalSpace R
inst_5 : SMul R M
inst_6 : ContinuousSMul R M
⊢ ContinuousSMul R C(α, M)

Tactic:
⟨(continuous_postcomp ⟨_, continuous_smul⟩).comp continuous_prodMk_const⟩

Premises used: ContinuousMap.continuous_prodMk_const, ContinuousMap.continuous_postcomp, ContinuousMap.mk, Continuous.comp, ContinuousSMul.mk, ContinuousSMul.continuous_smul
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_3
M : Type u_5
inst_1 : TopologicalSpace M
inst_2 : SMul R M
inst_3 : ContinuousConstSMul R M
c : R
f : C(α, M)
⊢ (⇑(c • f) : (a : α) → M) = HSMul.hSMul (β := (a : α) → M) c (⇑f : (a : α) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
inst : TopologicalSpace α
R : Type u_3
M : Type u_5
inst_1 : TopologicalSpace M
inst_2 : SMul R M
inst_3 : ContinuousConstSMul R M
c : R
f : C(α, M)
a : α
⊢ (c • f : (a : α) → M) a = HSMul.hSMul (β := M) c ((f : (a : α) → M) a : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
R : Type u_3
M : Type u_5
inst_2 : TopologicalSpace M
inst_3 : SMul R M
inst_4 : ContinuousConstSMul R M
r : R
f : C(β, M)
g : C(α, β)
⊢ (r • f).comp g = r • f.comp g

Tactic:
rfl

Premises used: ContinuousMap.comp, rfl
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
h :
  ∀ (a : α),
    Eq.{u_3 + 1} (α := A)
      (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) 1, continuous_toFun := ⋯ } : (a : α) → A) a : A)
      ((1 : (a : α) → A) a : A)
⊢ Eq (α := C(α, A)) { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) 1, continuous_toFun := ⋯ } 1

Tactic:
ext _
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
a : α
⊢ Eq.{u_3 + 1} (α := A)
    (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) 1, continuous_toFun := ⋯ } : (a : α) → A) a : A)
    ((1 : (a : α) → A) a : A)

Tactic:
(algebraMap R A).map_one

Premises used: Algebra.algebraMap, RingHom.map_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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
a : α
⊢ Eq.{u_3 + 1} (α := A)
    (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) 1, continuous_toFun := ⋯ } : (a : α) → A) a : A)
    ((1 : (a : α) → A) a : A)

Tactic:
exact (algebraMap R A).map_one

Premises used: Algebra.algebraMap, RingHom.map_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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c₁ c₂ : R
h :
  ∀ (a : α),
    Eq.{u_3 + 1} (α := A)
      (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) (c₁ * c₂), continuous_toFun := ⋯ } : (a : α) → A) a : A)
      ((HMul.hMul (α := C(α, A))
              { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₁, continuous_toFun := ⋯ : C(α, A) }
              { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₂, continuous_toFun := ⋯ : C(α, A) } :
            (a : α) → A)
          a :
        A)
⊢ { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) (c₁ * c₂), continuous_toFun := ⋯ } =
    HMul.hMul (α := C(α, A))
      { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₁, continuous_toFun := ⋯ : C(α, A) }
      { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₂, continuous_toFun := ⋯ : C(α, A) }

Tactic:
ext _
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c₁ c₂ : R
a : α
⊢ Eq.{u_3 + 1} (α := A)
    (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) (c₁ * c₂), continuous_toFun := ⋯ } : (a : α) → A) a : A)
    ((HMul.hMul (α := C(α, A))
            { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₁, continuous_toFun := ⋯ : C(α, A) }
            { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₂, continuous_toFun := ⋯ : C(α, A) } :
          (a : α) → A)
        a :
      A)

Tactic:
(algebraMap R A).map_mul _ _

Premises used: Algebra.algebraMap, RingHom.map_mul
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c₁ c₂ : R
a : α
⊢ Eq.{u_3 + 1} (α := A)
    (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) (c₁ * c₂), continuous_toFun := ⋯ } : (a : α) → A) a : A)
    ((HMul.hMul (α := C(α, A))
            { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₁, continuous_toFun := ⋯ : C(α, A) }
            { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₂, continuous_toFun := ⋯ : C(α, A) } :
          (a : α) → A)
        a :
      A)

Tactic:
exact (algebraMap R A).map_mul _ _

Premises used: Algebra.algebraMap, RingHom.map_mul
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
h :
  ∀ (a : α),
    Eq.{u_3 + 1} (α := A)
      (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) 0, continuous_toFun := ⋯ } : (a : α) → A) a : A)
      ((0 : (a : α) → A) a : A)
⊢ Eq (α := C(α, A)) { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) 0, continuous_toFun := ⋯ } 0

Tactic:
ext _
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
a : α
⊢ Eq.{u_3 + 1} (α := A)
    (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) 0, continuous_toFun := ⋯ } : (a : α) → A) a : A)
    ((0 : (a : α) → A) a : A)

Tactic:
(algebraMap R A).map_zero

Premises used: Algebra.algebraMap, RingHom.map_zero
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
a : α
⊢ Eq.{u_3 + 1} (α := A)
    (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) 0, continuous_toFun := ⋯ } : (a : α) → A) a : A)
    ((0 : (a : α) → A) a : A)

Tactic:
exact (algebraMap R A).map_zero

Premises used: Algebra.algebraMap, RingHom.map_zero
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c₁ c₂ : R
h :
  ∀ (a : α),
    Eq.{u_3 + 1} (α := A)
      (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) (c₁ + c₂), continuous_toFun := ⋯ } : (a : α) → A) a : A)
      ((HAdd.hAdd (α := C(α, A))
              { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₁, continuous_toFun := ⋯ : C(α, A) }
              { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₂, continuous_toFun := ⋯ : C(α, A) } :
            (a : α) → A)
          a :
        A)
⊢ { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) (c₁ + c₂), continuous_toFun := ⋯ } =
    HAdd.hAdd (α := C(α, A))
      { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₁, continuous_toFun := ⋯ : C(α, A) }
      { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₂, continuous_toFun := ⋯ : C(α, A) }

Tactic:
ext _
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c₁ c₂ : R
a : α
⊢ Eq.{u_3 + 1} (α := A)
    (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) (c₁ + c₂), continuous_toFun := ⋯ } : (a : α) → A) a : A)
    ((HAdd.hAdd (α := C(α, A))
            { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₁, continuous_toFun := ⋯ : C(α, A) }
            { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₂, continuous_toFun := ⋯ : C(α, A) } :
          (a : α) → A)
        a :
      A)

Tactic:
(algebraMap R A).map_add _ _

Premises used: Algebra.algebraMap, RingHom.map_add
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c₁ c₂ : R
a : α
⊢ Eq.{u_3 + 1} (α := A)
    (({ toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) (c₁ + c₂), continuous_toFun := ⋯ } : (a : α) → A) a : A)
    ((HAdd.hAdd (α := C(α, A))
            { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₁, continuous_toFun := ⋯ : C(α, A) }
            { toFun := fun (x : α) ↦ (algebraMap R A : (a : R) → A) c₂, continuous_toFun := ⋯ : C(α, A) } :
          (a : α) → A)
        a :
      A)

Tactic:
exact (algebraMap R A).map_add _ _

Premises used: Algebra.algebraMap, RingHom.map_add
-- 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
r : R
a : α
⊢ Eq.{u_3 + 1} (α := A) ((((C : (a : R) → C(α, A)) r : C(α, A)) : (a : α) → A) a : A)
    ((algebraMap R A : (a : R) → A) r : A)

Tactic:
rfl

Premises used: rfl
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c : R
f : C(α, A)
h :
  ∀ (x : α),
    Eq.{u_3 + 1} (α := A)
      ((HMul.hMul (α := C(α, A)) (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) f : (a : α) → A) x : A)
      ((HMul.hMul (β := C(α, A)) f (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) : (a : α) → A) x : A)
⊢ HMul.hMul (α := C(α, A)) (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) f =
    HMul.hMul (β := C(α, A)) f (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A))

Tactic:
ext x
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c : R
f : C(α, A)
x : α
⊢ Eq.{u_3 + 1} (α := A)
    ((HMul.hMul (α := C(α, A)) (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) f : (a : α) → A) x : A)
    ((HMul.hMul (β := C(α, A)) f (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) : (a : α) → A) x : A)

Tactic:
Algebra.commutes' _ _

Premises used: Algebra.commutes'
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c : R
f : C(α, A)
x : α
⊢ Eq.{u_3 + 1} (α := A)
    ((HMul.hMul (α := C(α, A)) (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) f : (a : α) → A) x : A)
    ((HMul.hMul (β := C(α, A)) f (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) : (a : α) → A) x : A)

Tactic:
exact Algebra.commutes' _ _

Premises used: Algebra.commutes'
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c : R
f : C(α, A)
h :
  ∀ (x : α),
    Eq.{u_3 + 1} (α := A) ((c • f : (a : α) → A) x : A)
      ((HMul.hMul (α := C(α, A)) (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) f : (a : α) → A) x : A)
⊢ c • f = HMul.hMul (α := C(α, A)) (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) f

Tactic:
ext x
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c : R
f : C(α, A)
x : α
⊢ Eq.{u_3 + 1} (α := A) ((c • f : (a : α) → A) x : A)
    ((HMul.hMul (α := C(α, A)) (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) f : (a : α) → A) x : A)

Tactic:
Algebra.smul_def' _ _

Premises used: Algebra.smul_def'
-- 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
A₂ : Type u_4
inst_6 : TopologicalSpace A₂
inst_7 : Semiring A₂
inst_8 : Algebra R A₂
inst_9 : IsTopologicalSemiring A₂
c : R
f : C(α, A)
x : α
⊢ Eq.{u_3 + 1} (α := A) ((c • f : (a : α) → A) x : A)
    ((HMul.hMul (α := C(α, A)) (((C : R →+* C(α, A)) : (a : R) → C(α, A)) c : C(α, A)) f : (a : α) → A) x : A)

Tactic:
exact Algebra.smul_def' _ _

Premises used: Algebra.smul_def'
-- Module: Mathlib.Topology.ContinuousMap.Algebra
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsTopologicalSemiring A
α : Type u_5
β : Type u_6
inst_5 : TopologicalSpace α
inst_6 : TopologicalSpace β
f : C(α, β)
⊢ Continuous (X := C(β, A)) (Y := C(α, A)) (⇑(compRightAlgHom R A f) : (a : C(β, A)) → C(α, A))

Tactic:
continuous_precomp f

Premises used: ContinuousMap.comp, ContinuousMap.continuous_precomp
-- 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
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun (s : Subalgebra R C(α, A)) ↦ s.SeparatesPoints) s
x y : α
n : x ≠ y
obtain :
  ∀ (f : α → A)
    (m : Membership.mem (γ := Set (α → A)) ((fun (f : C(α, A)) ↦ (⇑f : (a : α) → A)) '' (↑s : Set C(α, A))) f)
    (w : f x ≠ f y),
    ∃ (f : α → A),
      Membership.mem (γ := Set (α → A)) ((fun (f : C(α, A)) ↦ (⇑f : (a : α) → A)) '' (↑s' : Set C(α, A))) f ∧ f x ≠ f y
⊢ ∃ (f : α → A),
    Membership.mem (γ := Set (α → A)) ((fun (f : C(α, A)) ↦ (⇑f : (a : α) → A)) '' (↑s' : Set C(α, A))) f ∧ f x ≠ f y

Tactic:
obtain ⟨f, m, w⟩ := h n
-- 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
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun (s : Subalgebra R C(α, A)) ↦ s.SeparatesPoints) s
x y : α
n : x ≠ y
f : α → A
m : Membership.mem (γ := Set (α → A)) ((fun (f : C(α, A)) ↦ (⇑f : (a : α) → A)) '' (↑s : Set C(α, A))) f
w : f x ≠ f y
rcases :
  ∀ (f : C(α, A)) (m : f ∈ (↑s : Set C(α, A)))
    (w :
      Ne.{u_3 + 1} (α := A) ((fun (f : C(α, A)) ↦ ((⇑f : (a : α) → A) : (a : α) → A)) f x)
        ((fun (f : C(α, A)) ↦ ((⇑f : (a : α) → A) : (a : α) → A)) f y)),
    ∃ (f : α → A),
      Membership.mem (γ := Set (α → A)) ((fun (f : C(α, A)) ↦ (⇑f : (a : α) → A)) '' (↑s' : Set C(α, A))) f ∧ f x ≠ f y
⊢ ∃ (f : α → A),
    Membership.mem (γ := Set (α → A)) ((fun (f : C(α, A)) ↦ (⇑f : (a : α) → A)) '' (↑s' : Set C(α, A))) f ∧ f x ≠ f y

Tactic:
rcases m with ⟨f, ⟨m, rfl⟩⟩

Premises used: rfl
-- 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
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun (s : Subalgebra R C(α, A)) ↦ s.SeparatesPoints) s
x y : α
n : x ≠ y
f : C(α, A)
m : f ∈ (↑s : Set C(α, A))
w :
  Ne.{u_3 + 1} (α := A) ((fun (f : C(α, A)) ↦ ((⇑f : (a : α) → A) : (a : α) → A)) f x)
    ((fun (f : C(α, A)) ↦ ((⇑f : (a : α) → A) : (a : α) → A)) f y)
⊢ ∃ (f : α → A),
    Membership.mem (γ := Set (α → A)) ((fun (f : C(α, A)) ↦ (⇑f : (a : α) → A)) '' (↑s' : Set C(α, A))) f ∧ f x ≠ f y

Tactic:
⟨_, ⟨f, ⟨r m, rfl⟩⟩, w⟩

Premises used: And.intro, Exists.intro, rfl
-- 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
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun (s : Subalgebra R C(α, A)) ↦ s.SeparatesPoints) s
x y : α
n : x ≠ y
f : C(α, A)
m : f ∈ (↑s : Set C(α, A))
w :
  Ne.{u_3 + 1} (α := A) ((fun (f : C(α, A)) ↦ ((⇑f : (a : α) → A) : (a : α) → A)) f x)
    ((fun (f : C(α, A)) ↦ ((⇑f : (a : α) → A) : (a : α) → A)) f y)
⊢ ∃ (f : α → A),
    Membership.mem (γ := Set (α → A)) ((fun (f : C(α, A)) ↦ (⇑f : (a : α) → A)) '' (↑s' : Set C(α, A))) f ∧ f x ≠ f y

Tactic:
exact ⟨_, ⟨f, ⟨r m, rfl⟩⟩, w⟩