awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
Goal:
α : Type u_1
M : Type u_3
R : Type u_6
inst : Zero M
inst_1 : MonoidWithZero R
inst_2 : MulActionWithZero R M
a b : α
f : α → M
r : R
pos :
  ∀ (h : a = b),
    HSMul.hSMul.{u_6, u_3, u_3} (α := R) ((single a r : (a : α) → R) b : R) (f a) = (single a (r • f b) : (a : α) → M) b
⊢ HSMul.hSMul.{u_6, u_3, u_3} (α := R) ((single a r : (a : α) → R) b : R) (f a) = (single a (r • f b) : (a : α) → M) b
have neg : ∀ (h : ¬a = b),
  HSMul.hSMul.{u_6, u_3, u_3} (α := R) ((single a r : (a : α) → R) b : R) (f a) = (single a (r • f b) : (a : α) → M) b
Tactic: by_cases h : a = b
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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' : G
f : α →₀ M
⊢ (g * g') • f = g • g' • f
have rw : mapDomain (fun (x : α) ↦ (g * g') • x) f = g • g' • f
Tactic: rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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' : G
f : α →₀ M
rw : mapDomain (fun (x : α) ↦ (g * g') • x) f = g • g' • f
⊢ (g * g') • f = g • g' • f
have rw₁ : Eq (α := α →₀ M) (mapDomain (fun (x : α) ↦ (g * g') • x) f) (mapDomain (fun (x : α) ↦ g • x) (g' • f))
Tactic: rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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' : G
f : α →₀ M
rw : mapDomain (fun (x : α) ↦ (g * g') • x) f = g • g' • f
rw₁ : Eq (α := α →₀ M) (mapDomain (fun (x : α) ↦ (g * g') • x) f) (mapDomain (fun (x : α) ↦ g • x) (g' • f))
⊢ (g * g') • f = g • g' • f
have rw₂ : Eq (α := α →₀ M) (mapDomain (fun (x : α) ↦ (g * g') • x) f)
  (mapDomain (fun (x : α) ↦ g • x) (mapDomain (fun (x : α) ↦ g' • x) f))
Tactic: rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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' : G
f : α →₀ M
rw : mapDomain (fun (x : α) ↦ (g * g') • x) f = g • g' • f
rw₁ : Eq (α := α →₀ M) (mapDomain (fun (x : α) ↦ (g * g') • x) f) (mapDomain (fun (x : α) ↦ g • x) (g' • f))
rw₂ :
  Eq (α := α →₀ M) (mapDomain (fun (x : α) ↦ (g * g') • x) f)
    (mapDomain (fun (x : α) ↦ g • x) (mapDomain (fun (x : α) ↦ g' • x) f))
⊢ (g * g') • f = g • g' • f
have rw₃ : Eq (α := α →₀ M) (mapDomain ((fun (x : α) ↦ g • x) ∘ fun (x : α) ↦ g' • x) f)
  (mapDomain (fun (x : α) ↦ g • x) (mapDomain (fun (x : α) ↦ g' • x) f))
Tactic: rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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' : G
f : α →₀ M
rw : mapDomain (fun (x : α) ↦ (g * g') • x) f = g • g' • f
rw₁ : Eq (α := α →₀ M) (mapDomain (fun (x : α) ↦ (g * g') • x) f) (mapDomain (fun (x : α) ↦ g • x) (g' • f))
rw₂ :
  Eq (α := α →₀ M) (mapDomain (fun (x : α) ↦ (g * g') • x) f)
    (mapDomain (fun (x : α) ↦ g • x) (mapDomain (fun (x : α) ↦ g' • x) f))
rw₃ :
  Eq (α := α →₀ M) (mapDomain ((fun (x : α) ↦ g • x) ∘ fun (x : α) ↦ g' • x) f)
    (mapDomain (fun (x : α) ↦ g • x) (mapDomain (fun (x : α) ↦ g' • x) f))
⊢ (g * g') • f = g • g' • f
have rw₄ : Eq (α := α →₀ M) (mapDomain (fun (x : α) ↦ g • x) (mapDomain (fun (x : α) ↦ g' • x) f))
  (mapDomain (fun (x : α) ↦ g • x) (mapDomain (fun (x : α) ↦ g' • x) f))
Tactic: rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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
f : α →₀ M
⊢ HSMul.hSMul (α := G) 1 f = f
have rw : mapDomain (fun (x : α) ↦ HSMul.hSMul.{u_5, u_1, u_1} (α := G) 1 x) f = f
Tactic: rw [comapSMul_def, one_smul_eq_id, mapDomain_id]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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
f : α →₀ M
rw : mapDomain (fun (x : α) ↦ HSMul.hSMul.{u_5, u_1, u_1} (α := G) 1 x) f = f
⊢ HSMul.hSMul (α := G) 1 f = f
have rw₁ : mapDomain id f = f
Tactic: rw [comapSMul_def, one_smul_eq_id, mapDomain_id]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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
f : α →₀ M
rw : mapDomain (fun (x : α) ↦ HSMul.hSMul.{u_5, u_1, u_1} (α := G) 1 x) f = f
rw₁ : mapDomain id f = f
⊢ HSMul.hSMul (α := G) 1 f = f
have rw₂ : f = f
Tactic: rw [comapSMul_def, one_smul_eq_id, mapDomain_id]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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
⊢ HSMul.hSMul (β := α →₀ M) g 0 = 0
have h : ∀ (a : α), Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (β := α →₀ M) g 0 : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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
a : α
⊢ Eq.{u_3 + 1} (α := M) ((HSMul.hSMul (β := α →₀ M) g 0 : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
have h : Eq.{u_3 + 1} (α := M) ((mapDomain (fun (x : α) ↦ g • x) 0 : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
Tactic: simp only [comapSMul_def]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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
⊢ g • (f + f') = g • f + g • f'
have h : ∀ (a : α), Eq.{u_3 + 1} (α := M) ((g • (f + f') : (a : α) → M) a : M) ((g • f + g • f' : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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) ((g • (f + f') : (a : α) → M) a : M) ((g • f + g • f' : (a : α) → M) a : M)
have 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)
Tactic: simp only [comapSMul_def]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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 : α
| ((g • f : (a : α) → M) a : M)
have rw : ((g • f : (a : α) → M) (g • g⁻¹ • a) : M)
Tactic: rw [← smul_inv_smul g a]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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) a : M) ((f : (a : α) → M) (g⁻¹ • a) : M)
have conv_lhs : Eq.{u_3 + 1} (α := M) ((g • f : (a : α) → M) (g • g⁻¹ • a) : M) ((f : (a : α) → M) (g⁻¹ • a) : M)
Tactic: conv_lhs => rw [← smul_inv_smul g a]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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
⊢ 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))
have 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))
Tactic: simp only [filter_eq_indicator, coe_smul]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
Goal:
α : Type u_1
R : Type u_6
inst : MulZeroOneClass R
a : α
b : R
⊢ HSMul.hSMul (β := α →₀ R) b (single a 1) = single a b
have rw : Eq (α := α →₀ R) (single a (HSMul.hSMul (β := R) b 1)) (single a b)
Tactic: rw [smul_single, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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)
⊢ HSMul.hSMul (β := α →₀ R) b (single a 1) = single a b
have rw₁ : Eq (α := α →₀ R) (single a (b * 1)) (single a b)
Tactic: rw [smul_single, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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)
⊢ HSMul.hSMul (β := α →₀ R) b (single a 1) = single a b
have rw₂ : Eq (α := α →₀ R) (single a b) (single a b)
Tactic: rw [smul_single, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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 β))
⊢ comapDomain f (r • v) hfrv = r • comapDomain f v hfv
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMul (goal)
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)
⊢ f = g
have h : ∀ (i : ι), Eq.{u_3 + 1} (α := M) ((f : (a : ι) → M) i : M) ((g : (a : ι) → M) i : M)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMulWithZero (goal)
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
⊢ HSMul.hSMul (β := α →₀ M) a 0 = 0
have h : ∀ (a_1 : α), Eq.{u_5 + 1} (α := M) ((HSMul.hSMul (β := α →₀ M) a 0 : (a : α) → M) a_1 : M) ((0 : (a : α) → M) a_1 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMulWithZero (goal)
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
⊢ HSMul.hSMul (α := R) 0 f = 0
have h : ∀ (i : α), Eq.{u_5 + 1} (α := M) ((HSMul.hSMul (α := R) 0 f : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMulWithZero (goal)
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 : α
⊢ a ∈ (b • g).support → a ∈ g.support
have simp : ¬HSMul.hSMul (β := M) b ((g : (a : α) → M) a : M) = 0 → ¬Eq.{u_5 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M)
Tactic: simp only [smul_apply, mem_support_iff, Ne]
-- Lean 4 proof step from Mathlib.Data.Finsupp.SMulWithZero (goal)
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
⊢ mapRange f hf (c • v) = d • mapRange f hf v
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
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
⊢ 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)
have 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)
Tactic: rcases i with ⟨k, i⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
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
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
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)
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
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
⊢ 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)
have 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)) sorry :
          ι ((Sigma.mk (β := fun (k : κ) ↦ ι k) k i).fst (β := fun (k : κ) ↦ ι k))) :
      M)
Tactic: subst h
Cleared hypotheses: k_1, f, h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
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) ((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)
have pos : Eq.{u_3 + 1} (α := M)
  ((embDomain { toFun := Sigma.mk (β := ι) k, inj' := sorry : ι k ↪ (x : κ) × ι x } f : (a : (k : κ) × ι k) → M)
      (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) :
    M)
  ((f : (a : ι k) → M) i : M)
Tactic: simp only [embSigma, Embedding.sigmaMk]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
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
⊢ Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
    (0 : M)
have neg : Eq.{u_3 + 1} (α := M)
  ((embDomain { toFun := Sigma.mk (β := ι) k_1, inj' := sorry : ι k_1 ↪ (x : κ) × ι x } f : (a : (k : κ) × ι k) → M)
      (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) :
    M)
  (0 : M)
Tactic: simp only [embSigma, Embedding.sigmaMk]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
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
⊢ 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)
have neg : Sigma.mk (β := fun (k : κ) ↦ ι k) k i ∉
  Set.range (ι := ι k_1) (⇑{ toFun := Sigma.mk (β := ι) k_1, inj' := sorry } : (a : ι k_1) → (k : κ) × ι k)
Tactic: rw [embDomain_notin_range]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
f : Finsupp.{u_2, u_3} (ι k) M
i : ι k
⊢ Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
    ((f : (a : ι k) → M) i : M)
have rw : Eq.{u_3 + 1} (α := M)
  ((embDomain (Embedding.sigmaMk (β := ι) k) f : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
  ((f : (a : ι k) → M) i : M)
Tactic: rw [embSigma]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k k' : κ
f : Finsupp.{u_2, u_3} (ι k) M
hk : k' ≠ k
i : ι k'
⊢ Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
    (0 : M)
have h : Sigma.mk (β := fun (k : κ) ↦ ι k) k' i ∉
  Set.range (ι := ι k) (⇑(Embedding.sigmaMk (β := ι) k) : (a : ι k) → (k : κ) × ι k)
Tactic: apply embDomain_notin_range
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
f g : Finsupp.{u_2, u_3} (ι k) M
h : f.embSigma (ι := ι) = g.embSigma (ι := ι)
⊢ f = g
have h₁ : ∀ (i : ι k), Eq.{u_3 + 1} (α := M) ((f : (a : ι k) → M) i : M) ((g : (a : ι k) → M) i : M)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (hypothesis)
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : Zero M
k : κ
f g : Finsupp.{u_2, u_3} (ι k) M
h : f.embSigma (ι := ι) = g.embSigma (ι := ι)
i : ι k
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : ι k) → M) i : M) ((g : (a : ι k) → M) i : M)
have this : Eq.{u_3 + 1} (α := M) ((f.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
  ((g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k i) : M)
Tactic: have := congr_fun (congrArg (⇑) h) ⟨k, i⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : AddMonoid M
k : κ
f g : Finsupp.{u_2, u_3} (ι k) M
⊢ (f + g).embSigma (ι := ι) = f.embSigma (ι := ι) + g.embSigma (ι := ι)
have h : ∀ (k' : κ) (i : ι k'),
  Eq.{u_3 + 1} (α := M)
    (((f + g).embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
    ((f.embSigma (ι := ι) + g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
Tactic: ext ⟨k', i⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : AddMonoid M
k : κ
f g : Finsupp.{u_2, u_3} (ι k) M
k' : κ
i : ι k'
⊢ Eq.{u_3 + 1} (α := M)
    (((f + g).embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
    ((f.embSigma (ι := ι) + g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
have pos : ∀ (hk : k' = k),
  Eq.{u_3 + 1} (α := M)
    (((f + g).embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
    ((f.embSigma (ι := ι) + g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
Tactic: by_cases hk : k' = k
-- Lean 4 proof step from Mathlib.Data.Finsupp.Sigma (goal)
Goal:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst : AddMonoid M
k : κ
f g : Finsupp.{u_2, u_3} (ι k) M
k' : κ
i : ι k'
pos :
  ∀ (hk : k' = k),
    Eq.{u_3 + 1} (α := M)
      (((f + g).embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
      ((f.embSigma (ι := ι) + g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) :
        M)
⊢ Eq.{u_3 + 1} (α := M)
    (((f + g).embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
    ((f.embSigma (ι := ι) + g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
have neg : ∀ (hk : ¬k' = k),
  Eq.{u_3 + 1} (α := M)
    (((f + g).embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
    ((f.embSigma (ι := ι) + g.embSigma (ι := ι) : (a : (k : κ) × ι k) → M) (Sigma.mk (β := fun (k : κ) ↦ ι k) k' i) : M)
Tactic: by_cases hk : k' = k