awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃
hf : Injective.{u_10 + 1, u_11 + 1} (α := M₂) (β := M₃) (⇑f : (a : M₂) → M₃)
g₁ g₂ : M₁ →ₛₗ[σ₁₂] M₂
h : f ∘ₛₗ g₁ = f ∘ₛₗ g₂
x : M₁
rw :
  Eq.{u_11 + 1} (α := M₃) ((f ∘ₛₗ g₁ : (a : M₁) → M₃) x : M₃) ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)
rw₁ :
  Eq.{u_11 + 1} (α := M₃) ((f ∘ₛₗ g₂ : (a : M₁) → M₃) x : M₃) ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)
rw₂ rw₃ :
  Eq.{u_11 + 1} (α := M₃) ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)
    ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : M₂) → M₃) ((g₁ : (a : M₁) → M₂) x : M₂) : M₃)
    ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)

Tactic:
rw [← comp_apply, h, comp_apply]

Premises used: LinearMap.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₃
σ₃₂ : R₃ →+* R₂
inst_7 : RingHomInvPair σ₂₃ σ₃₂
inst_8 : RingHomCompTriple σ₁₃ σ₃₂ σ₁₂
hf : ∃ (f' : M₃ →ₛₗ[σ₃₂] M₂), f ∘ₛₗ f' = id
h : M₁ →ₛₗ[σ₁₃] M₃
obtain :
  ∀ (f' : M₃ →ₛₗ[σ₃₂] M₂) (hf' : f ∘ₛₗ f' = id), ∃ (a : M₁ →ₛₗ[σ₁₂] M₂), (fun (g : M₁ →ₛₗ[σ₁₂] M₂) ↦ f ∘ₛₗ g) a = h
⊢ ∃ (a : M₁ →ₛₗ[σ₁₂] M₂), (fun (g : M₁ →ₛₗ[σ₁₂] M₂) ↦ f ∘ₛₗ g) a = h

Tactic:
obtain ⟨f', hf'⟩ := hf
-- 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₃
σ₃₂ : R₃ →+* R₂
inst_7 : RingHomInvPair σ₂₃ σ₃₂
inst_8 : RingHomCompTriple σ₁₃ σ₃₂ σ₁₂
h : M₁ →ₛₗ[σ₁₃] M₃
f' : M₃ →ₛₗ[σ₃₂] M₂
hf' : f ∘ₛₗ f' = id
⊢ ∃ (a : M₁ →ₛₗ[σ₁₂] M₂), (fun (g : M₁ →ₛₗ[σ₁₂] M₂) ↦ f ∘ₛₗ g) a = h

Tactic:
⟨f'.comp h, ?_⟩

Premises used: LinearMap.comp, Exists.intro
-- 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₃
σ₃₂ : R₃ →+* R₂
inst_7 : RingHomInvPair σ₂₃ σ₃₂
inst_8 : RingHomCompTriple σ₁₃ σ₃₂ σ₁₂
h : M₁ →ₛₗ[σ₁₃] M₃
f' : M₃ →ₛₗ[σ₃₂] M₂
hf' : f ∘ₛₗ f' = id
refine : (fun (g : M₁ →ₛₗ[σ₁₂] M₂) ↦ f ∘ₛₗ g) (f' ∘ₛₗ h) = h
⊢ ∃ (a : M₁ →ₛₗ[σ₁₂] M₂), (fun (g : M₁ →ₛₗ[σ₁₂] M₂) ↦ f ∘ₛₗ g) a = h

Tactic:
refine ⟨f'.comp h, ?_⟩
-- 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₃
σ₃₂ : R₃ →+* R₂
inst_7 : RingHomInvPair σ₂₃ σ₃₂
inst_8 : RingHomCompTriple σ₁₃ σ₃₂ σ₁₂
h : M₁ →ₛₗ[σ₁₃] M₃
f' : M₃ →ₛₗ[σ₃₂] M₂
hf' : f ∘ₛₗ f' = id
simp_rw simp_rw₁ : f ∘ₛₗ f' ∘ₛₗ h = h
simp_rw₂ : (f ∘ₛₗ f') ∘ₛₗ h = h
simp_rw₃ : id ∘ₛₗ h = h
⊢ (fun (g : M₁ →ₛₗ[σ₁₂] M₂) ↦ f ∘ₛₗ g) (f' ∘ₛₗ h) = h

Tactic:
simp_rw [← comp_assoc, hf', id_comp]

Premises used: LinearMap.comp_assoc, LinearMap.id_comp
-- 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 g' : M₁ →ₛₗ[σ₁₂] M₂
hf : Injective.{u_10 + 1, u_11 + 1} (α := M₂) (β := M₃) (⇑f : (a : M₂) → M₃)
⊢ f ∘ₛₗ g = f ∘ₛₗ g' ↔ g = g'

Tactic:
hf.injective_linearMapComp_left.eq_iff

Premises used: Function.Injective.injective_linearMapComp_left, Function.Injective.eq_iff
-- 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 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Module R M
inst_6 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_7 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g ((f : (a : M) → M₂) x) = x
h₂ : ∀ (x : M₂), (f : (a : M) → M₂) (g x) = x
x y : M₂
rw : g ((f : (a : M) → M₂) (g (x + y))) = g ((f : (a : M) → M₂) (g x + g y))
⊢ g (x + y) = g x + g y

Tactic:
rw [← h₁ (g (x + y)), ← h₁ (g x + g y)]

Premises used: HAdd.hAdd
-- 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 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Module R M
inst_6 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_7 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g ((f : (a : M) → M₂) x) = x
h₂ : ∀ (x : M₂), (f : (a : M) → M₂) (g x) = x
x y : M₂
⊢ g ((f : (a : M) → M₂) (g (x + y))) = g ((f : (a : M) → M₂) (g x + g y))

Tactic:
simp [h₂]
-- 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 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Module R M
inst_6 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_7 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g ((f : (a : M) → M₂) x) = x
h₂ : ∀ (x : M₂), (f : (a : M) → M₂) (g x) = x
a : S
b : M₂
rw :
  g ((f : (a : M) → M₂) (g (a • b))) =
    g ((f : (a : M) → M₂) (HSMul.hSMul.{u_1, u_8, u_8} (α := R) ((σ' : (a : S) → R) a : R) (g b)))
⊢ g (a • b) = HSMul.hSMul.{u_1, u_8, u_8} (α := R) ((σ' : (a : S) → R) a : R) (g b)

Tactic:
rw [← h₁ (g (a • b)), ← h₁ (σ' a • g b)]

Premises used: HSMul.hSMul, 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 S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Module R M
inst_6 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_7 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g ((f : (a : M) → M₂) x) = x
h₂ : ∀ (x : M₂), (f : (a : M) → M₂) (g x) = x
a : S
b : M₂
⊢ g ((f : (a : M) → M₂) (g (a • b))) =
    g ((f : (a : M) → M₂) (HSMul.hSMul.{u_1, u_8, u_8} (α := R) ((σ' : (a : S) → R) a : R) (g b)))

Tactic:
simp [h₂]
-- 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 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Module R M
inst_6 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_7 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g ((f : (a : M) → M₂) x) = x
h₂ : ∀ (x : M₂), (f : (a : M) → M₂) (g x) = x
⊢ M₂ →ₛₗ[σ'] M

Tactic:
exact
    { toFun := g
      map_add' := fun x y ↦ by rw [← h₁ (g (x + y)), ← h₁ (g x + g y)]; simp [h₂]
      map_smul' := fun a b ↦ by
        rw [← h₁ (g (a • b)), ← h₁ (σ' a • g b)]
        simp [h₂] }
-- 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 S M₂
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g ∘ₛₗ f = id
simp_rw : Injective (α := M) (β := M) (⇑(g ∘ₛₗ f) : (a : M) → M)
simp_rw₁ : Injective.{u_8 + 1, u_8 + 1} (α := M) (β := M) (⇑id : (a : M) → M)
simp_rw₂ : Injective.{u_8 + 1, u_8 + 1} (α := M) _root_.id
⊢ Injective.{u_8 + 1, u_8 + 1} (α := M) (β := M)
    (Function.comp.{u_8 + 1, u_10 + 1, u_8 + 1} (β := M₂) (⇑g : (a : M₂) → M) (⇑f : (a : M) → M₂))

Tactic:
simp_rw [← coe_comp, h, id_coe, bijective_id.1]

Premises used: Function.bijective_id, LinearMap.id_coe, And.left, LinearMap.coe_comp
-- 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 S M₂
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g ∘ₛₗ f = id
simp_rw : Surjective (α := M) (β := M) (⇑(g ∘ₛₗ f) : (a : M) → M)
simp_rw₁ : Surjective.{u_8 + 1, u_8 + 1} (α := M) (β := M) (⇑id : (a : M) → M)
simp_rw₂ : Surjective.{u_8 + 1, u_8 + 1} (α := M) _root_.id
⊢ Surjective.{u_8 + 1, u_8 + 1} (α := M) (β := M)
    (Function.comp.{u_8 + 1, u_10 + 1, u_8 + 1} (β := M₂) (⇑g : (a : M₂) → M) (⇑f : (a : M) → M₂))

Tactic:
simp_rw [← coe_comp, h, id_coe, bijective_id.2]

Premises used: Function.bijective_id, LinearMap.id_coe, And.right, LinearMap.coe_comp
-- 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 : AddCommGroup M
inst_3 : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S M₂
σ : R →+* S
f : M →ₛₗ[σ] M₂
x : M
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) (-x) : M₂) (-(f : (a : M) → M₂) x : M₂)

Tactic:
map_neg f x

Premises used: map_neg
-- 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 : AddCommGroup M
inst_3 : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S M₂
σ : R →+* S
f : M →ₛₗ[σ] M₂
x y : M
⊢ (f : (a : M) → M₂) (x - y) = HSub.hSub (α := M₂) (β := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) y : M₂)

Tactic:
map_sub f x y

Premises used: map_sub
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : 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
inst_1 : Semiring S_1
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S_1 M₂
σ : R →+* S_1
f : M →ₛₗ[σ] M₂
S : Type u_14
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
⊢ (fₗ : (a : M) → M₂) (HSMul.hSMul (α := ℤ) 0 x) = HSMul.hSMul (α := ℤ) (β := M₂) 0 ((fₗ : (a : M) → M₂) x : M₂)

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_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
inst_1 : Semiring S_1
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S_1 M₂
σ : R →+* S_1
f : M →ₛₗ[σ] M₂
S : Type u_14
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
n : ℕ
ih :
  (fₗ : (a : M) → M₂) (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) =
    HSMul.hSMul (α := ℤ) (β := M₂) (↑n : ℤ) ((fₗ : (a : M) → M₂) x : M₂)
⊢ (fₗ : (a : M) → M₂) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 • x) =
    HSMul.hSMul (β := M₂) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ((fₗ : (a : M) → M₂) x : M₂)

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : 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
inst_1 : Semiring S_1
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S_1 M₂
σ : R →+* S_1
f : M →ₛₗ[σ] M₂
S : Type u_14
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
n : ℕ
ih :
  (fₗ : (a : M) → M₂) (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) =
    HSMul.hSMul (α := ℤ) (β := M₂) (-(↑n : ℤ)) ((fₗ : (a : M) → M₂) x : M₂)
⊢ (fₗ : (a : M) → M₂) (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 • x) =
    HSMul.hSMul (β := M₂) (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) ((fₗ : (a : M) → M₂) x : M₂)

Tactic:
simp [sub_smul]

Premises used: sub_smul
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : 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
inst_1 : Semiring S_1
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S_1 M₂
σ : R →+* S_1
f : M →ₛₗ[σ] M₂
S : Type u_14
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : Module S M₂
fₗ : M →ₗ[S] M₂
c : ℤ
x : M
zero : (fₗ : (a : M) → M₂) (HSMul.hSMul (α := ℤ) 0 x) = HSMul.hSMul (α := ℤ) (β := M₂) 0 ((fₗ : (a : M) → M₂) x : M₂)
succ :
  ∀ (n : ℕ)
    (ih :
      (fₗ : (a : M) → M₂) (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) =
        HSMul.hSMul (α := ℤ) (β := M₂) (↑n : ℤ) ((fₗ : (a : M) → M₂) x : M₂)),
    (fₗ : (a : M) → M₂) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 • x) =
      HSMul.hSMul (β := M₂) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ((fₗ : (a : M) → M₂) x : M₂)
pred :
  ∀ (n : ℕ)
    (ih :
      (fₗ : (a : M) → M₂) (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) =
        HSMul.hSMul (α := ℤ) (β := M₂) (-(↑n : ℤ)) ((fₗ : (a : M) → M₂) x : M₂)),
    (fₗ : (a : M) → M₂) (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 • x) =
      HSMul.hSMul (β := M₂) (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) ((fₗ : (a : M) → M₂) x : M₂)
⊢ (fₗ : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((fₗ : (a : M) → M₂) x : M₂)

Tactic:
induction c with
    | zero => simp
    | succ n ih => simp [add_smul]
    | pred n ih => simp [sub_smul]

Premises used: sub_smul, add_smul
-- 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 : AddCommGroup M
inst_3 : AddCommGroup M₂
module_M : Module R_1 M
module_M₂ : Module S_1 M₂
σ : R_1 →+* S_1
f : M →ₛₗ[σ] M₂
R : Type u_14
S : Type u_15
inst_4 : Monoid R
inst_5 : MulAction R M
inst_6 : MulAction R M₂
inst_7 : Semiring S
inst_8 : Module S M
inst_9 : Module S M₂
inst_10 : CompatibleSMul M M₂ R S
⊢ CompatibleSMul.{u_8, u_10, u_14, u_15} M M₂ Rˣ S

Tactic:
⟨fun fₗ c x ↦ (CompatibleSMul.map_smul fₗ (c : R) x :)⟩

Premises used: Units.val, LinearMap.CompatibleSMul.mk, LinearMap.CompatibleSMul.map_smul
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : Semiring S
inst_5 : Module S M₂
σ : R →+* S
f : M →ₑ+[(↑σ : R →* S)] M₂
⊢ Eq (α := (a : M) → M₂)
    (⇑(↑f :
          [inst_6 : FunLike (M →ₑ+[(↑σ : R →* S)] M₂) M M₂] →
            [SemilinearMapClass (M →ₑ+[(↑σ : R →* S)] M₂) σ M M₂] → M →ₛₗ[σ] M₂) :
      (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 : AddCommMonoid M
inst_1 : AddCommMonoid M₂
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : Semiring S
inst_5 : Module S M₂
σ : R →+* S
f g : M →ₑ+[(↑σ : R →* S)] M₂
h :
  Eq (α := M →ₛₗ[σ] M₂)
    (↑f :
      [inst_6 : FunLike (M →ₑ+[(↑σ : R →* S)] M₂) M M₂] →
        [SemilinearMapClass (M →ₑ+[(↑σ : R →* S)] M₂) σ M M₂] → M →ₛₗ[σ] M₂)
    (↑g :
      [inst_6 : FunLike (M →ₑ+[(↑σ : R →* S)] M₂) M M₂] →
        [SemilinearMapClass (M →ₑ+[(↑σ : R →* S)] M₂) σ M M₂] → M →ₛₗ[σ] M₂)
a : ∀ (m : M), Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) m : M₂) ((g : (a : M) → M₂) m : M₂)
⊢ f = g

Tactic:
ext m
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : Semiring S
inst_5 : Module S M₂
σ : R →+* S
f g : M →ₑ+[(↑σ : R →* S)] M₂
h :
  Eq (α := M →ₛₗ[σ] M₂)
    (↑f :
      [inst_6 : FunLike (M →ₑ+[(↑σ : R →* S)] M₂) M M₂] →
        [SemilinearMapClass (M →ₑ+[(↑σ : R →* S)] M₂) σ M M₂] → M →ₛₗ[σ] M₂)
    (↑g :
      [inst_6 : FunLike (M →ₑ+[(↑σ : R →* S)] M₂) M M₂] →
        [SemilinearMapClass (M →ₑ+[(↑σ : R →* S)] M₂) σ M M₂] → M →ₛₗ[σ] M₂)
m : M
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) m : M₂) ((g : (a : M) → M₂) m : M₂)

Tactic:
LinearMap.congr_fun h m

Premises used: LinearMap.congr_fun
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : Semiring S
inst_5 : Module S M₂
σ : R →+* S
f g : M →ₑ+[(↑σ : R →* S)] M₂
h :
  Eq (α := M →ₛₗ[σ] M₂)
    (↑f :
      [inst_6 : FunLike (M →ₑ+[(↑σ : R →* S)] M₂) M M₂] →
        [SemilinearMapClass (M →ₑ+[(↑σ : R →* S)] M₂) σ M M₂] → M →ₛₗ[σ] M₂)
    (↑g :
      [inst_6 : FunLike (M →ₑ+[(↑σ : R →* S)] M₂) M M₂] →
        [SemilinearMapClass (M →ₑ+[(↑σ : R →* S)] M₂) σ M M₂] → M →ₛₗ[σ] M₂)
m : M
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) m : M₂) ((g : (a : M) → M₂) m : M₂)

Tactic:
exact LinearMap.congr_fun h m

Premises used: LinearMap.congr_fun
-- 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 → M₂
lin : IsLinearMap R f
x : M
⊢ (mk' f lin : (a : M) → M₂) x = f x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : R
⊢ IsLinearMap R (M₂ := M) fun (z : M) ↦ c • z

Tactic:
IsLinearMap.mk (smul_add c) ?_

Premises used: IsLinearMap.mk, smul_add
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : R
refine : ∀ (c_1 : R) (x : M), c • c_1 • x = c_1 • c • x
⊢ IsLinearMap R (M₂ := M) fun (z : M) ↦ c • z

Tactic:
refine IsLinearMap.mk (smul_add c) ?_

Premises used: IsLinearMap.mk
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c c_1 : R
_ : ∀ (x : M), c • c_1 • x = c_1 • c • x
⊢ ∀ (x : M), c • c_1 • x = c_1 • c • x

Tactic:
_
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c c_1 : R
x : M
⊢ c • c_1 • x = c_1 • c • x

Tactic:
simp only [smul_smul, mul_comm]

Premises used: smul_smul, mul_comm
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_14
M : Type u_15
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : M
⊢ IsLinearMap.{u_14, u_14, u_15} R (M₂ := M) fun (c : R) ↦ c • a

Tactic:
IsLinearMap.mk (fun x y ↦ add_smul x y a) fun x y ↦ mul_smul x y a

Premises used: add_smul, IsLinearMap.mk, SemigroupAction.mul_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 → M₂
lin : IsLinearMap R f
⊢ f 0 = 0

Tactic:
(lin.mk' f).map_zero

Premises used: LinearMap.map_zero, IsLinearMap.mk'
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
M : Type u_8
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ IsLinearMap R (M₂ := M) fun (z : M) ↦ -z

Tactic:
IsLinearMap.mk neg_add fun x y ↦ (smul_neg x y).symm

Premises used: neg_add, smul_neg, Eq.symm, IsLinearMap.mk
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M → M₂
lin : IsLinearMap R f
x : M
⊢ f (-x) = -f x

Tactic:
(lin.mk' f).map_neg x

Premises used: LinearMap.map_neg, IsLinearMap.mk'
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M → M₂
lin : IsLinearMap R f
x y : M
⊢ f (x - y) = f x - f y

Tactic:
(lin.mk' f).map_sub x y

Premises used: LinearMap.map_sub, IsLinearMap.mk'
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
M : Type u_8
M₂ : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
f g : M →+ M₂
h : f.toNatLinearMap = g.toNatLinearMap
h₁ : ∀ (x : M), Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
M : Type u_8
M₂ : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
f g : M →+ M₂
h : f.toNatLinearMap = g.toNatLinearMap
x : M
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)

Tactic:
LinearMap.congr_fun h x

Premises used: LinearMap.congr_fun
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
M : Type u_8
M₂ : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
f g : M →+ M₂
h : f.toNatLinearMap = g.toNatLinearMap
x : M
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)

Tactic:
exact LinearMap.congr_fun h x

Premises used: LinearMap.congr_fun
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
M : Type u_8
M₂ : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
f : M →+ M₂
⊢ Eq (α := (a : M) → M₂) (⇑f.toNatLinearMap : (a : M) → M₂) (⇑f : (a : M) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
M : Type u_8
M₂ : Type u_10
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
f g : M →+ M₂
h : f.toIntLinearMap = g.toIntLinearMap
h₁ : ∀ (x : M), Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
M : Type u_8
M₂ : Type u_10
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
f g : M →+ M₂
h : f.toIntLinearMap = g.toIntLinearMap
x : M
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)

Tactic:
LinearMap.congr_fun h x

Premises used: LinearMap.congr_fun
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
M : Type u_8
M₂ : Type u_10
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
f g : M →+ M₂
h : f.toIntLinearMap = g.toIntLinearMap
x : M
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)

Tactic:
exact LinearMap.congr_fun h x

Premises used: LinearMap.congr_fun