awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
succ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
succ₁ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₂ : (g₂ ∘ₗ g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₃ : g₂ ∘ₛₗ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₄ : g₂ ∘ₛₗ f ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
succ₅ : (g₂ ∘ₛₗ f) ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
succ₆ : (f ∘ₛₗ g) ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
succ₇ : f ∘ₛₗ (g ∘ₗ g ^ k) = f ∘ₛₗ (g * g ^ k)
succ₈ succ₉ : f ∘ₛₗ (g ∘ₗ g ^ k) = f ∘ₛₗ (g ∘ₗ g ^ k)
⊢ (g₂ ^ (k + 1)) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))

Tactic:
rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]

Premises used: Module.End.mul_eq_comp, LinearMap.comp_assoc, pow_succ'
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
zero : HPow.hPow (β := ℕ) g₂ 0 ∘ₛₗ f = f ∘ₛₗ HPow.hPow (β := ℕ) g 0
succ : ∀ (k : ℕ) (ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)), (g₂ ^ (k + 1)) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
⊢ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)

Tactic:
induction k with
  | zero => simp [one_eq_id]
  | succ k ih => rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]

Premises used: Module.End.mul_eq_comp, Module.End.one_eq_id, LinearMap.comp_assoc, pow_succ'
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
⊢ HPow.hPow (α := M →ₗ[R] M) LinearMap.id n = LinearMap.id

Tactic:
one_pow n

Premises used: one_pow
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
rw : f' ^ n * f' = (f' ^ n) ∘ₗ f'
rw₁ rw₂ : (f' ^ n) ∘ₗ f' = (f' ^ n) ∘ₗ f'
⊢ f' ^ (n + 1) = (f' ^ n) ∘ₗ f'

Tactic:
rw [pow_succ, mul_eq_comp]

Premises used: Module.End.mul_eq_comp, pow_succ
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
rw : f' * f' ^ n = f' ∘ₗ f' ^ n
rw₁ rw₂ : f' ∘ₗ f' ^ n = f' ∘ₗ f' ^ n
⊢ f' ^ (n + 1) = f' ∘ₗ f' ^ n

Tactic:
rw [pow_succ', mul_eq_comp]

Premises used: Module.End.mul_eq_comp, pow_succ'
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
h : Surjective (α := M) (β := M) (⇑f' : (a : M) → M)
n : ℕ
rw : Surjective (α := M) (β := M) (⇑((f' ^ n) ∘ₗ f') : (a : M) → M)
⊢ Surjective (α := M) (β := M) (⇑(f' ^ (n + 1)) : (a : M) → M)

Tactic:
rw [iterate_succ]

Premises used: Module.End.iterate_succ
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
h : Surjective (α := M) (β := M) (⇑f' : (a : M) → M)
n : ℕ
⊢ Surjective (α := M) (β := M) (⇑((f' ^ n) ∘ₗ f') : (a : M) → M)

Tactic:
(iterate_surjective h n).comp h

Premises used: Function.Surjective.comp
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
h : Surjective (α := M) (β := M) (⇑f' : (a : M) → M)
n : ℕ
⊢ Surjective (α := M) (β := M) (⇑((f' ^ n) ∘ₗ f') : (a : M) → M)

Tactic:
exact (iterate_surjective h n).comp h

Premises used: Function.Surjective.comp
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
h : Injective (α := M) (β := M) (⇑f' : (a : M) → M)
n : ℕ
rw : Injective (α := M) (β := M) (⇑((f' ^ n) ∘ₗ f') : (a : M) → M)
⊢ Injective (α := M) (β := M) (⇑(f' ^ (n + 1)) : (a : M) → M)

Tactic:
rw [iterate_succ]

Premises used: Module.End.iterate_succ
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
h : Injective (α := M) (β := M) (⇑f' : (a : M) → M)
n : ℕ
⊢ Injective (α := M) (β := M) (⇑((f' ^ n) ∘ₗ f') : (a : M) → M)

Tactic:
(iterate_injective h n).comp h

Premises used: Function.Injective.comp
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
h : Injective (α := M) (β := M) (⇑f' : (a : M) → M)
n : ℕ
⊢ Injective (α := M) (β := M) (⇑((f' ^ n) ∘ₗ f') : (a : M) → M)

Tactic:
exact (iterate_injective h n).comp h

Premises used: Function.Injective.comp
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
h : Bijective (α := M) (β := M) (⇑f' : (a : M) → M)
n : ℕ
rw : Bijective (α := M) (β := M) (⇑((f' ^ n) ∘ₗ f') : (a : M) → M)
⊢ Bijective (α := M) (β := M) (⇑(f' ^ (n + 1)) : (a : M) → M)

Tactic:
rw [iterate_succ]

Premises used: Module.End.iterate_succ
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
h : Bijective (α := M) (β := M) (⇑f' : (a : M) → M)
n : ℕ
⊢ Bijective (α := M) (β := M) (⇑((f' ^ n) ∘ₗ f') : (a : M) → M)

Tactic:
(iterate_bijective h n).comp h

Premises used: Function.Bijective.comp
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
h : Bijective (α := M) (β := M) (⇑f' : (a : M) → M)
n : ℕ
⊢ Bijective (α := M) (β := M) (⇑((f' ^ n) ∘ₗ f') : (a : M) → M)

Tactic:
exact (iterate_bijective h n).comp h

Premises used: Function.Bijective.comp
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Injective (α := M) (β := M) (⇑(f' ^ n) : (a : M) → M)
⊢ 0 < n

Tactic:
lia
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Injective (α := M) (β := M) (⇑(f' ^ n) : (a : M) → M)
⊢ Injective (α := M) (β := M) (Function.comp (β := M) (⇑(f' ^ n.pred) : (a : M) → M) (⇑f' : (a : M) → M))

Tactic:
rw [← Nat.succ_pred_eq_of_pos (show 0 < n by lia), iterate_succ, coe_comp] at h

Premises used: Nat.succ_pred_eq_of_pos, LinearMap.coe_comp, Module.End.iterate_succ
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Injective (α := M) (β := M) (Function.comp (β := M) (⇑(f' ^ n.pred) : (a : M) → M) (⇑f' : (a : M) → M))
⊢ Injective (α := M) (β := M) (⇑f' : (a : M) → M)

Tactic:
h.of_comp

Premises used: Function.Injective.of_comp
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Injective (α := M) (β := M) (Function.comp (β := M) (⇑(f' ^ n.pred) : (a : M) → M) (⇑f' : (a : M) → M))
⊢ Injective (α := M) (β := M) (⇑f' : (a : M) → M)

Tactic:
exact h.of_comp

Premises used: Function.Injective.of_comp
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Surjective (α := M) (β := M) (⇑(f' ^ n) : (a : M) → M)
⊢ Surjective (α := M) (β := M) (Function.comp (β := M) (⇑f' : (a : M) → M) (⇑(f' ^ n.pred) : (a : M) → M))

Tactic:
rw [← Nat.succ_pred_eq_of_pos (Nat.pos_iff_ne_zero.mpr hn), pow_succ', coe_mul] at h

Premises used: Iff.mpr, Nat.succ_pred_eq_of_pos, Nat.pos_iff_ne_zero, Module.End.coe_mul, pow_succ'
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Surjective (α := M) (β := M) (Function.comp (β := M) (⇑f' : (a : M) → M) (⇑(f' ^ n.pred) : (a : M) → M))
⊢ Surjective (α := M) (β := M) (⇑f' : (a : M) → M)

Tactic:
Surjective.of_comp h

Premises used: Function.Surjective.of_comp
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Surjective (α := M) (β := M) (Function.comp (β := M) (⇑f' : (a : M) → M) (⇑(f' ^ n.pred) : (a : M) → M))
⊢ Surjective (α := M) (β := M) (⇑f' : (a : M) → M)

Tactic:
exact Surjective.of_comp h

Premises used: Function.Surjective.of_comp
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommGroup N₁
inst_3 : Module R M
inst_4 : Module R N₁
inst_5 : Monoid S
inst_6 : DistribMulAction S M
inst_7 : SMulCommClass R S M
f' : End R M
α : R
hα : α ∈ Set.center R
β : R
x : M
⊢ α • β • x = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) β : R) (α • x)

Tactic:
simp [smul_smul, ((Set.mem_center_iff.mp hα).comm β).eq]

Premises used: smul_smul, IsMulCentral.comm, Set.mem_center_iff, Iff.mp, Commute.eq
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
M : Type u_4
inst : AddCommMonoid M
R : Type u_9
inst_1 : CommSemiring R
inst_2 : Module R M
α : R
hα : α ∈ Set.center R
⊢ smulLeft α hα = HSMul.hSMul (β := End R M) α LinearMap.id

Tactic:
rfl

Premises used: Module.End.smulLeft, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
a : M
⊢ f • a = (f : (a : M) → M) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommGroup N₁
inst_3 : Module R M
inst_4 : Module R N₁
⊢ FaithfulSMul (End R M) M

Tactic:
⟨LinearMap.ext⟩

Premises used: LinearMap.ext, FaithfulSMul.mk
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommGroup N₁
inst_3 : Module R M
inst_4 : Module R N₁
inst_5 : SMul S R
inst_6 : SMul S M
inst_7 : IsScalarTower S R M
⊢ SMulCommClass (End R M) S M

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommGroup N₁
inst_3 : Module R M
inst_4 : Module R N₁
inst_5 : Monoid S
inst_6 : DistribMulAction S M
inst_7 : SMulCommClass R S M
⊢ IsScalarTower S (End R M) M

Tactic:
⟨fun _ _ _ ↦ rfl⟩

Premises used: IsScalarTower.mk, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
N₁ : Type u_8
inst : Semiring R
n : ℕ
inst_1 : AddCommMonoid N₁
inst_2 : Module R N₁
⊢ Eq (α := End R N₁) ((↑n : End R N₁) : End R N₁) ((toModuleEnd R N₁ : (a : ℕ) → End R N₁) n : End R N₁)

Tactic:
rfl

Premises used: DistribSMul.toLinearMap, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
N₁ : Type u_8
inst : Semiring R
z : ℤ
inst_1 : AddCommGroup N₁
inst_2 : Module R N₁
⊢ Eq (α := End R N₁) ((↑z : End R N₁) : End R N₁) ((toModuleEnd R N₁ : (a : ℤ) → End R N₁) z : End R N₁)

Tactic:
rfl

Premises used: DistribSMul.toLinearMap, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : M₁ →ₗ[R] S
x_1 : M
x y : M₁
rw :
  HAdd.hAdd (α := S) (β := S) ((f : (a : M₁) → S) x : S) ((f : (a : M₁) → S) y : S) • x_1 =
    HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) x : S) x_1 +
      HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x_1
rw₁ rw₂ :
  HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) x : S) x_1 +
      HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x_1 =
    HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) x : S) x_1 +
      HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x_1
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) (x + y) : S) x_1 =
    HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) x : S) x_1 +
      HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x_1

Tactic:
rw [f.map_add, add_smul]

Premises used: LinearMap.map_add, add_smul
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
b : R
y : M₁
rw :
  HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) (b • y) : S) x =
    b • HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x
rw₁ :
  HSMul.hSMul (β := S) b ((f : (a : M₁) → S) y : S) • x =
    b • HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x
rw₂ rw₃ :
  b • HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x =
    b • HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) (b • y) : S) x =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) b : R)
      (HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x)

Tactic:
rw [RingHom.id_apply, map_smul, smul_assoc]

Premises used: RingHom.id_apply, smul_assoc, map_smul
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
⊢ Eq (α := (a : M₁) → M) (⇑(f.smulRight x) : (a : M₁) → M) fun (c : M₁) ↦
    HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) c : S) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
c : M₁
⊢ (f.smulRight x : (a : M₁) → M) c = HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) c : S) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : M₁ →ₗ[R] S
h : ∀ (x : M₁), Eq.{u_4 + 1} (α := M) ((f.smulRight 0 : (a : M₁) → M) x : M) ((0 : (a : M₁) → M) x : M)
⊢ Eq (α := M₁ →ₗ[R] M) (f.smulRight 0) 0

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M₁
⊢ Eq.{u_4 + 1} (α := M) ((f.smulRight 0 : (a : M₁) → M) x : M) ((0 : (a : M₁) → M) x : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
x : M
h :
  ∀ (x_1 : M₁),
    Eq.{u_4 + 1} (α := M) ((smulRight.{u_1, u_3, u_4, u_5} (S := S) 0 x : (a : M₁) → M) x_1 : M)
      ((0 : (a : M₁) → M) x_1 : M)
⊢ Eq (α := M₁ →ₗ[R] M) (smulRight.{u_1, u_3, u_4, u_5} (S := S) 0 x) 0

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
x : M
x_1 : M₁
⊢ Eq.{u_4 + 1} (α := M) ((smulRight.{u_1, u_3, u_4, u_5} (S := S) 0 x : (a : M₁) → M) x_1 : M)
    ((0 : (a : M₁) → M) x_1 : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
inst_9 : IsDomain S
f : M₁ →ₗ[R] S
x : M
inst_10 : Module.IsTorsionFree S M
⊢ Eq (α := M₁ →ₗ[R] M) (f.smulRight x) 0 ↔ f = 0 ∨ x = 0

Tactic:
simp [DFunLike.ext_iff, forall_or_right]

Premises used: DFunLike.ext_iff, forall_or_right
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
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 R M₁
inst_7 : Module R M₂
inst_8 : Module S M₁
inst_9 : Module S M₂
inst_10 : SMulCommClass R S M₁
inst_11 : SMulCommClass R S M₂
inst_12 : CompatibleSMul M₁ M₂ S R
f : M₁ →ₗ[R] M₂
g : M →ₗ[R] M₁
⊢ (compRight S f : (a : M →ₗ[R] M₁) → M →ₗ[R] M₂) g = f ∘ₗ g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f_1 : M →ₗ[R] M₂
f : M₂ →ₗ[R] R
m m' : M
h :
  ∀ (x : M₂),
    Eq.{u_4 + 1} (α := M) ((f.smulRight (m + m') : (a : M₂) → M) x : M)
      ((HAdd.hAdd (α := M₂ →ₗ[R] M) (f.smulRight m) (f.smulRight m') : (a : M₂) → M) x : M)
⊢ f.smulRight (m + m') = HAdd.hAdd (α := M₂ →ₗ[R] M) (f.smulRight m) (f.smulRight m')

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f_1 : M →ₗ[R] M₂
f : M₂ →ₗ[R] R
m m' : M
x : M₂
⊢ Eq.{u_4 + 1} (α := M) ((f.smulRight (m + m') : (a : M₂) → M) x : M)
    ((HAdd.hAdd (α := M₂ →ₗ[R] M) (f.smulRight m) (f.smulRight m') : (a : M₂) → M) x : M)

Tactic:
apply smul_add

Premises used: smul_add
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f_1 : M →ₗ[R] M₂
f : M₂ →ₗ[R] R
c : R
m : M
h :
  ∀ (x : M₂),
    Eq.{u_4 + 1} (α := M) ((f.smulRight (c • m) : (a : M₂) → M) x : M)
      ((HSMul.hSMul (α := R) (β := M₂ →ₗ[R] M) ((RingHom.id R : (a : R) → R) c : R) (f.smulRight m) : (a : M₂) → M) x :
        M)
⊢ f.smulRight (c • m) = HSMul.hSMul (α := R) (β := M₂ →ₗ[R] M) ((RingHom.id R : (a : R) → R) c : R) (f.smulRight m)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f_1 : M →ₗ[R] M₂
f : M₂ →ₗ[R] R
c : R
m : M
x : M₂
⊢ Eq.{u_4 + 1} (α := M) ((f.smulRight (c • m) : (a : M₂) → M) x : M)
    ((HSMul.hSMul (α := R) (β := M₂ →ₗ[R] M) ((RingHom.id R : (a : R) → R) c : R) (f.smulRight m) : (a : M₂) → M) x : M)

Tactic:
apply smul_comm

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f_1 : M →ₗ[R] M₂
f f' : M₂ →ₗ[R] R
h :
  ∀ (x : M) (x_1 : M₂),
    Eq.{u_4 + 1} (α := M)
      (((({ toFun := (f + f').smulRight, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) :
            (a : M₂) → M)
          x_1 :
        M)
      ((((HAdd.hAdd (α := M →ₗ[R] M₂ →ₗ[R] M)
                    { toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M₂ →ₗ[R] M }
                    { toFun := f'.smulRight, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M₂ →ₗ[R] M } :
                  (a : M) → M₂ →ₗ[R] M)
                x :
              M₂ →ₗ[R] M) :
            (a : M₂) → M)
          x_1 :
        M)
⊢ { toFun := (f + f').smulRight, map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := M →ₗ[R] M₂ →ₗ[R] M) { toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M₂ →ₗ[R] M }
      { toFun := f'.smulRight, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M₂ →ₗ[R] M }

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LinearMap.End
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f_1 : M →ₗ[R] M₂
f f' : M₂ →ₗ[R] R
x : M
x_1 : M₂
⊢ Eq.{u_4 + 1} (α := M)
    (((({ toFun := (f + f').smulRight, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) :
          (a : M₂) → M)
        x_1 :
      M)
    ((((HAdd.hAdd (α := M →ₗ[R] M₂ →ₗ[R] M) { toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M₂ →ₗ[R] M }
                  { toFun := f'.smulRight, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M₂ →ₗ[R] M } :
                (a : M) → M₂ →ₗ[R] M)
              x :
            M₂ →ₗ[R] M) :
          (a : M₂) → M)
        x_1 :
      M)

Tactic:
apply add_smul

Premises used: add_smul