awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
toAlgHom : A →ₐ[R] B
cont : Continuous[inst_2, inst_4] (↑(↑toAlgHom.toRingHom : A →* B) : OneHom A B).toFun
toAlgHom_1 : A →ₐ[R] B
cont_1 : Continuous[inst_2, inst_4] (↑(↑toAlgHom_1.toRingHom : A →* B) : OneHom A B).toFun
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom, cont := cont })
    ((fun (f : A →A[R] B) ↦ ((⇑f.toAlgHom : (a : A) → B) : (a : A) → B)) { toAlgHom := toAlgHom_1, cont := cont_1 })
⊢ toAlgHom = toAlgHom_1

Tactic:
exact AlgHom.ext (congrFun h)

Premises used: AlgHom.ext, congrFun
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →A[R] B
⊢ (↑f : A →ₐ[R] B) = (↑f : A →ₐ[R] B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f g : A →A[R] B
mk :
  ∀ (toAlgHom : A →ₐ[R] B) (cont : Continuous[inst_2, inst_4] (↑(↑toAlgHom.toRingHom : A →* B) : OneHom A B).toFun),
    (↑{ toAlgHom := toAlgHom, cont := cont : A →A[R] B } : A →ₐ[R] B) = (↑g : A →ₐ[R] B) ↔
      { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = g
⊢ (↑f : A →ₐ[R] B) = (↑g : A →ₐ[R] B) ↔ f = g

Tactic:
cases f
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
g : A →A[R] B
toAlgHom : A →ₐ[R] B
cont : Continuous[inst_2, inst_4] (↑(↑toAlgHom.toRingHom : A →* B) : OneHom A B).toFun
mk :
  ∀ (toAlgHom_1 : A →ₐ[R] B)
    (cont_1 : Continuous[inst_2, inst_4] (↑(↑toAlgHom_1.toRingHom : A →* B) : OneHom A B).toFun),
    (↑{ toAlgHom := toAlgHom, cont := cont : A →A[R] B } : A →ₐ[R] B) =
        (↑{ toAlgHom := toAlgHom_1, cont := cont_1 : A →A[R] B } : A →ₐ[R] B) ↔
      { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = { toAlgHom := toAlgHom_1, cont := cont_1 }
⊢ (↑{ toAlgHom := toAlgHom, cont := cont : A →A[R] B } : A →ₐ[R] B) = (↑g : A →ₐ[R] B) ↔
    { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = g

Tactic:
cases g
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
toAlgHom : A →ₐ[R] B
cont : Continuous[inst_2, inst_4] (↑(↑toAlgHom.toRingHom : A →* B) : OneHom A B).toFun
toAlgHom_1 : A →ₐ[R] B
cont_1 : Continuous[inst_2, inst_4] (↑(↑toAlgHom_1.toRingHom : A →* B) : OneHom A B).toFun
⊢ (↑{ toAlgHom := toAlgHom, cont := cont : A →A[R] B } : A →ₐ[R] B) =
      (↑{ toAlgHom := toAlgHom_1, cont := cont_1 : A →A[R] B } : A →ₐ[R] B) ↔
    { toAlgHom := toAlgHom, cont := cont : A →A[R] B } = { toAlgHom := toAlgHom_1, cont := cont_1 }

Tactic:
simp only [mk.injEq]

Premises used: ContinuousAlgHom.mk.injEq
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →ₐ[R] B
h : Continuous[inst_2, inst_4] (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun
⊢ (↑{ toAlgHom := f, cont := h : A →A[R] B } : A →ₐ[R] B) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →ₐ[R] B
h : Continuous[inst_2, inst_4] (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun
⊢ Eq (α := (a : A) → B) (⇑{ toAlgHom := f, cont := h : A →A[R] B } : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →A[R] B
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →ₐ[R] B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →A[R] B
⊢ Continuous[inst_2, inst_4] (⇑f : (a : A) → B)

Tactic:
f.2

Premises used: ContinuousAlgHom.cont
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
E₁ : Type u_4
E₂ : Type u_5
inst_1 : UniformSpace E₁
inst_2 : UniformSpace E₂
inst_3 : Ring E₁
inst_4 : Ring E₂
inst_5 : Algebra R E₁
inst_6 : Algebra R E₂
inst_7 : IsUniformAddGroup E₁
inst_8 : IsUniformAddGroup E₂
f : E₁ →A[R] E₂
⊢ UniformContinuous.{u_4, u_5} (α := E₁) (β := E₂) (⇑f : (a : E₁) → E₂)

Tactic:
uniformContinuous_addMonoidHom_of_continuous f.continuous

Premises used: ContinuousAlgHom.continuous, uniformContinuous_addMonoidHom_of_continuous
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f g : A →A[R] B
h : ∀ (x : A), Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) x : B) ((g : (a : A) → B) x : B)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →A[R] B
f' : A → B
h : f' = (⇑f : (a : A) → B)
r : R
⊢ (↑(↑((↑f : A →ₐ[R] B).copy f' h) : A →* B) : OneHom A B).toFun ((algebraMap R A : (a : R) → A) r) =
    (algebraMap R B : (a : R) → B) r

Tactic:
simp only [AlgHom.toRingHom_eq_coe, h, RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe,
        MonoidHom.toOneHom_coe, MonoidHom.coe_coe, RingHom.coe_copy, AlgHomClass.commutes f r]

Premises used: RingHom.toMonoidHom_eq_coe, MonoidHom.toOneHom_coe, MonoidHom.coe_coe, RingHom.coe_copy, AlgHomClass.commutes, AlgHom.toRingHom_eq_coe, OneHom.toFun_eq_coe
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →A[R] B
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ (⇑(f.copy f' h) : (a : A) → B) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →A[R] B
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →A[R] B
⊢ Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) 0 : B) (0 : B)

Tactic:
map_zero f

Premises used: map_zero
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →A[R] B
x y : A
⊢ (f : (a : A) → B) (x + y) = HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)

Tactic:
map_add f x y

Premises used: map_add
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →A[R] B
c : R
x : A
⊢ (f : (a : A) → B) (c • x) = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B)

Tactic:
map_smul ..

Premises used: map_smul
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
A : Type u_2
inst : Semiring A
inst_1 : TopologicalSpace A
B : Type u_3
inst_2 : Semiring B
inst_3 : TopologicalSpace B
R : Type u_4
S : Type u_5
inst_4 : CommSemiring S
inst_5 : SMul R A
inst_6 : Algebra S A
inst_7 : SMul R B
inst_8 : Algebra S B
inst_9 : MulActionHomClass (A →A[S] B) R A B
f : A →A[S] B
c : R
x : A
⊢ (f : (a : A) → B) (c • x) = HSMul.hSMul (β := B) c ((f : (a : A) → B) x : B)

Tactic:
map_smul f c x

Premises used: map_smul
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
ι : Type u_4
f : A →A[R] B
s : Finset ι
g : ι → A
⊢ Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) (∑ i ∈ s, g i) : B) (∑ i ∈ s, (f : (a : A) → B) (g i) : B)

Tactic:
map_sum ..

Premises used: map_sum
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
inst_4 : TopologicalSpace R
f g : R →A[R] A
⊢ f = g

Tactic:
coe_inj.mp (ext_id _ _ _)

Premises used: ContinuousAlgHom.coe_inj, Iff.mp, Algebra.ext_id
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
inst_4 : TopologicalSpace R
f g : R →A[R] A
⊢ f = g ↔ Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) 1 : A) ((g : (a : R) → A) 1 : A)

Tactic:
⟨fun h => h ▸ rfl, fun _ => ext_ring ⟩

Premises used: ContinuousAlgHom.ext_ring, Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : T2Space B
s : Set A
f g : A →A[R] B
h : EqOn.{u_2, u_3} (β := B) (⇑f : (a : A) → B) (⇑g : (a : A) → B) s
⊢ EqOn.{u_2, u_3} (β := B) (⇑f : (a : A) → B) (⇑g : (a : A) → B) (closure[inst_2] (↑(adjoin R s) : Set A))

Tactic:
Set.EqOn.closure (AlgHom.eqOn_adjoin_iff.mpr h) f.continuous g.continuous

Premises used: Iff.mpr, Set.EqOn.closure, ContinuousAlgHom.continuous, AlgHom.eqOn_adjoin_iff
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : T2Space B
s : Set A
hs : Dense (↑(adjoin R s) : Set A)
f g : A →A[R] B
h : EqOn.{u_2, u_3} (β := B) (⇑f : (a : A) → B) (⇑g : (a : A) → B) s
⊢ f = g

Tactic:
ext fun x => eqOn_closure_adjoin h (hs x)

Premises used: ContinuousAlgHom.eqOn_closure_adjoin, ContinuousAlgHom.ext
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
e : A →A[R] B
⊢ Eq (α := (a : A) → B) (⇑e.toContinuousLinearMap : (a : A) → B) (⇑e : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : IsSemitopologicalSemiring A
s : Subalgebra R A
r : R
a : Membership.mem (α := A) (↑s : Set A) ((algebraMap R A : (a : R) → A) r : A)
⊢ Membership.mem (α := A) (closure[inst_2] (↑s : Set A)) ((algebraMap R A : (a : R) → A) r : A)

Tactic:
apply subset_closure

Premises used: subset_closure
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : IsSemitopologicalSemiring A
s : Subalgebra R A
r : R
⊢ Membership.mem (α := A) (↑s : Set A) ((algebraMap R A : (a : R) → A) r : A)

Tactic:
algebraMap_mem s r

Premises used: algebraMap_mem
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : IsSemitopologicalSemiring A
s : Subalgebra R A
r : R
⊢ Membership.mem (α := A) (↑s : Set A) ((algebraMap R A : (a : R) → A) r : A)

Tactic:
exact algebraMap_mem s r

Premises used: algebraMap_mem
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : IsSemitopologicalSemiring A
inst_8 : IsSemitopologicalSemiring B
f : A →A[R] B
s : Subalgebra R A
⊢ map (↑f : A →ₐ[R] B) s.topologicalClosure ≤ (map (↑f : A →ₐ[R] B) s).topologicalClosure

Tactic:
image_closure_subset_closure_image f.continuous

Premises used: Set.Mem, setOf, Set.Subset, ContinuousAlgHom.continuous, closure, image_closure_subset_closure_image, Set.image, Set.sInter
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : IsSemitopologicalSemiring A
inst_8 : IsSemitopologicalSemiring B
f : A →ₐ[R] B
hf : IsClosedMap.{u_2, u_3} (X := A) (Y := B) (⇑f : (a : A) → B)
s : Subalgebra R A
⊢ (map f s).topologicalClosure ≤ map f s.topologicalClosure

Tactic:
hf.closure_image_subset _

Premises used: IsClosedMap.closure_image_subset, Set.Mem, setOf, Set.Subset, closure, Set.image, Set.sInter
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : IsSemitopologicalSemiring A
inst_8 : IsSemitopologicalSemiring B
f : A →A[R] B
hf : IsClosedMap.{u_2, u_3} (X := A) (Y := B) (⇑f : (a : A) → B)
s : Subalgebra R A
⊢ (map (↑f : A →ₐ[R] B) s).topologicalClosure = map (↑f : A →ₐ[R] B) s.topologicalClosure

Tactic:
SetLike.coe_injective <| hf.closure_image_eq_of_continuous f.continuous _

Premises used: SetLike.coe_injective, ContinuousAlgHom.continuous, IsClosedMap.closure_image_eq_of_continuous
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s : Subalgebra R A
⊢ (↑s.topologicalClosure : Set A) = closure[inst_2] (↑s : Set A)

Tactic:
rfl

Premises used: Set.Mem, setOf, closure, Set.sInter, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : IsSemitopologicalSemiring A
inst_8 : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange.{u_3, u_2} (X := B) (α := A) (⇑f : (a : A) → B)
s : Subalgebra R A
hs : s.topologicalClosure = ⊤
rw :
  ∀ (hs : (↑s.topologicalClosure : Set A) = (↑⊤ : Set A)),
    (↑(map (↑f : A →ₐ[R] B) s).topologicalClosure : Set B) = (↑⊤ : Set B)
⊢ (map (↑f : A →ₐ[R] B) s).topologicalClosure = ⊤

Tactic:
rw [SetLike.ext'_iff] at hs ⊢

Premises used: SetLike.ext'_iff
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : IsSemitopologicalSemiring A
inst_8 : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange.{u_3, u_2} (X := B) (α := A) (⇑f : (a : A) → B)
s : Subalgebra R A
hs : (↑s.topologicalClosure : Set A) = (↑⊤ : Set A)
simp : ∀ (hs : Dense (↑s : Set A)), Dense.{u_3} (X := B) ((⇑(↑f : A →ₐ[R] B) : (a : A) → B) '' (↑s : Set A))
⊢ (↑(map (↑f : A →ₐ[R] B) s).topologicalClosure : Set B) = (↑⊤ : Set B)

Tactic:
simp only [Subalgebra.topologicalClosure_coe, coe_top, ← dense_iff_closure_eq,
    Subalgebra.coe_map] at hs ⊢

Premises used: Subalgebra.topologicalClosure_coe, Algebra.coe_top, dense_iff_closure_eq, Subalgebra.coe_map
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : IsSemitopologicalSemiring A
inst_8 : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange.{u_3, u_2} (X := B) (α := A) (⇑f : (a : A) → B)
s : Subalgebra R A
hs : Dense (↑s : Set A)
⊢ Dense.{u_3} (X := B) ((⇑(↑f : A →ₐ[R] B) : (a : A) → B) '' (↑s : Set A))

Tactic:
hf'.dense_image f.continuous hs

Premises used: ContinuousAlgHom.continuous, DenseRange.dense_image
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : IsSemitopologicalSemiring A
inst_8 : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange.{u_3, u_2} (X := B) (α := A) (⇑f : (a : A) → B)
s : Subalgebra R A
hs : Dense (↑s : Set A)
⊢ Dense.{u_3} (X := B) ((⇑(↑f : A →ₐ[R] B) : (a : A) → B) '' (↑s : Set A))

Tactic:
exact hf'.dense_image f.continuous hs

Premises used: ContinuousAlgHom.continuous, DenseRange.dense_image
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
⊢ Eq (α := A →A[R] A) 1 (ContinuousAlgHom.id R A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
x : A
⊢ (ContinuousAlgHom.id R A : (a : A) → A) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
⊢ Eq (α := A →ₐ[R] A) (↑(ContinuousAlgHom.id R A) : A →ₐ[R] A) (AlgHom.id R A)

Tactic:
rfl

Premises used: AlgHom.id, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
⊢ Eq (α := (a : A) → A) (⇑(ContinuousAlgHom.id R A) : (a : A) → A) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
f : A →A[R] A
rw : (↑f : A →ₐ[R] A) = (↑(ContinuousAlgHom.id R A) : A →ₐ[R] A) ↔ f = ContinuousAlgHom.id R A
rw₁ rw₂ : f = ContinuousAlgHom.id R A ↔ f = ContinuousAlgHom.id R A
⊢ (↑f : A →ₐ[R] A) = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A

Tactic:
rw [← coe_id, coe_inj]

Premises used: ContinuousAlgHom.coe_id, ContinuousAlgHom.coe_inj
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
x : A
⊢ (1 : (a : A) → A) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
C : Type u_4
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : TopologicalSpace C
h : B →A[R] C
f : A →A[R] B
⊢ (↑(h.comp f) : A →ₐ[R] C) = (↑h : B →ₐ[R] C).comp (↑f : A →ₐ[R] B)

Tactic:
rfl

Premises used: AlgHom.comp, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
C : Type u_4
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : TopologicalSpace C
h : B →A[R] C
f : A →A[R] B
⊢ Eq (α := (a : A) → C) (⇑(h.comp f) : (a : A) → C)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := B) (⇑h : (a : B) → C) (⇑f : (a : A) → B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
C : Type u_4
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : TopologicalSpace C
g : B →A[R] C
f : A →A[R] B
x : A
⊢ Eq.{u_4 + 1} (α := C) ((g.comp f : (a : A) → C) x : C) ((g : (a : B) → C) ((f : (a : A) → B) x : B) : C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →A[R] B
⊢ f.comp (ContinuousAlgHom.id R A) = f

Tactic:
ext fun _x => rfl

Premises used: ContinuousAlgHom.ext, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →A[R] B
⊢ comp (ContinuousAlgHom.id R B) f = f

Tactic:
ext fun _x => rfl

Premises used: ContinuousAlgHom.ext, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
C : Type u_4
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : TopologicalSpace C
D : Type u_5
inst_10 : Semiring D
inst_11 : Algebra R D
inst_12 : TopologicalSpace D
h : C →A[R] D
g : B →A[R] C
f : A →A[R] B
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
rfl

Premises used: ContinuousAlgHom.comp, AlgHom.comp, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
f g : A →A[R] A
⊢ f * g = f.comp g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
f g : A →A[R] A
⊢ Eq (α := (a : A) → A) (⇑(f * g) : (a : A) → A) (Function.comp (β := A) (⇑f : (a : A) → A) (⇑g : (a : A) → A))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
f g : A →A[R] A
x : A
⊢ Eq (α := A) ((f * g : (a : A) → A) x : A) ((f : (a : A) → A) ((g : (a : A) → A) x : A) : A)

Tactic:
rfl

Premises used: rfl