awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
⊢ (∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v) ↔ u + v = embDomain f y

Tactic:
⟨fun ⟨w, z, h, hw, hz⟩ ↦ ?_, fun h ↦ ⟨u.comapDomain f f.injective.injOn,
    ⟨v.comapDomain f f.injective.injOn, ?_, ?_, ?_⟩⟩⟩

Premises used: Function.Injective.injOn, _private.0.Finsupp.image_prodMap_embDomain_antidiagonal.match_1, HAdd.hAdd, And.intro, Iff.intro, Exists.intro, Function.Embedding.injective, Finsupp.embDomain, Finsupp.comapDomain, Eq, DFunLike.coe
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h :
  (∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v) →
    ∀ (w z : α →₀ ℕ) (h : w + z = y) (hw : embDomain f w = u) (hz : embDomain f z = v), u + v = embDomain f y
h₁ : ∀ (h : u + v = embDomain f y), comapDomain (⇑f : (a : α) → β) u ⋯ + comapDomain (⇑f : (a : α) → β) v ⋯ = y
h₂ : ∀ (h : u + v = embDomain f y), embDomain f (comapDomain (⇑f : (a : α) → β) u ⋯) = u
h₃ : ∀ (h : u + v = embDomain f y), embDomain f (comapDomain (⇑f : (a : α) → β) v ⋯) = v
⊢ (∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v) ↔ u + v = embDomain f y

Tactic:
refine ⟨fun ⟨w, z, h, hw, hz⟩ ↦ ?_, fun h ↦ ⟨u.comapDomain f f.injective.injOn,
    ⟨v.comapDomain f f.injective.injOn, ?_, ?_, ?_⟩⟩⟩
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h_1 : ∃ (a : α →₀ ℕ) (b : α →₀ ℕ), a + b = y ∧ embDomain f a = u ∧ embDomain f b = v
w z : α →₀ ℕ
h : w + z = y
hw : embDomain f w = u
hz : embDomain f z = v
h₁ : embDomain f w + v = embDomain f y
h₂ : embDomain f w + embDomain f z = embDomain f y
h₃ : embDomain f (w + z) = embDomain f y
h₄ h₅ : embDomain f y = embDomain f y
⊢ u + v = embDomain f y

Tactic:
rw [← hw, ← hz, ← embDomain_add, h]

Premises used: Finsupp.embDomain_add
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
h₁ : comapDomain (⇑f : (a : α) → β) (u + v) ⋯ = y
h₂ : comapDomain (⇑f : (a : α) → β) (embDomain f y) ⋯ = y
h₃ h₄ : y = y
⊢ comapDomain (⇑f : (a : α) → β) u ⋯ + comapDomain (⇑f : (a : α) → β) v ⋯ = y

Tactic:
rw [← comapDomain_add_of_injective f.injective, h, comapDomain_embDomain]

Premises used: Finsupp.comapDomain_embDomain, Function.Embedding.injective, Finsupp.comapDomain_add_of_injective
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
⊢ Membership.mem (γ := Set (β →₀ ℕ)) (Set.range (embDomain f)) (embDomain f y)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
h₁ h₂ : u = u
⊢ embDomain f (comapDomain (⇑f : (a : α) → β) u ⋯) = u

Tactic:
rw [embDomain_comapDomain ((mem_range_embDomain_iff ..).mp
      (isLowerSet_range_embDomain f (le_iff_exists_add.mpr ⟨v, h.symm⟩) (by simp)))]

Premises used: Iff.mpr, le_iff_exists_add, Finsupp.mem_range_embDomain_iff, Finsupp.isLowerSet_range_embDomain, Finsupp.embDomain_comapDomain, Exists.intro, Iff.mp, Eq.symm
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
h₁ h₂ : v = v
⊢ embDomain f (comapDomain (⇑f : (a : α) → β) v ⋯) = v

Tactic:
rw [embDomain_comapDomain ((mem_range_embDomain_iff ..).mp
      (isLowerSet_range_embDomain f (le_iff_exists_add'.mpr ⟨u, h.symm⟩) (by simp)))]

Premises used: Iff.mpr, Finsupp.mem_range_embDomain_iff, Finsupp.isLowerSet_range_embDomain, Finsupp.embDomain_comapDomain, Exists.intro, Iff.mp, le_iff_exists_add', Eq.symm
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
h :
  ∀ (u v : α ⊕ β →₀ ℕ),
    Membership.mem (γ := Finset ((α ⊕ β →₀ ℕ) × (α ⊕ β →₀ ℕ)))
        (image
          (fun (x : Prod.{u, u_1} ((α →₀ ℕ) × (α →₀ ℕ)) ((β →₀ ℕ) × (β →₀ ℕ))) ↦
            match (motive := Prod.{u, u_1} ((α →₀ ℕ) × (α →₀ ℕ)) ((β →₀ ℕ) × (β →₀ ℕ)) → (α ⊕ β →₀ ℕ) × (α ⊕ β →₀ ℕ))
              x with
            | ((x, y), z, w) => (x.sumElim z, y.sumElim w))
          (@antidiagonal _ instAddMonoid _ x ×ˢ @antidiagonal _ instAddMonoid _ y))
        (u, v) ↔
      (u, v) ∈ @antidiagonal _ instAddMonoid _ (x.sumElim y)
⊢ image
      (fun (x : Prod.{u, u_1} ((α →₀ ℕ) × (α →₀ ℕ)) ((β →₀ ℕ) × (β →₀ ℕ))) ↦
        match (motive := Prod.{u, u_1} ((α →₀ ℕ) × (α →₀ ℕ)) ((β →₀ ℕ) × (β →₀ ℕ)) → (α ⊕ β →₀ ℕ) × (α ⊕ β →₀ ℕ)) x with
        | ((x, y), z, w) => (x.sumElim z, y.sumElim w))
      (@antidiagonal _ instAddMonoid _ x ×ˢ @antidiagonal _ instAddMonoid _ y) =
    @antidiagonal _ instAddMonoid _ (x.sumElim y)

Tactic:
ext ⟨u, v⟩
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h :
  (∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
      (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v) ↔
    u + v = x.sumElim y
⊢ Membership.mem (γ := Finset ((α ⊕ β →₀ ℕ) × (α ⊕ β →₀ ℕ)))
      (image
        (fun (x : Prod.{u, u_1} ((α →₀ ℕ) × (α →₀ ℕ)) ((β →₀ ℕ) × (β →₀ ℕ))) ↦
          match (motive := Prod.{u, u_1} ((α →₀ ℕ) × (α →₀ ℕ)) ((β →₀ ℕ) × (β →₀ ℕ)) → (α ⊕ β →₀ ℕ) × (α ⊕ β →₀ ℕ))
            x with
          | ((x, y), z, w) => (x.sumElim z, y.sumElim w))
        (@antidiagonal _ instAddMonoid _ x ×ˢ @antidiagonal _ instAddMonoid _ y))
      (u, v) ↔
    (u, v) ∈ @antidiagonal _ instAddMonoid _ (x.sumElim y)

Tactic:
simp only [mem_antidiagonal, mem_image, mem_product, Prod.mk.injEq, Prod.exists]

Premises used: Finset.mem_image, Finset.HasAntidiagonal.mem_antidiagonal, Prod.mk.injEq, Prod.exists, Finset.mem_product
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
⊢ (∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
      (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v) ↔
    u + v = x.sumElim y

Tactic:
⟨fun ⟨a, b, a', b', h1, h2, h3⟩ ↦ ?_, fun h ↦
    ⟨u.comapDomain Sum.inl Sum.inl_injective.injOn, v.comapDomain Sum.inl Sum.inl_injective.injOn,
    u.comapDomain Sum.inr Sum.inr_injective.injOn, v.comapDomain Sum.inr Sum.inr_injective.injOn,
    ⟨?_, ?_⟩, comapDomain_sumElim_comapDomain .., comapDomain_sumElim_comapDomain ..⟩⟩

Premises used: Sum.inr_injective, Function.Injective.injOn, Sum.inl_injective, Sum.inl, HAdd.hAdd, Finsupp.comapDomain_sumElim_comapDomain, Sum.inr, And.intro, Iff.intro, Exists.intro, _private.0.Finsupp.image_sumElim_product_antidiagonal.match_2, Finsupp.comapDomain, Finsupp.sumElim, Eq
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h :
  (∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
      (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v) →
    ∀ (a b : α →₀ ℕ) (a' b' : β →₀ ℕ) (h1 : a + b = x ∧ a' + b' = y) (h2 : a.sumElim a' = u) (h3 : b.sumElim b' = v),
      u + v = x.sumElim y
h₁ : ∀ (h : u + v = x.sumElim y), comapDomain Sum.inl u ⋯ + comapDomain Sum.inl v ⋯ = x
h₂ : ∀ (h : u + v = x.sumElim y), comapDomain Sum.inr u ⋯ + comapDomain Sum.inr v ⋯ = y
⊢ (∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
      (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v) ↔
    u + v = x.sumElim y

Tactic:
refine ⟨fun ⟨a, b, a', b', h1, h2, h3⟩ ↦ ?_, fun h ↦
    ⟨u.comapDomain Sum.inl Sum.inl_injective.injOn, v.comapDomain Sum.inl Sum.inl_injective.injOn,
    u.comapDomain Sum.inr Sum.inr_injective.injOn, v.comapDomain Sum.inr Sum.inr_injective.injOn,
    ⟨?_, ?_⟩, comapDomain_sumElim_comapDomain .., comapDomain_sumElim_comapDomain ..⟩⟩
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h_1 :
  ∃ (a : α →₀ ℕ) (b : α →₀ ℕ) (a_1 : β →₀ ℕ) (b_1 : β →₀ ℕ),
    (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v
a b : α →₀ ℕ
a' b' : β →₀ ℕ
h1 : a + b = x ∧ a' + b' = y
h2 : a.sumElim a' = u
h3 : b.sumElim b' = v
h : a.sumElim a' + v = x.sumElim y
h₁ : a.sumElim a' + b.sumElim b' = x.sumElim y
h₂ : (a + b).sumElim (a' + b') = x.sumElim y
h₃ : x.sumElim (a' + b') = x.sumElim y
h₄ h₅ : x.sumElim y = x.sumElim y
⊢ u + v = x.sumElim y

Tactic:
rw [← h2, ← h3, ← sumElim_add, h1.left, h1.right]

Premises used: And.right, And.left, Finsupp.sumElim_add
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
h₁ : comapDomain Sum.inl (u + v) ⋯ = x
h₂ : comapDomain Sum.inl (x.sumElim y) ⋯ = x
h₃ h₄ : x = x
⊢ comapDomain Sum.inl u ⋯ + comapDomain Sum.inl v ⋯ = x

Tactic:
rw [← comapDomain_add_of_injective Sum.inl_injective, h, comapDomain_inl_sumElim]

Premises used: Finsupp.comapDomain_inl_sumElim, Sum.inl_injective, Finsupp.comapDomain_add_of_injective
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
h₁ : comapDomain Sum.inr (u + v) ⋯ = y
h₂ : comapDomain Sum.inr (x.sumElim y) ⋯ = y
h₃ h₄ : y = y
⊢ comapDomain Sum.inr u ⋯ + comapDomain Sum.inr v ⋯ = y

Tactic:
rw [← comapDomain_add_of_injective Sum.inr_injective, h, comapDomain_inr_sumElim]

Premises used: Sum.inr_injective, Finsupp.comapDomain_add_of_injective, Finsupp.comapDomain_inr_sumElim
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
m : M
f : α →₀ M
simp_rw :
  (∃ (a_1 : α),
      Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a_1 : M) (0 : M) ∧
        ({ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M) a_1 = (a, m)) ↔
    (f : (a : α) → M) a = m ∧ m ≠ 0
⊢ (a, m) ∈ f.graph ↔ (f : (a : α) → M) a = m ∧ m ≠ 0

Tactic:
simp_rw [graph, mem_map, mem_support_iff]

Premises used: Finsupp.mem_support_iff, Finsupp.graph, Finset.mem_map
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
m : M
f : α →₀ M
mp :
  (∃ (a_1 : α),
      Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a_1 : M) (0 : M) ∧
        ({ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M) a_1 = (a, m)) →
    (f : (a : α) → M) a = m ∧ m ≠ 0
mpr :
  (f : (a : α) → M) a = m ∧ m ≠ 0 →
    ∃ (a_2 : α),
      Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a_2 : M) (0 : M) ∧
        ({ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M) a_2 = (a, m)
⊢ (∃ (a_1 : α),
      Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a_1 : M) (0 : M) ∧
        ({ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M) a_1 = (a, m)) ↔
    (f : (a : α) → M) a = m ∧ m ≠ 0

Tactic:
constructor
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
f : α →₀ M
ha : Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) ((f : (a : α) → M) a : M) ∧
    Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)

Tactic:
⟨rfl, ha⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
f : α →₀ M
ha : Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) ((f : (a : α) → M) a : M) ∧
    Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)

Tactic:
exact ⟨rfl, ha⟩
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
f : α →₀ M
ha : Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ ∃ (a_1 : α),
    Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a_1 : M) (0 : M) ∧
      Eq (α := α × M)
        (({ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M) a_1 : α × M)
        ((a, (f : (a : α) → M) a) : α × M)

Tactic:
⟨a, ha, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
f : α →₀ M
ha : Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ ∃ (a_1 : α),
    Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a_1 : M) (0 : M) ∧
      Eq (α := α × M)
        (({ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M) a_1 : α × M)
        ((a, (f : (a : α) → M) a) : α × M)

Tactic:
exact ⟨a, ha, rfl⟩
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
c : α × M
f : α →₀ M
mk : ∀ (fst : α) (snd : M), (fst, snd) ∈ f.graph ↔ (f : (a : α) → M) (fst, snd).1 = (fst, snd).2 ∧ (fst, snd).2 ≠ 0
⊢ c ∈ f.graph ↔ (f : (a : α) → M) c.1 = c.2 ∧ c.2 ≠ 0

Tactic:
cases c
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
fst : α
snd : M
⊢ (fst, snd) ∈ f.graph ↔ (f : (a : α) → M) (fst, snd).1 = (fst, snd).2 ∧ (fst, snd).2 ≠ 0

Tactic:
mk_mem_graph_iff

Premises used: Finsupp.mk_mem_graph_iff
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
fst : α
snd : M
⊢ (fst, snd) ∈ f.graph ↔ (f : (a : α) → M) (fst, snd).1 = (fst, snd).2 ∧ (fst, snd).2 ≠ 0

Tactic:
exact mk_mem_graph_iff

Premises used: Finsupp.mk_mem_graph_iff
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
a : α
ha : a ∈ f.support
⊢ Membership.mem (α := α × M) f.graph ((a, (f : (a : α) → M) a) : α × M)

Tactic:
mk_mem_graph_iff.2 ⟨rfl, mem_support_iff.1 ha⟩

Premises used: Iff.mpr, Finsupp.mem_support_iff, Finsupp.mk_mem_graph_iff, And.intro, Iff.mp, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
m : M
f : α →₀ M
h : (a, m) ∈ f.graph
⊢ (f : (a : α) → M) a = m

Tactic:
(mem_graph_iff.1 h).1

Premises used: And.left, Iff.mp, Finsupp.mem_graph_iff
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
f : α →₀ M
⊢ (a, 0) ∉ f.graph

Tactic:
fun h =>
  (mem_graph_iff.1 h).2.irrefl

Premises used: Ne.irrefl, And.right, Iff.mp, Finsupp.mem_graph_iff, Not
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
simp_rw :
  image Prod.fst (map { toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } f.support) = f.support
simp_rw₁ :
  image (α := α × M) Prod.fst
      (image (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M)
        f.support) =
    f.support
simp_rw₂ :
  image
      (comp (β := α × M) Prod.fst
        (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M))
      f.support =
    f.support
simp_rw₃ : image (comp (β := α × M) Prod.fst fun (a : α) ↦ (a, (f : (a : α) → M) a)) f.support = f.support
simp_rw₄ : image (fun (x : α) ↦ x) f.support = f.support
⊢ image Prod.fst f.graph = f.support

Tactic:
simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']

Premises used: Function.comp_def, Finset.image_id', Finset.map_eq_image, Finsupp.graph, Function.Embedding.coeFn_mk, Finset.image_image
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
simp_rw :
  image Prod.fst (map { toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } f.support) = f.support
simp_rw₁ :
  image (α := α × M) Prod.fst
      (image (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M)
        f.support) =
    f.support
simp_rw₂ :
  image
      (comp (β := α × M) Prod.fst
        (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M))
      f.support =
    f.support
simp_rw₃ : image (comp (β := α × M) Prod.fst fun (a : α) ↦ (a, (f : (a : α) → M) a)) f.support = f.support
simp_rw₄ : image (fun (x : α) ↦ x) f.support = f.support
⊢ image Prod.fst f.graph = f.support

Tactic:
classical
  simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']

Premises used: Function.comp_def, Finset.image_id', Finset.map_eq_image, Finsupp.graph, Function.Embedding.coeFn_mk, Finset.image_image
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
rw : image Prod.fst f.graph = g.support
rw₁ : image Prod.fst g.graph = g.support
rw₂ rw₃ : g.support = g.support
⊢ f.support = g.support

Tactic:
rw [← image_fst_graph, h, image_fst_graph]

Premises used: Finsupp.image_fst_graph
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ f.support = g.support

Tactic:
have hsup : f.support = g.support := by rw [← image_fst_graph, h, image_fst_graph]
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
hsup : f.support = g.support
⊢ f = g

Tactic:
ext_iff'.2 ⟨hsup, fun x hx => apply_eq_of_mem_graph <| h.symm ▸ ?_⟩

Premises used: Iff.mpr, Finsupp.ext_iff', Eq.rec, And.intro, Eq.symm, Finsupp.apply_eq_of_mem_graph
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
hsup : f.support = g.support
refine : ∀ (x : α) (hx : x ∈ f.support), Membership.mem (α := α × M) g.graph ((x, (g : (a : α) → M) x) : α × M)
⊢ f = g

Tactic:
refine ext_iff'.2 ⟨hsup, fun x hx => apply_eq_of_mem_graph <| h.symm ▸ ?_⟩

Premises used: Iff.mpr, Finsupp.ext_iff', Eq.rec, And.intro, Eq.symm, Finsupp.apply_eq_of_mem_graph
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
hsup : f.support = g.support
x : α
hx : x ∈ f.support
⊢ Membership.mem (α := α × M) g.graph ((x, (g : (a : α) → M) x) : α × M)

Tactic:
mk_mem_graph _ (hsup ▸ hx)

Premises used: Eq.rec, Finsupp.mk_mem_graph
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
hsup : f.support = g.support
x : α
hx : x ∈ f.support
⊢ Membership.mem (α := α × M) g.graph ((x, (g : (a : α) → M) x) : α × M)

Tactic:
exact mk_mem_graph _ (hsup ▸ hx)

Premises used: Finsupp.mk_mem_graph
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
have : f.support = g.support
have₁ : ∀ (hsup : f.support = g.support), f = g
have₂ : f.support = g.support
have₃ have₄ : ∀ (hsup : f.support = g.support), f = g
have₅ :
  ∀ (hsup : f.support = g.support) (x : α) (hx : x ∈ f.support),
    Membership.mem (α := α × M) g.graph ((x, (g : (a : α) → M) x) : α × M)
⊢ f = g

Tactic:
classical
    have hsup : f.support = g.support := by rw [← image_fst_graph, h, image_fst_graph]
    refine ext_iff'.2 ⟨hsup, fun x hx => apply_eq_of_mem_graph <| h.symm ▸ ?_⟩
    exact mk_mem_graph _ (hsup ▸ hx)

Premises used: Finsupp.mk_mem_graph
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f g : α →₀ M
⊢ f.graph = g.graph ↔ f = g

Tactic:
(graph_injective α M).eq_iff

Premises used: Function.Injective.eq_iff, Finsupp.graph_injective
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
⊢ Eq (α := Finset (α × M)) (graph 0) ∅

Tactic:
simp [graph]

Premises used: Finsupp.graph
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
f : α →₀ M
⊢ f.graph = ∅ ↔ f = 0

Tactic:
(graph_injective α M).eq_iff' graph_zero

Premises used: Function.Injective.eq_iff', Finsupp.graph_zero, Finsupp.graph_injective
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
N : Type u_6
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
F : Type u_12
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
m : Multiset (α →₀ M)
⊢ Eq (α := α →₀ N) (mapRange (⇑f : (a : M) → N) ⋯ m.sum)
    (Multiset.sum (Multiset.map (fun (x : α →₀ M) ↦ mapRange (⇑f : (a : M) → N) ⋯ x) m))

Tactic:
(mapRange.addMonoidHom (f : M →+ N) : (α →₀ _) →+ _).map_multiset_sum _

Premises used: Finsupp.mapRange.addMonoidHom, AddMonoidHomClass.toAddMonoidHom, Finsupp.onFinset, AddMonoidHom.map_multiset_sum, Finsupp.mapRange
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_4
M : Type u_5
N : Type u_6
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
F : Type u_12
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
s : Finset ι
g : ι → α →₀ M
⊢ Eq (α := α →₀ N) (mapRange (⇑f : (a : M) → N) ⋯ (∑ x ∈ s, g x)) (∑ x ∈ s, mapRange (⇑f : (a : M) → N) ⋯ (g x))

Tactic:
map_sum (mapRange.addMonoidHom (f : M →+ N)) _ _

Premises used: Finsupp.mapRange.addMonoidHom, AddMonoidHomClass.toAddMonoidHom, map_sum, Finsupp.onFinset, Finsupp.mapRange
-- 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
a : β
simp :
  l.toFun ((f.symm : (a : β) → α) a) ≠ 0 ↔
    Ne.{u_5 + 1} (α := M) ((l : (a : α) → M) ((f.symm : (a : β) → α) a : α) : M) (0 : M)
⊢ a ∈ map f.toEmbedding l.support ↔ Ne.{u_5 + 1} (α := M) ((l : (a : α) → M) ((f.symm : (a : β) → α) a : α) : M) (0 : M)

Tactic:
simp only [Finset.mem_map_equiv, mem_support_toFun]

Premises used: Finset.mem_map_equiv, 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
a : β
⊢ l.toFun ((f.symm : (a : β) → α) a) ≠ 0 ↔
    Ne.{u_5 + 1} (α := M) ((l : (a : α) → M) ((f.symm : (a : β) → α) a : α) : M) (0 : M)

Tactic:
rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ≃ β
l : α →₀ M
b : β
⊢ Eq.{u_5 + 1} (α := M) ((equivMapDomain f l : (a : β) → M) b : M)
    ((l : (a : α) → M) ((f.symm : (a : β) → α) b : α) : M)

Tactic:
rfl

Premises used: rfl
-- 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) ((equivMapDomain f.symm l : (a : α) → M) a : M)
    ((l : (a : β) → M) ((f : (a : α) → β) a : β) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
l : α →₀ M
h : ∀ (x : α), Eq.{u_5 + 1} (α := M) ((equivMapDomain (Equiv.refl α) l : (a : α) → M) x : M) ((l : (a : α) → M) x : M)
⊢ equivMapDomain (Equiv.refl α) l = l

Tactic:
ext x
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
l : α →₀ M
x : α
⊢ Eq.{u_5 + 1} (α := M) ((equivMapDomain (Equiv.refl α) l : (a : α) → M) x : M) ((l : (a : α) → M) x : M)

Tactic:
rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
h :
  ∀ (x : α →₀ M) (a : α),
    Eq.{u_5 + 1} (α := M) ((equivMapDomain (Equiv.refl α) x : (a : α) → M) a : M) ((id x : (a : α) → M) a : M)
⊢ Eq (α := (l : α →₀ M) → α →₀ M) (equivMapDomain (Equiv.refl α)) id

Tactic:
ext x
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
x : α →₀ M
a : α
⊢ Eq.{u_5 + 1} (α := M) ((equivMapDomain (Equiv.refl α) x : (a : α) → M) a : M) ((id x : (a : α) → M) a : M)

Tactic:
rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : Zero M
f : α ≃ β
g : β ≃ γ
l : α →₀ M
h :
  ∀ (x : γ),
    Eq.{u_5 + 1} (α := M) ((equivMapDomain (f.trans g) l : (a : γ) → M) x : M)
      ((equivMapDomain g (equivMapDomain f l) : (a : γ) → M) x : M)
⊢ equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l)

Tactic:
ext x