awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
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)
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)
⊢ Sum.elim 0 (t • f) = HSMul.hSMul (α := R) (β := κ ⊕ ι → R) ((RingHom.id R : (a : R) → R) t : R) (Sum.elim 0 f)

Tactic:
ext (i | i)
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
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
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:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
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
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:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
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)
h₁ :
  ∀ (i : κ),
    Sum.elim (f + g) 0 (inr i) = HAdd.hAdd (α := ι ⊕ κ → R) (β := ι ⊕ κ → R) (Sum.elim f 0) (Sum.elim g 0) (inr i)
⊢ Sum.elim (f + g) 0 = HAdd.hAdd (α := ι ⊕ κ → R) (Sum.elim f 0) (Sum.elim g 0)

Tactic:
ext (i | i)
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
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
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:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
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
i : κ
⊢ Sum.elim (f + g) 0 (inr i) = HAdd.hAdd (α := ι ⊕ κ → R) (β := ι ⊕ κ → R) (Sum.elim f 0) (Sum.elim g 0) (inr i)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
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)
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)
⊢ Sum.elim (t • f) 0 = HSMul.hSMul (α := R) (β := ι ⊕ κ → R) ((RingHom.id R : (a : R) → R) t : R) (Sum.elim f 0)

Tactic:
ext (i | i)
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
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
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:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
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
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:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
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
rw rw₁ : HSMul.hSMul (β := M₂) r ((f : (a : M) → M₂) x : M₂) = HSMul.hSMul (β := M₂) r ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (r • x) = HSMul.hSMul (β := M₂) r ((f : (a : M) → M₂) x : M₂)

Tactic:
rw [map_smul]

Premises used: map_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 : 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
rw : HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) 0 : S) ((f : (a : M) → M₃) 0 : M₃) = 0
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : M) → M₃) 0 : M₃) (0 : M₃)

Tactic:
rw [← zero_smul R (0 : M), map_smulₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ, zero_smul, OfNat.ofNat
-- 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
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
⊢ HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) 0 : S) ((f : (a : M) → M₃) 0 : M₃) = 0

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
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
rw 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₃)
⊢ (f : (a : M) → M₃) (c • x) =
    HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) c : S) ((f : (a : M) → M₃) x : M₃)

Tactic:
rw [map_smulₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
F : Type u_14
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 : F
inst_6 : FunLike F M M₃
inst_7 : SemilinearMapClass F σ M M₃
σ' : S →+* R
inst_8 : RingHomInvPair σ σ'
c : S
x : M
⊢ HSMul.hSMul (β := M₃) c ((f : (a : M) → M₃) x : M₃) =
    (f : (a : M) → M₃) (HSMul.hSMul.{u_1, u_8, u_8} (α := R) ((σ' : (a : S) → R) c : R) x)

Tactic:
simp [map_smulₛₗ _]

Premises used: MulActionSemiHomClass.map_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 : 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)
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
⊢ f = g

Tactic:
cases f
-- 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 : 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)
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 }
⊢ { toAddHom := toAddHom, map_smul' := map_smul' : M →ₛₗ[σ] M₃ } = g

Tactic:
cases g
-- 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 : 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 })
mk : toAddHom = toAddHom_1
⊢ { toAddHom := toAddHom, map_smul' := map_smul' : M →ₛₗ[σ] M₃ } = { toAddHom := toAddHom_1, map_smul' := map_smul'_1 }

Tactic:
congr
-- 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 : 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 })
mk : Eq (α := (a : M) → M₃) (⇑toAddHom : (a : M) → M₃) (⇑toAddHom_1 : (a : M) → M₃)
⊢ toAddHom = toAddHom_1

Tactic:
apply DFunLike.coe_injective'

Premises used: DFunLike.coe_injective'
-- 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 : 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 })
⊢ Eq (α := (a : M) → M₃) (⇑toAddHom : (a : M) → M₃) (⇑toAddHom_1 : (a : M) → M₃)

Tactic:
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 : 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 })
⊢ Eq (α := (a : M) → M₃) (⇑toAddHom : (a : M) → M₃) (⇑toAddHom_1 : (a : M) → M₃)

Tactic:
exact h
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
F : Type u_14
inst_6 : FunLike F M M₃
inst_7 : SemilinearMapClass F σ M M₃
f : F
⊢ Eq (α := (a : M) → M₃)
    (⇑(↑f : [inst_8 : FunLike F M M₃] → [SemilinearMapClass F σ 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_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
f : M →ₛₗ[σ] M₃
⊢ Eq (α := (a : M) → M₃) (⇑f.toAddHom : (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_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
f : M →ₛₗ[σ] M₃
⊢ f.toFun = (⇑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_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
f g : M →ₛₗ[σ] M₃
h : ∀ (x : M), Eq.{u_11 + 1} (α := M₃) ((f : (a : M) → M₃) x : M₃) ((g : (a : M) → M₃) x : M₃)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
f : M →ₛₗ[σ] M₃
f' : M → M₃
h : f' = (⇑f : (a : M) → M₃)
⊢ (⇑(f.copy f' h) : (a : M) → M₃) = f'

Tactic:
rfl

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

Tactic:
DFunLike.ext' h

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

Tactic:
rfl

Premises used: AddHomClass.toAddHom, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
F : 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₃)
h₁ : ∀ (x : M), Eq.{u_11 + 1} (α := M₃) ((f : (a : M) → M₃) x : M₃) ((g : (a : M) → M₃) x : M₃)
⊢ f = g

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
F : 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₃)
m : M
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : M) → M₃) m : M₃) ((g : (a : M) → M₃) m : M₃)

Tactic:
DFunLike.congr_fun h m

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
F : 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₃)
m : M
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : M) → M₃) m : M₃) ((g : (a : M) → M₃) m : M₃)

Tactic:
exact DFunLike.congr_fun h m

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
M : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ (id : (a : M) → M) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
M : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{u_8 + 1} (α := (a : M) → M) (⇑id : (a : M) → M) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : Semiring R
inst_1 : Semiring S
inst_2 : 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
⊢ σ = RingHom.id R

Tactic:
have := (RingHomId.eq_id : σ = _)
-- 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 : 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
subst : ∀ [RingHomId (RingHom.id R)], r • x = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x
⊢ r • x = HSMul.hSMul (α := R) ((σ : (a : R) → R) r : R) x

Tactic:
subst this
-- 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 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R M₂
inst_8 : Module S M₃
σ : R →+* S
r : R
x : M
inst_9 : RingHomId (RingHom.id R)
⊢ r • x = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
M : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
σ : R →+* R
inst_3 : RingHomId σ
⊢ Eq.{u_8 + 1} (α := (a : M) → M) (⇑id' : (a : M) → M) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
fₗ : M →ₗ[R] M₂
⊢ IsLinearMap.{u_1, u_8, u_10} R (M := M) (M₂ := M₂) (⇑fₗ : (a : M) → M₂)

Tactic:
⟨fₗ.map_add', fₗ.map_smul'⟩

Premises used: LinearMap.toAddHom, AddHom.map_add', LinearMap.map_smul', IsLinearMap.mk
-- Module: Mathlib.Algebra.Module.LinearMap.Defs
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module S M₃
σ : R →+* S
⊢ Injective (α := M →ₛₗ[σ] M₃) (β := (a : M) → M₃) (DFunLike.coe (β := fun (x : M) ↦ M₃))

Tactic:
DFunLike.coe_injective

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

Tactic:
DFunLike.congr_arg f

Premises used: DFunLike.congr_arg