awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
f g : M →ₛₗ[σ] M₃
h : f = g
x : M
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : M) → M₃) x : M₃) ((g : (a : M) → M₃) x : M₃)

Tactic:
DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
f : M →ₛₗ[σ] M₃
h :
  ∀ (m : R) (x : M),
    AddHom.toFun (↑f : M →ₙ+ M₃) (m • x) =
      HSMul.hSMul.{u_5, u_11, u_11} (α := S) ((σ : (a : R) → S) m : S) (AddHom.toFun (↑f : M →ₙ+ M₃) x)
⊢ { toAddHom := (↑f : M →ₙ+ M₃), map_smul' := h : M →ₛₗ[σ] M₃ } = f

Tactic:
rfl

Premises used: AddHomClass.toAddHom, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
f : M →ₛₗ[σ] M₃
h : ∀ (m : R) (x : M), f.toFun (m • x) = HSMul.hSMul.{u_5, u_11, u_11} (α := S) ((σ : (a : R) → S) m : S) (f.toFun x)
⊢ { toAddHom := f.toAddHom, map_smul' := h : M →ₛₗ[σ] M₃ } = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
f : M →ₛₗ[σ] M₃
x y : M
⊢ (f : (a : M) → M₃) (x + y) = HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) x : M₃) ((f : (a : M) → M₃) y : M₃)

Tactic:
map_add f x y

Premises used: map_add
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
f : M →ₛₗ[σ] M₃
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : M) → M₃) 0 : M₃) (0 : M₃)

Tactic:
map_zero f

Premises used: map_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
f : M →ₛₗ[σ] M₃
c : R
x : M
⊢ (f : (a : M) → M₃) (c • x) =
    HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) c : S) ((f : (a : M) → M₃) x : M₃)

Tactic:
map_smulₛₗ f c x

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
fₗ : M →ₗ[R] M₂
c : R
x : M
⊢ (fₗ : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((fₗ : (a : M) → M₂) x : M₂)

Tactic:
map_smul fₗ c x

Premises used: map_smul
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
f : M →ₛₗ[σ] M₃
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
c : S
x : M
⊢ HSMul.hSMul (β := M₃) c ((f : (a : M) → M₃) x : M₃) =
    (f : (a : M) → M₃) (HSMul.hSMul.{u_1, u_8, u_8} (α := R) ((σ' : (a : S) → R) c : R) x)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
f : M →ₛₗ[σ] M₃
h : Injective.{u_8 + 1, u_11 + 1} (α := M) (β := M₃) (⇑f : (a : M) → M₃)
x : M
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : M) → M₃) x : M₃) (0 : M₃) ↔ x = 0

Tactic:
_root_.map_eq_zero_iff f h

Premises used: map_eq_zero_iff
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R_1 : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S_1 : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : Semiring R_1
inst_1 : Semiring S_1
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R_1 M
inst_7 : Module R_1 M₂
inst_8 : Module S_1 M₃
σ : R_1 →+* S_1
fₗ_1 : M →ₗ[R_1] M₂
f g : M →ₛₗ[σ] M₃
R : Type u_14
S : Type u_15
inst_9 : Semiring S
inst_10 : SMul R M
inst_11 : Module S M
inst_12 : SMul R M₂
inst_13 : Module S M₂
inst_14 : SMul R S
inst_15 : IsScalarTower R S M
inst_16 : IsScalarTower R S M₂
fₗ : M →ₗ[S] M₂
c : R
x : M
rw : (fₗ : (a : M) → M₂) (HSMul.hSMul (β := S) c 1 • x) = HSMul.hSMul (β := M₂) c ((fₗ : (a : M) → M₂) x : M₂)
rw₁ :
  (fₗ : (a : M) → M₂) (HSMul.hSMul (β := S) c 1 • x) =
    HSMul.hSMul (β := M₂) (HSMul.hSMul (β := S) c 1) ((fₗ : (a : M) → M₂) x : M₂)
rw₂ rw₃ :
  HSMul.hSMul (β := M₂) (HSMul.hSMul (β := S) c 1) ((fₗ : (a : M) → M₂) x : M₂) =
    HSMul.hSMul (β := M₂) (HSMul.hSMul (β := S) c 1) ((fₗ : (a : M) → M₂) x : M₂)
⊢ (fₗ : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((fₗ : (a : M) → M₂) x : M₂)

Tactic:
rw [← smul_one_smul S c x, ← smul_one_smul S c (fₗ x), map_smul]

Premises used: smul_one_smul, DFunLike.coe, map_smul
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
M : Type u_8
M₂ : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
R : Type u_14
S : Type u_15
inst_2 : Semiring S
inst_3 : SMul R M
inst_4 : Module S M
inst_5 : SMul R M₂
inst_6 : Module S M₂
inst_7 : CompatibleSMul M M₂ R S
fₗ : M →ₗ[S] M₂
c : R
x : M
⊢ (fₗ : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((fₗ : (a : M) → M₂) x : M₂)

Tactic:
CompatibleSMul.map_smul fₗ c x

Premises used: LinearMap.CompatibleSMul.map_smul
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
M : Type u_8
M₂ : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
R : Type u_14
S : Type u_15
inst_2 : Semiring S
inst_3 : SMul R M
inst_4 : Module S M
inst_5 : SMul R M₂
inst_6 : Module S M₂
F : Type u_16
inst_7 : CompatibleSMul M M₂ R S
inst_8 : FunLike F M M₂
inst_9 : LinearMapClass F S M M₂
fₗ : F
c : R
x : M
⊢ (fₗ : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((fₗ : (a : M) → M₂) x : M₂)

Tactic:
LinearMap.CompatibleSMul.map_smul (fₗ : M →ₗ[S] M₂) c x

Premises used: SemilinearMapClass.semilinearMap, LinearMap.CompatibleSMul.map_smul
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
M : Type u_8
M₂ : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
R : Type u_14
S : Type u_15
inst_2 : Semiring S
inst_3 : SMul R M
inst_4 : Module S M
inst_5 : SMul R M₂
inst_6 : Module S M₂
inst_7 : SMul R S
inst_8 : CompatibleSMul M M₂ R S
inst_9 : IsScalarTower R S M₂
f : M →ₗ[S] M₂
hf : Injective.{u_8 + 1, u_10 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
r : R
s : S
x : M
rw : (f : (a : M) → M₂) ((r • s) • x) = HSMul.hSMul (β := M₂) r ((f : (a : M) → M₂) (s • x) : M₂)
rw₁ :
  HSMul.hSMul (β := M₂) (r • s) ((f : (a : M) → M₂) x : M₂) = HSMul.hSMul (β := M₂) r ((f : (a : M) → M₂) (s • x) : M₂)
rw₂ :
  HSMul.hSMul (β := M₂) (r • s) ((f : (a : M) → M₂) x : M₂) = r • HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)
rw₃ rw₄ :
  r • HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂) = r • HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) ((r • s) • x) : M₂) ((f : (a : M) → M₂) (r • s • x) : M₂)

Tactic:
rw [f.map_smul_of_tower r, map_smul, map_smul, smul_assoc]

Premises used: smul_assoc, LinearMap.map_smul_of_tower, map_smul
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
F : Type u_16
M : Type u_17
N : Type u_18
inst : AddGroup M
inst_1 : AddGroup N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
c : ℤˣ
m : M
⊢ (f : (a : M) → N) (c • m) = HSMul.hSMul (β := N) c ((f : (a : M) → N) m : N)

Tactic:
simp [Units.smul_def]

Premises used: Units.smul_def
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M₁ : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
modM₁ : Module R M₁
modM₂ : Module S M₂
σ : R →+* S
f : M₁ →ₛₗ[σ] M₂
⊢ Eq (α := (a : M₁) → M₂) (⇑f.toAddMonoidHom : (a : M₁) → M₂) (⇑f : (a : M₁) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module S M
inst_7 : Module S M₂
inst_8 : CompatibleSMul M M₂ R S
f : M →ₗ[S] M₂
⊢ Eq (α := (a : M) → M₂)
    (⇑((↑R :
            {S : Type u_5} →
              {M : Type u_8} →
                {M₂ : Type u_10} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      (a : M) → M₂)
    (⇑f : (a : M) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M →ₗ[R] M₂
⊢ (↑R :
        {S : Type u_1} →
          {M : Type u_8} →
            {M₂ : Type u_10} →
              [inst : Semiring R] →
                [inst_5 : Semiring S] →
                  [inst_6 : AddCommMonoid M] →
                    [inst_7 : AddCommMonoid M₂] →
                      [inst_8 : Module R M] →
                        [inst_9 : Module R M₂] →
                          [inst_10 : Module S M] →
                            [inst_11 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f =
    f

Tactic:
rfl

Premises used: LinearMap.restrictScalars, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module S M
inst_7 : Module S M₂
inst_8 : CompatibleSMul M M₂ R S
fₗ : M →ₗ[S] M₂
x : M
⊢ Eq.{u_10 + 1} (α := M₂)
    (((↑R :
              {S : Type u_5} →
                {M : Type u_8} →
                  {M₂ : Type u_10} →
                    [inst : Semiring R] →
                      [inst_9 : Semiring S] →
                        [inst_10 : AddCommMonoid M] →
                          [inst_11 : AddCommMonoid M₂] →
                            [inst_12 : Module R M] →
                              [inst_13 : Module R M₂] →
                                [inst_14 : Module S M] →
                                  [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            fₗ :
          (a : M) → M₂)
        x :
      M₂)
    ((fₗ : (a : M) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module S M
inst_7 : Module S M₂
inst_8 : CompatibleSMul M M₂ R S
⊢ Injective (α := M →ₗ[S] M₂) (β := M →ₗ[R] M₂)
    (↑R :
      {S : Type u_5} →
        {M : Type u_8} →
          {M₂ : Type u_10} →
            [inst : Semiring R] →
              [inst_9 : Semiring S] →
                [inst_10 : AddCommMonoid M] →
                  [inst_11 : AddCommMonoid M₂] →
                    [inst_12 : Module R M] →
                      [inst_13 : Module R M₂] →
                        [inst_14 : Module S M] →
                          [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)

Tactic:
fun _ _ h ↦
  ext (LinearMap.congr_fun h :)

Premises used: LinearMap.ext, LinearMap.congr_fun, Function.Injective
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module S M
inst_7 : Module S M₂
inst_8 : CompatibleSMul M M₂ R S
fₗ gₗ : M →ₗ[S] M₂
⊢ Eq (α := M →ₗ[R] M₂)
      ((↑R :
          {S : Type u_5} →
            {M : Type u_8} →
              {M₂ : Type u_10} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        fₗ)
      ((↑R :
          {S : Type u_5} →
            {M : Type u_8} →
              {M₂ : Type u_10} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        gₗ) ↔
    fₗ = gₗ

Tactic:
(restrictScalars_injective R).eq_iff

Premises used: Function.Injective.eq_iff, LinearMap.restrictScalars_injective
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : CompatibleSMul M M R S
⊢ Eq.{u_8 + 1} (α := M →ₗ[R] M)
    ((↑R :
        {S : Type u_5} →
          {M M₂ : Type u_8} →
            [inst : Semiring R] →
              [inst_6 : Semiring S] →
                [inst_7 : AddCommMonoid M] →
                  [inst_8 : AddCommMonoid M₂] →
                    [inst_9 : Module R M] →
                      [inst_10 : Module R M₂] →
                        [inst_11 : Module S M] →
                          [inst_12 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := S) id)
    id

Tactic:
rfl

Premises used: LinearMap.restrictScalars, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
⊢ Injective (α := M →ₛₗ[σ] M₃) toAddMonoidHom

Tactic:
fun fₗ gₗ h ↦
  ext <| (DFunLike.congr_fun h : ∀ x, fₗ.toAddMonoidHom x = gₗ.toAddMonoidHom x)

Premises used: DFunLike.congr_fun, LinearMap.ext, Function.Injective
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₃
inst_3 : Module S M₃
σ : R →+* S
f g : R →ₛₗ[σ] M₃
h : Eq.{u_11 + 1} (α := M₃) ((f : (a : R) → M₃) 1 : M₃) ((g : (a : R) → M₃) 1 : M₃)
x : R
rw : Eq.{u_11 + 1} (α := M₃) ((f : (a : R) → M₃) (x * 1) : M₃) ((g : (a : R) → M₃) (x * 1) : M₃)
rw₁ :
  Eq.{u_11 + 1} (α := M₃) ((f : (a : R) → M₃) (HSMul.hSMul (β := R) x 1) : M₃)
    ((g : (a : R) → M₃) (HSMul.hSMul (β := R) x 1) : M₃)
rw₂ :
  HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) x : S) ((f : (a : R) → M₃) 1 : M₃) =
    (g : (a : R) → M₃) (HSMul.hSMul (β := R) x 1)
rw₃ :
  HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) x : S) ((f : (a : R) → M₃) 1 : M₃) =
    HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) x : S) ((g : (a : R) → M₃) 1 : M₃)
rw₄ rw₅ :
  HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) x : S) ((g : (a : R) → M₃) 1 : M₃) =
    HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) x : S) ((g : (a : R) → M₃) 1 : M₃)
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : R) → M₃) x : M₃) ((g : (a : R) → M₃) x : M₃)

Tactic:
rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]

Premises used: LinearMap.map_smulₛₗ, smul_eq_mul, mul_one
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
⊢ Eq (α := (a : R) → S) (⇑f.toSemilinearMap : (a : R) → S) (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring R₁
inst_3 : Semiring R₂
inst_4 : Semiring R₃
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₂
inst_8 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₂] M₂
⊢ ∀ (x y : M₁),
    (f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) (x + y) : M₂) =
      HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) x : M₂) : M₃)
        ((f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) y : M₂) : M₃)

Tactic:
simp only [map_add, forall_const]

Premises used: map_add, forall_const
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring R₁
inst_3 : Semiring R₂
inst_4 : Semiring R₃
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₂
inst_8 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₂] M₂
r : R₁
x : M₁
⊢ (f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) (r • x) : M₂) =
    HSMul.hSMul.{u_4, u_11, u_11} (α := R₃) (β := M₃) ((σ₁₃ : (a : R₁) → R₃) r : R₃)
      ((f : (a : M₂) → M₃) ((g : (a : M₁) → M₂) x : M₂) : M₃)

Tactic:
simp only [map_smulₛₗ _, RingHomCompTriple.comp_apply]

Premises used: MulActionSemiHomClass.map_smulₛₗ, RingHomCompTriple.comp_apply
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₂] M₂
x : M₁
⊢ Eq.{u_11 + 1} (α := 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.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₂] M₂
⊢ Eq (α := (a : M₁) → M₃) (⇑(f ∘ₛₗ g) : (a : M₁) → M₃)
    (Function.comp.{u_9 + 1, u_10 + 1, u_11 + 1} (β := M₂) (⇑f : (a : M₂) → M₃) (⇑g : (a : M₁) → M₂))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₂ : Type u_3
R₃ : Type u_4
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R₂
inst_1 : Semiring R₃
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₂₃ : R₂ →+* R₃
f : M₂ →ₛₗ[σ₂₃] M₃
⊢ f ∘ₛₗ id = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₂ : Type u_3
R₃ : Type u_4
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R₂
inst_1 : Semiring R₃
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₂₃ : R₂ →+* R₃
f : M₂ →ₛₗ[σ₂₃] M₃
⊢ id ∘ₛₗ f = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
R₄ : Type u_14
M₄ : Type u_15
inst_7 : Semiring R₄
inst_8 : AddCommMonoid M₄
inst_9 : Module R₄ M₄
σ₃₄ : R₃ →+* R₄
σ₂₄ : R₂ →+* R₄
σ₁₄ : R₁ →+* R₄
inst_10 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst_11 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst_12 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
f : M₁ →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
h : M₃ →ₛₗ[σ₃₄] M₄
⊢ (h ∘ₛₗ g) ∘ₛₗ f = h ∘ₛₗ g ∘ₛₗ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₁ →ₛₗ[σ₁₂] M₂
hg : Surjective.{u_9 + 1, u_10 + 1} (α := M₁) (β := M₂) (⇑g : (a : M₁) → M₂)
⊢ Injective (β := M₁ →ₛₗ[σ₁₃] M₃) fun (f : M₂ →ₛₗ[σ₂₃] M₃) ↦ f ∘ₛₗ g

Tactic:
fun _ _ h ↦ ext <| hg.forall.2 (LinearMap.ext_iff.1 h)

Premises used: Iff.mpr, Function.Surjective.forall, LinearMap.ext, LinearMap.ext_iff, Iff.mp, Function.Injective
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₂] M₂
f' : M₂ →ₛₗ[σ₂₃] M₃
hg : Surjective.{u_9 + 1, u_10 + 1} (α := M₁) (β := M₂) (⇑g : (a : M₁) → M₂)
⊢ f ∘ₛₗ g = f' ∘ₛₗ g ↔ f = f'

Tactic:
hg.injective_linearMapComp_right.eq_iff

Premises used: Function.Injective.eq_iff, Function.Surjective.injective_linearMapComp_right