awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : RingHomSurjective σ₁₂
inst_9 : TopologicalSpace R₁
inst_10 : TopologicalSpace R₂
inst_11 : ContinuousSMul R₁ M₁
inst_12 : ContinuousAdd M₁
inst_13 : ContinuousSMul R₂ M₂
inst_14 : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
hf' : DenseRange.{u_6, u_4} (X := M₂) (α := M₁) (⇑f : (a : M₁) → M₂)
s : Submodule R₁ M₁
hs : s.topologicalClosure = ⊤
rw :
  ∀ (hs : (↑s.topologicalClosure : Set M₁) = (↑⊤ : Set M₁)),
    (↑(Submodule.map (↑f : M₁ →ₛₗ[σ₁₂] M₂) s).topologicalClosure : Set M₂) = (↑⊤ : Set M₂)
⊢ (Submodule.map (↑f : M₁ →ₛₗ[σ₁₂] M₂) s).topologicalClosure = ⊤

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

Premises used: SetLike.ext'_iff
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : RingHomSurjective σ₁₂
inst_9 : TopologicalSpace R₁
inst_10 : TopologicalSpace R₂
inst_11 : ContinuousSMul R₁ M₁
inst_12 : ContinuousAdd M₁
inst_13 : ContinuousSMul R₂ M₂
inst_14 : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
hf' : DenseRange.{u_6, u_4} (X := M₂) (α := M₁) (⇑f : (a : M₁) → M₂)
s : Submodule R₁ M₁
hs : (↑s.topologicalClosure : Set M₁) = (↑⊤ : Set M₁)
simp : ∀ (hs : Dense (↑s : Set M₁)), Dense (↑(Submodule.map (↑f : M₁ →ₛₗ[σ₁₂] M₂) s) : Set M₂)
⊢ (↑(Submodule.map (↑f : M₁ →ₛₗ[σ₁₂] M₂) s).topologicalClosure : Set M₂) = (↑⊤ : Set M₂)

Tactic:
simp only [Submodule.topologicalClosure_coe, Submodule.top_coe, ← dense_iff_closure_eq] at hs ⊢

Premises used: dense_iff_closure_eq, Submodule.topologicalClosure_coe, Submodule.top_coe
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : RingHomSurjective σ₁₂
inst_9 : TopologicalSpace R₁
inst_10 : TopologicalSpace R₂
inst_11 : ContinuousSMul R₁ M₁
inst_12 : ContinuousAdd M₁
inst_13 : ContinuousSMul R₂ M₂
inst_14 : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
hf' : DenseRange.{u_6, u_4} (X := M₂) (α := M₁) (⇑f : (a : M₁) → M₂)
s : Submodule R₁ M₁
hs : Dense (↑s : Set M₁)
⊢ Dense (↑(Submodule.map (↑f : M₁ →ₛₗ[σ₁₂] M₂) s) : Set M₂)

Tactic:
hf'.dense_image f.continuous hs

Premises used: setOf, ContinuousLinearMap.continuous, Set.image, DenseRange.dense_image
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : RingHomSurjective σ₁₂
inst_9 : TopologicalSpace R₁
inst_10 : TopologicalSpace R₂
inst_11 : ContinuousSMul R₁ M₁
inst_12 : ContinuousAdd M₁
inst_13 : ContinuousSMul R₂ M₂
inst_14 : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
hf' : DenseRange.{u_6, u_4} (X := M₂) (α := M₁) (⇑f : (a : M₁) → M₂)
s : Submodule R₁ M₁
hs : Dense (↑s : Set M₁)
⊢ Dense (↑(Submodule.map (↑f : M₁ →ₛₗ[σ₁₂] M₂) s) : Set M₂)

Tactic:
exact hf'.dense_image f.continuous hs

Premises used: ContinuousLinearMap.continuous, DenseRange.dense_image
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
S₂ : Type u_9
inst_8 : DistribSMul S₂ M₂
inst_9 : SMulCommClass R₂ S₂ M₂
inst_10 : ContinuousConstSMul S₂ M₂
c : S₂
f : M₁ →SL[σ₁₂] M₂
x : M₁
⊢ (c • f : (a : M₁) → M₂) x = HSMul.hSMul (β := M₂) c ((f : (a : M₁) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
S₂ : Type u_9
inst_8 : DistribSMul S₂ M₂
inst_9 : SMulCommClass R₂ S₂ M₂
inst_10 : ContinuousConstSMul S₂ M₂
c : S₂
f : M₁ →SL[σ₁₂] M₂
⊢ (↑(c • f) : M₁ →ₛₗ[σ₁₂] M₂) = c • (↑f : M₁ →ₛₗ[σ₁₂] M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
S₂ : Type u_9
inst_8 : DistribSMul S₂ M₂
inst_9 : SMulCommClass R₂ S₂ M₂
inst_10 : ContinuousConstSMul S₂ M₂
c : S₂
f : M₁ →SL[σ₁₂] M₂
⊢ (⇑(c • f) : (a : M₁) → M₂) = HSMul.hSMul (β := (a : M₁) → M₂) c (⇑f : (a : M₁) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
S₂ : Type u_9
T₂ : Type u_10
inst_17 : DistribSMul S₂ M₂
inst_18 : SMulCommClass R₂ S₂ M₂
inst_19 : ContinuousConstSMul S₂ M₂
inst_20 : DistribSMul T₂ M₂
inst_21 : SMulCommClass R₂ T₂ M₂
inst_22 : ContinuousConstSMul T₂ M₂
inst_23 : SMul S₂ T₂
inst_24 : IsScalarTower S₂ T₂ M₂
⊢ IsScalarTower S₂ T₂ (M₁ →SL[σ₁₂] M₂)

Tactic:
⟨fun a b f => ext fun x => smul_assoc a b (f x)⟩

Premises used: smul_assoc, IsScalarTower.mk, DFunLike.coe, ContinuousLinearMap.ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
S₂ : Type u_9
T₂ : Type u_10
inst_17 : DistribSMul S₂ M₂
inst_18 : SMulCommClass R₂ S₂ M₂
inst_19 : ContinuousConstSMul S₂ M₂
inst_20 : DistribSMul T₂ M₂
inst_21 : SMulCommClass R₂ T₂ M₂
inst_22 : ContinuousConstSMul T₂ M₂
inst_23 : SMulCommClass S₂ T₂ M₂
⊢ SMulCommClass S₂ T₂ (M₁ →SL[σ₁₂] M₂)

Tactic:
⟨fun a b f => ext fun x => smul_comm a b (f x)⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, DFunLike.coe, ContinuousLinearMap.ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
⊢ Eq (α := M₁ →SL[σ₁₂] M₂) default 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
x : M₁
⊢ Eq.{u_6 + 1} (α := M₂) ((0 : (a : M₁) → M₂) x : M₂) (0 : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
⊢ Eq (α := M₁ →ₛₗ[σ₁₂] M₂) (↑0 : M₁ →ₛₗ[σ₁₂] M₂) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
⊢ Eq (α := (a : M₁) → M₂) (⇑0 : (a : M₁) → M₂) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
⊢ Eq (α := M₁ →ₜ+ M₂) (↑0 : M₁ →ₜ+ M₂) 0

Tactic:
rfl

Premises used: ContinuousAddMonoidHom.toContinuousAddMonoidHom, AddMonoidHomClass.toAddMonoidHom, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
hf : f ≠ 0
by_contra! : ∀ (h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((f : (a : M₁) → M₂) x : M₂) (0 : M₂)), False
⊢ ∃ (x : M₁), Ne.{u_6 + 1} (α := M₂) ((f : (a : M₁) → M₂) x : M₂) (0 : M₂)

Tactic:
by_contra! h
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
hf : f ≠ 0
h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((f : (a : M₁) → M₂) x : M₂) (0 : M₂)
⊢ False

Tactic:
hf (ContinuousLinearMap.ext h)

Premises used: ContinuousLinearMap.ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
hf : f ≠ 0
h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((f : (a : M₁) → M₂) x : M₂) (0 : M₂)
⊢ False

Tactic:
exact hf (ContinuousLinearMap.ext h)

Premises used: ContinuousLinearMap.ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
⊢ Eq (α := M₁ →L[R₁] M₁) 1 (ContinuousLinearMap.id R₁ M₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
x : M₁
⊢ (ContinuousLinearMap.id R₁ M₁ : (a : M₁) → M₁) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
⊢ Eq (α := M₁ →ₗ[R₁] M₁) (↑(ContinuousLinearMap.id R₁ M₁) : M₁ →ₗ[R₁] M₁) LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
⊢ Eq (α := (a : M₁) → M₁) (⇑(ContinuousLinearMap.id R₁ M₁) : (a : M₁) → M₁) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
⊢ Eq.{u_4 + 1} (α := M₁ →ₗ[R₁] M₁) (↑1 : M₁ →ₗ[R₁] M₁) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
⊢ Eq (α := M₁ →L[R₁] M₁) { toLinearMap := LinearMap.id, cont := ⋯ } (ContinuousLinearMap.id R₁ M₁)

Tactic:
rfl

Premises used: ContinuousLinearMap.id, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
⊢ Eq.{u_4 + 1} (α := M₁ →L[R₁] M₁) { toLinearMap := 1, cont := ⋯ } 1

Tactic:
rfl

Premises used: ContinuousLinearMap.id, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
⊢ Eq (α := M₁ →ₜ+ M₁) (↑(ContinuousLinearMap.id R₁ M₁) : M₁ →ₜ+ M₁) (ContinuousAddMonoidHom.id M₁)

Tactic:
rfl

Premises used: ContinuousAddMonoidHom.id, ContinuousAddMonoidHom.toContinuousAddMonoidHom, AddMonoidHomClass.toAddMonoidHom, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
f : M₁ →L[R₁] M₁
rw : (↑f : M₁ →ₗ[R₁] M₁) = (↑(ContinuousLinearMap.id R₁ M₁) : M₁ →ₗ[R₁] M₁) ↔ f = ContinuousLinearMap.id R₁ M₁
rw₁ rw₂ : f = ContinuousLinearMap.id R₁ M₁ ↔ f = ContinuousLinearMap.id R₁ M₁
⊢ (↑f : M₁ →ₗ[R₁] M₁) = LinearMap.id ↔ f = ContinuousLinearMap.id R₁ M₁

Tactic:
rw [← coe_id, coe_inj]

Premises used: ContinuousLinearMap.coe_inj, ContinuousLinearMap.coe_id
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
x : M₁
⊢ (1 : (a : M₁) → M₁) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : Nontrivial M₁
e : Eq.{u_4 + 1} (α := M₁ →L[R₁] M₁) 0 1
x : M₁
hx : x ≠ 0
⊢ x = 0

Tactic:
simpa using DFunLike.congr_fun e.symm x

Premises used: DFunLike.congr_fun, Eq.symm
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : ContinuousAdd M₂
f g : M₁ →SL[σ₁₂] M₂
x : M₁
⊢ (f + g : (a : M₁) → M₂) x = HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M₁) → M₂) x : M₂) ((g : (a : M₁) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : ContinuousAdd M₂
f g : M₁ →SL[σ₁₂] M₂
⊢ (↑(f + g) : M₁ →ₛₗ[σ₁₂] M₂) = (↑f : M₁ →ₛₗ[σ₁₂] M₂) + (↑g : M₁ →ₛₗ[σ₁₂] M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : ContinuousAdd M₂
f g : M₁ →SL[σ₁₂] M₂
⊢ (⇑(f + g) : (a : M₁) → M₂) = HAdd.hAdd (α := (a : M₁) → M₂) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₁) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : ContinuousAdd M₂
f g : M₁ →SL[σ₁₂] M₂
⊢ (↑(f + g) : M₁ →ₜ+ M₂) = HAdd.hAdd (α := M₁ →ₜ+ M₂) (↑f : M₁ →ₜ+ M₂) (↑g : M₁ →ₜ+ M₂)

Tactic:
rfl

Premises used: ContinuousAddMonoidHom.toContinuousAddMonoidHom, ContinuousAddMonoidHom.comp, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : ContinuousAdd M₂
a b c : M₁ →SL[σ₁₂] M₂
h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((a + b + c : (a : M₁) → M₂) x : M₂) ((a + (b + c) : (a : M₁) → M₂) x : M₂)
⊢ a + b + c = a + (b + c)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : ContinuousAdd M₂
a b c : M₁ →SL[σ₁₂] M₂
x : M₁
⊢ Eq.{u_6 + 1} (α := M₂) ((a + b + c : (a : M₁) → M₂) x : M₂) ((a + (b + c) : (a : M₁) → M₂) x : M₂)

Tactic:
apply_rules [zero_add, add_assoc, add_zero, neg_add_cancel, add_comm]

Premises used: add_assoc, zero_add, add_comm, neg_add_cancel, add_zero
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : ContinuousAdd M₂
a : M₁ →SL[σ₁₂] M₂
h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((0 + a : (a : M₁) → M₂) x : M₂) ((a : (a : M₁) → M₂) x : M₂)
⊢ 0 + a = a

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : ContinuousAdd M₂
a : M₁ →SL[σ₁₂] M₂
x : M₁
⊢ Eq.{u_6 + 1} (α := M₂) ((0 + a : (a : M₁) → M₂) x : M₂) ((a : (a : M₁) → M₂) x : M₂)

Tactic:
apply_rules [zero_add, add_assoc, add_zero, neg_add_cancel, add_comm]

Premises used: add_assoc, zero_add, add_comm, neg_add_cancel, add_zero
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : ContinuousAdd M₂
a : M₁ →SL[σ₁₂] M₂
h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((a + 0 : (a : M₁) → M₂) x : M₂) ((a : (a : M₁) → M₂) x : M₂)
⊢ a + 0 = a

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst_3 : TopologicalSpace M₁
inst_4 : AddCommMonoid M₁
M'₁ : Type u_5
inst_5 : TopologicalSpace M'₁
inst_6 : AddCommMonoid M'₁
M₂ : Type u_6
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
M₃ : Type u_7
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
M₄ : Type u_8
inst_11 : TopologicalSpace M₄
inst_12 : AddCommMonoid M₄
inst_13 : Module R₁ M₁
inst_14 : Module R₁ M'₁
inst_15 : Module R₂ M₂
inst_16 : Module R₃ M₃
inst_17 : ContinuousAdd M₂
a : M₁ →SL[σ₁₂] M₂
x : M₁
⊢ Eq.{u_6 + 1} (α := M₂) ((a + 0 : (a : M₁) → M₂) x : M₂) ((a : (a : M₁) → M₂) x : M₂)

Tactic:
apply_rules [zero_add, add_assoc, add_zero, neg_add_cancel, add_comm]

Premises used: add_assoc, zero_add, add_comm, neg_add_cancel, add_zero