awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Ext
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H :
  ∀ (x : α),
    Eq (α := MonoidHom.{u_2, u_3} (Multiplicative M) N)
      (f.comp
        ((AddMonoidHom.toMultiplicative : (a : M →+ α →₀ M) → Multiplicative M →* Multiplicative (α →₀ M))
          (singleAddHom x)))
      (g.comp
        ((AddMonoidHom.toMultiplicative : (a : M →+ α →₀ M) → Multiplicative M →* Multiplicative (α →₀ M))
          (singleAddHom x)))
⊢ f = g

Tactic:
mulHom_ext fun x => DFunLike.congr_fun (H x)

Premises used: DFunLike.congr_fun, Finsupp.mulHom_ext
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
t : Fin (n + 1) →₀ M
⊢ Eq (α := M) ((t.tail : (a : Fin n) → M) i : M) ((t : (a : Fin (n + 1)) → M) i.succ : M)

Tactic:
rfl

Premises used: Fin.tail, rfl
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
⊢ (cons y s : (a : Fin (n + 1)) → M) 0 = y

Tactic:
rfl

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, rfl
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
⊢ Eq (α := M) ((cons y s : (a : Fin (n + 1)) → M) i.succ : M) ((s : (a : Fin n) → M) i : M)

Tactic:
rfl

Premises used: Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, rfl
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
k : Fin n
⊢ Eq (α := M) (((cons y s).tail : (a : Fin n) → M) k : M) ((s : (a : Fin n) → M) k : M)

Tactic:
simp only [tail_apply, cons_succ]

Premises used: Finsupp.cons_succ, Finsupp.tail_apply
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
t : Fin (n + 1) →₀ M
⊢ (t.update 0 y).tail = t.tail

Tactic:
simp [tail]

Premises used: Finsupp.tail
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
t : Fin (n + 1) →₀ M
h :
  ∀ (a : Fin n),
    Eq (α := M) (((t.update i.succ y).tail : (a : Fin n) → M) a : M) ((t.tail.update i y : (a : Fin n) → M) a : M)
⊢ (t.update i.succ y).tail = t.tail.update i y

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
t : Fin (n + 1) →₀ M
a : Fin n
⊢ Eq (α := M) (((t.update i.succ y).tail : (a : Fin n) → M) a : M) ((t.tail.update i y : (a : Fin n) → M) a : M)

Tactic:
simp [tail]

Premises used: Finsupp.tail
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
t : Fin (n + 1) →₀ M
h :
  ∀ (a : Fin (n + 1)),
    Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
      ((t : (a : Fin (n + 1)) → M) a)
⊢ cons ((t : (a : Fin (n + 1)) → M) 0) t.tail = t

Tactic:
ext a
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
pos :
  ∀ (c_a : a = 0),
    Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
      ((t : (a : Fin (n + 1)) → M) a)
neg :
  ∀ (c_a : ¬a = 0),
    Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
      ((t : (a : Fin (n + 1)) → M) a)
⊢ Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
    ((t : (a : Fin (n + 1)) → M) a)

Tactic:
by_cases c_a : a = 0
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : a = 0
pos :
  Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) 0 : M)
    ((t : (a : Fin (n + 1)) → M) 0 : M)
pos₁ pos₂ : Eq (α := M) ((t : (a : Fin (n + 1)) → M) 0 : M) ((t : (a : Fin (n + 1)) → M) 0 : M)
⊢ Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
    ((t : (a : Fin (n + 1)) → M) a)

Tactic:
rw [c_a, cons_zero]

Premises used: Finsupp.cons_zero
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : ¬a = 0
neg :
  Eq (α := M)
    (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) (a.pred c_a).succ : M)
    ((t : (a : Fin (n + 1)) → M) (a.pred c_a).succ : M)
neg₁ : Eq (α := M) ((t.tail : (a : Fin n) → M) (a.pred c_a) : M) ((t : (a : Fin (n + 1)) → M) (a.pred c_a).succ : M)
neg₂ neg₃ : Eq (α := M) ((t.tail : (a : Fin n) → M) (a.pred c_a) : M) ((t.tail : (a : Fin n) → M) (a.pred c_a) : M)
⊢ Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
    ((t : (a : Fin (n + 1)) → M) a)

Tactic:
rw [← Fin.succ_pred a c_a, cons_succ, ← tail_apply]

Premises used: Finsupp.cons_succ, Finsupp.tail_apply, Fin.succ_pred
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
h : ∀ (j : Fin (n + 1)), Eq (α := M) ((cons y 0 : (a : Fin (n + 1)) → M) j : M) ((single 0 y : (a : Fin (n + 1)) → M) j)
⊢ Eq (α := Fin (n + 1) →₀ M) (cons y 0) (single 0 y)

Tactic:
ext j
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
j : Fin (n + 1)
h : Eq (α := M) ((cons y 0 : (a : Fin (n + 1)) → M) 0 : M) ((single 0 y : (a : Fin (n + 1)) → M) 0 : M)
h₁ :
  ∀ (i : Fin n),
    Eq (α := M) ((cons y 0 : (a : Fin (n + 1)) → M) i.succ : M) ((single 0 y : (a : Fin (n + 1)) → M) i.succ : M)
⊢ Eq (α := M) ((cons y 0 : (a : Fin (n + 1)) → M) j : M) ((single 0 y : (a : Fin (n + 1)) → M) j)

Tactic:
cases j using Fin.cases
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
⊢ Eq (α := M) ((cons y 0 : (a : Fin (n + 1)) → M) 0 : M) ((single 0 y : (a : Fin (n + 1)) → M) 0 : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
i : Fin n
⊢ Eq (α := M) ((cons y 0 : (a : Fin (n + 1)) → M) i.succ : M) ((single 0 y : (a : Fin (n + 1)) → M) i.succ : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
h :
  ∀ (j : Fin (n + 1)),
    Eq (α := M) ((cons 0 (single i y) : (a : Fin (n + 1)) → M) j : M) ((single i.succ y : (a : Fin (n + 1)) → M) j)
⊢ Eq (α := Fin (n + 1) →₀ M) (cons 0 (single i y)) (single i.succ y)

Tactic:
ext j
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
j : Fin (n + 1)
h : Eq (α := M) ((cons 0 (single i y) : (a : Fin (n + 1)) → M) 0 : M) ((single i.succ y : (a : Fin (n + 1)) → M) 0 : M)
h₁ :
  ∀ (i_1 : Fin n),
    Eq (α := M) ((cons 0 (single i y) : (a : Fin (n + 1)) → M) i_1.succ : M)
      ((single i.succ y : (a : Fin (n + 1)) → M) i_1.succ : M)
⊢ Eq (α := M) ((cons 0 (single i y) : (a : Fin (n + 1)) → M) j : M) ((single i.succ y : (a : Fin (n + 1)) → M) j)

Tactic:
cases j using Fin.cases
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
⊢ Eq (α := M) ((cons 0 (single i y) : (a : Fin (n + 1)) → M) 0 : M) ((single i.succ y : (a : Fin (n + 1)) → M) 0 : M)

Tactic:
simp [single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
i_1 : Fin n
⊢ Eq (α := M) ((cons 0 (single i y) : (a : Fin (n + 1)) → M) i_1.succ : M)
    ((single i.succ y : (a : Fin (n + 1)) → M) i_1.succ : M)

Tactic:
simp [single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
⊢ Eq.{u_1 + 1} (α := Fin (n + 1) →₀ M) (cons 0 0) 0

Tactic:
simp [cons_zero_eq_single_zero]

Premises used: Finsupp.cons_zero_eq_single_zero
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
h : y ≠ 0
contrapose : ∀ (c : cons y s = 0), y = 0
⊢ cons y s ≠ 0

Tactic:
contrapose h with c
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
rw : Eq (α := M) ((cons y s : (a : Fin (n + 1)) → M) 0 : M) (0 : M)
rw₁ : Eq.{u_1 + 1} (α := M) ((0 : (a : Fin (n + 1)) → M) 0 : M) (0 : M)
rw₂ : Eq.{u_1 + 1} (α := M) (0 0) 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := M) 0 0
⊢ y = 0

Tactic:
rw [← cons_zero y s, c, Finsupp.coe_zero, Pi.zero_apply]

Premises used: Pi.zero_apply, Finsupp.cons_zero, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
h : s ≠ 0
contrapose : ∀ (c : cons y s = 0), s = 0
⊢ cons y s ≠ 0

Tactic:
contrapose h with c
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
h : ∀ (a : Fin n), Eq (α := M) ((s : (a : Fin n) → M) a : M) ((0 : (a : Fin n) → M) a : M)
⊢ s = 0

Tactic:
ext a
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
a : Fin n
⊢ Eq (α := M) ((s : (a : Fin n) → M) a : M) ((0 : (a : Fin n) → M) a : M)

Tactic:
simp [← cons_succ a y s, c]

Premises used: Finsupp.cons_succ
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
⊢ cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0

Tactic:
⟨fun h => ?_, fun h => h.casesOn cons_ne_zero_of_left cons_ne_zero_of_right⟩

Premises used: Or.casesOn, Iff.intro
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
refine : ∀ (h : cons y s ≠ 0), y ≠ 0 ∨ s ≠ 0
⊢ cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0

Tactic:
refine ⟨fun h => ?_, fun h => h.casesOn cons_ne_zero_of_left cons_ne_zero_of_right⟩
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
h : cons y s ≠ 0
⊢ y ≠ 0 ∨ s ≠ 0

Tactic:
imp_iff_not_or.1 fun h' c => h ?_

Premises used: imp_iff_not_or, Iff.mp
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
h : cons y s ≠ 0
refine : ∀ (h' : y = 0) (c : s = 0), cons y s = 0
⊢ y ≠ 0 ∨ s ≠ 0

Tactic:
refine imp_iff_not_or.1 fun h' c => h ?_

Premises used: imp_iff_not_or, Iff.mp
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
h : cons y s ≠ 0
h' : y = 0
c : s = 0
rw : cons 0 s = 0
rw₁ : Eq.{u_1 + 1} (α := Fin (n + 1) →₀ M) (cons 0 0) 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := Fin (n + 1) →₀ M) 0 0
⊢ cons y s = 0

Tactic:
rw [h', c, Finsupp.cons_zero_zero]

Premises used: Finsupp.cons_zero_zero
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
i : Fin (n + 1)
hi : i ∈ (cons y s).support
this : i = 0 ∨ ∃ (a : Fin n), ¬Eq (α := M) ((s : (a : Fin n) → M) a : M) (0 : M) ∧ a.succ = i
⊢ i ∈ insert 0 (Finset.map (Fin.succEmb n) s.support)

Tactic:
simpa
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
i : Fin (n + 1)
hi : i ∈ (cons y s).support
suffices : i = 0 ∨ ∃ (a : Fin n), ¬Eq (α := M) ((s : (a : Fin n) → M) a : M) (0 : M) ∧ a.succ = i
⊢ i ∈ insert 0 (Finset.map (Fin.succEmb n) s.support)

Tactic:
suffices i = 0 ∨ ∃ a, ¬s a = 0 ∧ a.succ = i by simpa
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
i : Fin (n + 1)
hi : i ∈ (cons y s).support
apply : ∀ (a : Fin n), i = a.succ → ¬Eq (α := M) ((s : (a : Fin n) → M) a : M) (0 : M) ∧ a.succ = i
⊢ i = 0 ∨ ∃ (a : Fin n), ¬Eq (α := M) ((s : (a : Fin n) → M) a : M) (0 : M) ∧ a.succ = i

Tactic:
apply (Fin.eq_zero_or_eq_succ i).imp id (Exists.imp _)

Premises used: id, Exists.imp, Fin.eq_zero_or_eq_succ, Or.imp
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
i : Fin n
hi : i.succ ∈ (cons y s).support
⊢ ¬Eq (α := M) ((s : (a : Fin n) → M) i : M) (0 : M) ∧ i.succ = i.succ

Tactic:
simpa [Finsupp.mem_support_iff] using hi

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
⊢ Injective (α := Fin n →₀ M) (cons y)

Tactic:
(equivFunOnFinite.symm.injective.comp ((Fin.cons_right_injective _).comp DFunLike.coe_injective))

Premises used: Finsupp.equivFunOnFinite, Function.Injective.comp, DFunLike.coe_injective, Equiv.injective, Equiv.symm, Finsupp.cons, Fin.cons_right_injective
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
⊢ Injective2.{u_1 + 1, u_1 + 1, u_1 + 1} (α := M) (β := Fin n →₀ M) cons

Tactic:
fun x₀ y₀ x y h ↦ ?_

Premises used: Function.Injective2
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
refine : ∀ (x₀ y₀ : M) (x y : Fin n →₀ M) (h : cons x₀ x = cons y₀ y), x₀ = y₀ ∧ x = y
⊢ Injective2.{u_1 + 1, u_1 + 1, u_1 + 1} (α := M) (β := Fin n →₀ M) cons

Tactic:
refine fun x₀ y₀ x y h ↦ ?_
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
x₀ y₀ : M
x y : Fin n →₀ M
h : cons x₀ x = cons y₀ y
⊢ Eq (α := M) ((cons x₀ x : (a : Fin (n + 1)) → M) 0 : M) ((cons y₀ y : (a : Fin (n + 1)) → M) 0 : M)

Tactic:
have := DFunLike.congr_fun h 0
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
x₀ y₀ : M
x y : Fin n →₀ M
h : cons x₀ x = cons y₀ y
this : x₀ = y₀
⊢ x₀ = y₀ ∧ x = y

Tactic:
⟨this, cons_right_injective y₀ (this ▸ h)⟩

Premises used: Eq.rec, Finsupp.cons_right_injective, And.intro, Eq.symm
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
x₀ y₀ : M
x y : Fin n →₀ M
h : cons x₀ x = cons y₀ y
this : x₀ = y₀
⊢ x₀ = y₀ ∧ x = y

Tactic:
exact ⟨this, cons_right_injective y₀ (this ▸ h)⟩
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
x : M
rw : cons x s = cons y 0 ↔ s = 0 ∧ x = y
rw₁ : x = y ∧ s = 0 ↔ s = 0 ∧ x = y
rw₂ rw₃ : s = 0 ∧ x = y ↔ s = 0 ∧ x = y
⊢ cons x s = single 0 y ↔ s = 0 ∧ x = y

Tactic:
rw [← cons_zero_eq_single_zero, cons_injective2.eq_iff, and_comm]

Premises used: and_comm, Finsupp.cons_zero_eq_single_zero, Function.Injective2.eq_iff, Finsupp.cons_injective2
-- Module: Mathlib.Data.Finsupp.Fin
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
x : M
rw : cons x s = cons 0 (single i y) ↔ s = single i y ∧ x = 0
rw₁ : x = 0 ∧ s = single i y ↔ s = single i y ∧ x = 0
rw₂ rw₃ : s = single i y ∧ x = 0 ↔ s = single i y ∧ x = 0
⊢ cons x s = single i.succ y ↔ s = single i y ∧ x = 0

Tactic:
rw [← cons_zero_single_eq_single_succ, cons_injective2.eq_iff, and_comm]

Premises used: Finsupp.cons_zero_single_eq_single_succ, and_comm, Function.Injective2.eq_iff, Finsupp.cons_injective2
-- Module: Mathlib.Data.Finsupp.Fintype
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Zero α
inst_3 : Fintype α
inst_4 : Nontrivial α
inst_5 : Infinite ι
⊢ Infinite (ι →₀ α)

Tactic:
let ⟨_, hm⟩ := exists_ne (0 : α)
  Infinite.of_injective _ <| Finsupp.single_left_injective hm

Premises used: Infinite.of_injective, exists_ne, Finsupp.single_left_injective, _private.0.Finsupp.infinite_of_left.match_1, Infinite, OfNat.ofNat, Finsupp, Finsupp.single
-- Module: Mathlib.Data.Finsupp.Fintype
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Zero α
inst_3 : Fintype α
inst_4 : Infinite α
inst_5 : Nonempty ι
⊢ Infinite (ι →₀ α)

Tactic:
Infinite.of_injective (fun i => Finsupp.single (Classical.arbitrary ι) i)
    (Finsupp.single_injective (Classical.arbitrary ι))

Premises used: Finsupp.single_injective, Infinite.of_injective, Classical.arbitrary, Finsupp.single
-- Module: Mathlib.Data.Finsupp.Fintype
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : Zero α
inst_3 : Fintype α
⊢ card (ι →₀ α) = card α ^ card ι

Tactic:
simp [card_congr Finsupp.equivFunOnFinite]

Premises used: Fintype.card_congr, Finsupp.equivFunOnFinite
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s_1 t : Finset ι
f_1 : (i : ι) → i ∈ s_1 → α
i_1 : ι
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
⊢ Membership.mem (γ := Finset ι) (map (α := ↥s) (Embedding.subtype fun (x : ι) ↦ x ∈ s) {i : ↥s | f (↑i : ι) ⋯ ≠ 0}) i ↔
    Ne.{u_2 + 1} (α := α) (if H : i ∈ s then f i H else 0) 0

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s_1 t : Finset ι
f_1 : (i : ι) → i ∈ s_1 → α
i_1 : ι
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
⊢ Membership.mem (γ := Finset ι) (map (α := ↥s) (Embedding.subtype fun (x : ι) ↦ x ∈ s) {i : ↥s | f (↑i : ι) ⋯ ≠ 0}) i ↔
    Ne.{u_2 + 1} (α := α) (if H : i ∈ s then f i H else 0) 0

Tactic:
classical simp
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
i : ι
hi : i ∈ s
f : (i : ι) → i ∈ s → α
⊢ (indicator s f : (a : ι) → α) i = f i hi

Tactic:
@dif_pos _ (id _) hi _ _ _

Premises used: dif_pos, dite
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
i : ι
hi : i ∉ s
f : (i : ι) → i ∈ s → α
⊢ Eq.{u_2 + 1} (α := α) ((indicator s f : (a : ι) → α) i : α) (0 : α)

Tactic:
@dif_neg _ (id _) hi _ _ _

Premises used: dif_neg, dite
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
inst_1 : DecidableEq ι
simp : Eq.{u_2 + 1} (α := α) (if H : i ∈ s then f i H else 0) (if hi : i ∈ s then f i hi else 0)
⊢ Eq.{u_2 + 1} (α := α) ((indicator s f : (a : ι) → α) i : α) (if hi : i ∈ s then f i hi else 0 : α)

Tactic:
simp only [indicator, ne_eq, coe_mk]

Premises used: Finsupp.indicator, ne_eq, Finsupp.coe_mk
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
inst_1 : DecidableEq ι
⊢ Eq.{u_2 + 1} (α := α) (if H : i ∈ s then f i H else 0) (if hi : i ∈ s then f i hi else 0)

Tactic:
congr
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h :
  Eq (α := ι →₀ α) ((fun (f : (i : ι) → i ∈ s → α) ↦ (indicator s f : ι →₀ α)) a)
    ((fun (f : (i : ι) → i ∈ s → α) ↦ (indicator s f : ι →₀ α)) b)
h₁ : ∀ (i : ι) (hi : i ∈ s), a i hi = b i hi
⊢ a = b

Tactic:
ext i hi
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h :
  Eq (α := ι →₀ α) ((fun (f : (i : ι) → i ∈ s → α) ↦ (indicator s f : ι →₀ α)) a)
    ((fun (f : (i : ι) → i ∈ s → α) ↦ (indicator s f : ι →₀ α)) b)
i : ι
hi : i ∈ s
h₁ : Eq.{u_2 + 1} (α := α) ((indicator s a : (a : ι) → α) i : α) ((indicator s b : (a : ι) → α) i : α)
⊢ a i hi = b i hi

Tactic:
rw [← indicator_of_mem hi a, ← indicator_of_mem hi b]

Premises used: Finsupp.indicator_of_mem
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h :
  Eq (α := ι →₀ α) ((fun (f : (i : ι) → i ∈ s → α) ↦ (indicator s f : ι →₀ α)) a)
    ((fun (f : (i : ι) → i ∈ s → α) ↦ (indicator s f : ι →₀ α)) b)
i : ι
hi : i ∈ s
⊢ Eq.{u_2 + 1} (α := α) ((indicator s a : (a : ι) → α) i : α) ((indicator s b : (a : ι) → α) i : α)

Tactic:
DFunLike.congr_fun h i

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h :
  Eq (α := ι →₀ α) ((fun (f : (i : ι) → i ∈ s → α) ↦ (indicator s f : ι →₀ α)) a)
    ((fun (f : (i : ι) → i ∈ s → α) ↦ (indicator s f : ι →₀ α)) b)
i : ι
hi : i ∈ s
⊢ Eq.{u_2 + 1} (α := α) ((indicator s a : (a : ι) → α) i : α) ((indicator s b : (a : ι) → α) i : α)

Tactic:
exact DFunLike.congr_fun h i

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : i ∈ support (indicator s f)
⊢ Ne.{u_2 + 1} (α := α) ((indicator s f : (a : ι) → α) i : α) (0 : α)

Tactic:
rw [mem_support_iff] at hi

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : Ne.{u_2 + 1} (α := α) ((indicator s f : (a : ι) → α) i : α) (0 : α)
by_contra : ∀ (h : i ∉ s), False
⊢ i ∈ s

Tactic:
by_contra h
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : Ne.{u_2 + 1} (α := α) ((indicator s f : (a : ι) → α) i : α) (0 : α)
h : i ∉ s
⊢ False

Tactic:
hi (indicator_of_notMem h _)

Premises used: Finsupp.indicator_of_notMem
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : Ne.{u_2 + 1} (α := α) ((indicator s f : (a : ι) → α) i : α) (0 : α)
h : i ∉ s
⊢ False

Tactic:
exact hi (indicator_of_notMem h _)

Premises used: Finsupp.indicator_of_notMem
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
a : ι
f : (j : ι) → Membership.mem (γ := Finset ι) {a} j → α
h : ∀ (j : ι), Eq.{u_2 + 1} (α := α) ((indicator {a} f : (a : ι) → α) j : α) ((single a (f a ⋯) : (a : ι) → α) j : α)
⊢ Eq (α := ι →₀ α) (indicator {a} f) (single a (f a ⋯))

Tactic:
ext j
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
a : ι
f : (j : ι) → Membership.mem (γ := Finset ι) {a} j → α
j : ι
h : (if h : j = a then f j ⋯ else 0) = if j = a then f a ⋯ else 0
⊢ Eq.{u_2 + 1} (α := α) ((indicator {a} f : (a : ι) → α) j : α) ((single a (f a ⋯) : (a : ι) → α) j : α)

Tactic:
simp only [single_apply, indicator_apply, mem_singleton, @eq_comm _ a j]

Premises used: Finset.mem_singleton, Finsupp.indicator_apply, eq_comm, Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
a : ι
f : (j : ι) → Membership.mem (γ := Finset ι) {a} j → α
j : ι
pos : ∀ (h : j = a), f j ⋯ = f a ⋯
neg : ∀ (h : ¬j = a), Eq.{u_2 + 1} (α := α) 0 0
⊢ (if h : j = a then f j ⋯ else 0) = if j = a then f a ⋯ else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
a : ι
f : (j : ι) → Membership.mem (γ := Finset ι) {a} j → α
j : ι
h : j = a
⊢ f j ⋯ = f a ⋯

Tactic:
simp [h]
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
a : ι
f : (j : ι) → Membership.mem (γ := Finset ι) {a} j → α
j : ι
h : ¬j = a
⊢ Eq.{u_2 + 1} (α := α) 0 0

Tactic:
simp [h]
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
a : ι
f : (j : ι) → Membership.mem (γ := Finset ι) {a} j → α
h : ∀ (j : ι), Eq.{u_2 + 1} (α := α) ((indicator {a} f : (a : ι) → α) j : α) ((single a (f a ⋯) : (a : ι) → α) j : α)
h₁ : ∀ (j : ι), (if h : j = a then f j ⋯ else 0) = if j = a then f a ⋯ else 0
⊢ Eq (α := ι →₀ α) (indicator {a} f) (single a (f a ⋯))

Tactic:
classical
  ext j
  simp only [single_apply, indicator_apply, mem_singleton, @eq_comm _ a j]
  split_ifs with h <;> simp [h]

Premises used: Finset.mem_singleton, Finsupp.indicator_apply, Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
i : ι
b : α
⊢ Eq (α := ι →₀ α) (single i b) (indicator {i} fun (x : ι) (x_1 : Membership.mem (γ := Finset ι) {i} x) ↦ b)

Tactic:
(indicator_singleton i (fun _ _ => b)).symm

Premises used: Finsupp.indicator_singleton, Eq.symm
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
g : ι → α
h : ∀ (i : ι), (indicator s fun (i : ι) (x : i ∈ s) ↦ g i : (a : ι) → α) i = (↑s : Set ι).indicator g i
⊢ (⇑(indicator s fun (i : ι) (x : i ∈ s) ↦ g i) : (a : ι) → α) = (↑s : Set ι).indicator g

Tactic:
ext i
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
g : ι → α
i : ι
⊢ (indicator s fun (i : ι) (x : i ∈ s) ↦ g i : (a : ι) → α) i = (↑s : Set ι).indicator g i

Tactic:
simp [indicator_apply, Set.indicator_apply]

Premises used: Set.indicator_apply, Finsupp.indicator_apply
-- Module: Mathlib.Data.Finsupp.Indicator
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
g : ι → α
h : ∀ (i : ι), (indicator s fun (i : ι) (x : i ∈ s) ↦ g i : (a : ι) → α) i = (↑s : Set ι).indicator g i
⊢ (⇑(indicator s fun (i : ι) (x : i ∈ s) ↦ g i) : (a : ι) → α) = (↑s : Set ι).indicator g

Tactic:
classical
  ext i
  simp [indicator_apply, Set.indicator_apply]

Premises used: Set.indicator_apply, Finsupp.indicator_apply