awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
h : ∀ (a : α), Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
⊢ v₁ = v₂

Tactic:
ext a
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
a : α
pos : ∀ (h : a ∈ v₁.support ∪ v₂.support), Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
neg : ∀ (h : a ∉ v₁.support ∪ v₂.support), Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)

Tactic:
by_cases h : a ∈ v₁.support ∪ v₂.support

Premises used: Finsupp.support
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
rw rw₁ : a ∈ S
⊢ Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)

Tactic:
rw [← mapDomain_apply' S _ hv₁ hf _, ← mapDomain_apply' S _ hv₂ hf _, eq]

Premises used: Finsupp.mapDomain_apply'
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
a₁ : a ∈ (↑v₁.support : Set α) ∪ (↑v₂.support : Set α)
⊢ a ∈ S

Tactic:
apply Set.union_subset hv₁ hv₂

Premises used: Set.union_subset
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ (↑v₁.support : Set α) ∪ (↑v₂.support : Set α)

Tactic:
mod_cast h

Premises used: congrArg, Finset.coe_union._simp_1, Finsupp.support, cast, Membership.mem, Finset.mem_coe._simp_1, congrFun', Eq.symm, Eq.trans
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ (↑v₁.support : Set α) ∪ (↑v₂.support : Set α)

Tactic:
exact mod_cast h
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∉ v₁.support ∪ v₂.support
⊢ Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)

Tactic:
simp_all
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₁
v₂ : α →₀ M
hv₂ : Membership.mem (γ := Set (α →₀ M)) {w : α →₀ M | (↑w.support : Set α) ⊆ S} v₂
eq : mapDomain f v₁ = mapDomain f v₂
a : α
pos : ∀ (h : a ∈ v₁.support ∪ v₂.support), Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
neg neg₁ :
  ∀ (h : a ∉ v₁.support ∪ v₂.support), Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)

Tactic:
classical
    by_cases h : a ∈ v₁.support ∪ v₂.support
    · rw [← mapDomain_apply' S _ hv₁ hf _, ← mapDomain_apply' S _ hv₂ hf _, eq] <;>
        · apply Set.union_subset hv₁ hv₂
          exact mod_cast h
    · simp_all

Premises used: Finsupp.support, Set.union_subset, Finsupp.mapDomain_apply'
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_12
inst : AddCommMonoid M
f : α ≃ β
l : α →₀ M
h :
  ∀ (x : β),
    Eq.{u_12 + 1} (α := M) ((equivMapDomain f l : (a : β) → M) x : M)
      ((mapDomain (⇑f : (a : α) → β) l : (a : β) → M) x : M)
⊢ equivMapDomain f l = mapDomain (⇑f : (a : α) → β) l

Tactic:
ext x
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_12
inst : AddCommMonoid M
f : α ≃ β
l : α →₀ M
x : β
⊢ Eq.{u_12 + 1} (α := M) ((equivMapDomain f l : (a : β) → M) x : M)
    ((mapDomain (⇑f : (a : α) → β) l : (a : β) → M) x : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α → β
l : β →₀ M
hf : Set.InjOn f (f ⁻¹' (↑l.support : Set β))
a : α
rw : f a ∈ l.support ↔ Ne.{u_5 + 1} (α := M) ((l : (a : β) → M) (f a) : M) (0 : M)
⊢ a ∈ l.support.preimage f hf ↔ Ne.{u_5 + 1} (α := M) ((l : (a : β) → M) (f a) : M) (0 : M)

Tactic:
rw [Finset.mem_preimage]

Premises used: Finset.mem_preimage
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α → β
l : β →₀ M
hf : Set.InjOn f (f ⁻¹' (↑l.support : Set β))
a : α
⊢ f a ∈ l.support ↔ Ne.{u_5 + 1} (α := M) ((l : (a : β) → M) (f a) : M) (0 : M)

Tactic:
l.mem_support_toFun (f a)

Premises used: Finsupp.mem_support_toFun
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α → β
l : β →₀ M
hf : Set.InjOn f (f ⁻¹' (↑l.support : Set β))
a : α
⊢ f a ∈ l.support ↔ Ne.{u_5 + 1} (α := M) ((l : (a : β) → M) (f a) : M) (0 : M)

Tactic:
exact l.mem_support_toFun (f a)

Premises used: Finsupp.mem_support_toFun
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
l : β →₀ M
hf : Set.InjOn f (f ⁻¹' (↑l.support : Set β))
a : α
⊢ Eq.{u_5 + 1} (α := M) ((comapDomain f l hf : (a : α) → M) a : M) ((l : (a : β) → M) (f a) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : Zero M
inst_1 : AddCommMonoid N
f : α → β
l : β →₀ M
g : β → M → N
hf : Set.BijOn f (f ⁻¹' (↑l.support : Set β)) (↑l.support : Set β)
⊢ (comapDomain f l ⋯).sum (g ∘ f) = l.sum g

Tactic:
Finset.sum_preimage_of_bij f _ hf fun x => g x (l x)

Premises used: Finset.sum_preimage_of_bij, Finsupp.sum, Finset.map, Set.toFinset, Set.Finite.toFinset, Finset.preimage, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' (↑l.support : Set β)) (↑l.support : Set β)
rw :
  { support := l.support.preimage f ⋯, toFun := fun (a : α) ↦ (l : (a : β) → M) (f a), mem_support_toFun := ⋯ :
          α →₀ M }.support =
      ∅ →
    l.support = ∅
⊢ comapDomain f l ⋯ = 0 → l = 0

Tactic:
rw [← support_eq_empty, ← support_eq_empty, comapDomain]

Premises used: Finsupp.support_eq_empty, Finsupp.comapDomain
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' (↑l.support : Set β)) (↑l.support : Set β)
simp_rw : (∀ (a : α), f a ∉ l.support) → ∀ (a : β), a ∉ l.support
⊢ { support := l.support.preimage f ⋯, toFun := fun (a : α) ↦ (l : (a : β) → M) (f a), mem_support_toFun := ⋯ :
          α →₀ M }.support =
      ∅ →
    l.support = ∅

Tactic:
simp_rw [Finset.ext_iff, Finset.notMem_empty, iff_false, mem_preimage]

Premises used: iff_false, Finset.ext_iff, Finset.notMem_empty, Finset.mem_preimage
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' (↑l.support : Set β)) (↑l.support : Set β)
h : ∀ (a : α), f a ∉ l.support
a : β
ha : a ∈ l.support
obtain : ∀ (b : α) (hb : b ∈ f ⁻¹' (↑l.support : Set β) ∧ f b = a), False
⊢ False

Tactic:
obtain ⟨b, hb⟩ := hf.2.2 ha

Premises used: And.right
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' (↑l.support : Set β)) (↑l.support : Set β)
h : ∀ (a : α), f a ∉ l.support
a : β
ha : a ∈ l.support
b : α
hb : b ∈ f ⁻¹' (↑l.support : Set β) ∧ f b = a
⊢ False

Tactic:
h b (hb.2.symm ▸ ha)

Premises used: Eq.rec, And.right, Eq.symm
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
l : β →₀ M
hf : Set.BijOn f (f ⁻¹' (↑l.support : Set β)) (↑l.support : Set β)
h : ∀ (a : α), f a ∉ l.support
a : β
ha : a ∈ l.support
b : α
hb : b ∈ f ⁻¹' (↑l.support : Set β) ∧ f b = a
⊢ False

Tactic:
exact h b (hb.2.symm ▸ ha)

Premises used: Eq.rec, And.right, Eq.symm
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
b : β
hb : b ∉ Set.range f
m : M
hf : Set.InjOn f (f ⁻¹' (↑(support (single b m)) : Set β))
h : ∀ (a : α), Eq.{u_5 + 1} (α := M) ((comapDomain f (single b m) hf : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
⊢ comapDomain f (single b m) hf = 0

Tactic:
ext a
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
b : β
hb : b ∉ Set.range f
m : M
hf : Set.InjOn f (f ⁻¹' (↑(support (single b m)) : Set β))
a : α
h : b = f a → m = 0
⊢ Eq.{u_5 + 1} (α := M) ((comapDomain f (single b m) hf : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)

Tactic:
simp only [comapDomain, single_apply, coe_mk, coe_zero, Pi.zero_apply, ite_eq_right_iff]

Premises used: Pi.zero_apply, ite_eq_right_iff, Finsupp.single_apply, Finsupp.comapDomain, Finsupp.coe_mk, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
m : M
a : α
hb : f a ∉ Set.range f
hf : Set.InjOn f (f ⁻¹' (↑(support (single (f a) m)) : Set β))
⊢ m = 0

Tactic:
simp at hb
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
b : β
hb : b ∉ Set.range f
m : M
hf : Set.InjOn f (f ⁻¹' (↑(support (single b m)) : Set β))
h : ∀ (a : α), Eq.{u_5 + 1} (α := M) ((comapDomain f (single b m) hf : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
h₁ : ∀ (a : α), b = f a → m = 0
h₂ : ∀ (a : α) (hb : f a ∉ Set.range f) (hf : Set.InjOn f (f ⁻¹' (↑(support (single (f a) m)) : Set β))), m = 0
⊢ comapDomain f (single b m) hf = 0

Tactic:
classical
  ext a
  simp only [comapDomain, single_apply, coe_mk, coe_zero, Pi.zero_apply, ite_eq_right_iff]
  rintro rfl
  simp at hb

Premises used: Pi.zero_apply, ite_eq_right_iff, Finsupp.single_apply, Finsupp.comapDomain, Finsupp.coe_mk, rfl, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
hg : (↑g.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
h :
  ∀ (b : β),
    Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) b : M)
      ((g : (a : β) → M) b : M)
⊢ embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) = g

Tactic:
ext b
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
hg : (↑g.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
b : β
pos :
  ∀ (hb : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b),
    Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) b : M)
      ((g : (a : β) → M) b : M)
neg :
  ∀ (hb : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)),
    Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) b : M)
      ((g : (a : β) → M) b : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) b : M)
    ((g : (a : β) → M) b : M)

Tactic:
by_cases hb : b ∈ Set.range f

Premises used: Set.range, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
hg : (↑g.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
b : β
hb : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b
pos :
  ∀ (a : α),
    Eq.{u_5 + 1} (α := M)
      ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) ((f : (a : α) → β) a : β) : M)
      ((g : (a : β) → M) ((f : (a : α) → β) a : β) : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) b : M)
    ((g : (a : β) → M) b : M)

Tactic:
obtain ⟨a, rfl⟩ := hb

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
hg : (↑g.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
a : α
pos :
  Eq.{u_5 + 1} (α := M) ((comapDomain (⇑f : (a : α) → β) g ⋯ : (a : α) → M) a : M)
    ((g : (a : β) → M) ((f : (a : α) → β) a : β) : M)
pos₁ pos₂ :
  Eq.{u_5 + 1} (α := M) ((g : (a : β) → M) ((f : (a : α) → β) a : β) : M)
    ((g : (a : β) → M) ((f : (a : α) → β) a : β) : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) ((f : (a : α) → β) a : β) : M)
    ((g : (a : β) → M) ((f : (a : α) → β) a : β) : M)

Tactic:
rw [embDomain_apply_self, comapDomain_apply]

Premises used: Finsupp.comapDomain_apply, Finsupp.embDomain_apply_self
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
hg : (↑g.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
b : β
hb : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ Eq.{u_5 + 1} (α := M) ((g : (a : β) → M) b : M) (0 : M)

Tactic:
replace hg : g b = 0 := notMem_support_iff.mp <| mt (hg ·) hb
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
g : β →₀ M
b : β
hb : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
hg : Eq.{u_5 + 1} (α := M) ((g : (a : β) → M) b : M) (0 : M)
neg : Eq.{u_5 + 1} (α := M) (0 : M) ((g : (a : β) → M) b : M)
neg₁ neg₂ : Eq.{u_5 + 1} (α := M) 0 0
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f (comapDomain (⇑f : (a : α) → β) g ⋯) : (a : β) → M) b : M)
    ((g : (a : β) → M) b : M)

Tactic:
rw [embDomain_notin_range _ _ _ hb, hg]

Premises used: Finsupp.embDomain_notin_range
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
l : α →₀ M
h :
  ∀ (a : α),
    Eq.{u_5 + 1} (α := M) ((comapDomain (⇑f : (a : α) → β) (embDomain f l) ⋯ : (a : α) → M) a : M)
      ((l : (a : α) → M) a : M)
⊢ comapDomain (⇑f : (a : α) → β) (embDomain f l) ⋯ = l

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ↪ β
l : α →₀ M
a : α
⊢ Eq.{u_5 + 1} (α := M) ((comapDomain (⇑f : (a : α) → β) (embDomain f l) ⋯ : (a : α) → M) a : M)
    ((l : (a : α) → M) a : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
hif : Set.InjOn f (f ⁻¹' (↑(support.{u_2, u_5} (M := M) 0) : Set β))
h : ∀ (a : α), Eq.{u_5 + 1} (α := M) ((comapDomain f 0 hif : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
⊢ comapDomain f 0 hif = 0

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
hif : Set.InjOn f (f ⁻¹' (↑(support.{u_2, u_5} (M := M) 0) : Set β))
a : α
⊢ Eq.{u_5 + 1} (α := M) ((comapDomain f 0 hif : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)

Tactic:
rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' (↑(support (single (f a) m)) : Set β))
inl :
  ∀ (hif : Set.InjOn f (f ⁻¹' (↑(support.{u_2, u_5} (M := M) (single (f a) 0)) : Set β))),
    comapDomain f (single (f a) 0) hif = single a 0
inr : ∀ (hm : m ≠ 0), comapDomain f (single (f a) m) hif = single a m
⊢ comapDomain f (single (f a) m) hif = single a m

Tactic:
rcases eq_or_ne m 0 with (rfl | hm)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
a : α
hif : Set.InjOn f (f ⁻¹' (↑(support.{u_2, u_5} (M := M) (single (f a) 0)) : Set β))
inl : Eq (α := α →₀ M) (comapDomain f 0 ⋯) 0
⊢ comapDomain f (single (f a) 0) hif = single a 0

Tactic:
simp_rw [single_zero, comapDomain_zero]

Premises used: Finset.coe_empty, Finsupp.comapDomain_zero, Eq.rec, Eq.symm, Finsupp.single_zero, Set.injOn_empty
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' (↑(support (single (f a) m)) : Set β))
hm : m ≠ 0
inr : f ⁻¹' {f a} ⊆ {a} ∧ m = m
⊢ comapDomain f (single (f a) m) hif = single a m

Tactic:
rw [eq_single_iff, comapDomain_apply, comapDomain_support, ← Finset.coe_subset, coe_preimage,
      support_single _ hm, coe_singleton, coe_singleton, single_eq_same]

Premises used: Finsupp.support_single, Finset.coe_singleton, Finsupp.single_eq_same, Finsupp.eq_single_iff, Finsupp.comapDomain_apply, Finset.coe_preimage, Finsupp.comapDomain_support, Finset.coe_subset
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' (↑(support (single (f a) m)) : Set β))
hm : m ≠ 0
⊢ Set.InjOn f (f ⁻¹' {f a})

Tactic:
rw [support_single _ hm, coe_singleton] at hif

Premises used: Finsupp.support_single, Finset.coe_singleton
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' (↑(support (single (f a) m)) : Set β))
hm : m ≠ 0
hif₁ : Set.InjOn f (f ⁻¹' {f a})
⊢ m ≠ 0

Tactic:
rw [support_single _ hm, coe_singleton] at hif

Premises used: Finsupp.support_single, Finset.coe_singleton
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' {f a})
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m

Tactic:
⟨fun x hx => hif hx rfl hx, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' {f a})
hm : m ≠ 0
⊢ f ⁻¹' {f a} ⊆ {a} ∧ m = m

Tactic:
exact ⟨fun x hx => hif hx rfl hx, rfl⟩
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
hf : Injective f
l' : α →₀ M
h : (fun (l : β →₀ M) ↦ comapDomain f l ⋯) (embDomain { toFun := f, inj' := hf : α ↪ β } l') = l'
⊢ ∃ (a : β →₀ M), (fun (l : β →₀ M) ↦ comapDomain f l ⋯) a = l'

Tactic:
use l'.embDomain ⟨f, hf⟩

Premises used: Function.Embedding.mk, Finsupp.embDomain
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
hf : Injective f
l' : α →₀ M
⊢ (fun (l : β →₀ M) ↦ comapDomain f l ⋯) (embDomain { toFun := f, inj' := hf : α ↪ β } l') = l'

Tactic:
Finsupp.comapDomain_embDomain ..

Premises used: Finsupp.comapDomain_embDomain
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α → β
hf : Injective f
l' : α →₀ M
⊢ (fun (l : β →₀ M) ↦ comapDomain f l ⋯) (embDomain { toFun := f, inj' := hf : α ↪ β } l') = l'

Tactic:
exact Finsupp.comapDomain_embDomain ..

Premises used: Finsupp.comapDomain_embDomain
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddZeroClass M
f : α → β
v₁ v₂ : β →₀ M
hv₁ : Set.InjOn f (f ⁻¹' (↑v₁.support : Set β))
hv₂ : Set.InjOn f (f ⁻¹' (↑v₂.support : Set β))
hv₁₂ : Set.InjOn f (f ⁻¹' (↑(v₁ + v₂).support : Set β))
h :
  ∀ (a : α),
    Eq.{u_5 + 1} (α := M) ((comapDomain f (v₁ + v₂) hv₁₂ : (a : α) → M) a : M)
      ((comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂ : (a : α) → M) a : M)
⊢ comapDomain f (v₁ + v₂) hv₁₂ = comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddZeroClass M
f : α → β
v₁ v₂ : β →₀ M
hv₁ : Set.InjOn f (f ⁻¹' (↑v₁.support : Set β))
hv₂ : Set.InjOn f (f ⁻¹' (↑v₂.support : Set β))
hv₁₂ : Set.InjOn f (f ⁻¹' (↑(v₁ + v₂).support : Set β))
a : α
⊢ Eq.{u_5 + 1} (α := M) ((comapDomain f (v₁ + v₂) hv₁₂ : (a : α) → M) a : M)
    ((comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂ : (a : α) → M) a : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddZeroClass M
f : α → β
hf : Injective f
v₁ v₂ : β →₀ M
⊢ comapDomain f (v₁ + v₂) ⋯ = comapDomain f v₁ ⋯ + comapDomain f v₂ ⋯

Tactic:
comapDomain_add ..

Premises used: Finsupp.comapDomain_add
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : (↑l.support : Set β) ⊆ Set.range f
rw :
  mapDomain (⇑{ toFun := f, inj' := hf : α ↪ β } : (a : α) → β)
    (comapDomain (⇑{ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) l ⋯)
| l

Tactic:
rw [← embDomain_comapDomain (f := ⟨f, hf⟩) hl (M := M), embDomain_eq_mapDomain]

Premises used: Finsupp.embDomain_comapDomain, Finsupp.embDomain_eq_mapDomain
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : (↑l.support : Set β) ⊆ Set.range f
conv_rhs :
  mapDomain f (comapDomain f l ⋯) =
    mapDomain (⇑{ toFun := f, inj' := hf : α ↪ β } : (a : α) → β)
      (comapDomain (⇑{ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) l ⋯)
⊢ mapDomain f (comapDomain f l ⋯) = l

Tactic:
conv_rhs => rw [← embDomain_comapDomain (f := ⟨f, hf⟩) hl (M := M), embDomain_eq_mapDomain]

Premises used: Finsupp.embDomain_comapDomain, Finsupp.embDomain_eq_mapDomain
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : (↑l.support : Set β) ⊆ Set.range f
⊢ mapDomain f (comapDomain f l ⋯) =
    mapDomain (⇑{ toFun := f, inj' := hf : α ↪ β } : (a : α) → β)
      (comapDomain (⇑{ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) l ⋯)

Tactic:
rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
M : Type u_5
inst : AddCommMonoid M
l : ℕ →₀ M
⊢ mapDomain (fun (x : ℕ) ↦ x + 1) ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ M) → ℕ →₀ M) l) =
    erase 0 l

Tactic:
.trans ?_ (mapDomain_comapDomain _ (add_left_injective 1) _ fun _ ↦ ?_)

Premises used: Finsupp.mapDomain_comapDomain, add_left_injective, OfNat.ofNat, Eq.trans