awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
M : Type u_8
M₂ : Type u_10
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
f : M →+ M₂
⊢ Eq (α := (a : M) → M₂) (⇑f.toIntLinearMap : (a : M) → M₂) (⇑f : (a : M) → M₂)

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 R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : DistribSMul S M₂
inst_7 : SMulCommClass R₂ S M₂
inst_8 : DistribSMul T M₂
inst_9 : SMulCommClass R₂ T M₂
a : S
f : M →ₛₗ[σ₁₂] M₂
x y : M
⊢ HSMul.hSMul (β := (a : M) → M₂) a (⇑f : (a : M) → M₂) (x + y) =
    HSMul.hSMul (β := (a : M) → M₂) a (⇑f : (a : M) → M₂) x + HSMul.hSMul (β := (a : M) → M₂) a (⇑f : (a : M) → M₂) y

Tactic:
simp only [Pi.smul_apply, f.map_add, smul_add]

Premises used: LinearMap.map_add, smul_add, Pi.smul_apply
-- 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 R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : DistribSMul S M₂
inst_7 : SMulCommClass R₂ S M₂
inst_8 : DistribSMul T M₂
inst_9 : SMulCommClass R₂ T M₂
a : S
f : M →ₛₗ[σ₁₂] M₂
c : R
x : M
⊢ HSMul.hSMul (β := (a : M) → M₂) a (⇑f : (a : M) → M₂) (c • x) =
    HSMul.hSMul.{u_3, u_10, u_10} (α := R₂) ((σ₁₂ : (a : R) → R₂) c : R₂)
      (HSMul.hSMul (β := (a : M) → M₂) a (⇑f : (a : M) → M₂) x)

Tactic:
simp [Pi.smul_apply, smul_comm]

Premises used: SMulCommClass.smul_comm, Pi.smul_apply
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
R₂ : Type u_3
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : DistribSMul S M₂
inst_7 : SMulCommClass R₂ S M₂
a : S
f : M →ₛₗ[σ₁₂] M₂
x : M
⊢ (a • f : (a : M) → M₂) x = HSMul.hSMul (β := M₂) a ((f : (a : M) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
R₂ : Type u_3
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : DistribSMul S M₂
inst_7 : SMulCommClass R₂ S M₂
a : S
f : M →ₛₗ[σ₁₂] M₂
⊢ (⇑(a • f) : (a : M) → M₂) = HSMul.hSMul (β := (a : M) → M₂) a (⇑f : (a : M) → M₂)

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 R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
inst_6 : DistribSMul S M₂
inst_7 : SMulCommClass R₂ S M₂
inst_8 : DistribSMul T M₂
inst_9 : SMulCommClass R₂ T M₂
inst_10 : SMulCommClass S T M₂
⊢ SMulCommClass S T (M →ₛₗ[σ₁₂] M₂)

Tactic:
⟨fun _ _ _ ↦ ext fun _ ↦ smul_comm _ _ _⟩

Premises used: LinearMap.ext, SMulCommClass.smul_comm, SMulCommClass.mk, DFunLike.coe
-- 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 R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
⊢ ∀ (x y : M), 0 (x + y) = HAdd.hAdd (α := M₂) (0 x) (0 y)

Tactic:
simp
-- 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 R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
⊢ ∀ (m : R₁) (x : M), 0 (m • x) = HSMul.hSMul.{u_3, u_10, u_10} (α := R₂) (β := M₂) ((σ₁₂ : (a : R₁) → R₂) m : R₂) (0 x)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R₁ M
inst_5 : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
f : M →ₛₗ[σ₁₂] M₂
⊢ Eq (α := (a : M) → M₂) (⇑f : (a : M) → M₂) 0 ↔ f = 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R₁ M
inst_5 : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
x : M
⊢ Eq.{u_10 + 1} (α := M₂) ((0 : (a : M) → M₂) x : M₂) (0 : 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_8
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₃
inst_6 : Module R₁ M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
c : M
rw : Eq.{u_11 + 1} (α := M₃) ((g : (a : M₂) → M₃) ((0 : (a : M) → M₂) c : M₂) : M₃) ((0 : (a : M) → M₃) c : M₃)
rw₁ : Eq.{u_11 + 1} (α := M₃) ((g : (a : M₂) → M₃) 0 : M₃) ((0 : (a : M) → M₃) c : M₃)
rw₂ : Eq.{u_11 + 1} (α := M₃) ((g : (a : M₂) → M₃) 0 : M₃) (0 : M₃)
rw₃ rw₄ : Eq.{u_11 + 1} (α := M₃) 0 0
⊢ Eq.{u_11 + 1} (α := M₃) ((g.comp (σ₁₂ := σ₁₂) 0 : (a : M) → M₃) c : M₃) ((0 : (a : M) → M₃) c : M₃)

Tactic:
rw [comp_apply, zero_apply, zero_apply, g.map_zero]

Premises used: LinearMap.zero_apply, LinearMap.comp_apply, LinearMap.map_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_8
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₃
inst_6 : Module R₁ M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
⊢ Eq (α := M →ₛₗ[σ₁₃] M₃) (comp (σ₂₃ := σ₂₃) 0 f) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R₁ M
inst_5 : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
⊢ Eq (α := M →ₛₗ[σ₁₂] M₂) default 0

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 R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_14 : Subsingleton M
f : M →ₛₗ[σ₁₂] M₂
x : M
rw : Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) 0 : M₂) ((default : (a : M) → M₂) 0 : M₂)
rw₁ : Eq.{u_10 + 1} (α := M₂) (0 : M₂) ((default : (a : M) → M₂) 0 : M₂)
rw₂ rw₃ : Eq.{u_10 + 1} (α := M₂) 0 0
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((default : (a : M) → M₂) x : M₂)

Tactic:
rw [Subsingleton.elim x 0, map_zero, map_zero]

Premises used: map_zero, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R₁ M
inst_5 : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
inst_6 : Nontrivial M
f : M →ₛₗ[σ₁₂] M₂
hf : Injective.{u_8 + 1, u_10 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
x : M
ne : x ≠ 0
h : f = 0
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) 0 : M₂)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R₁ M
inst_5 : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
inst_6 : Nontrivial M₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_8 + 1, u_10 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
have : ∀ (y : M₂) (ne : y ≠ 0), f ≠ 0
⊢ f ≠ 0

Tactic:
have ⟨y, ne⟩ := exists_ne (0 : M₂)
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R₁ M
inst_5 : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
inst_6 : Nontrivial M₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_8 + 1, u_10 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
y : M₂
ne : y ≠ 0
obtain : ∀ (x : M) (ne : Ne.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)), f ≠ 0
⊢ f ≠ 0

Tactic:
obtain ⟨x, rfl⟩ := hf y

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R₁ M
inst_5 : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
inst_6 : Nontrivial M₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_8 + 1, u_10 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
x : M
ne : Ne.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)
⊢ f ≠ 0

Tactic:
fun h ↦ ne congr($h x)

Premises used: congrArg, id, DFunLike.coe, Not
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R₁ M
inst_5 : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
inst_6 : Nontrivial M₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_8 + 1, u_10 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
x : M
ne : Ne.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)
⊢ f ≠ 0

Tactic:
exact fun h ↦ ne congr($h x)
-- 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 R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] M₂
⊢ ∀ (x y : M),
    HAdd.hAdd (α := (a : M) → M₂) (β := (a : M) → M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (x + y) =
      HAdd.hAdd (α := (a : M) → M₂) (β := (a : M) → M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) x +
        HAdd.hAdd (α := (a : M) → M₂) (β := (a : M) → M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) y

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- 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 R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] M₂
⊢ ∀ (m : R₁) (x : M),
    HAdd.hAdd (α := (a : M) → M₂) (β := (a : M) → M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) (m • x) =
      HSMul.hSMul.{u_3, u_10, u_10} (α := R₂) ((σ₁₂ : (a : R₁) → R₂) m : R₂)
        (HAdd.hAdd (α := (a : M) → M₂) (β := (a : M) → M₂) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₂) x)

Tactic:
simp [smul_add]

Premises used: smul_add
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R₁ M
inst_5 : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
f g : M →ₛₗ[σ₁₂] 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.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_8
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₃
inst_6 : Module R₁ M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g h : M₂ →ₛₗ[σ₂₃] M₃
⊢ (h + g) ∘ₛₗ f = h ∘ₛₗ f + 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_8
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₃
inst_6 : Module R₁ M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] M₂
h : M₂ →ₛₗ[σ₂₃] M₃
⊢ h ∘ₛₗ (f + g) = h ∘ₛₗ f + h ∘ₛₗ g

Tactic:
ext fun _ ↦ h.map_add _ _

Premises used: LinearMap.map_add, LinearMap.ext, DFunLike.coe
-- 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 R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] N₂
⊢ ∀ (x y : M),
    (-(⇑f : (a : M) → N₂)) (x + y) =
      HAdd.hAdd (α := N₂) (β := N₂) ((-(⇑f : (a : M) → N₂)) x : N₂) ((-(⇑f : (a : M) → N₂)) y : N₂)

Tactic:
simp [add_comm]

Premises used: add_comm
-- 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 R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] N₂
⊢ ∀ (m : R₁) (x : M),
    (-(⇑f : (a : M) → N₂)) (m • x) =
      HSMul.hSMul.{u_3, u_12, u_12} (α := R₂) (β := N₂) ((σ₁₂ : (a : R₁) → R₂) m : R₂) ((-(⇑f : (a : M) → N₂)) x : N₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
N₂ : Type u_12
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommGroup N₂
inst_4 : Module R₁ M
inst_5 : Module R₂ N₂
σ₁₂ : R₁ →+* R₂
f : M →ₛₗ[σ₁₂] N₂
⊢ Eq (α := (a : M) → N₂) (⇑(-f) : (a : M) → N₂) (-(⇑f : (a : M) → N₂))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
N₂ : Type u_12
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommGroup N₂
inst_4 : Module R₁ M
inst_5 : Module R₂ N₂
σ₁₂ : R₁ →+* R₂
f : M →ₛₗ[σ₁₂] N₂
x : M
⊢ Eq.{u_12 + 1} (α := N₂) ((-f : (a : M) → N₂) x : N₂) (-(f : (a : M) → N₂) x : N₂)

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_8
M₂ : Type u_10
N₃ : Type u_13
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommGroup N₃
inst_6 : Module R₁ M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] N₃
⊢ (-g) ∘ₛₗ f = -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_8
N₂ : Type u_12
N₃ : Type u_13
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommGroup N₂
inst_5 : AddCommGroup N₃
inst_6 : Module R₁ M
inst_7 : Module R₂ N₂
inst_8 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] N₂
g : N₂ →ₛₗ[σ₂₃] N₃
⊢ g ∘ₛₗ (-f) = -g ∘ₛₗ f

Tactic:
ext fun _ ↦ g.map_neg _

Premises used: LinearMap.ext, LinearMap.map_neg, DFunLike.coe
-- 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 R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] N₂
x y : M
⊢ HSub.hSub (α := (a : M) → N₂) (β := (a : M) → N₂) (⇑f : (a : M) → N₂) (⇑g : (a : M) → N₂) (x + y) =
    HSub.hSub (α := (a : M) → N₂) (β := (a : M) → N₂) (⇑f : (a : M) → N₂) (⇑g : (a : M) → N₂) x +
      HSub.hSub (α := (a : M) → N₂) (β := (a : M) → N₂) (⇑f : (a : M) → N₂) (⇑g : (a : M) → N₂) y

Tactic:
simp only [Pi.sub_apply, map_add, add_sub_add_comm]

Premises used: map_add, add_sub_add_comm, Pi.sub_apply
-- 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 R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] N₂
r : R₁
x : M
⊢ HSub.hSub (α := (a : M) → N₂) (β := (a : M) → N₂) (⇑f : (a : M) → N₂) (⇑g : (a : M) → N₂) (r • x) =
    HSMul.hSMul.{u_3, u_12, u_12} (α := R₂) ((σ₁₂ : (a : R₁) → R₂) r : R₂)
      (HSub.hSub (α := (a : M) → N₂) (β := (a : M) → N₂) (⇑f : (a : M) → N₂) (⇑g : (a : M) → N₂) x)

Tactic:
simp [Pi.sub_apply, smul_sub]

Premises used: smul_sub, Pi.sub_apply
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
N₂ : Type u_12
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommGroup N₂
inst_4 : Module R₁ M
inst_5 : Module R₂ N₂
σ₁₂ : R₁ →+* R₂
f g : M →ₛₗ[σ₁₂] N₂
x : M
⊢ (f - g : (a : M) → N₂) x = HSub.hSub (α := N₂) (β := N₂) ((f : (a : M) → N₂) x : N₂) ((g : (a : M) → N₂) x : N₂)

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_8
M₂ : Type u_10
N₃ : Type u_13
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommGroup N₃
inst_6 : Module R₁ M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g h : M₂ →ₛₗ[σ₂₃] N₃
⊢ (g - h) ∘ₛₗ f = g ∘ₛₗ f - h ∘ₛₗ 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_8
N₂ : Type u_12
N₃ : Type u_13
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommGroup N₂
inst_5 : AddCommGroup N₃
inst_6 : Module R₁ M
inst_7 : Module R₂ N₂
inst_8 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] N₂
h : N₂ →ₛₗ[σ₂₃] N₃
⊢ h ∘ₛₗ (g - f) = h ∘ₛₗ g - h ∘ₛₗ f

Tactic:
ext fun _ ↦ h.map_sub _ _

Premises used: LinearMap.ext, LinearMap.map_sub, DFunLike.coe
-- 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 R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
h :
  ∀ (x : M),
    Eq.{u_10 + 1} (α := M₂)
      ((toAddMonoidHom.{u_2, u_3, u_8, u_10} (R := R₁) (S := R₂) (modM₁ := inst_8) (modM₂ := inst_9) (σ := σ₁₂) 0 :
            (a : M) → M₂)
          x :
        M₂)
      ((0 : (a : M) → M₂) x : M₂)
⊢ Eq (α := M →+ M₂)
    (toAddMonoidHom.{u_2, u_3, u_8, u_10} (R := R₁) (S := R₂) (modM₁ := inst_8) (modM₂ := inst_9) (σ := σ₁₂) 0) 0

Tactic:
ext
-- 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 R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
x : M
⊢ Eq.{u_10 + 1} (α := M₂)
    ((toAddMonoidHom.{u_2, u_3, u_8, u_10} (R := R₁) (S := R₂) (modM₁ := inst_8) (modM₂ := inst_9) (σ := σ₁₂) 0 :
          (a : M) → M₂)
        x :
      M₂)
    ((0 : (a : M) → M₂) x : M₂)

Tactic:
rfl