awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
hg : Function.Injective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑g : (a : M₂) → M₃)
h : g ∘SL f₁ = g ∘SL f₂
x : M₁
⊢ Eq.{u_6 + 1} (α := M₂) ((f₁ : (a : M₁) → M₂) x : M₂) ((f₂ : (a : M₁) → M₂) x : M₂)

Tactic:
hg congr($h x)

Premises used: congrArg, id, DFunLike.coe
-- 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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
hg : Function.Injective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑g : (a : M₂) → M₃)
h : g ∘SL f₁ = g ∘SL f₂
x : M₁
⊢ Eq.{u_6 + 1} (α := M₂) ((f₁ : (a : M₁) → M₂) x : M₂) ((f₂ : (a : M₁) → M₂) x : M₂)

Tactic:
exact hg congr($h x)

Premises used: congrArg, id, DFunLike.coe
-- 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_6
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
M₃ : Type u_7
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R₁ M₁
inst_10 : Module R₂ M₂
inst_11 : Module R₃ M₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
hg : Function.Injective.{u_6 + 1, u_7 + 1} (α := M₂) (β := M₃) (⇑g : (a : M₂) → M₃)
⊢ g ∘SL f₁ = g ∘SL f₂ ↔ f₁ = f₂

Tactic:
⟨cancel_left hg, congr_arg (fun f => g ∘SL f)⟩

Premises used: ContinuousLinearMap.comp, congr_arg, Iff.intro, ContinuousLinearMap.cancel_left
-- 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 g : M₁ →L[R₁] M₁
⊢ f * g = f ∘SL g

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₁
f g : M₁ →L[R₁] M₁
⊢ (↑(f * g) : M₁ →ₗ[R₁] M₁) = (↑f : M₁ →ₗ[R₁] M₁) * (↑g : M₁ →ₗ[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₁
f g : M₁ →L[R₁] M₁
⊢ Eq (α := (a : M₁) → M₁) (⇑(f * g) : (a : M₁) → M₁) (Function.comp (β := 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
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
f g : M₁ →L[R₁] M₁
x : M₁
⊢ Eq (α := M₁) ((f * g : (a : M₁) → M₁) x : M₁) ((f : (a : M₁) → M₁) ((g : (a : M₁) → M₁) x : M₁) : 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₁
f : M₁ →L[R₁] M₁
n : ℕ
⊢ Eq (α := (a : M₁) → M₁) (⇑(f ^ n) : (a : M₁) → M₁) (⇑f : (a : M₁) → M₁)^[n]

Tactic:
hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _

Premises used: hom_coe_pow
-- 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₁
n : ℕ
⊢ (↑(f ^ n) : M₁ →ₗ[R₁] M₁) = (↑f : M₁ →ₗ[R₁] M₁) ^ n

Tactic:
DFunLike.ext' <| (coe_pow' f n).trans <| .symm <| hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _

Premises used: ContinuousLinearMap.coe_pow', hom_coe_pow, DFunLike.ext', Eq.symm, Eq.trans
-- 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₁
inst_4 : ContinuousAdd M₁
n : ℕ
m : M₁
⊢ ((↑n : M₁ →L[R₁] M₁) : (a : M₁) → M₁) m = n • 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₁
inst_4 : ContinuousAdd M₁
n : ℕ
inst_5 : n.AtLeastTwo
m : M₁
⊢ (OfNat.ofNat n : (a : M₁) → M₁) m = HSMul.hSMul (α := ℕ) (OfNat.ofNat n) 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₃
inst_17 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
rw : ((↑T⁻¹ : M₁ →L[R₁] M₁) * (↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x = x
rw₁ : (1 : (a : M₁) → M₁) x = x
rw₂ rw₃ : x = x
⊢ ((↑T⁻¹ : M₁ →L[R₁] M₁) : (a : M₁) → M₁) (((↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x : M₁) = x

Tactic:
rw [← mul_apply, Units.inv_mul, one_apply]

Premises used: ContinuousLinearMap.mul_apply, Units.inv_mul, ContinuousLinearMap.one_apply
-- 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 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
rw : ((↑T : M₁ →L[R₁] M₁) * (↑T⁻¹ : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x = x
rw₁ : (1 : (a : M₁) → M₁) x = x
rw₂ rw₃ : x = x
⊢ ((↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁) (((↑T⁻¹ : M₁ →L[R₁] M₁) : (a : M₁) → M₁) x : M₁) = x

Tactic:
rw [← mul_apply, Units.mul_inv, one_apply]

Premises used: ContinuousLinearMap.mul_apply, Units.mul_inv, ContinuousLinearMap.one_apply
-- 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₁
T : M₁ →L[R₁] M₁
hT : IsUnit T
obtain : ∀ (T : (M₁ →L[R₁] M₁)ˣ), IsHomeomorph (X := M₁) (Y := M₁) (⇑(↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁)
⊢ IsHomeomorph (X := M₁) (Y := M₁) (⇑T : (a : M₁) → M₁)

Tactic:
obtain ⟨T, rfl⟩ := hT

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₁
T : (M₁ →L[R₁] M₁)ˣ
⊢ IsHomeomorph (X := M₁) (Y := M₁) (⇑(↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁)

Tactic:
(homeomorphOfUnit T).isHomeomorph

Premises used: ContinuousLinearMap.homeomorphOfUnit, Homeomorph.isHomeomorph
-- 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₁
T : (M₁ →L[R₁] M₁)ˣ
⊢ IsHomeomorph (X := M₁) (Y := M₁) (⇑(↑T : M₁ →L[R₁] M₁) : (a : M₁) → M₁)

Tactic:
exact (homeomorphOfUnit T).isHomeomorph

Premises used: ContinuousLinearMap.homeomorphOfUnit, Homeomorph.isHomeomorph
-- 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₁
inst_4 : ContinuousAdd M₁
f : M₁ →L[R₁] M₁
a : M₁
⊢ f • a = (f : (a : M₁) → M₁) a

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 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_18 : ContinuousAdd M₁
⊢ FaithfulSMul (M₁ →L[R₁] M₁) M₁

Tactic:
⟨fun {_ _} => ContinuousLinearMap.ext⟩

Premises used: FaithfulSMul.mk, 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₃
inst_17 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_18 : ContinuousAdd M₁
⊢ ContinuousConstSMul (M₁ →L[R₁] M₁) M₁

Tactic:
⟨ContinuousLinearMap.continuous⟩

Premises used: ContinuousConstSMul.mk, ContinuousLinearMap.continuous
-- 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 : T1Space M₂
f : M₁ →SL[σ₁₂] M₂
⊢ IsClosed[inst_2] (↑(↑f : M₁ →ₛₗ[σ₁₂] M₂).ker : Set M₁)

Tactic:
continuous_iff_isClosed.1 (map_continuous f) _ isClosed_singleton

Premises used: Set.Mem, setOf, continuous_iff_isClosed, Set.preimage, Set.singleton, Iff.mp, ContinuousMapClass.map_continuous, isClosed_singleton
-- 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_6
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
inst_4 : Module R₂ M₂
M' : Type u_9
inst_5 : UniformSpace M'
inst_6 : CompleteSpace M'
inst_7 : AddCommMonoid M'
inst_8 : Module R₁ M'
inst_9 : T1Space M₂
f : M' →SL[σ₁₂] M₂
⊢ IsComplete (↑(↑f : M' →ₛₗ[σ₁₂] M₂).ker : Set M')

Tactic:
(isClosed_ker f).isComplete

Premises used: ContinuousLinearMap.isClosed_ker, IsClosed.isComplete
-- 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 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
M' : Type u_9
inst_18 : UniformSpace M'
inst_19 : CompleteSpace M'
inst_20 : AddCommMonoid M'
inst_21 : Module R₁ M'
inst_22 : T1Space M₂
f : M' →SL[σ₁₂] M₂
⊢ CompleteSpace.{u_9} ↥(↑f : M' →ₛₗ[σ₁₂] M₂).ker

Tactic:
(isComplete_ker f).completeSpace_coe

Premises used: IsComplete.completeSpace_coe, ContinuousLinearMap.isComplete_ker
-- 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 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
M' : Type u_9
inst_18 : UniformSpace M'
inst_19 : CompleteSpace M'
inst_20 : AddCommMonoid M'
inst_21 : Module R₁ M'
inst_22 : T2Space M₂
f g : M' →SL[σ₁₂] M₂
⊢ CompleteSpace.{u_9} ↥(LinearMap.eqLocus f g)

Tactic:
IsClosed.completeSpace_coe (hs := isClosed_eq (map_continuous f) (map_continuous g))

Premises used: IsClosed.completeSpace_coe
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
M₁ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
M₂ : Type u_6
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R S
inst_9 : Module S M₂
inst_10 : IsScalarTower R S M₂
inst_11 : TopologicalSpace S
inst_12 : ContinuousSMul S M₂
c : M₁ →L[R] S
f : M₂
x : M₁
⊢ (c.smulRight f : (a : M₁) → M₂) x = HSMul.hSMul.{u_10, u_6, u_6} (α := S) ((c : (a : M₁) → S) x : S) f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
M₁ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
M₂ : Type u_6
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R S
inst_9 : Module S M₂
inst_10 : IsScalarTower R S M₂
inst_11 : TopologicalSpace S
inst_12 : ContinuousSMul S M₂
f : M₁ →L[R] S
h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((f.smulRight 0 : (a : M₁) → M₂) x : M₂) ((0 : (a : M₁) → M₂) x : M₂)
⊢ Eq (α := M₁ →L[R] M₂) (f.smulRight 0) 0

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
M₁ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
M₂ : Type u_6
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R S
inst_9 : Module S M₂
inst_10 : IsScalarTower R S M₂
inst_11 : TopologicalSpace S
inst_12 : ContinuousSMul S M₂
f : M₁ →L[R] S
x : M₁
⊢ Eq.{u_6 + 1} (α := M₂) ((f.smulRight 0 : (a : M₁) → M₂) x : M₂) ((0 : (a : M₁) → M₂) x : M₂)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
M₁ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
M₂ : Type u_6
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R S
inst_9 : Module S M₂
inst_10 : IsScalarTower R S M₂
inst_11 : TopologicalSpace S
inst_12 : ContinuousSMul S M₂
x : M₂
h :
  ∀ (x_1 : M₁),
    Eq.{u_6 + 1} (α := M₂) ((smulRight.{u_4, u_6, u_9, u_10} (S := S) 0 x : (a : M₁) → M₂) x_1 : M₂)
      ((0 : (a : M₁) → M₂) x_1 : M₂)
⊢ Eq (α := M₁ →L[R] M₂) (smulRight.{u_4, u_6, u_9, u_10} (S := S) 0 x) 0

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
M₁ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
M₂ : Type u_6
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : Module R M₁
inst_7 : Module R M₂
inst_8 : Module R S
inst_9 : Module S M₂
inst_10 : IsScalarTower R S M₂
inst_11 : TopologicalSpace S
inst_12 : ContinuousSMul S M₂
x : M₂
x_1 : M₁
⊢ Eq.{u_6 + 1} (α := M₂) ((smulRight.{u_4, u_6, u_9, u_10} (S := S) 0 x : (a : M₁) → M₂) x_1 : M₂)
    ((0 : (a : M₁) → M₂) x_1 : M₂)

Tactic:
simp
-- 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₁
M₂ : Type u_6
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₁ M₁
inst_6 : Module R₁ M₂
inst_7 : TopologicalSpace R₁
inst_8 : ContinuousSMul R₁ M₂
M₃ : Type u_9
inst_9 : AddCommMonoid M₃
inst_10 : Module R₁ M₃
inst_11 : TopologicalSpace M₃
inst_12 : ContinuousSMul R₁ M₃
f : M₃ →L[R₁] R₁
g : M₁ →L[R₁] R₁
x : M₂
y : M₃
h :
  ∀ (x_1 : M₁),
    Eq.{u_6 + 1} (α := M₂) ((f.smulRight x ∘SL g.smulRight y : (a : M₁) → M₂) x_1 : M₂)
      ((g.smulRight (HSMul.hSMul.{u_1, u_6, u_6} (α := R₁) ((f : (a : M₃) → R₁) y : R₁) x) : (a : M₁) → M₂) x_1 : M₂)
⊢ Eq (α := M₁ →L[R₁] M₂) (f.smulRight x ∘SL g.smulRight y)
    (g.smulRight (HSMul.hSMul.{u_1, u_6, u_6} (α := R₁) ((f : (a : M₃) → R₁) y : R₁) x))

Tactic:
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₁
M₂ : Type u_6
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₁ M₁
inst_6 : Module R₁ M₂
inst_7 : TopologicalSpace R₁
inst_8 : ContinuousSMul R₁ M₂
M₃ : Type u_9
inst_9 : AddCommMonoid M₃
inst_10 : Module R₁ M₃
inst_11 : TopologicalSpace M₃
inst_12 : ContinuousSMul R₁ M₃
f : M₃ →L[R₁] R₁
g : M₁ →L[R₁] R₁
x : M₂
y : M₃
x_1 : M₁
⊢ Eq.{u_6 + 1} (α := M₂) ((f.smulRight x ∘SL g.smulRight y : (a : M₁) → M₂) x_1 : M₂)
    ((g.smulRight (HSMul.hSMul.{u_1, u_6, u_6} (α := R₁) ((f : (a : M₃) → R₁) y : R₁) x) : (a : M₁) → M₂) x_1 : M₂)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
M₁ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
M₂ : Type u_6
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
R : Type u_9
inst_4 : DivisionSemiring R
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : TopologicalSpace R
inst_8 : ContinuousSMul R M₂
f : M₁ →L[R] R
hf : f ≠ 0
x : M₂
⊢ (↑f : M₁ →ₗ[R] R) ≠ 0

Tactic:
simpa [coe_inj, ← coe_zero] using hf

Premises used: ContinuousLinearMap.coe_inj, ContinuousLinearMap.coe_zero
-- 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₁
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₁
x : M₁
r : R₁
⊢ (toSpanSingleton R₁ x : (a : R₁) → M₁) r = r • 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₁
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₁
h : Eq.{u_4 + 1} (α := M₁) ((toSpanSingleton R₁ 0 : (a : R₁) → M₁) 1 : M₁) ((0 : (a : R₁) → M₁) 1 : M₁)
⊢ Eq (α := R₁ →L[R₁] M₁) (toSpanSingleton R₁ 0) 0

Tactic:
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₁
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₁
⊢ Eq.{u_4 + 1} (α := M₁) ((toSpanSingleton R₁ 0 : (a : R₁) → M₁) 1 : M₁) ((0 : (a : R₁) → M₁) 1 : M₁)

Tactic:
simp
-- 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₁
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₁
x : M₁
⊢ (toSpanSingleton R₁ x : (a : R₁) → M₁) 1 = x

Tactic:
one_smul _ _

Premises used: one_smul
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₂ : Type u_6
inst_1 : TopologicalSpace M₂
inst_2 : AddCommMonoid M₂
inst_3 : Module R₁ M₂
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₂
c : R₁ →L[R₁] M₂
h :
  Eq.{u_6 + 1} (α := M₂) (((toSpanSingleton R₁ ((c : (a : R₁) → M₂) 1) : R₁ →L[R₁] M₂) : (a : R₁) → M₂) 1 : M₂)
    ((c : (a : R₁) → M₂) 1 : M₂)
⊢ toSpanSingleton R₁ ((c : (a : R₁) → M₂) 1) = c

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₂ : Type u_6
inst_1 : TopologicalSpace M₂
inst_2 : AddCommMonoid M₂
inst_3 : Module R₁ M₂
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₂
c : R₁ →L[R₁] M₂
⊢ Eq.{u_6 + 1} (α := M₂) (((toSpanSingleton R₁ ((c : (a : R₁) → M₂) 1) : R₁ →L[R₁] M₂) : (a : R₁) → M₂) 1 : M₂)
    ((c : (a : R₁) → M₂) 1 : M₂)

Tactic:
simp [← ContinuousLinearMap.map_smul_of_tower]

Premises used: ContinuousLinearMap.map_smul_of_tower
-- 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₁
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₁
inst_6 : ContinuousAdd M₁
x y : M₁
⊢ toSpanSingleton R₁ (x + y) = HAdd.hAdd (α := R₁ →L[R₁] M₁) (toSpanSingleton R₁ x) (toSpanSingleton R₁ y)

Tactic:
coe_inj.mp <| LinearMap.toSpanSingleton_add _ _

Premises used: ContinuousLinearMap.coe_inj, Iff.mp, LinearMap.toSpanSingleton_add
-- 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₁
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₁
α : Type u_9
inst_6 : Monoid α
inst_7 : DistribMulAction α M₁
inst_8 : ContinuousConstSMul α M₁
inst_9 : SMulCommClass R₁ α M₁
c : α
x : M₁
⊢ toSpanSingleton R₁ (c • x) = HSMul.hSMul (β := R₁ →L[R₁] M₁) c (toSpanSingleton R₁ x)

Tactic:
coe_inj.mp <| LinearMap.toSpanSingleton_smul _ _

Premises used: ContinuousLinearMap.coe_inj, LinearMap.toSpanSingleton_smul, Iff.mp
-- 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₁
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₁
⊢ Eq (α := (f : M₁) → R₁ →L[R₁] M₁) (smulRight (ContinuousLinearMap.id R₁ R₁)) (toSpanSingleton R₁)

Tactic:
rfl

Premises used: ContinuousLinearMap.smulRight, ContinuousLinearMap.toSpanSingleton, LinearMap.toSpanSingleton, 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₁
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₁
x : M₁
⊢ Eq (α := R₁ →L[R₁] M₁) (smulRight (S := R₁) 1 x) (toSpanSingleton R₁ x)

Tactic:
rfl

Premises used: ContinuousLinearMap.smulRight, ContinuousLinearMap.toSpanSingleton, LinearMap.toSpanSingleton, rfl