awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Basic (goal)
Goal:
R_1 : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst : Semiring R
f g : ι → R
h :
  ∀ (i : κ),
    Sum.elim 0 (f + g) (inl i) = HAdd.hAdd (α := κ ⊕ ι → R) (β := κ ⊕ ι → R) (Sum.elim 0 f) (Sum.elim 0 g) (inl i)
⊢ Sum.elim 0 (f + g) = HAdd.hAdd (α := κ ⊕ ι → R) (Sum.elim 0 f) (Sum.elim 0 g)
have h₁ : ∀ (i : ι),
  Sum.elim.{u_7, u_6, u_8 + 1} (α := κ) 0 (f + g) (inr i) =
    HAdd.hAdd (α := κ ⊕ ι → R) (β := κ ⊕ ι → R) (Sum.elim 0 f) (Sum.elim 0 g) (inr i)
Tactic: ext (i | i)
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Basic (goal)
Goal:
R_1 : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst : Semiring R
t : R
f : ι → R
⊢ Sum.elim 0 (t • f) = HSMul.hSMul (α := R) (β := κ ⊕ ι → R) ((RingHom.id R : (a : R) → R) t : R) (Sum.elim 0 f)
have h : ∀ (i : κ),
  Sum.elim 0 (t • f) (inl i) =
    HSMul.hSMul (α := R) (β := κ ⊕ ι → R) ((RingHom.id R : (a : R) → R) t : R) (Sum.elim 0 f) (inl i)
Tactic: ext (i | i)
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Basic (goal)
Goal:
R_1 : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst : Semiring R
t : R
f : ι → R
h :
  ∀ (i : κ),
    Sum.elim 0 (t • f) (inl i) =
      HSMul.hSMul (α := R) (β := κ ⊕ ι → R) ((RingHom.id R : (a : R) → R) t : R) (Sum.elim 0 f) (inl i)
⊢ Sum.elim 0 (t • f) = HSMul.hSMul (α := R) (β := κ ⊕ ι → R) ((RingHom.id R : (a : R) → R) t : R) (Sum.elim 0 f)
have h₁ : ∀ (i : ι),
  Sum.elim.{u_7, u_6, u_8 + 1} (α := κ) 0 (t • f) (inr i) =
    HSMul.hSMul (α := R) (β := κ ⊕ ι → R) ((RingHom.id R : (a : R) → R) t : R) (Sum.elim 0 f) (inr i)
Tactic: ext (i | i)
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Basic (goal)
Goal:
R_1 : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst : Semiring R
f g : ι → R
⊢ Sum.elim (f + g) 0 = HAdd.hAdd (α := ι ⊕ κ → R) (Sum.elim f 0) (Sum.elim g 0)
have h : ∀ (i : ι),
  Sum.elim.{u_6, u_7, u_8 + 1} (β := κ) (f + g) 0 (inl i) =
    HAdd.hAdd (α := ι ⊕ κ → R) (β := ι ⊕ κ → R) (Sum.elim f 0) (Sum.elim g 0) (inl i)
Tactic: ext (i | i)
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Basic (goal)
Goal:
R_1 : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst : Semiring R
f g : ι → R
h :
  ∀ (i : ι),
    Sum.elim.{u_6, u_7, u_8 + 1} (β := κ) (f + g) 0 (inl i) =
      HAdd.hAdd (α := ι ⊕ κ → R) (β := ι ⊕ κ → R) (Sum.elim f 0) (Sum.elim g 0) (inl i)
⊢ Sum.elim (f + g) 0 = HAdd.hAdd (α := ι ⊕ κ → R) (Sum.elim f 0) (Sum.elim g 0)
have h₁ : ∀ (i : κ),
  Sum.elim (f + g) 0 (inr i) = HAdd.hAdd (α := ι ⊕ κ → R) (β := ι ⊕ κ → R) (Sum.elim f 0) (Sum.elim g 0) (inr i)
Tactic: ext (i | i)
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Basic (goal)
Goal:
R_1 : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst : Semiring R
t : R
f : ι → R
⊢ Sum.elim (t • f) 0 = HSMul.hSMul (α := R) (β := ι ⊕ κ → R) ((RingHom.id R : (a : R) → R) t : R) (Sum.elim f 0)
have h : ∀ (i : ι),
  Sum.elim.{u_6, u_7, u_8 + 1} (β := κ) (t • f) 0 (inl i) =
    HSMul.hSMul (α := R) (β := ι ⊕ κ → R) ((RingHom.id R : (a : R) → R) t : R) (Sum.elim f 0) (inl i)
Tactic: ext (i | i)
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Basic (goal)
Goal:
R_1 : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst : Semiring R
t : R
f : ι → R
h :
  ∀ (i : ι),
    Sum.elim.{u_6, u_7, u_8 + 1} (β := κ) (t • f) 0 (inl i) =
      HSMul.hSMul (α := R) (β := ι ⊕ κ → R) ((RingHom.id R : (a : R) → R) t : R) (Sum.elim f 0) (inl i)
⊢ Sum.elim (t • f) 0 = HSMul.hSMul (α := R) (β := ι ⊕ κ → R) ((RingHom.id R : (a : R) → R) t : R) (Sum.elim f 0)
have h₁ : ∀ (i : κ),
  Sum.elim (t • f) 0 (inr i) =
    HSMul.hSMul (α := R) (β := ι ⊕ κ → R) ((RingHom.id R : (a : R) → R) t : R) (Sum.elim f 0) (inr i)
Tactic: ext (i | i)
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R : Type u_14
M : Type u_15
M₂ : Type u_16
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
F : Type u_17
inst_5 : FunLike F M M₂
inst_6 : LinearMapClass F R M M₂
f : F
r : R
x : M
⊢ (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) r ((f : (a : M) → M₂) x : M₂)
have rw : HSMul.hSMul (β := M₂) r ((f : (a : M) → M₂) x : M₂) = HSMul.hSMul (β := M₂) r ((f : (a : M) → M₂) x : M₂)
Tactic: rw [map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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
F : Type u_14
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
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 S M₃
σ : R →+* S
inst_9 : FunLike F M M₃
inst_10 : SemilinearMapClass F σ M M₃
f : F
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : M) → M₃) 0 : M₃) (0 : M₃)
have rw : HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) 0 : S) ((f : (a : M) → M₃) 0 : M₃) = 0
Tactic: rw [← zero_smul R (0 : M), map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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
F : Type u_14
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
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 S M₃
σ : R →+* S
inst_9 : FunLike F M M₃
inst_10 : SemilinearMapClass F σ M M₃
f : F
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₃)
have rw : HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) c : S) ((f : (a : M) → M₃) x : M₃) =
  HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) c : S) ((f : (a : M) → M₃) x : M₃)
Tactic: rw [map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R M₂
inst_8 : Module S M₃
σ : R →+* S
f g : M →ₛₗ[σ] M₃
h : Eq (α := (a : M) → M₃) ((fun (f : M →ₛₗ[σ] M₃) ↦ f.toFun) f) ((fun (f : M →ₛₗ[σ] M₃) ↦ f.toFun) g)
⊢ f = g
have mk : ∀ (toAddHom : M →ₙ+ M₃)
  (map_smul' :
    ∀ (m : R) (x : M),
      toAddHom.toFun (m • x) = HSMul.hSMul.{u_5, u_11, u_11} (α := S) ((σ : (a : R) → S) m : S) (toAddHom.toFun x))
  (h :
    Eq (α := (a : M) → M₃) ((fun (f : M →ₛₗ[σ] M₃) ↦ f.toFun) { toAddHom := toAddHom, map_smul' := map_smul' })
      ((fun (f : M →ₛₗ[σ] M₃) ↦ f.toFun) g)),
  { toAddHom := toAddHom, map_smul' := map_smul' : M →ₛₗ[σ] M₃ } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R M₂
inst_8 : Module S M₃
σ : R →+* S
g : M →ₛₗ[σ] M₃
toAddHom : M →ₙ+ M₃
map_smul' :
  ∀ (m : R) (x : M),
    toAddHom.toFun (m • x) = HSMul.hSMul.{u_5, u_11, u_11} (α := S) ((σ : (a : R) → S) m : S) (toAddHom.toFun x)
h :
  Eq (α := (a : M) → M₃) ((fun (f : M →ₛₗ[σ] M₃) ↦ f.toFun) { toAddHom := toAddHom, map_smul' := map_smul' })
    ((fun (f : M →ₛₗ[σ] M₃) ↦ f.toFun) g)
⊢ { toAddHom := toAddHom, map_smul' := map_smul' : M →ₛₗ[σ] M₃ } = g
have mk : ∀ (toAddHom_1 : M →ₙ+ M₃)
  (map_smul'_1 :
    ∀ (m : R) (x : M),
      toAddHom_1.toFun (m • x) = HSMul.hSMul.{u_5, u_11, u_11} (α := S) ((σ : (a : R) → S) m : S) (toAddHom_1.toFun x))
  (h :
    Eq (α := (a : M) → M₃) ((fun (f : M →ₛₗ[σ] M₃) ↦ f.toFun) { toAddHom := toAddHom, map_smul' := map_smul' })
      ((fun (f : M →ₛₗ[σ] M₃) ↦ f.toFun) { toAddHom := toAddHom_1, map_smul' := map_smul'_1 })),
  { toAddHom := toAddHom, map_smul' := map_smul' : M →ₛₗ[σ] M₃ } = { toAddHom := toAddHom_1, map_smul' := map_smul'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R M₂
inst_8 : Module S M₃
σ : R →+* S
toAddHom : M →ₙ+ M₃
map_smul' :
  ∀ (m : R) (x : M),
    toAddHom.toFun (m • x) = HSMul.hSMul.{u_5, u_11, u_11} (α := S) ((σ : (a : R) → S) m : S) (toAddHom.toFun x)
toAddHom_1 : M →ₙ+ M₃
map_smul'_1 :
  ∀ (m : R) (x : M),
    toAddHom_1.toFun (m • x) = HSMul.hSMul.{u_5, u_11, u_11} (α := S) ((σ : (a : R) → S) m : S) (toAddHom_1.toFun x)
h :
  Eq (α := (a : M) → M₃) ((fun (f : M →ₛₗ[σ] M₃) ↦ f.toFun) { toAddHom := toAddHom, map_smul' := map_smul' })
    ((fun (f : M →ₛₗ[σ] M₃) ↦ f.toFun) { toAddHom := toAddHom_1, map_smul' := map_smul'_1 })
⊢ { toAddHom := toAddHom, map_smul' := map_smul' : M →ₛₗ[σ] M₃ } = { toAddHom := toAddHom_1, map_smul' := map_smul'_1 }
have mk : toAddHom = toAddHom_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R M₂
inst_8 : Module S M₃
σ : R →+* S
toAddHom : M →ₙ+ M₃
map_smul' :
  ∀ (m : R) (x : M),
    toAddHom.toFun (m • x) = HSMul.hSMul.{u_5, u_11, u_11} (α := S) ((σ : (a : R) → S) m : S) (toAddHom.toFun x)
toAddHom_1 : M →ₙ+ M₃
map_smul'_1 :
  ∀ (m : R) (x : M),
    toAddHom_1.toFun (m • x) = HSMul.hSMul.{u_5, u_11, u_11} (α := S) ((σ : (a : R) → S) m : S) (toAddHom_1.toFun x)
h :
  Eq (α := (a : M) → M₃) ((fun (f : M →ₛₗ[σ] M₃) ↦ f.toFun) { toAddHom := toAddHom, map_smul' := map_smul' })
    ((fun (f : M →ₛₗ[σ] M₃) ↦ f.toFun) { toAddHom := toAddHom_1, map_smul' := map_smul'_1 })
⊢ toAddHom = toAddHom_1
have mk : Eq (α := (a : M) → M₃) (⇑toAddHom : (a : M) → M₃) (⇑toAddHom_1 : (a : M) → M₃)
Tactic: apply DFunLike.coe_injective'
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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 : Type u_14
inst_6 : FunLike F M M₃
inst_7 : SemilinearMapClass F σ M M₃
f g : F
h :
  Eq (α := M →ₛₗ[σ] M₃) (↑f : [inst_8 : FunLike F M M₃] → [SemilinearMapClass F σ M M₃] → M →ₛₗ[σ] M₃)
    (↑g : [inst_8 : FunLike F M M₃] → [SemilinearMapClass F σ M M₃] → M →ₛₗ[σ] M₃)
⊢ f = g
have h₁ : ∀ (x : M), Eq.{u_11 + 1} (α := M₃) ((f : (a : M) → M₃) x : M₃) ((g : (a : M) → M₃) x : M₃)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (hypothesis)
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 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R M₂
inst_8 : Module S M₃
σ_1 : R →+* S
σ : R →+* R
inst_9 : RingHomId σ
r : R
x : M
⊢ r • x = HSMul.hSMul (α := R) ((σ : (a : R) → R) r : R) x
have this : σ = RingHom.id R
Tactic: have := (RingHomId.eq_id : σ = _)
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R M₂
inst_8 : Module S M₃
σ_1 : R →+* S
σ : R →+* R
inst_9 : RingHomId σ
r : R
x : M
this : σ = RingHom.id R
⊢ r • x = HSMul.hSMul (α := R) ((σ : (a : R) → R) r : R) x
have subst : ∀ [RingHomId (RingHom.id R)], r • x = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x
Tactic: subst this
Cleared hypotheses: σ, inst_9, this
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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
⊢ (fₗ : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((fₗ : (a : M) → M₂) x : M₂)
have rw : (fₗ : (a : M) → M₂) (HSMul.hSMul (β := S) c 1 • 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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₂)
⊢ (fₗ : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((fₗ : (a : M) → M₂) x : M₂)
have 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₂)
Tactic: rw [← smul_one_smul S c x, ← smul_one_smul S c (fₗ x), map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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₂)
⊢ (fₗ : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((fₗ : (a : M) → M₂) x : M₂)
have 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₂)
Tactic: rw [← smul_one_smul S c x, ← smul_one_smul S c (fₗ x), map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) ((r • s) • x) : M₂) ((f : (a : M) → M₂) (r • s • x) : M₂)
have rw : (f : (a : M) → M₂) ((r • s) • x) = HSMul.hSMul (β := M₂) r ((f : (a : M) → M₂) (s • x) : M₂)
Tactic: rw [f.map_smul_of_tower r, map_smul, map_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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₂)
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) ((r • s) • x) : M₂) ((f : (a : M) → M₂) (r • s • x) : M₂)
have rw₁ : HSMul.hSMul (β := M₂) (r • s) ((f : (a : M) → M₂) x : M₂) = HSMul.hSMul (β := M₂) r ((f : (a : M) → M₂) (s • x) : M₂)
Tactic: rw [f.map_smul_of_tower r, map_smul, map_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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₂)
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) ((r • s) • x) : M₂) ((f : (a : M) → M₂) (r • s • x) : M₂)
have rw₂ : HSMul.hSMul (β := M₂) (r • s) ((f : (a : M) → M₂) x : M₂) = r • HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)
Tactic: rw [f.map_smul_of_tower r, map_smul, map_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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₂)
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) ((r • s) • x) : M₂) ((f : (a : M) → M₂) (r • s • x) : M₂)
have rw₃ : r • HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂) = r • HSMul.hSMul (β := M₂) s ((f : (a : M) → M₂) x : M₂)
Tactic: rw [f.map_smul_of_tower r, map_smul, map_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : R) → M₃) x : M₃) ((g : (a : R) → M₃) x : M₃)
have rw : Eq.{u_11 + 1} (α := M₃) ((f : (a : R) → M₃) (x * 1) : M₃) ((g : (a : R) → M₃) (x * 1) : M₃)
Tactic: rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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₃)
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : R) → M₃) x : M₃) ((g : (a : R) → M₃) x : M₃)
have 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₃)
Tactic: rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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₃)
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : R) → M₃) x : M₃) ((g : (a : R) → M₃) x : M₃)
have 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)
Tactic: rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
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)
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : R) → M₃) x : M₃) ((g : (a : R) → M₃) x : M₃)
have 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₃)
Tactic: rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]