awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
c : R
n : ℕ
ihn : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n = toSpanSingleton R (c ^ n)
succ : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n * toSpanSingleton R c = toSpanSingleton R (c ^ (n + 1))
succ₁ : HMul.hMul (α := R →L[R] R) (toSpanSingleton R (c ^ n)) (toSpanSingleton R c) = toSpanSingleton R (c ^ (n + 1))
succ₂ : Eq (α := R →L[R] R) (toSpanSingleton R (c ^ n) ∘SL toSpanSingleton R c) (toSpanSingleton R (c ^ (n + 1)))
succ₃ : Eq (α := R →L[R] R) (toSpanSingleton R (c • c ^ n)) (toSpanSingleton R (c ^ (n + 1)))
succ₄ : Eq (α := R →L[R] R) (toSpanSingleton R (c * c ^ n)) (toSpanSingleton R (c ^ (n + 1)))
succ₅ succ₆ : Eq (α := R →L[R] R) (toSpanSingleton R (c * c ^ n)) (toSpanSingleton R (c * c ^ n))
⊢ HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) (n + 1) = toSpanSingleton R (c ^ (n + 1))

Tactic:
rw [pow_succ, ihn, mul_def, toSpanSingleton_comp_toSpanSingleton, smul_eq_mul, pow_succ']

Premises used: pow_succ, ContinuousLinearMap.toSpanSingleton_comp_toSpanSingleton, ContinuousLinearMap.mul_def, smul_eq_mul, pow_succ'
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
c : R
n : ℕ
zero : HPow.hPow (α := R →L[R] R) (β := ℕ) (toSpanSingleton R c) 0 = toSpanSingleton R (HPow.hPow (β := ℕ) c 0)
succ :
  ∀ (n : ℕ) (ihn : HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n = toSpanSingleton R (c ^ n)),
    HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) (n + 1) = toSpanSingleton R (c ^ (n + 1))
⊢ HPow.hPow (α := R →L[R] R) (toSpanSingleton R c) n = toSpanSingleton R (c ^ n)

Tactic:
induction n with
  | zero => ext; simp
  | succ n ihn =>
    rw [pow_succ, ihn, mul_def, toSpanSingleton_comp_toSpanSingleton, smul_eq_mul, pow_succ']

Premises used: pow_succ, ContinuousLinearMap.zero, ContinuousLinearMap.toSpanSingleton_comp_toSpanSingleton, ContinuousLinearMap.mul_def, smul_eq_mul, pow_succ'
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
M : Type u_2
inst : TopologicalSpace R
inst_1 : DivisionRing R
inst_2 : ContinuousSub R
inst_3 : AddCommGroup M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : Module R M
inst_7 : ContinuousSMul R M
f : StrongDual R M
hf : f ≠ 0
x : M
hx : Ne.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (0 : R)
y : M
⊢ Continuous[inst, inst_4] fun (a : R) ↦
    y +
      HSub.hSub (β := R) a ((f : (a : M) → R) y : R) •
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (((f : (a : M) → R) x)⁻¹ : R) x

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
M : Type u_2
inst : TopologicalSpace R
inst_1 : DivisionRing R
inst_2 : ContinuousSub R
inst_3 : AddCommGroup M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : Module R M
inst_7 : ContinuousSMul R M
f : StrongDual R M
hf : f ≠ 0
x : M
hx : Ne.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (0 : R)
y : M
⊢ (fun (a : R) ↦
        y +
          HSub.hSub (β := R) a ((f : (a : M) → R) y : R) •
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) (((f : (a : M) → R) x)⁻¹ : R) x)
      ((f : (a : M) → R) y) =
    y

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
M : Type u_2
inst : TopologicalSpace R
inst_1 : DivisionRing R
inst_2 : ContinuousSub R
inst_3 : AddCommGroup M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : Module R M
inst_7 : ContinuousSMul R M
f : StrongDual R M
hf : f ≠ 0
x : M
hx : Ne.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (0 : R)
y : M
a : R
⊢ (f : (a : M) → R)
      ((fun (a : R) ↦
          y +
            HSub.hSub (β := R) a ((f : (a : M) → R) y : R) •
              HSMul.hSMul.{u_1, u_2, u_2} (α := R) (((f : (a : M) → R) x)⁻¹ : R) x)
        a) =
    a

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
S₃ : Type u_5
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Monoid S₃
M : Type u_6
inst_4 : TopologicalSpace M
inst_5 : AddCommMonoid M
inst_6 : Module R M
M₂ : Type u_7
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
inst_9 : Module R₂ M₂
M₃ : Type u_8
inst_10 : TopologicalSpace M₃
inst_11 : AddCommMonoid M₃
inst_12 : Module R₃ M₃
inst_13 : DistribMulAction S₃ M₃
inst_14 : SMulCommClass R₃ S₃ M₃
inst_15 : ContinuousConstSMul S₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_16 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
c : S₃
h : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
⊢ (c • h) ∘SL f = c • h ∘SL f

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
S : Type u_4
inst : Semiring R
inst_1 : Monoid S
M : Type u_6
inst_2 : TopologicalSpace M
inst_3 : AddCommMonoid M
inst_4 : Module R M
N₂ : Type u_9
inst_5 : TopologicalSpace N₂
inst_6 : AddCommMonoid N₂
inst_7 : Module R N₂
N₃ : Type u_10
inst_8 : TopologicalSpace N₃
inst_9 : AddCommMonoid N₃
inst_10 : Module R N₃
inst_11 : DistribMulAction S N₃
inst_12 : SMulCommClass R S N₃
inst_13 : ContinuousConstSMul S N₃
inst_14 : DistribMulAction S N₂
inst_15 : ContinuousConstSMul S N₂
inst_16 : SMulCommClass R S N₂
inst_17 : LinearMap.CompatibleSMul N₂ N₃ S R
hₗ : N₂ →L[R] N₃
c : S
fₗ : M →L[R] N₂
h : ∀ (x : M), Eq.{u_10 + 1} (α := N₃) ((hₗ ∘SL (c • fₗ) : (a : M) → N₃) x : N₃) ((c • hₗ ∘SL fₗ : (a : M) → N₃) x : N₃)
⊢ hₗ ∘SL (c • fₗ) = c • hₗ ∘SL fₗ

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
S : Type u_4
inst : Semiring R
inst_1 : Monoid S
M : Type u_6
inst_2 : TopologicalSpace M
inst_3 : AddCommMonoid M
inst_4 : Module R M
N₂ : Type u_9
inst_5 : TopologicalSpace N₂
inst_6 : AddCommMonoid N₂
inst_7 : Module R N₂
N₃ : Type u_10
inst_8 : TopologicalSpace N₃
inst_9 : AddCommMonoid N₃
inst_10 : Module R N₃
inst_11 : DistribMulAction S N₃
inst_12 : SMulCommClass R S N₃
inst_13 : ContinuousConstSMul S N₃
inst_14 : DistribMulAction S N₂
inst_15 : ContinuousConstSMul S N₂
inst_16 : SMulCommClass R S N₂
inst_17 : LinearMap.CompatibleSMul N₂ N₃ S R
hₗ : N₂ →L[R] N₃
c : S
fₗ : M →L[R] N₂
x : M
⊢ Eq.{u_10 + 1} (α := N₃) ((hₗ ∘SL (c • fₗ) : (a : M) → N₃) x : N₃) ((c • hₗ ∘SL fₗ : (a : M) → N₃) x : N₃)

Tactic:
hₗ.map_smul_of_tower c (fₗ x)

Premises used: ContinuousLinearMap.map_smul_of_tower, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
S : Type u_4
inst : Semiring R
inst_1 : Monoid S
M : Type u_6
inst_2 : TopologicalSpace M
inst_3 : AddCommMonoid M
inst_4 : Module R M
N₂ : Type u_9
inst_5 : TopologicalSpace N₂
inst_6 : AddCommMonoid N₂
inst_7 : Module R N₂
N₃ : Type u_10
inst_8 : TopologicalSpace N₃
inst_9 : AddCommMonoid N₃
inst_10 : Module R N₃
inst_11 : DistribMulAction S N₃
inst_12 : SMulCommClass R S N₃
inst_13 : ContinuousConstSMul S N₃
inst_14 : DistribMulAction S N₂
inst_15 : ContinuousConstSMul S N₂
inst_16 : SMulCommClass R S N₂
inst_17 : LinearMap.CompatibleSMul N₂ N₃ S R
hₗ : N₂ →L[R] N₃
c : S
fₗ : M →L[R] N₂
x : M
⊢ Eq.{u_10 + 1} (α := N₃) ((hₗ ∘SL (c • fₗ) : (a : M) → N₃) x : N₃) ((c • hₗ ∘SL fₗ : (a : M) → N₃) x : N₃)

Tactic:
exact hₗ.map_smul_of_tower c (fₗ x)

Premises used: ContinuousLinearMap.map_smul_of_tower, 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₃
M : Type u_6
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
M₂ : Type u_7
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
M₃ : Type u_8
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
inst_11 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : SMulCommClass R₂ R₂ M₂
inst_14 : SMulCommClass R₃ R₃ M₃
inst_15 : ContinuousConstSMul R₂ M₂
inst_16 : ContinuousConstSMul R₃ M₃
h : M₂ →SL[σ₂₃] M₃
c : R₂
f : M →SL[σ₁₂] M₂
h₁ :
  ∀ (x : M),
    Eq.{u_8 + 1} (α := M₃) ((h ∘SL (c • f) : (a : M) → M₃) x : M₃)
      ((HSMul.hSMul (α := R₃) ((σ₂₃ : (a : R₂) → R₃) c : R₃) (h ∘SL f) : (a : M) → M₃) x : M₃)
⊢ h ∘SL (c • f) = HSMul.hSMul (α := R₃) ((σ₂₃ : (a : R₂) → R₃) c : R₃) (h ∘SL f)

Tactic:
ext x
-- 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₃
M : Type u_6
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M
inst_5 : Module R M
M₂ : Type u_7
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R₂ M₂
M₃ : Type u_8
inst_9 : TopologicalSpace M₃
inst_10 : AddCommMonoid M₃
inst_11 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_13 : SMulCommClass R₂ R₂ M₂
inst_14 : SMulCommClass R₃ R₃ M₃
inst_15 : ContinuousConstSMul R₂ M₂
inst_16 : ContinuousConstSMul R₃ M₃
h : M₂ →SL[σ₂₃] M₃
c : R₂
f : M →SL[σ₁₂] M₂
x : M
⊢ Eq.{u_8 + 1} (α := M₃) ((h ∘SL (c • f) : (a : M) → M₃) x : M₃)
    ((HSMul.hSMul (α := R₃) ((σ₂₃ : (a : R₂) → R₃) c : R₃) (h ∘SL f) : (a : M) → M₃) x : M₃)

Tactic:
simp only [coe_smul', coe_comp', Function.comp_apply, Pi.smul_apply, map_smulₛₗ]

Premises used: ContinuousLinearMap.coe_comp', ContinuousLinearMap.coe_smul', MulActionSemiHomClass.map_smulₛₗ, Function.comp_apply, Pi.smul_apply
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid U
inst_2 : Module R U
inst_3 : TopologicalSpace U
inst_4 : AddCommMonoid V
inst_5 : Module R V
inst_6 : TopologicalSpace V
inst_7 : AddCommMonoid W
inst_8 : Module R W
inst_9 : TopologicalSpace W
inst_10 : ContinuousAdd W
inst_11 : ContinuousConstSMul R W
f : U →L[R] V
x x_1 : V →L[R] W
⊢ (x + x_1) ∘SL f = x ∘SL f + x_1 ∘SL f

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid U
inst_2 : Module R U
inst_3 : TopologicalSpace U
inst_4 : AddCommMonoid V
inst_5 : Module R V
inst_6 : TopologicalSpace V
inst_7 : AddCommMonoid W
inst_8 : Module R W
inst_9 : TopologicalSpace W
inst_10 : ContinuousAdd W
inst_11 : ContinuousConstSMul R W
f : U →L[R] V
x : R
x_1 : V →L[R] W
⊢ (x • x_1) ∘SL f = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (x_1 ∘SL f)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid U
inst_2 : Module R U
inst_3 : TopologicalSpace U
inst_4 : AddCommMonoid V
inst_5 : Module R V
inst_6 : TopologicalSpace V
inst_7 : ContinuousAdd V
inst_8 : ContinuousConstSMul R V
inst_9 : AddCommMonoid W
inst_10 : Module R W
inst_11 : TopologicalSpace W
inst_12 : ContinuousAdd W
inst_13 : ContinuousConstSMul R W
x x_1 : U →L[R] V
h :
  ∀ (x_2 : V →L[R] W) (x_3 : U),
    Eq.{u_4 + 1} (α := W) ((((lcomp W (x + x_1) : (a : V →L[R] W) → U →L[R] W) x_2 : U →L[R] W) : (a : U) → W) x_3 : W)
      ((((HAdd.hAdd (α := (V →L[R] W) →ₗ[R] U →L[R] W) (lcomp W x) (lcomp W x_1) : (a : V →L[R] W) → U →L[R] W) x_2 :
              U →L[R] W) :
            (a : U) → W)
          x_3 :
        W)
⊢ lcomp W (x + x_1) = HAdd.hAdd (α := (V →L[R] W) →ₗ[R] U →L[R] W) (lcomp W x) (lcomp W x_1)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid U
inst_2 : Module R U
inst_3 : TopologicalSpace U
inst_4 : AddCommMonoid V
inst_5 : Module R V
inst_6 : TopologicalSpace V
inst_7 : ContinuousAdd V
inst_8 : ContinuousConstSMul R V
inst_9 : AddCommMonoid W
inst_10 : Module R W
inst_11 : TopologicalSpace W
inst_12 : ContinuousAdd W
inst_13 : ContinuousConstSMul R W
x x_1 : U →L[R] V
x_2 : V →L[R] W
x_3 : U
⊢ Eq.{u_4 + 1} (α := W) ((((lcomp W (x + x_1) : (a : V →L[R] W) → U →L[R] W) x_2 : U →L[R] W) : (a : U) → W) x_3 : W)
    ((((HAdd.hAdd (α := (V →L[R] W) →ₗ[R] U →L[R] W) (lcomp W x) (lcomp W x_1) : (a : V →L[R] W) → U →L[R] W) x_2 :
            U →L[R] W) :
          (a : U) → W)
        x_3 :
      W)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid U
inst_2 : Module R U
inst_3 : TopologicalSpace U
inst_4 : AddCommMonoid V
inst_5 : Module R V
inst_6 : TopologicalSpace V
inst_7 : ContinuousAdd V
inst_8 : ContinuousConstSMul R V
inst_9 : AddCommMonoid W
inst_10 : Module R W
inst_11 : TopologicalSpace W
inst_12 : ContinuousAdd W
inst_13 : ContinuousConstSMul R W
x : R
x_1 : U →L[R] V
h :
  ∀ (x_2 : V →L[R] W) (x_3 : U),
    Eq.{u_4 + 1} (α := W) ((((lcomp W (x • x_1) : (a : V →L[R] W) → U →L[R] W) x_2 : U →L[R] W) : (a : U) → W) x_3 : W)
      ((((HSMul.hSMul (α := R) (β := (V →L[R] W) →ₗ[R] U →L[R] W) ((RingHom.id R : (a : R) → R) x : R) (lcomp W x_1) :
                  (a : V →L[R] W) → U →L[R] W)
                x_2 :
              U →L[R] W) :
            (a : U) → W)
          x_3 :
        W)
⊢ lcomp W (x • x_1) =
    HSMul.hSMul (α := R) (β := (V →L[R] W) →ₗ[R] U →L[R] W) ((RingHom.id R : (a : R) → R) x : R) (lcomp W x_1)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid U
inst_2 : Module R U
inst_3 : TopologicalSpace U
inst_4 : AddCommMonoid V
inst_5 : Module R V
inst_6 : TopologicalSpace V
inst_7 : ContinuousAdd V
inst_8 : ContinuousConstSMul R V
inst_9 : AddCommMonoid W
inst_10 : Module R W
inst_11 : TopologicalSpace W
inst_12 : ContinuousAdd W
inst_13 : ContinuousConstSMul R W
x : R
x_1 : U →L[R] V
x_2 : V →L[R] W
x_3 : U
⊢ Eq.{u_4 + 1} (α := W) ((((lcomp W (x • x_1) : (a : V →L[R] W) → U →L[R] W) x_2 : U →L[R] W) : (a : U) → W) x_3 : W)
    ((((HSMul.hSMul (α := R) (β := (V →L[R] W) →ₗ[R] U →L[R] W) ((RingHom.id R : (a : R) → R) x : R) (lcomp W x_1) :
                (a : V →L[R] W) → U →L[R] W)
              x_2 :
            U →L[R] W) :
          (a : U) → W)
        x_3 :
      W)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass R S M
inst_6 : TopologicalSpace M
inst_7 : ContinuousAdd M
inst_8 : ContinuousConstSMul S M
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R M
x : M
⊢ (fun (f : R →L[R] M) ↦ ((f : (a : R) → M) 1 : M)) (toSpanSingleton R x) = x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass R S M
inst_6 : TopologicalSpace M
inst_7 : ContinuousAdd M
inst_8 : ContinuousConstSMul S M
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R M
f : R →L[R] M
h :
  Eq.{u_3 + 1} (α := M) ((toSpanSingleton R ((fun (f : R →L[R] M) ↦ ((f : (a : R) → M) 1 : M)) f) : (a : R) → M) 1 : M)
    ((f : (a : R) → M) 1 : M)
⊢ toSpanSingleton R ((fun (f : R →L[R] M) ↦ ((f : (a : R) → M) 1 : M)) f) = f

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass R S M
inst_6 : TopologicalSpace M
inst_7 : ContinuousAdd M
inst_8 : ContinuousConstSMul S M
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R M
f : R →L[R] M
⊢ Eq.{u_3 + 1} (α := M) ((toSpanSingleton R ((fun (f : R →L[R] M) ↦ ((f : (a : R) → M) 1 : M)) f) : (a : R) → M) 1 : M)
    ((f : (a : R) → M) 1 : M)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Module R S
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₂
inst_6 : Module S M₂
inst_7 : IsScalarTower R S M₂
inst_8 : TopologicalSpace S
inst_9 : TopologicalSpace M₂
inst_10 : ContinuousSMul S M₂
inst_11 : TopologicalSpace M
inst_12 : AddCommMonoid M
inst_13 : Module R M
inst_14 : ContinuousAdd M₂
inst_15 : Module T M₂
inst_16 : ContinuousConstSMul T M₂
inst_17 : SMulCommClass R T M₂
inst_18 : SMulCommClass S T M₂
c : M →L[R] S
x y : M₂
h :
  ∀ (e : M),
    Eq.{u_5 + 1} (α := M₂) ((c.smulRight (x + y) : (a : M) → M₂) e : M₂)
      ((HAdd.hAdd (α := M →L[R] M₂) (c.smulRight x) (c.smulRight y) : (a : M) → M₂) e : M₂)
⊢ c.smulRight (x + y) = HAdd.hAdd (α := M →L[R] M₂) (c.smulRight x) (c.smulRight y)

Tactic:
ext e
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Module R S
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₂
inst_6 : Module S M₂
inst_7 : IsScalarTower R S M₂
inst_8 : TopologicalSpace S
inst_9 : TopologicalSpace M₂
inst_10 : ContinuousSMul S M₂
inst_11 : TopologicalSpace M
inst_12 : AddCommMonoid M
inst_13 : Module R M
inst_14 : ContinuousAdd M₂
inst_15 : Module T M₂
inst_16 : ContinuousConstSMul T M₂
inst_17 : SMulCommClass R T M₂
inst_18 : SMulCommClass S T M₂
c : M →L[R] S
x y : M₂
e : M
⊢ Eq.{u_5 + 1} (α := M₂) ((c.smulRight (x + y) : (a : M) → M₂) e : M₂)
    ((HAdd.hAdd (α := M →L[R] M₂) (c.smulRight x) (c.smulRight y) : (a : M) → M₂) e : M₂)

Tactic:
apply smul_add (c e)

Premises used: DFunLike.coe, smul_add
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Module R S
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₂
inst_6 : Module S M₂
inst_7 : IsScalarTower R S M₂
inst_8 : TopologicalSpace S
inst_9 : TopologicalSpace M₂
inst_10 : ContinuousSMul S M₂
inst_11 : TopologicalSpace M
inst_12 : AddCommMonoid M
inst_13 : Module R M
inst_14 : ContinuousAdd M₂
inst_15 : Module T M₂
inst_16 : ContinuousConstSMul T M₂
inst_17 : SMulCommClass R T M₂
inst_18 : SMulCommClass S T M₂
c : M →L[R] S
a : T
x : M₂
h :
  ∀ (e : M),
    Eq.{u_5 + 1} (α := M₂) ((c.smulRight (a • x) : (a : M) → M₂) e : M₂)
      ((HSMul.hSMul (α := T) (β := M →L[R] M₂) ((RingHom.id T : (a : T) → T) a : T) (c.smulRight x) : (a : M) → M₂) e :
        M₂)
⊢ c.smulRight (a • x) = HSMul.hSMul (α := T) (β := M →L[R] M₂) ((RingHom.id T : (a : T) → T) a : T) (c.smulRight x)

Tactic:
ext e
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Module R S
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₂
inst_6 : Module S M₂
inst_7 : IsScalarTower R S M₂
inst_8 : TopologicalSpace S
inst_9 : TopologicalSpace M₂
inst_10 : ContinuousSMul S M₂
inst_11 : TopologicalSpace M
inst_12 : AddCommMonoid M
inst_13 : Module R M
inst_14 : ContinuousAdd M₂
inst_15 : Module T M₂
inst_16 : ContinuousConstSMul T M₂
inst_17 : SMulCommClass R T M₂
inst_18 : SMulCommClass S T M₂
c : M →L[R] S
a : T
x : M₂
e : M
h :
  HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((c : (a : M) → S) e : S) (a • x) =
    a • HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((c : (a : M) → S) e : S) x
⊢ Eq.{u_5 + 1} (α := M₂) ((c.smulRight (a • x) : (a : M) → M₂) e : M₂)
    ((HSMul.hSMul (α := T) (β := M →L[R] M₂) ((RingHom.id T : (a : T) → T) a : T) (c.smulRight x) : (a : M) → M₂) e :
      M₂)

Tactic:
dsimp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Module R S
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₂
inst_6 : Module S M₂
inst_7 : IsScalarTower R S M₂
inst_8 : TopologicalSpace S
inst_9 : TopologicalSpace M₂
inst_10 : ContinuousSMul S M₂
inst_11 : TopologicalSpace M
inst_12 : AddCommMonoid M
inst_13 : Module R M
inst_14 : ContinuousAdd M₂
inst_15 : Module T M₂
inst_16 : ContinuousConstSMul T M₂
inst_17 : SMulCommClass R T M₂
inst_18 : SMulCommClass S T M₂
c : M →L[R] S
a : T
x : M₂
e : M
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((c : (a : M) → S) e : S) (a • x) =
    a • HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((c : (a : M) → S) e : S) x

Tactic:
apply smul_comm

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Module R S
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₂
inst_6 : Module S M₂
inst_7 : IsScalarTower R S M₂
inst_8 : TopologicalSpace S
inst_9 : TopologicalSpace M₂
inst_10 : ContinuousSMul S M₂
inst_11 : TopologicalSpace M
inst_12 : AddCommMonoid M
inst_13 : Module R M
inst_14 : ContinuousAdd M₂
inst_15 : Module T M₂
inst_16 : ContinuousConstSMul T M₂
inst_17 : SMulCommClass R T M₂
inst_18 : SMulCommClass S T M₂
c : M →L[R] S
⊢ Eq (α := (a : M₂) → M →L[R] M₂) (⇑c.smulRightₗ : (a : M₂) → M →L[R] M₂) c.smulRight

Tactic:
rfl

Premises used: ContinuousLinearMap.smulRight, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : CommSemiring S
inst_5 : Module S M
inst_6 : SMulCommClass R S M
inst_7 : SMul S R
inst_8 : IsScalarTower S R M
inst_9 : ContinuousConstSMul S M
inst_10 : IsTopologicalAddGroup M
r : S
m : M
⊢ (((algebraMap S (M →L[R] M) : (a : S) → M →L[R] M) r : M →L[R] M) : (a : M) → M) m = r • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : AddCommMonoid E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : ContinuousConstSMul 𝕜 𝕜
v : E →L[𝕜] 𝕜
x : E
⊢ Eq.{u_1 + 1} (α := 𝕜) ((((topDualPairing 𝕜 E : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜) v : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) x : 𝕜)
    ((v : (a : E) → 𝕜) x : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
f : M →L[R] M
⊢ IsIdempotentElem (↑f : M →ₗ[R] M) ↔ IsIdempotentElem f

Tactic:
simp only [IsIdempotentElem, Module.End.mul_eq_comp, ← coe_comp, mul_def, coe_inj]

Premises used: Module.End.mul_eq_comp, ContinuousLinearMap.coe_inj, ContinuousLinearMap.coe_comp, IsIdempotentElem, ContinuousLinearMap.mul_def
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
p q : M →L[R] M
hp : IsIdempotentElem p
hq : IsIdempotentElem q
⊢ p = q ↔ (↑p : M →ₗ[R] M).range = (↑q : M →ₗ[R] M).range ∧ (↑p : M →ₗ[R] M).ker = (↑q : M →ₗ[R] M).ker

Tactic:
simpa using LinearMap.IsIdempotentElem.ext_iff hp.toLinearMap hq.toLinearMap

Premises used: LinearMap.IsIdempotentElem.ext_iff, ContinuousLinearMap.IsIdempotentElem.toLinearMap
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
f T : M →L[R] M
hf : IsIdempotentElem f
⊢ (↑f : M →ₗ[R] M).range ∈ Module.End.invtSubmodule (↑T : M →ₗ[R] M) ↔ f ∘SL T ∘SL f = T ∘SL f

Tactic:
simpa [← ContinuousLinearMap.coe_comp] using
    LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff (T := T) hf.toLinearMap

Premises used: ContinuousLinearMap.IsIdempotentElem.toLinearMap, ContinuousLinearMap.coe_comp, LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff