awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst_10 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_11 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_12 : Nonempty α
inst_13 : FaithfulSMul R M
⊢ FaithfulSMul R (α →₀ M)

Tactic:
.of_injective (Finsupp.lsingle <| Classical.arbitrary _) (Finsupp.single_injective _)

Premises used: Finsupp.single_injective, FaithfulSMul.of_injective, Classical.arbitrary, Finsupp.lsingle
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set α
f : α →₀ M
⊢ Eq (α := Finsupp.{u_1, u_2} (↑s : Type u_1) M)
    ((lsubtypeDomain s : (a : α →₀ M) → (↑s : Type u_1) →₀ M) f : Finsupp.{u_1, u_2} (↑s : Type u_1) M)
    (subtypeDomain (fun (x : α) ↦ x ∈ s) f : Finsupp.{u_1, u_2} { x : α // x ∈ s } M)

Tactic:
rfl

Premises used: Finsupp.subtypeDomain, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : α
b : M
⊢ Eq (α := α →₀ M) ((lsingle a : (a : M) → α →₀ M) b : α →₀ M) (single a b : α →₀ M)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : α
f : α →₀ M
⊢ Eq.{u_2 + 1} (α := M) ((lapply a : (a : α →₀ M) → M) f : M) ((f : (a : α) → M) a : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : α
h : ∀ (x : M), Eq (α := M) ((lapply a ∘ₗ lsingle a : (a : M) → M) x : M) ((LinearMap.id : (a : M) → M) x : M)
⊢ Eq.{u_2 + 1} (α := M →ₗ[R] M) (lapply a ∘ₗ lsingle a) LinearMap.id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : α
x : M
⊢ Eq (α := M) ((lapply a ∘ₗ lsingle a : (a : M) → M) x : M) ((LinearMap.id : (a : M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a a' : α
h : a ≠ a'
h₁ : ∀ (x : M), Eq (α := M) ((lapply a ∘ₗ lsingle a' : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
⊢ Eq.{u_2 + 1} (α := M →ₗ[R] M) (lapply a ∘ₗ lsingle a') 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a a' : α
h : a ≠ a'
x : M
⊢ Eq (α := M) ((lapply a ∘ₗ lsingle a' : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)

Tactic:
simp [h.symm]

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α' : Type u_9
f : α → α'
l : α →₀ M
⊢ (lmapDomain M R f : (a : α →₀ M) → α' →₀ M) l = mapDomain f l

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.mapDomain, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α' : Type u_9
f : α → α'
⊢ Eq (α := (a : α →₀ M) → α' →₀ M) (⇑(lmapDomain M R f) : (a : α →₀ M) → α' →₀ M) (mapDomain f)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.mapDomain, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := (α →₀ M) →ₗ[R] α →₀ M) (lmapDomain M R _root_.id) LinearMap.id

Tactic:
LinearMap.ext fun _ => mapDomain_id

Premises used: LinearMap.ext, Finsupp.mapDomain_id
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α' : Type u_9
α'' : Type u_10
f : α → α'
g : α' → α''
⊢ Eq (α := (α →₀ M) →ₗ[R] α'' →₀ M) (lmapDomain M R (g ∘ f)) (lmapDomain M R g ∘ₗ lmapDomain M R f)

Tactic:
LinearMap.ext fun _ => mapDomain_comp

Premises used: LinearMap.ext, Finsupp.mapDomain_comp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst_10 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_11 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
α' : Type u_9
α'' : Type u_10
f : α ≃ α'
x : α →₀ M
⊢ mapDomain (⇑f.symm : (a : α') → α) (AddHom.toFun (toAddHom (lmapDomain M R f.toFun)) x) = x

Tactic:
simp [← mapDomain_comp]

Premises used: Finsupp.mapDomain_comp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst_10 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_11 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
α' : Type u_9
α'' : Type u_10
f : α ≃ α'
x : α' →₀ M
⊢ AddHom.toFun (toAddHom (lmapDomain M R f.toFun)) (mapDomain (⇑f.symm : (a : α') → α) x) = x

Tactic:
simp [← mapDomain_comp]

Premises used: Finsupp.mapDomain_comp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α' : Type u_9
f : α ≃ α'
⊢ Eq (α := (a : α →₀ M) → α' →₀ M) (⇑(linearEquiv M R f) : (a : α →₀ M) → α' →₀ M) (mapDomain (⇑f : (a : α) → α'))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.mapDomain, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α' : Type u_9
f : α ≃ α'
⊢ Eq (α := (α →₀ M) →ₗ[R] α' →₀ M) (↑(linearEquiv M R f) : (α →₀ M) →ₗ[R] α' →₀ M) (lmapDomain M R (⇑f : (a : α) → α'))

Tactic:
rfl

Premises used: Finsupp.lmapDomain, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α' : Type u_9
f : α ≃ α'
⊢ Eq (α := (α' →₀ M) ≃ₗ[R] α →₀ M) (LinearEquiv.symm (linearEquiv M R f)) (linearEquiv M R f.symm)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, LinearEquiv.symm, Finsupp.mapDomain.linearEquiv, Finsupp.mapDomain, Finsupp.sum, Finsupp.lmapDomain, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst_10 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_11 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
β : Type u_9
f : α → β
hf : Function.Injective f
x y : β →₀ M
h :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := M) ((comapDomain f (x + y) ⋯ : (a : α) → M) a : M)
      ((comapDomain f x ⋯ + comapDomain f y ⋯ : (a : α) → M) a : M)
⊢ comapDomain f (x + y) ⋯ = comapDomain f x ⋯ + comapDomain f y ⋯

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst_10 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_11 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
β : Type u_9
f : α → β
hf : Function.Injective f
x y : β →₀ M
a : α
⊢ Eq.{u_2 + 1} (α := M) ((comapDomain f (x + y) ⋯ : (a : α) → M) a : M)
    ((comapDomain f x ⋯ + comapDomain f y ⋯ : (a : α) → M) a : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst_10 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_11 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
β : Type u_9
f : α → β
hf : Function.Injective f
c : R
x : β →₀ M
h :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := M) ((comapDomain f (c • x) ⋯ : (a : α) → M) a : M)
      ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (comapDomain f x ⋯) : (a : α) → M) a : M)
⊢ comapDomain f (c • x) ⋯ = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (comapDomain f x ⋯)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst_10 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_11 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
β : Type u_9
f : α → β
hf : Function.Injective f
c : R
x : β →₀ M
a : α
⊢ Eq.{u_2 + 1} (α := M) ((comapDomain f (c • x) ⋯ : (a : α) → M) a : M)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (comapDomain f x ⋯) : (a : α) → M) a : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
β : Type u_9
f : α → β
hf : Function.Injective f
⊢ Function.LeftInverse (α := α →₀ M) (⇑(lcomapDomain f hf) : (a : β →₀ M) → α →₀ M) (mapDomain f)

Tactic:
comapDomain_mapDomain f hf

Premises used: Function.LeftInverse, Finsupp.comapDomain_mapDomain, Finsupp.comapDomain
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := (α →₀ M) →ₗ[R] α →₀ M) (linearMap LinearMap.id) LinearMap.id

Tactic:
LinearMap.ext mapRange_id

Premises used: LinearMap.ext, Finsupp.mapRange_id
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R₂ N
inst_7 : AddCommMonoid P
inst_8 : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : N →ₛₗ[σ₂₃] P
f₂ : M →ₛₗ[σ₁₂] N
⊢ Eq (α := (α →₀ M) →ₛₗ[σ₁₃] α →₀ P) (linearMap (f ∘ₛₗ f₂)) (linearMap f ∘ₛₗ linearMap f₂)

Tactic:
LinearMap.ext <| mapRange_comp f f.map_zero f₂ f₂.map_zero (comp f f₂).map_zero

Premises used: LinearMap.ext, LinearMap.map_zero, Finsupp.mapRange_comp, LinearMap.comp, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] N
⊢ Eq (α := (α →₀ M) →+ α →₀ N) (toAddMonoidHom (linearMap f)) (addMonoidHom f.toAddMonoidHom)

Tactic:
AddMonoidHom.ext fun _ => rfl

Premises used: AddMonoidHom.ext, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := (α →₀ M) ≃ₗ[R] α →₀ M) (linearEquiv (LinearEquiv.refl R M)) (LinearEquiv.refl R (α →₀ M))

Tactic:
LinearEquiv.ext mapRange_id

Premises used: LinearEquiv.ext, Finsupp.mapRange_id
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R₂ N
inst_7 : AddCommMonoid P
inst_8 : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_11 : RingHomInvPair σ₁₂ σ₂₁
inst_12 : RingHomInvPair σ₂₁ σ₁₂
inst_13 : RingHomInvPair σ₂₃ σ₃₂
inst_14 : RingHomInvPair σ₃₂ σ₂₃
inst_15 : RingHomInvPair σ₁₃ σ₃₁
inst_16 : RingHomInvPair σ₃₁ σ₁₃
f : M ≃ₛₗ[σ₁₂] N
f₂ : N ≃ₛₗ[σ₂₃] P
⊢ Eq (α := (α →₀ M) ≃ₛₗ[σ₁₃] α →₀ P) (linearEquiv (f.trans f₂)) (LinearEquiv.trans (linearEquiv f) (linearEquiv f₂))

Tactic:
LinearEquiv.ext <| mapRange_comp f₂ f₂.map_zero f f.map_zero (f.trans f₂).map_zero

Premises used: LinearEquiv.map_zero, LinearEquiv.ext, Finsupp.mapRange_comp, LinearEquiv.trans, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
f : M ≃ₛₗ[σ₁₂] N
⊢ Eq (α := (α →₀ N) ≃ₛₗ[σ₂₁] α →₀ M) (LinearEquiv.symm (linearEquiv f)) (linearEquiv f.symm)

Tactic:
LinearEquiv.ext fun _x => rfl

Premises used: LinearEquiv.ext, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
f : M ≃ₛₗ[σ₁₂] N
⊢ Eq (α := (α →₀ M) ≃+ (α →₀ N)) (LinearEquiv.toAddEquiv (linearEquiv f)) (addEquiv f.toAddEquiv)

Tactic:
AddEquiv.ext fun _ => rfl

Premises used: AddEquiv.ext, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R₂ N
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
f : M ≃ₛₗ[σ₁₂] N
⊢ Eq (α := (α →₀ M) →ₛₗ[σ₁₂] α →₀ N) (↑(linearEquiv f) : (α →₀ M) →ₛₗ[σ₁₂] α →₀ N) (linearMap (↑f : M →ₛₗ[σ₁₂] N))

Tactic:
LinearMap.ext fun _ => rfl

Premises used: LinearMap.ext, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α_1 : Type u_1
M_1 : Type u_2
N : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ₁₂ : R_1 →+* R₂
σ₂₁ : R₂ →+* R_1
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R_1 →+* R₃
σ₃₁ : R₃ →+* R_1
inst_10 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_11 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
α : Type u_9
β : Type u_10
R : Type u_11
M : Type u_12
inst_12 : Semiring R
inst_13 : AddCommMonoid M
inst_14 : Module R M
c : R
f : α × β →₀ M
h :
  ∀ (a : α) (a_1 : β),
    Eq.{u_12 + 1} (α := M)
      ((((Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) (c • f) : (a : α) → β →₀ M) a : β →₀ M) : (a : β) → M) a_1 : M)
      ((((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) f) :
                  (a : α) → β →₀ M)
                a :
              β →₀ M) :
            (a : β) → M)
          a_1 :
        M)
⊢ Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) (c • f) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) f)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α_1 : Type u_1
M_1 : Type u_2
N : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ₁₂ : R_1 →+* R₂
σ₂₁ : R₂ →+* R_1
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R_1 →+* R₃
σ₃₁ : R₃ →+* R_1
inst_10 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_11 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
α : Type u_9
β : Type u_10
R : Type u_11
M : Type u_12
inst_12 : Semiring R
inst_13 : AddCommMonoid M
inst_14 : Module R M
c : R
f : α × β →₀ M
a : α
a_1 : β
⊢ Eq.{u_12 + 1} (α := M)
    ((((Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) (c • f) : (a : α) → β →₀ M) a : β →₀ M) : (a : β) → M) a_1 : M)
    ((((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) f) :
                (a : α) → β →₀ M)
              a :
            β →₀ M) :
          (a : β) → M)
        a_1 :
      M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
α : Type u_9
β : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α →₀ β →₀ M
xy : α × β
⊢ Eq.{u_12 + 1} (α := M)
    ((((LinearEquiv.symm (curryLinearEquiv R) : (a : α →₀ β →₀ M) → α × β →₀ M) f : α × β →₀ M) : (a : α × β) → M) xy :
      M)
    ((((f : (a : α) → β →₀ M) xy.1 : β →₀ M) : (a : β) → M) xy.2 : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
R : Type u_4
M : Type u_5
ι : Type u_6
inst_5 : Semiring R
inst_6 : Subsingleton R
inst_7 : AddCommMonoid M
inst_8 : Module R M
f : ι →₀ R
⊢ (fun (x : M) ↦ (0 : ι →₀ R)) ((fun (x : ι →₀ R) ↦ (0 : M)) f) = f

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x : ι →₀ M
⊢ (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (HSMul.hSMul (β := ι →₀ M) g 0) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) 0)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x : ι →₀ M
i : ι
m : M
h :
  ∀ (j : ι),
    Eq.{u_6 + 1} (α := M)
      ((((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (HSMul.hSMul (β := ι →₀ M) g (single i m)) :
              ι →₀ M) :
            (a : ι) → M)
          j :
        M)
      ((HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
              ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
              ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) :
            (a : ι) → M)
          j :
        M)
⊢ (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (HSMul.hSMul (β := ι →₀ M) g (single i m)) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M)

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x : ι →₀ M
i : ι
m : M
j : ι
h :
  Eq (α := M) ((f : (a : M) → M) (lapply j ∘ₗ g ∘ₗ lsingle i • m) : M)
    ((HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
            ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
            ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) :
          (a : ι) → M)
        j :
      M)
⊢ Eq.{u_6 + 1} (α := M)
    ((((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (HSMul.hSMul (β := ι →₀ M) g (single i m)) :
            ι →₀ M) :
          (a : ι) → M)
        j :
      M)
    ((HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
            ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
            ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) :
          (a : ι) → M)
        j :
      M)

Tactic:
change f (Finsupp.lapply j ∘ₗ g ∘ₗ Finsupp.lsingle i • m) = _

Premises used: LinearMap.comp, HSMul.hSMul, Finsupp.lapply, DFunLike.coe, Finsupp.lsingle
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x : ι →₀ M
i : ι
m : M
j : ι
h :
  HSMul.hSMul (β := M) (lapply j ∘ₗ g ∘ₗ lsingle i) ((f : (a : M) → M) m : M) =
    (HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
          ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
          ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) :
        (a : ι) → M)
      j
⊢ Eq (α := M) ((f : (a : M) → M) (lapply j ∘ₗ g ∘ₗ lsingle i • m) : M)
    ((HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
            ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
            ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) :
          (a : ι) → M)
        j :
      M)

Tactic:
rw [map_smul]

Premises used: map_smul
-- Module: Mathlib.LinearAlgebra.Finsupp.Defs
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x : ι →₀ M
i : ι
m : M
j : ι
⊢ HSMul.hSMul (β := M) (lapply j ∘ₗ g ∘ₗ lsingle i) ((f : (a : M) → M) m : M) =
    (HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
          ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
          ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) :
        (a : ι) → M)
      j

Tactic:
simp