awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst : Monoid G
inst_1 : MulAction G α
inst_2 : AddCommMonoid M
g : G
f f' : α →₀ M
a : α
h :
  Eq.{u_3 + 1} (α := M) ((mapDomain (fun (x : α) ↦ g • x) (f + f') : (a : α) → M) a : M)
    ((HAdd.hAdd (α := α →₀ M) (mapDomain (fun (x : α) ↦ g • x) f) (mapDomain (fun (x : α) ↦ g • x) f') : (a : α) → M)
        a :
      M)
⊢ Eq.{u_3 + 1} (α := M) ((g • (f + f') : (a : α) → M) a : M) ((g • f + g • f' : (a : α) → M) a : M)

Tactic:
simp only [comapSMul_def]

Premises used: Finsupp.comapSMul_def
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst : Monoid G
inst_1 : MulAction G α
inst_2 : AddCommMonoid M
g : G
f f' : α →₀ M
a : α
⊢ Eq.{u_3 + 1} (α := M) ((mapDomain (fun (x : α) ↦ g • x) (f + f') : (a : α) → M) a : M)
    ((HAdd.hAdd (α := α →₀ M) (mapDomain (fun (x : α) ↦ g • x) f) (mapDomain (fun (x : α) ↦ g • x) f') : (a : α) → M)
        a :
      M)

Tactic:
simp [mapDomain_add]

Premises used: Finsupp.mapDomain_add
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
G : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : AddCommMonoid M
g : G
f : α →₀ M
a : α
rw : ((g • f : (a : α) → M) (g • g⁻¹ • a) : M)
| ((g • f : (a : α) → M) a : M)

Tactic:
rw [← smul_inv_smul g a]

Premises used: smul_inv_smul
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
G : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : AddCommMonoid M
g : G
f : α →₀ M
a : α
conv_lhs : Eq.{u_3 + 1} (α := M) ((g • f : (a : α) → M) (g • g⁻¹ • a) : M) ((f : (a : α) → M) (g⁻¹ • a) : M)
⊢ Eq.{u_3 + 1} (α := M) ((g • f : (a : α) → M) a : M) ((f : (a : α) → M) (g⁻¹ • a) : M)

Tactic:
conv_lhs => rw [← smul_inv_smul g a]

Premises used: smul_inv_smul
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
G : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : AddCommMonoid M
g : G
f : α →₀ M
a : α
⊢ Eq.{u_3 + 1} (α := M) ((g • f : (a : α) → M) (g • g⁻¹ • a) : M) ((f : (a : α) → M) (g⁻¹ • a) : M)

Tactic:
mapDomain_apply (MulAction.injective g) _ (g⁻¹ • a)

Premises used: Finsupp.mapDomain_apply, Inv.inv, HSMul.hSMul, MulAction.injective
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
G : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : AddCommMonoid M
g : G
f : α →₀ M
a : α
⊢ Eq.{u_3 + 1} (α := M) ((g • f : (a : α) → M) (g • g⁻¹ • a) : M) ((f : (a : α) → M) (g⁻¹ • a) : M)

Tactic:
exact mapDomain_apply (MulAction.injective g) _ (g⁻¹ • a)

Premises used: Finsupp.mapDomain_apply, Inv.inv, HSMul.hSMul, MulAction.injective
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
R : Type u_6
inst : Zero M
inst_1 : SMulZeroClass R M
k : R
hk : IsSMulRegular M k
⊢ IsSMulRegular (α →₀ M) k

Tactic:
fun _ _ h => ext fun i => hk (DFunLike.congr_fun h i)

Premises used: DFunLike.congr_fun, Finsupp.ext, IsSMulRegular, Function.Injective
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst : Nonempty α
inst_1 : Zero M
inst_2 : SMulZeroClass R M
inst_3 : FaithfulSMul R M
m₁ m₂ : R
h : ∀ (a : α →₀ M), m₁ • a = m₂ • a
a : α
m : M
⊢ m₁ • m = m₂ • m

Tactic:
simpa using DFunLike.congr_fun (h (single a m)) a

Premises used: DFunLike.congr_fun, Finsupp.single
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
R : Type u_6
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.IsTorsionFree R M
b : R
hb : b ≠ 0
g : α →₀ M
a : α
⊢ a ∈ (b • g).support ↔ a ∈ g.support

Tactic:
simp [Finsupp.smul_apply, hb]

Premises used: Finsupp.smul_apply
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
R : Type u_6
p : α → Prop
inst : DecidablePred p
inst_1 : Zero M
inst_2 : SMulZeroClass R M
b : R
v : α →₀ M
simp :
  Set.indicator {x : α | p x} (HSMul.hSMul (β := (a : α) → M) b (⇑v : (a : α) → M)) =
    HSMul.hSMul (β := (a : α) → M) b (Set.indicator {x : α | p x} (⇑v : (a : α) → M))
⊢ Eq (α := (a : α) → M) ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) (filter p (b • v)))
    ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) (b • filter p v))

Tactic:
simp only [filter_eq_indicator, coe_smul]

Premises used: Finsupp.filter_eq_indicator, Finsupp.coe_smul
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
R : Type u_6
p : α → Prop
inst : DecidablePred p
inst_1 : Zero M
inst_2 : SMulZeroClass R M
b : R
v : α →₀ M
⊢ Set.indicator {x : α | p x} (HSMul.hSMul (β := (a : α) → M) b (⇑v : (a : α) → M)) =
    HSMul.hSMul (β := (a : α) → M) b (Set.indicator {x : α | p x} (⇑v : (a : α) → M))

Tactic:
Set.indicator_const_smul { x | p x } b v

Premises used: Set.indicator_const_smul, setOf, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
R : Type u_6
p : α → Prop
inst : DecidablePred p
inst_1 : Zero M
inst_2 : SMulZeroClass R M
b : R
v : α →₀ M
⊢ Set.indicator {x : α | p x} (HSMul.hSMul (β := (a : α) → M) b (⇑v : (a : α) → M)) =
    HSMul.hSMul (β := (a : α) → M) b (Set.indicator {x : α | p x} (⇑v : (a : α) → M))

Tactic:
exact Set.indicator_const_smul { x | p x } b v

Premises used: Set.indicator_const_smul, setOf, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
R : Type u_6
inst : AddCommMonoid M
inst_1 : DistribSMul R M
f : α → β
b : R
v : α →₀ M
⊢ mapDomain f (b • v) = b • mapDomain f v

Tactic:
mapDomain_mapRange _ _ _ _ (smul_add b)

Premises used: Finsupp.mapDomain_mapRange, smul_add
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
R : Type u_6
x : Semiring R
c : R
a : α
b : R
⊢ HSMul.hSMul (β := α →₀ R) c (single a b) = single a (c * b)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
R : Type u_6
inst : MulZeroOneClass R
a : α
b : R
rw : Eq (α := α →₀ R) (single a (HSMul.hSMul (β := R) b 1)) (single a b)
rw₁ : Eq (α := α →₀ R) (single a (b * 1)) (single a b)
rw₂ rw₃ : Eq (α := α →₀ R) (single a b) (single a b)
⊢ HSMul.hSMul (β := α →₀ R) b (single a 1) = single a b

Tactic:
rw [smul_single, smul_eq_mul, mul_one]

Premises used: smul_eq_mul, mul_one, Finsupp.smul_single
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
R : Type u_6
inst : Zero M
inst_1 : SMulZeroClass R M
f : α → β
r : R
v : β →₀ M
hfv : Set.InjOn f (f ⁻¹' (↑v.support : Set β))
hfrv : Set.InjOn f (f ⁻¹' (↑(r • v).support : Set β))
h :
  ∀ (a : α),
    Eq.{u_3 + 1} (α := M) ((comapDomain f (r • v) hfrv : (a : α) → M) a : M)
      ((r • comapDomain f v hfv : (a : α) → M) a : M)
⊢ comapDomain f (r • v) hfrv = r • comapDomain f v hfv

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
R : Type u_6
inst : Zero M
inst_1 : SMulZeroClass R M
f : α → β
r : R
v : β →₀ M
hfv : Set.InjOn f (f ⁻¹' (↑v.support : Set β))
hfrv : Set.InjOn f (f ⁻¹' (↑(r • v).support : Set β))
a : α
⊢ Eq.{u_3 + 1} (α := M) ((comapDomain f (r • v) hfrv : (a : α) → M) a : M)
    ((r • comapDomain f v hfv : (a : α) → M) a : M)

Tactic:
rfl
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
R : Type u_6
inst : Zero M
inst_1 : SMulZeroClass R M
f : α → β
hf : Injective f
r : R
v : β →₀ M
⊢ comapDomain f (r • v) ⋯ = r • comapDomain f v ⋯

Tactic:
comapDomain_smul _ _ _ _

Premises used: Finsupp.comapDomain_smul
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
R : Type u_6
inst : MulZeroClass R
inst_1 : AddCommMonoid M
g : α →₀ R
b : R
h : α → R → M
h0 : ∀ (i : α), h i 0 = 0
⊢ (b • g).sum h = g.sum fun (i : α) (a : R) ↦ h i (b * a)

Tactic:
Finsupp.sum_mapRange_index h0

Premises used: Finsupp.sum_mapRange_index
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
N : Type u_4
R : Type u_6
inst : Zero M
inst_1 : SMulZeroClass R M
inst_2 : AddCommMonoid N
g : α →₀ M
b : R
h : α → M → N
h0 : ∀ (i : α), h i 0 = 0
⊢ (b • g).sum h = g.sum fun (i : α) (c : M) ↦ h i (b • c)

Tactic:
Finsupp.sum_mapRange_index h0

Premises used: Finsupp.sum_mapRange_index
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
N : Type u_4
R : Type u_6
inst : AddZeroClass M
inst_1 : AddCommMonoid N
inst_2 : SMulZeroClass R M
g : α →₀ M
b : R
h : α → M →+ N
⊢ Eq.{u_4 + 1} (α := N) ((b • g).sum fun (a : α) ↦ (⇑(h a) : (a : M) → N))
    (g.sum fun (i : α) (c : M) ↦ (h i : (a : M) → N) (b • c))

Tactic:
sum_mapRange_index fun i => (h i).map_zero

Premises used: AddMonoidHom.map_zero, Finsupp.sum_mapRange_index
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_7
inst_3 : Module.IsTorsionFree R M
r : R
hr : IsRegular r
f g : ι →₀ M
hfg : Eq (α := ι →₀ M) ((fun (x : ι →₀ M) ↦ r • x) f) ((fun (x : ι →₀ M) ↦ r • x) g)
h : ∀ (i : ι), Eq.{u_3 + 1} (α := M) ((f : (a : ι) → M) i : M) ((g : (a : ι) → M) i : M)
⊢ f = g

Tactic:
ext i
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_7
inst_3 : Module.IsTorsionFree R M
r : R
hr : IsRegular r
f g : ι →₀ M
hfg : Eq (α := ι →₀ M) ((fun (x : ι →₀ M) ↦ r • x) f) ((fun (x : ι →₀ M) ↦ r • x) g)
i : ι
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : ι) → M) i : M) ((g : (a : ι) → M) i : M)

Tactic:
hr.isSMulRegular congr($hfg i)

Premises used: congrArg, id, IsRegular.isSMulRegular, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_7
inst_3 : Module.IsTorsionFree R M
r : R
hr : IsRegular r
f g : ι →₀ M
hfg : Eq (α := ι →₀ M) ((fun (x : ι →₀ M) ↦ r • x) f) ((fun (x : ι →₀ M) ↦ r • x) g)
i : ι
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : ι) → M) i : M) ((g : (a : ι) → M) i : M)

Tactic:
exact hr.isSMulRegular congr($hfg i)

Premises used: congrArg, id, IsRegular.isSMulRegular, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : AddMonoid N
inst_3 : DistribMulAction R M
inst_4 : DistribMulAction R N
a : α
k : R
m : M
⊢ ZeroHom.toFun (↑(singleAddHom a) : ZeroHom M (α →₀ M)) (k • m) =
    HSMul.hSMul (α := R) (β := α →₀ M) ((MonoidHom.id R : (a : R) → R) k : R)
      (ZeroHom.toFun (↑(singleAddHom a) : ZeroHom M (α →₀ M)) m)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
N : Type u_4
R : Type u_6
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : AddMonoid N
inst_3 : DistribMulAction R M
inst_4 : DistribMulAction R N
f g : (α →₀ M) →+[R] N
h :
  ∀ (a : α) (m : M),
    Eq.{u_4 + 1} (α := N) ((f : (a : α →₀ M) → N) (single a m) : N) ((g : (a : α →₀ M) → N) (single a m) : N)
⊢ f = g

Tactic:
DistribMulActionHom.toAddMonoidHom_injective <| addHom_ext h

Premises used: DistribMulActionHom.toAddMonoidHom_injective, Finsupp.addHom_ext
-- Module: Mathlib.Data.Finsupp.SMul
Goal:
α : Type u_1
M : Type u_3
N : Type u_4
R : Type u_6
inst : Monoid R
inst_1 : AddMonoid M
inst_2 : AddMonoid N
inst_3 : DistribMulAction R M
inst_4 : DistribMulAction R N
f g : (α →₀ M) →+[R] N
h : ∀ (a : α), f.comp (DistribMulActionHom.single a) = g.comp (DistribMulActionHom.single a)
⊢ f = g

Tactic:
distribMulActionHom_ext fun a => DistribMulActionHom.congr_fun (h a)

Premises used: DistribMulActionHom.congr_fun, Finsupp.distribMulActionHom_ext
-- Module: Mathlib.Data.Finsupp.SMulWithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst : Zero M
inst_1 : SMulZeroClass R M
a : R
h :
  ∀ (a_1 : α), Eq.{u_5 + 1} (α := M) ((HSMul.hSMul (β := α →₀ M) a 0 : (a : α) → M) a_1 : M) ((0 : (a : α) → M) a_1 : M)
⊢ HSMul.hSMul (β := α →₀ M) a 0 = 0

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.SMulWithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst : Zero M
inst_1 : SMulZeroClass R M
a : R
a_1 : α
⊢ Eq.{u_5 + 1} (α := M) ((HSMul.hSMul (β := α →₀ M) a 0 : (a : α) → M) a_1 : M) ((0 : (a : α) → M) a_1 : M)

Tactic:
apply smul_zero

Premises used: smul_zero
-- Module: Mathlib.Data.Finsupp.SMulWithZero
Goal:
α : Type u_1
M : Type u_5
R : Type u_11
inst : Zero M
inst_1 : SMulZeroClass R M
b : R
v : α →₀ M
⊢ (⇑(b • v) : (a : α) → M) = HSMul.hSMul (β := (a : α) → M) b (⇑v : (a : α) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.SMulWithZero
Goal:
α : Type u_1
M : Type u_5
R : Type u_11
inst : Zero M
inst_1 : SMulZeroClass R M
b : R
v : α →₀ M
a : α
⊢ (b • v : (a : α) → M) a = HSMul.hSMul (β := M) b ((v : (a : α) → M) a : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.SMulWithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
f : α →₀ M
h : ∀ (i : α), Eq.{u_5 + 1} (α := M) ((HSMul.hSMul (α := R) 0 f : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
⊢ HSMul.hSMul (α := R) 0 f = 0

Tactic:
ext i
-- Module: Mathlib.Data.Finsupp.SMulWithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
f : α →₀ M
i : α
⊢ Eq.{u_5 + 1} (α := M) ((HSMul.hSMul (α := R) 0 f : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)

Tactic:
zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.Data.Finsupp.SMulWithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst : Zero R
inst_1 : Zero M
inst_2 : SMulWithZero R M
f : α →₀ M
i : α
⊢ Eq.{u_5 + 1} (α := M) ((HSMul.hSMul (α := R) 0 f : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)

Tactic:
exact zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.Data.Finsupp.SMulWithZero
Goal:
α : Type u_1
M : Type u_5
R : Type u_11
inst : Zero M
inst_1 : SMulZeroClass R M
b : R
g : α →₀ M
a : α
simp : ¬HSMul.hSMul (β := M) b ((g : (a : α) → M) a : M) = 0 → ¬Eq.{u_5 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)
⊢ a ∈ (b • g).support → a ∈ g.support

Tactic:
simp only [smul_apply, mem_support_iff, Ne]

Premises used: Finsupp.mem_support_iff, Ne, Finsupp.smul_apply
-- Module: Mathlib.Data.Finsupp.SMulWithZero
Goal:
α : Type u_1
M : Type u_5
R : Type u_11
inst : Zero M
inst_1 : SMulZeroClass R M
b : R
g : α →₀ M
a : α
⊢ ¬HSMul.hSMul (β := M) b ((g : (a : α) → M) a : M) = 0 → ¬Eq.{u_5 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)

Tactic:
mt fun h => h.symm ▸ smul_zero _

Premises used: smul_zero, mt, Eq.rec, Eq.symm
-- Module: Mathlib.Data.Finsupp.SMulWithZero
Goal:
α : Type u_1
M : Type u_5
R : Type u_11
inst : Zero M
inst_1 : SMulZeroClass R M
b : R
g : α →₀ M
a : α
⊢ ¬HSMul.hSMul (β := M) b ((g : (a : α) → M) a : M) = 0 → ¬Eq.{u_5 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)

Tactic:
exact mt fun h => h.symm ▸ smul_zero _

Premises used: mt
-- Module: Mathlib.Data.Finsupp.SMulWithZero
Goal:
α : Type u_1
M : Type u_5
R : Type u_11
inst : Zero M
inst_1 : SMulZeroClass R M
c : R
a : α
b : M
⊢ HSMul.hSMul (β := α →₀ M) c (single a b) = single a (c • b)

Tactic:
mapRange_single

Premises used: Finsupp.mapRange_single
-- Module: Mathlib.Data.Finsupp.SMulWithZero
Goal:
α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
S : Type u_12
inst : Zero M
inst_1 : SMulZeroClass R M
inst_2 : Zero N
inst_3 : SMulZeroClass S N
f : M → N
hf : f 0 = 0
c : R
d : S
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = d • f x
h :
  ∀ (a : α),
    Eq.{u_7 + 1} (α := N) ((mapRange f hf (c • v) : (a : α) → N) a : N) ((d • mapRange f hf v : (a : α) → N) a : N)
⊢ mapRange f hf (c • v) = d • mapRange f hf v

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.SMulWithZero
Goal:
α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
S : Type u_12
inst : Zero M
inst_1 : SMulZeroClass R M
inst_2 : Zero N
inst_3 : SMulZeroClass S N
f : M → N
hf : f 0 = 0
c : R
d : S
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = d • f x
a : α
⊢ Eq.{u_7 + 1} (α := N) ((mapRange f hf (c • v) : (a : α) → N) a : N) ((d • mapRange f hf v : (a : α) → N) a : N)

Tactic:
simp [hsmul]
-- Module: Mathlib.Data.Finsupp.SMulWithZero
Goal:
α : Type u_1
M : Type u_5
N : Type u_7
R : Type u_11
inst : Zero M
inst_1 : SMulZeroClass R M
inst_2 : Zero N
inst_3 : SMulZeroClass R N
f : M → N
hf : f 0 = 0
c : R
v : α →₀ M
hsmul : ∀ (x : M), f (c • x) = c • f x
⊢ mapRange f hf (c • v) = c • mapRange f hf v

Tactic:
mapRange_smul' c c v hsmul

Premises used: Finsupp.mapRange_smul'
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
inst_1 : DecidableEq κ
k : κ
f : Finsupp.{u_2, u_3} (ι k) M
i : (k : κ) × ι k
rcases :
  ∀ (k_1 : κ) (i : ι k_1),
    Eq.{u_3 + 1} (α := M)
      ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k_1 i) : M)
      (if h : (Sigma.mk (β := fun (k : κ) ↦ ι k) k_1 i).fst (β := fun (k : κ) ↦ ι k) = k then
          (f : (a : ι k) → M)
            (Eq.rec (motive :=
                fun (x : κ) (h : (Sigma.mk (β := fun (k : κ) ↦ ι k) k_1 i).fst (β := fun (k : κ) ↦ ι k) = x) ↦ ι x)
                ((Sigma.mk (β := fun (k : κ) ↦ ι k) k_1 i).snd (β := fun (k : κ) ↦ ι k)) h :
              ι k)
        else 0 :
        M)
⊢ Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) i : M)
    (if h : i.fst (β := fun (k : κ) ↦ ι k) = k then
        (f : (a : ι k) → M)
          (Eq.rec (motive := fun (x : κ) (h : i.fst (β := fun (k : κ) ↦ ι k) = x) ↦ ι x)
              (i.snd (β := fun (k : κ) ↦ ι k)) h :
            ι k)
      else 0 :
      M)

Tactic:
rcases i with ⟨k, i⟩
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
inst_1 : DecidableEq κ
k_1 : κ
f : Finsupp.{u_2, u_3} (ι k_1) M
k : κ
i : ι k
pos :
  ∀ (h : (Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k) = k_1),
    Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
      ((f : (a : ι k_1) → M)
          (Eq.rec (motive :=
              fun (x : κ) (h : (Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k) = x) ↦ ι x)
              ((Sigma.mk (β := fun (k : κ) ↦ ι k) k i).snd (β := fun (k : κ) ↦ ι k)) h :
            ι k_1) :
        M)
neg :
  ∀ (h : ¬(Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k) = k_1),
    Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
      (0 : M)
⊢ Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
    (if h : (Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k) = k_1 then
        (f : (a : ι k_1) → M)
          (Eq.rec (motive :=
              fun (x : κ) (h : (Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k) = x) ↦ ι x)
              ((Sigma.mk (β := fun (k : κ) ↦ ι k) k i).snd (β := fun (k : κ) ↦ ι k)) h :
            ι k_1)
      else 0 :
      M)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
inst_1 : DecidableEq κ
k_1 : κ
f : Finsupp.{u_2, u_3} (ι k_1) M
k : κ
i : ι k
h : (Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k) = k_1
pos :
  ∀ (f : Finsupp.{u_2, u_3} (ι ((Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k))) M),
    Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
      ((f : (a : ι ⟨k, i⟩.fst) → M)
          (Eq.rec (motive :=
              fun (x : κ) (h : (Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k) = x) ↦ ι x)
              ((Sigma.mk (β := fun (k : κ) ↦ ι k) k i).snd (β := fun (k : κ) ↦ ι k)) ⋯ :
            ι ((Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k))) :
        M)
⊢ Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
    ((f : (a : ι k_1) → M)
        (Eq.rec (motive := fun (x : κ) (h : (Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k) = x) ↦
            ι x) ((Sigma.mk (β := fun (k : κ) ↦ ι k) k i).snd (β := fun (k : κ) ↦ ι k)) h :
          ι k_1) :
      M)

Tactic:
subst h
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
inst_1 : DecidableEq κ
k : κ
i : ι k
f : Finsupp.{u_2, u_3} (ι ((Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k))) M
pos :
  Eq.{u_3 + 1} (α := M)
    ((embDomain { toFun := Sigma.mk (β := ι) k, inj' := ⋯ : ι k ↪ (x : κ) × ι x } f : (a : (k : κ) × ι k) → M)
        (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) :
      M)
    ((f : (a : ι k) → M) i : M)
⊢ Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
    ((f : (a : ι ⟨k, i⟩.fst) → M)
        (Eq.rec (motive := fun (x : κ) (h : (Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k) = x) ↦
            ι x) ((Sigma.mk (β := fun (k : κ) ↦ ι k) k i).snd (β := fun (k : κ) ↦ ι k)) ⋯ :
          ι ((Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k))) :
      M)

Tactic:
simp only [embSigma, Embedding.sigmaMk]

Premises used: Function.Embedding.sigmaMk, Finsupp.embSigma
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
inst_1 : DecidableEq κ
k : κ
i : ι k
f : Finsupp.{u_2, u_3} (ι ((Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k))) M
⊢ Eq.{u_3 + 1} (α := M)
    ((embDomain { toFun := Sigma.mk (β := ι) k, inj' := ⋯ : ι k ↪ (x : κ) × ι x } f : (a : (k : κ) × ι k) → M)
        (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) :
      M)
    ((f : (a : ι k) → M) i : M)

Tactic:
apply embDomain_apply_self

Premises used: Finsupp.embDomain_apply_self
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
inst_1 : DecidableEq κ
k_1 : κ
f : Finsupp.{u_2, u_3} (ι k_1) M
k : κ
i : ι k
h : ¬(Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k) = k_1
neg :
  Eq.{u_3 + 1} (α := M)
    ((embDomain { toFun := Sigma.mk (β := ι) k_1, inj' := ⋯ : ι k_1 ↪ (x : κ) × ι x } f : (a : (k : κ) × ι k) → M)
        (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) :
      M)
    (0 : M)
⊢ Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
    (0 : M)

Tactic:
simp only [embSigma, Embedding.sigmaMk]

Premises used: Function.Embedding.sigmaMk, Finsupp.embSigma
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
inst_1 : DecidableEq κ
k_1 : κ
f : Finsupp.{u_2, u_3} (ι k_1) M
k : κ
i : ι k
h : ¬(Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k) = k_1
neg :
  Sigma.mk (β := fun (k : κ) ↦ ι k) k i ∉
    Set.range (ι := ι k_1) (⇑{ toFun := Sigma.mk (β := ι) k_1, inj' := ⋯ } : (a : ι k_1) → (k : κ) × ι k)
⊢ Eq.{u_3 + 1} (α := M)
    ((embDomain { toFun := Sigma.mk (β := ι) k_1, inj' := ⋯ : ι k_1 ↪ (x : κ) × ι x } f : (a : (k : κ) × ι k) → M)
        (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) :
      M)
    (0 : M)

Tactic:
rw [embDomain_notin_range]

Premises used: Finsupp.embDomain_notin_range
-- Module: Mathlib.Data.Finsupp.Sigma
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
inst_1 : DecidableEq κ
k_1 : κ
f : Finsupp.{u_2, u_3} (ι k_1) M
k : κ
i : ι k
h : ¬(Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k) = k_1
⊢ Sigma.mk (β := fun (k : κ) ↦ ι k) k i ∉
    Set.range (ι := ι k_1) (⇑{ toFun := Sigma.mk (β := ι) k_1, inj' := ⋯ } : (a : ι k_1) → (k : κ) × ι k)

Tactic:
simp_all