awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
h : (vecCons x v + w) 0 = vecCons (x + vecHead w) (v + vecTail w) 0
h₁ : ∀ (i : Fin n), (vecCons x v + w) i.succ = vecCons (x + vecHead w) (v + vecTail w) i.succ
⊢ (vecCons x v + w) i = vecCons (x + vecHead w) (v + vecTail w) i

Tactic:
refine i.cases ?_ ?_
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v + w) 0 = vecCons (x + vecHead w) (v + vecTail w) 0

Tactic:
simp [vecHead, vecTail]

Premises used: Matrix.vecHead, Matrix.vecTail
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (vecCons x v + w) i.succ = vecCons (x + vecHead w) (v + vecTail w) i.succ

Tactic:
simp [vecHead, vecTail]

Premises used: Matrix.vecHead, Matrix.vecTail
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
h : ∀ (i : Fin n.succ), (v + vecCons y w) i = vecCons (vecHead v + y) (vecTail v + w) i
⊢ v + vecCons y w = vecCons (vecHead v + y) (vecTail v + w)

Tactic:
ext i
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v + vecCons y w) i = vecCons (vecHead v + y) (vecTail v + w) i

Tactic:
i.cases ?_ ?_

Premises used: Fin.cases
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
h : (v + vecCons y w) 0 = vecCons (vecHead v + y) (vecTail v + w) 0
h₁ : ∀ (i : Fin n), (v + vecCons y w) i.succ = vecCons (vecHead v + y) (vecTail v + w) i.succ
⊢ (v + vecCons y w) i = vecCons (vecHead v + y) (vecTail v + w) i

Tactic:
refine i.cases ?_ ?_
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v + vecCons y w) 0 = vecCons (vecHead v + y) (vecTail v + w) 0

Tactic:
simp [vecHead, vecTail]

Premises used: Matrix.vecHead, Matrix.vecTail
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (v + vecCons y w) i.succ = vecCons (vecHead v + y) (vecTail v + w) i.succ

Tactic:
simp [vecHead, vecTail]

Premises used: Matrix.vecHead, Matrix.vecTail
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Add α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v + vecCons y w = vecCons (x + y) (v + w)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Add α
a b : Fin n.succ → α
⊢ vecHead (a + b) = vecHead a + vecHead b

Tactic:
rfl

Premises used: Matrix.vecHead, rfl
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Add α
a b : Fin n.succ → α
⊢ vecTail (a + b) = vecTail a + vecTail b

Tactic:
rfl

Premises used: Matrix.vecTail, rfl
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
inst : Sub α
v w : Fin 0 → α
⊢ v - w = ![]

Tactic:
empty_eq _

Premises used: Matrix.empty_eq
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
h : ∀ (i : Fin n.succ), (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i
⊢ vecCons x v - w = vecCons (x - vecHead w) (v - vecTail w)

Tactic:
ext i
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i

Tactic:
i.cases ?_ ?_

Premises used: Fin.cases
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
h : (vecCons x v - w) 0 = vecCons (x - vecHead w) (v - vecTail w) 0
h₁ : ∀ (i : Fin n), (vecCons x v - w) i.succ = vecCons (x - vecHead w) (v - vecTail w) i.succ
⊢ (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i

Tactic:
refine i.cases ?_ ?_
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v - w) 0 = vecCons (x - vecHead w) (v - vecTail w) 0

Tactic:
simp [vecHead, vecTail]

Premises used: Matrix.vecHead, Matrix.vecTail
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (vecCons x v - w) i.succ = vecCons (x - vecHead w) (v - vecTail w) i.succ

Tactic:
simp [vecHead, vecTail]

Premises used: Matrix.vecHead, Matrix.vecTail
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
h : ∀ (i : Fin n.succ), (v - vecCons y w) i = vecCons (vecHead v - y) (vecTail v - w) i
⊢ v - vecCons y w = vecCons (vecHead v - y) (vecTail v - w)

Tactic:
ext i
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v - vecCons y w) i = vecCons (vecHead v - y) (vecTail v - w) i

Tactic:
i.cases ?_ ?_

Premises used: Fin.cases
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
h : (v - vecCons y w) 0 = vecCons (vecHead v - y) (vecTail v - w) 0
h₁ : ∀ (i : Fin n), (v - vecCons y w) i.succ = vecCons (vecHead v - y) (vecTail v - w) i.succ
⊢ (v - vecCons y w) i = vecCons (vecHead v - y) (vecTail v - w) i

Tactic:
refine i.cases ?_ ?_
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v - vecCons y w) 0 = vecCons (vecHead v - y) (vecTail v - w) 0

Tactic:
simp [vecHead, vecTail]

Premises used: Matrix.vecHead, Matrix.vecTail
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (v - vecCons y w) i.succ = vecCons (vecHead v - y) (vecTail v - w) i.succ

Tactic:
simp [vecHead, vecTail]

Premises used: Matrix.vecHead, Matrix.vecTail
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Sub α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v - vecCons y w = vecCons (x - y) (v - w)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Sub α
a b : Fin n.succ → α
⊢ vecHead (a - b) = vecHead a - vecHead b

Tactic:
rfl

Premises used: Matrix.vecHead, rfl
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Sub α
a b : Fin n.succ → α
⊢ vecTail (a - b) = vecTail a - vecTail b

Tactic:
rfl

Premises used: Matrix.vecTail, rfl
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
inst : Zero α
⊢ Eq.{u_1 + 1} (α := Fin 0 → α) 0 ![]

Tactic:
empty_eq _

Premises used: Matrix.empty_eq
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Zero α
h : ∀ (i : Fin n.succ), Eq.{u_1 + 1} (α := α) (vecCons 0 0 i) (0 i)
⊢ Eq.{u_1 + 1} (α := Fin n.succ → α) (vecCons 0 0) 0

Tactic:
ext i
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Zero α
i : Fin n.succ
⊢ ∀ (i : Fin n), Eq.{u_1 + 1} (α := α) (vecCons 0 0 i.succ) (0 i.succ)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Zero α
i : Fin n.succ
⊢ Eq.{u_1 + 1} (α := α) (vecCons 0 0 i) (0 i)

Tactic:
exact i.cases rfl (by simp)
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Zero α
⊢ Eq.{u_1 + 1} (α := α) (vecHead (n := n) 0) 0

Tactic:
rfl

Premises used: Matrix.vecHead, rfl
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Zero α
⊢ Eq.{u_1 + 1} (α := Fin n → α) (vecTail 0) 0

Tactic:
rfl

Premises used: Matrix.vecTail, rfl
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Zero α
v : Fin n → α
x : α
h : vecCons x v = 0
⊢ vecTail (vecCons x v) = vecTail 0

Tactic:
congr_arg vecTail h

Premises used: congr_arg, Matrix.vecTail
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Zero α
v : Fin n → α
x : α
h : vecCons x v = 0
⊢ v = 0

Tactic:
convert! congr_arg vecTail h

Premises used: congr_arg, Matrix.vecTail
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Zero α
v : Fin n → α
x : α
h : x = 0 ∧ v = 0
hx : x = 0
hv : v = 0
⊢ vecCons x v = 0

Tactic:
simp [hx, hv]
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
inst : Neg α
v : Fin 0 → α
⊢ -v = ![]

Tactic:
empty_eq _

Premises used: Matrix.empty_eq
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Neg α
x : α
v : Fin n → α
h : ∀ (i : Fin n.succ), (-vecCons x v) i = vecCons (-x) (-v) i
⊢ -vecCons x v = vecCons (-x) (-v)

Tactic:
ext i
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ (-vecCons x v) i = vecCons (-x) (-v) i

Tactic:
i.cases ?_ ?_

Premises used: Fin.cases
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Neg α
x : α
v : Fin n → α
i : Fin n.succ
h : (-vecCons x v) 0 = vecCons (-x) (-v) 0
h₁ : ∀ (i : Fin n), (-vecCons x v) i.succ = vecCons (-x) (-v) i.succ
⊢ (-vecCons x v) i = vecCons (-x) (-v) i

Tactic:
refine i.cases ?_ ?_
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ (-vecCons x v) 0 = vecCons (-x) (-v) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), (-vecCons x v) i.succ = vecCons (-x) (-v) i.succ

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Neg α
a : Fin n.succ → α
⊢ vecHead (-a) = -vecHead a

Tactic:
rfl

Premises used: Matrix.vecHead, rfl
-- Module: Mathlib.Algebra.Group.Fin.Tuple
Goal:
α : Type u_1
n : ℕ
inst : Neg α
a : Fin n.succ → α
⊢ vecTail (-a) = -vecTail a

Tactic:
rfl

Premises used: Matrix.vecTail, rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
inst : Zero M
inst_1 : Zero N
inst_2 : FunLike F M N
inst_3 : ZeroHomClass F M N
e : F
i : ι
m : M
b : ι
⊢ Eq.{u_4 + 1} (α := N) ((e : (a : M) → N) ((single i m : (a : ι) → M) b : M) : N)
    (((single i ((e : (a : M) → N) m) : ι →₀ N) : (a : ι) → N) b : N)

Tactic:
apply_single' e (map_zero e) i m b

Premises used: map_zero, Finsupp.apply_single', DFunLike.coe
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : Zero M
h :
  ∀ (x : ι →₀ M) (a : ι),
    Eq.{u_3 + 1} (α := M) ((((zeroHom (ZeroHom.id M) : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
      ((((ZeroHom.id (ι →₀ M) : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
⊢ Eq (α := ZeroHom (ι →₀ M) (ι →₀ M)) (zeroHom (ZeroHom.id M)) (ZeroHom.id (ι →₀ M))

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : Zero M
x : ι →₀ M
a : ι
⊢ Eq.{u_3 + 1} (α := M) ((((zeroHom (ZeroHom.id M) : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
    ((((ZeroHom.id (ι →₀ M) : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
f : ZeroHom N O
f₂ : ZeroHom M N
h :
  ∀ (x : ι →₀ M) (a : ι),
    Eq.{u_5 + 1} (α := O) ((((zeroHom (f.comp f₂) : (a : ι →₀ M) → ι →₀ O) x : ι →₀ O) : (a : ι) → O) a : O)
      ((((ZeroHom.comp (zeroHom f) (zeroHom f₂) : (a : ι →₀ M) → ι →₀ O) x : ι →₀ O) : (a : ι) → O) a : O)
⊢ Eq (α := ZeroHom (ι →₀ M) (ι →₀ O)) (zeroHom (f.comp f₂)) (ZeroHom.comp (zeroHom f) (zeroHom f₂))

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
f : ZeroHom N O
f₂ : ZeroHom M N
x : ι →₀ M
a : ι
⊢ Eq.{u_5 + 1} (α := O) ((((zeroHom (f.comp f₂) : (a : ι →₀ M) → ι →₀ O) x : ι →₀ O) : (a : ι) → O) a : O)
    ((((ZeroHom.comp (zeroHom f) (zeroHom f₂) : (a : ι →₀ M) → ι →₀ O) x : ι →₀ O) : (a : ι) → O) a : O)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f g : ι →₀ M
⊢ (⇑(f + g) : (a : ι) → M) = HAdd.hAdd (α := (a : ι) → M) (⇑f : (a : ι) → M) (⇑g : (a : ι) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
g₁ g₂ : ι →₀ M
a : ι
⊢ (g₁ + g₂ : (a : ι) → M) a = HAdd.hAdd (α := M) (β := M) ((g₁ : (a : ι) → M) a : M) ((g₂ : (a : ι) → M) a : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
g₁ g₂ : ι →₀ M
inst_1 : DecidableEq ι
⊢ (g₁ + g₂).support ⊆ g₁.support ∪ g₂.support

Tactic:
support_zipWith

Premises used: Set.Mem, setOf, Finsupp.support_zipWith
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
g₁ g₂ : ι →₀ M
inst_1 : DecidableEq ι
h : Disjoint g₁.support g₂.support
a : ι
ha : a ∈ g₁.support ∪ g₂.support
inl : a ∈ g₁.support ∧ a ∉ g₂.support → a ∈ (g₁ + g₂).support
inr : a ∈ g₂.support ∧ a ∉ g₁.support → a ∈ (g₁ + g₂).support
⊢ a ∈ (g₁ + g₂).support

Tactic:
cases (Finset.mem_union_of_disjoint h).mp ha

Premises used: Finset.mem_union_of_disjoint, Iff.mp
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
g₁ g₂ : ι →₀ M
inst_1 : DecidableEq ι
h : Disjoint g₁.support g₂.support
a : ι
ha : a ∈ g₁.support ∪ g₂.support
h_1 : a ∈ g₁.support ∧ a ∉ g₂.support
⊢ a ∈ (g₁ + g₂).support

Tactic:
simp_all
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
g₁ g₂ : ι →₀ M
inst_1 : DecidableEq ι
h : Disjoint g₁.support g₂.support
a : ι
ha : a ∈ g₁.support ∪ g₂.support
h_1 : a ∈ g₂.support ∧ a ∉ g₁.support
⊢ a ∈ (g₁ + g₂).support

Tactic:
simp_all
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
i : ι
inst_1 : Subsingleton ι
m : M
j : ι
⊢ (((AddEquiv.symm (uniqueAddEquiv i) : (a : M) → ι →₀ M) m : ι →₀ M) : (a : ι) → M) j = m

Tactic:
simp [Subsingleton.elim j i]

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddZeroClass M
inst_1 : AddZeroClass N
f : M → N
hf : f 0 = 0
hf' : ∀ (x y : M), f (x + y) = f x + f y
v₁ v₂ : ι →₀ M
x : ι
⊢ Eq.{u_4 + 1} (α := N) ((mapRange f hf (v₁ + v₂) : (a : ι) → N) x : N)
    ((mapRange f hf v₁ + mapRange f hf v₂ : (a : ι) → N) x : N)

Tactic:
simp only [hf', add_apply, mapRange_apply]

Premises used: Finsupp.mapRange_apply, Finsupp.add_apply
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
inst : AddZeroClass M
inst_1 : AddZeroClass N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
g₁ g₂ : ι →₀ M
⊢ mapRange (⇑f : (a : M) → N) ⋯ (g₁ + g₂) =
    HAdd.hAdd (α := ι →₀ N) (mapRange (⇑f : (a : M) → N) ⋯ g₁) (mapRange (⇑f : (a : M) → N) ⋯ g₂)

Tactic:
mapRange_add (map_add f) g₁ g₂

Premises used: map_add, Finsupp.mapRange_add
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
f_1 : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
⊢ Eq (α := F →₀ M) (embDomain f 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
f_1 : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
h :
  ∀ (b : F),
    Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) b : M)
      ((embDomain f v + embDomain f w : (a : F) → M) b : M)
⊢ embDomain f (v + w) = embDomain f v + embDomain f w

Tactic:
ext b
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
f_1 : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
pos :
  ∀ (h : Membership.mem (γ := Set F) (Set.range.{u_2, u_1 + 1} (ι := ι) (⇑f : (a : ι) → F)) b),
    Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) b : M)
      ((embDomain f v + embDomain f w : (a : F) → M) b : M)
neg :
  ∀ (h : b ∉ Set.range.{u_2, u_1 + 1} (ι := ι) (⇑f : (a : ι) → F)),
    Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) b : M)
      ((embDomain f v + embDomain f w : (a : F) → M) b : M)
⊢ Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) b : M)
    ((embDomain f v + embDomain f w : (a : F) → M) b : M)

Tactic:
by_cases h : b ∈ Set.range f

Premises used: Set.range, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
f_1 : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
h : Membership.mem (γ := Set F) (Set.range.{u_2, u_1 + 1} (ι := ι) (⇑f : (a : ι) → F)) b
pos :
  ∀ (a : ι),
    Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) ((f : (a : ι) → F) a : F) : M)
      ((embDomain f v + embDomain f w : (a : F) → M) ((f : (a : ι) → F) a : F) : M)
⊢ Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) b : M)
    ((embDomain f v + embDomain f w : (a : F) → M) b : M)

Tactic:
rcases h with ⟨a, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
f_1 : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
a : ι
⊢ Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) ((f : (a : ι) → F) a : F) : M)
    ((embDomain f v + embDomain f w : (a : F) → M) ((f : (a : ι) → F) a : F) : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
f_1 : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
h : b ∉ Set.range.{u_2, u_1 + 1} (ι := ι) (⇑f : (a : ι) → F)
⊢ Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) b : M)
    ((embDomain f v + embDomain f w : (a : F) → M) b : M)

Tactic:
simp only [coe_add, Pi.add_apply, embDomain_notin_range _ _ _ h, add_zero]

Premises used: Pi.add_apply, Finsupp.coe_add, Finsupp.embDomain_notin_range, add_zero
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
F : Type u_2
M : Type u_3
inst : AddZeroClass M
f : ι ↪ F
v w : ι →₀ M
⊢ embDomain f (v + w) = embDomain f v + embDomain f w

Tactic:
(embDomain.addMonoidHom f).map_add v w

Premises used: Set.Mem, setOf, Finsupp.embDomain.addMonoidHom, Finsupp.embDomain, AddMonoidHom.map_add
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b₁ b₂ : M
⊢ single a (b₁ + b₂) = HAdd.hAdd (α := ι →₀ M) (single a b₁) (single a b₂)

Tactic:
(zipWith_single_single _ _ _ _ _).symm

Premises used: Finsupp.zipWith_single_single, Eq.symm
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
m₁ m₂ : M
b : ι
⊢ (single a (m₁ + m₂) : (a : ι) → M) b =
    HAdd.hAdd (α := M) (β := M) ((single a m₁ : (a : ι) → M) b : M) ((single a m₂ : (a : ι) → M) b : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
⊢ support (single a b) = {a}

Tactic:
have H := support_single a hb
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : support (single a b) = {a}
rw : Disjoint (support (single a b)) f.support
⊢ (single a b + f).support = cons a f.support ha

Tactic:
rw [support_add_eq, H, cons_eq_insert, insert_eq]

Premises used: Finset.insert_eq, Finsupp.support_add_eq, Finset.cons_eq_insert
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : support (single a b) = {a}
rwa : Disjoint {a} f.support
rwa₁ rwa₂ rwa₃ rwa₄ : a ∉ f.support
⊢ Disjoint (support (single a b)) f.support

Tactic:
rwa [H, disjoint_singleton_left]

Premises used: Finset.disjoint_singleton_left
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
have have₁ have₂ : ∀ (H : support (single a b) = {a}), (single a b + f).support = cons a f.support ha
have₃ : ∀ (H : support (single a b) = {a}), Disjoint (support (single a b)) f.support
⊢ (single a b + f).support = cons a f.support ha

Tactic:
classical
  have H := support_single a hb
  rw [support_add_eq, H, cons_eq_insert, insert_eq]
  rwa [H, disjoint_singleton_left]

Premises used: Finset.insert_eq, Finsupp.support_add_eq, Finset.cons_eq_insert, Finset.disjoint_singleton_left
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : support (single a b) = {a}
rw : Disjoint f.support (support (single a b))
⊢ (f + single a b).support = cons a f.support ha

Tactic:
rw [support_add_eq, H, union_comm, cons_eq_insert, insert_eq]

Premises used: Finset.insert_eq, Finset.union_comm, Finsupp.support_add_eq, Finset.cons_eq_insert
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : support (single a b) = {a}
rwa : Disjoint f.support {a}
rwa₁ rwa₂ rwa₃ rwa₄ : a ∉ f.support
⊢ Disjoint f.support (support (single a b))

Tactic:
rwa [H, disjoint_singleton_right]

Premises used: Finset.disjoint_singleton_right
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
have have₁ have₂ : ∀ (H : support (single a b) = {a}), (f + single a b).support = cons a f.support ha
have₃ : ∀ (H : support (single a b) = {a}), Disjoint f.support (support (single a b))
⊢ (f + single a b).support = cons a f.support ha

Tactic:
classical
  have H := support_single a hb
  rw [support_add_eq, H, union_comm, cons_eq_insert, insert_eq]
  rwa [H, disjoint_singleton_right]

Premises used: Finset.insert_eq, Finset.union_comm, Finsupp.support_add_eq, Finset.cons_eq_insert, Finset.disjoint_singleton_right
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
rw : Eq (α := Finset ι) ({f₁} ∪ {f₂}) {f₁, f₂}
rw₁ : Disjoint (support (single f₁ g₁)) (support (single f₂ g₂))
⊢ (HAdd.hAdd (α := ι →₀ M) (single f₁ g₁) (single f₂ g₂)).support = {f₁, f₂}

Tactic:
rw [support_add_eq, support_single _ hg₁, support_single _ hg₂]

Premises used: Finsupp.support_single, Finsupp.support_add_eq
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ Eq (α := Finset ι) ({f₁} ∪ {f₂}) {f₁, f₂}

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ Disjoint (support (single f₁ g₁)) (support (single f₂ g₂))

Tactic:
simp [support_single, *]

Premises used: Finsupp.support_single
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
⊢ (HAdd.hAdd (α := ι →₀ M) (single f₁ g₁) (single f₂ g₂)).support ⊆ {f₁, f₂}

Tactic:
subset_trans Finsupp.support_add <| union_subset_iff.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, subset_trans, And.intro, Finsupp.support_add, Finset.union_subset_iff