awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
simp_rw :
  a ∈
      (filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
            (l.entries (β := fun (_x : α) ↦ M))).keys
        (β := fun (_x : α) ↦ M) ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
simp_rw₁ :
  (∃ (b : M),
      Sigma.mk (β := fun (_x : α) ↦ M) a b ∈
        filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
          (l.entries (β := fun (_x : α) ↦ M))) ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
simp_rw₂ :
  (∃ (b : M), Sigma.mk (β := fun (_x : α) ↦ M) a b ∈ l.entries (β := fun (_x : α) ↦ M) ∧ decide (b ≠ 0) = true) ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
simp_rw₃ :
  (∃ b ∈ lookup (β := fun (_x : α) ↦ M) a l, decide (b ≠ 0) = true) ↔ (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
⊢ a ∈
      (filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
              (l.entries (β := fun (_x : α) ↦ M))).keys
          (β := fun (_x : α) ↦ M).toFinset ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0

Tactic:
classical
      simp_rw [mem_toFinset, List.mem_keys, List.mem_filter, ← mem_lookup_iff]
      cases lookup a l <;> simp

Premises used: List.mem_toFinset, List.mem_filter, List.mem_keys, AList.mem_lookup_iff
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
simp : (lookup (β := fun (_x : α) ↦ M) a l).getD 0 = (lookup (β := fun (_x : α) ↦ M) a l).getD 0
⊢ (l.lookupFinsupp : (a : α) → M) a = (lookup (β := fun (_x : α) ↦ M) a l).getD 0

Tactic:
simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]

Premises used: AList.lookupFinsupp, ne_eq, Finsupp.coe_mk
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
⊢ (lookup (β := fun (_x : α) ↦ M) a l).getD 0 = (lookup (β := fun (_x : α) ↦ M) a l).getD 0

Tactic:
congr
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
inst_2 : DecidableEq M
l : AList.{u_1, u_2} fun (_x : α) ↦ M
⊢ (filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0)) (l.entries (β := fun (_x : α) ↦ M))).keys
        (β := fun (_x : α) ↦ M).toFinset =
    (filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
            (l.entries (β := fun (_x : α) ↦ M))).keys
        (β := fun (_x : α) ↦ M).toFinset

Tactic:
congr!
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
x : M
hx : x ≠ 0
rw : (lookup (β := fun (_x : α) ↦ M) a l).getD 0 = x ↔ x ∈ lookup (β := fun (_x : α) ↦ M) a l
⊢ (l.lookupFinsupp : (a : α) → M) a = x ↔ x ∈ lookup (β := fun (_x : α) ↦ M) a l

Tactic:
rw [lookupFinsupp_apply]

Premises used: AList.lookupFinsupp_apply
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
x : M
hx : x ≠ 0
none : Option.getD Option.none 0 = x ↔ Membership.mem (γ := Option M) Option.none x
some : ∀ (m : M), (Option.some m).getD 0 = x ↔ x ∈ Option.some m
⊢ (lookup (β := fun (_x : α) ↦ M) a l).getD 0 = x ↔ x ∈ lookup (β := fun (_x : α) ↦ M) a l

Tactic:
rcases lookup a l with - | m

Premises used: AList.lookup
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
x : M
hx : x ≠ 0
⊢ Option.getD none 0 = x ↔ Membership.mem (γ := Option M) none x

Tactic:
simp [hx.symm]

Premises used: Ne.symm
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
x : M
hx : x ≠ 0
m : M
⊢ (some m).getD 0 = x ↔ x ∈ some m

Tactic:
simp [hx.symm]

Premises used: Ne.symm
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
rw :
  (lookup (β := fun (_x : α) ↦ M) a l).getD 0 = 0 ↔
    lookup (β := fun (_x : α) ↦ M) a l = none ∨ 0 ∈ lookup (β := fun (_x : α) ↦ M) a l
⊢ Eq.{u_2 + 1} (α := M) ((l.lookupFinsupp : (a : α) → M) a : M) (0 : M) ↔ a ∉ l ∨ 0 ∈ lookup (β := fun (_x : α) ↦ M) a l

Tactic:
rw [lookupFinsupp_apply, ← lookup_eq_none]

Premises used: AList.lookupFinsupp_apply, AList.lookup_eq_none
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
none :
  Eq.{u_2 + 1} (α := M) (Option.getD Option.none 0) 0 ↔
    Eq.{u_2 + 1} (α := Option M) Option.none Option.none ∨ Membership.mem (γ := Option M) Option.none 0
some : ∀ (m : M), (Option.some m).getD 0 = 0 ↔ Option.some m = Option.none ∨ 0 ∈ Option.some m
⊢ (lookup (β := fun (_x : α) ↦ M) a l).getD 0 = 0 ↔
    lookup (β := fun (_x : α) ↦ M) a l = Option.none ∨ 0 ∈ lookup (β := fun (_x : α) ↦ M) a l

Tactic:
rcases lookup a l with - | m

Premises used: AList.lookup
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
⊢ Eq.{u_2 + 1} (α := M) (Option.getD none 0) 0 ↔
    Eq.{u_2 + 1} (α := Option M) none none ∨ Membership.mem (γ := Option M) none 0

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
m : M
⊢ (some m).getD 0 = 0 ↔ some m = none ∨ 0 ∈ some m

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
⊢ Eq (α := α →₀ M) (lookupFinsupp ∅) 0

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, Option.getD, List.dedup, Multiset.zero, AList.lookupFinsupp, Finset.empty, List.toFinset, Multiset.ofList, List.pwFilter, List.foldr, rfl
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
m : M
h :
  ∀ (b : α),
    Eq.{u_2 + 1} (α := M) (((insert (β := fun (_x : α) ↦ M) a m l).lookupFinsupp : (a : α) → M) b : M)
      ((Finsupp.update l.lookupFinsupp a m : (a : α) → M) b : M)
⊢ Eq (α := α →₀ M) (insert (β := fun (_x : α) ↦ M) a m l).lookupFinsupp (Finsupp.update l.lookupFinsupp a m)

Tactic:
ext b
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
m : M
b : α
pos :
  ∀ (h : b = a),
    Eq.{u_2 + 1} (α := M) (((insert (β := fun (_x : α) ↦ M) a m l).lookupFinsupp : (a : α) → M) b : M)
      ((Finsupp.update l.lookupFinsupp a m : (a : α) → M) b : M)
neg :
  ∀ (h : ¬b = a),
    Eq.{u_2 + 1} (α := M) (((insert (β := fun (_x : α) ↦ M) a m l).lookupFinsupp : (a : α) → M) b : M)
      ((Finsupp.update l.lookupFinsupp a m : (a : α) → M) b : M)
⊢ Eq.{u_2 + 1} (α := M) (((insert (β := fun (_x : α) ↦ M) a m l).lookupFinsupp : (a : α) → M) b : M)
    ((Finsupp.update l.lookupFinsupp a m : (a : α) → M) b : M)

Tactic:
by_cases h : b = a
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
m : M
b : α
h : b = a
⊢ Eq.{u_2 + 1} (α := M) (((insert (β := fun (_x : α) ↦ M) a m l).lookupFinsupp : (a : α) → M) b : M)
    ((Finsupp.update l.lookupFinsupp a m : (a : α) → M) b : M)

Tactic:
simp [h]
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
m : M
b : α
h : ¬b = a
⊢ Eq.{u_2 + 1} (α := M) (((insert (β := fun (_x : α) ↦ M) a m l).lookupFinsupp : (a : α) → M) b : M)
    ((Finsupp.update l.lookupFinsupp a m : (a : α) → M) b : M)

Tactic:
simp [h]
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
a : α
m : M
⊢ Eq (α := α →₀ M) (lookupFinsupp (singleton (β := fun (_x : α) ↦ M) a m)) (Finsupp.single a m)

Tactic:
simp [← AList.insert_empty]

Premises used: AList.insert_empty
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
a : α
m : M
⊢ Eq (α := α →₀ M) (lookupFinsupp (singleton (β := fun (_x : α) ↦ M) a m)) (Finsupp.single a m)

Tactic:
classical
  simp [← AList.insert_empty]

Premises used: AList.insert_empty
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
h : ∀ (a : α), Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
⊢ f.toAList.lookupFinsupp = f

Tactic:
ext a
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
pos :
  ∀ (h : Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
    Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
neg :
  ∀ (h : ¬Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
    Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
⊢ Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)

Tactic:
by_cases h : f a = 0

Premises used: DFunLike.coe
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
h : Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
this : lookup (β := fun (_x : α) ↦ M) a f.toAList = none
⊢ Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)

Tactic:
simp [h, this]
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
h : Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
pos : lookup (β := fun (_x : α) ↦ M) a f.toAList = none
⊢ Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)

Tactic:
suffices f.toAList.lookup a = none by simp [h, this]
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
h : Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ lookup (β := fun (_x : α) ↦ M) a f.toAList = none

Tactic:
simp [lookup_eq_none, h]

Premises used: AList.lookup_eq_none
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
h : ¬Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
this : lookup (β := fun (_x : α) ↦ M) a f.toAList = some ((f : (a : α) → M) a)
⊢ Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)

Tactic:
simp [this]
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
h : ¬Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
neg : lookup (β := fun (_x : α) ↦ M) a f.toAList = some ((f : (a : α) → M) a)
⊢ Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)

Tactic:
suffices f.toAList.lookup a = some (f a) by simp [this]
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
h : ¬Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
neg : Sigma.mk (β := fun (_x : α) ↦ M) a ((f : (a : α) → M) a) ∈ f.toAList.entries (β := fun (_x : α) ↦ M)
⊢ lookup (β := fun (_x : α) ↦ M) a f.toAList = some ((f : (a : α) → M) a)

Tactic:
apply mem_lookup_iff.2

Premises used: Iff.mpr, AList.mem_lookup_iff
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
h : ¬Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ Sigma.mk (β := fun (_x : α) ↦ M) a ((f : (a : α) → M) a) ∈ f.toAList.entries (β := fun (_x : α) ↦ M)

Tactic:
simpa using h
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
pos :
  ∀ (h : Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
    Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
neg neg₁ :
  ∀ (h : ¬Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
    Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
⊢ Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)

Tactic:
classical
    by_cases h : f a = 0
    · suffices f.toAList.lookup a = none by simp [h, this]
      simp [lookup_eq_none, h]
    · suffices f.toAList.lookup a = some (f a) by simp [this]
      apply mem_lookup_iff.2
      simpa using h

Premises used: Iff.mpr, DFunLike.coe, AList.mem_lookup_iff, AList.lookup_eq_none
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
⊢ Function.Surjective (α := AList.{u_1, u_2} fun (_x : α) ↦ M) (β := α →₀ M) lookupFinsupp

Tactic:
fun f =>
  ⟨_, Finsupp.toAList_lookupFinsupp f⟩

Premises used: Finsupp.toAList, Exists.intro, Finsupp.toAList_lookupFinsupp, Function.Surjective
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
f : α →₀ ℕ
p : (α →₀ ℕ) × (α →₀ ℕ)
rcases : ∀ (p₁ p₂ : α →₀ ℕ), (p₁, p₂) ∈ f.antidiagonal'.support ↔ (p₁, p₂).1 + (p₁, p₂).2 = f
⊢ p ∈ f.antidiagonal'.support ↔ p.1 + p.2 = f

Tactic:
rcases p with ⟨p₁, p₂⟩
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
⊢ Eq (α := Finset ((α →₀ ℕ) × (α →₀ ℕ))) (@antidiagonal _ instAddMonoid _ 0) {(0, 0)}

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, List.dedup, Multiset.count, Multiset.cons, Multiset.zero, Prod.map, Finset.empty, List.countP.go, Multiset.ofList, List.pwFilter, Multiset.countP, List.foldr, rfl, ite
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
M : Type u_1
inst_1 : CommMonoid M
n : α →₀ ℕ
f : (α →₀ ℕ) → (α →₀ ℕ) → M
⊢ ∀ (i : (α →₀ ℕ) × (α →₀ ℕ)),
    i ∈ @antidiagonal _ instAddMonoid _ n ↔
      Membership.mem (α := (α →₀ ℕ) × (α →₀ ℕ)) (@antidiagonal _ instAddMonoid _ n)
        ((Equiv.prodComm (α →₀ ℕ) (α →₀ ℕ) : (a : (α →₀ ℕ) × (α →₀ ℕ)) → (α →₀ ℕ) × (α →₀ ℕ)) i : (α →₀ ℕ) × (α →₀ ℕ))

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
M : Type u_1
inst_1 : CommMonoid M
n : α →₀ ℕ
f : (α →₀ ℕ) → (α →₀ ℕ) → M
⊢ ∀ i ∈ @antidiagonal _ instAddMonoid _ n,
    f i.1 i.2 =
      f ((Equiv.prodComm (α →₀ ℕ) (α →₀ ℕ) : (a : (α →₀ ℕ) × (α →₀ ℕ)) → (α →₀ ℕ) × (α →₀ ℕ)) i).2
        ((Equiv.prodComm (α →₀ ℕ) (α →₀ ℕ) : (a : (α →₀ ℕ) × (α →₀ ℕ)) → (α →₀ ℕ) × (α →₀ ℕ)) i).1

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
h :
  ∀ (x y : α →₀ ℕ),
    Membership.mem (γ := Finset ((α →₀ ℕ) × (α →₀ ℕ))) (@antidiagonal _ instAddMonoid _ (single a n)) (x, y) ↔
      Membership.mem (γ := Finset ((α →₀ ℕ) × (α →₀ ℕ)))
        (map (Function.Embedding.prodMap { toFun := single a, inj' := ⋯ } { toFun := single a, inj' := ⋯ })
          (@antidiagonal _ Nat.instAddMonoid _ n))
        (x, y)
⊢ Eq (α := Finset ((α →₀ ℕ) × (α →₀ ℕ))) (@antidiagonal _ instAddMonoid _ (single a n))
    (map (Function.Embedding.prodMap { toFun := single a, inj' := ⋯ } { toFun := single a, inj' := ⋯ })
      (@antidiagonal _ Nat.instAddMonoid _ n))

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n ↔ ∃ (a_1 : ℕ) (b : ℕ), a_1 + b = n ∧ single a a_1 = x ∧ single a b = y
⊢ Membership.mem (γ := Finset ((α →₀ ℕ) × (α →₀ ℕ))) (@antidiagonal _ instAddMonoid _ (single a n)) (x, y) ↔
    Membership.mem (γ := Finset ((α →₀ ℕ) × (α →₀ ℕ)))
      (map (Function.Embedding.prodMap { toFun := single a, inj' := ⋯ } { toFun := single a, inj' := ⋯ })
        (@antidiagonal _ Nat.instAddMonoid _ n))
      (x, y)

Tactic:
simp only [mem_antidiagonal, mem_map, mem_antidiagonal, Function.Embedding.coe_prodMap,
    Function.Embedding.coeFn_mk, Prod.map_apply, Prod.mk.injEq, Prod.exists]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, Prod.mk.injEq, Function.Embedding.coeFn_mk, Prod.map_apply, Function.Embedding.coe_prodMap, Finset.mem_map, Prod.exists
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n → ∃ (a_2 : ℕ) (b : ℕ), a_2 + b = n ∧ single a a_2 = x ∧ single a b = y
h₁ : (∃ (a_1 : ℕ) (b : ℕ), a_1 + b = n ∧ single a a_1 = x ∧ single a b = y) → x + y = single a n
⊢ x + y = single a n ↔ ∃ (a_1 : ℕ) (b : ℕ), a_1 + b = n ∧ single a a_1 = x ∧ single a b = y

Tactic:
constructor
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
⊢ ∃ (a_1 : ℕ) (b : ℕ), a_1 + b = n ∧ single a a_1 = x ∧ single a b = y

Tactic:
⟨x a, y a, DFunLike.congr_fun h a |>.trans single_eq_same, ?_⟩

Premises used: DFunLike.congr_fun, Finsupp.single_eq_same, And.intro, Exists.intro, DFunLike.coe, Eq.trans
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
h₁ : single a ((x : (a : α) → ℕ) a) = x ∧ single a ((y : (a : α) → ℕ) a) = y
⊢ ∃ (a_1 : ℕ) (b : ℕ), a_1 + b = n ∧ single a a_1 = x ∧ single a b = y

Tactic:
refine ⟨x a, y a, DFunLike.congr_fun h a |>.trans single_eq_same, ?_⟩
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
h₁ :
  ∀ (x_1 : α),
    Eq (α := ℕ) (((single a ((x : (a : α) → ℕ) a) : α →₀ ℕ) : (a : α) → ℕ) x_1 : ℕ) ((x : (a : α) → ℕ) x_1 : ℕ) ∧
      Eq (α := ℕ) (((single a ((y : (a : α) → ℕ) a) : α →₀ ℕ) : (a : α) → ℕ) x_1 : ℕ) ((y : (a : α) → ℕ) x_1 : ℕ)
⊢ single a ((x : (a : α) → ℕ) a) = x ∧ single a ((y : (a : α) → ℕ) a) = y

Tactic:
simp_rw [DFunLike.ext_iff, ← forall_and]

Premises used: DFunLike.ext_iff, forall_and
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
i : α
⊢ Eq (α := ℕ) ((x + y : (a : α) → ℕ) i : ℕ) ((single a n : (a : α) → ℕ) i : ℕ)

Tactic:
replace h := DFunLike.congr_fun h i
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : Eq (α := ℕ) ((x + y : (a : α) → ℕ) i : ℕ) ((single a n : (a : α) → ℕ) i : ℕ)
h₁ :
  ∀ (h : HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : α) → ℕ) i : ℕ) ((y : (a : α) → ℕ) i : ℕ) = if a = i then n else 0),
    Eq (α := ℕ) (if a = i then (x : (a : α) → ℕ) a else 0 : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧
      Eq (α := ℕ) (if a = i then (y : (a : α) → ℕ) a else 0 : ℕ) ((y : (a : α) → ℕ) i : ℕ)
⊢ Eq (α := ℕ) (((single a ((x : (a : α) → ℕ) a) : α →₀ ℕ) : (a : α) → ℕ) i : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧
    Eq (α := ℕ) (((single a ((y : (a : α) → ℕ) a) : α →₀ ℕ) : (a : α) → ℕ) i : ℕ) ((y : (a : α) → ℕ) i : ℕ)

Tactic:
simp_rw [single_apply, Finsupp.add_apply] at h ⊢

Premises used: Finsupp.add_apply, Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : α) → ℕ) i : ℕ) ((y : (a : α) → ℕ) i : ℕ) = if a = i then n else 0
h₁ :
  ∀ (h : HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : α) → ℕ) a : ℕ) ((y : (a : α) → ℕ) a : ℕ) = if a = a then n else 0),
    Eq (α := ℕ) (if a = a then (x : (a : α) → ℕ) a else 0 : ℕ) ((x : (a : α) → ℕ) a : ℕ) ∧
      Eq (α := ℕ) (if a = a then (y : (a : α) → ℕ) a else 0 : ℕ) ((y : (a : α) → ℕ) a : ℕ)
h₂ :
  ∀ (hai : a ≠ i),
    Eq (α := ℕ) (if a = i then (x : (a : α) → ℕ) a else 0 : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧
      Eq (α := ℕ) (if a = i then (y : (a : α) → ℕ) a else 0 : ℕ) ((y : (a : α) → ℕ) i : ℕ)
⊢ Eq (α := ℕ) (if a = i then (x : (a : α) → ℕ) a else 0 : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧
    Eq (α := ℕ) (if a = i then (y : (a : α) → ℕ) a else 0 : ℕ) ((y : (a : α) → ℕ) i : ℕ)

Tactic:
obtain rfl | hai := Decidable.eq_or_ne a i

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : α) → ℕ) a : ℕ) ((y : (a : α) → ℕ) a : ℕ) = if a = a then n else 0
⊢ Eq (α := ℕ) (if a = a then (x : (a : α) → ℕ) a else 0 : ℕ) ((x : (a : α) → ℕ) a : ℕ) ∧
    Eq (α := ℕ) (if a = a then (y : (a : α) → ℕ) a else 0 : ℕ) ((y : (a : α) → ℕ) a : ℕ)

Tactic:
⟨if_pos rfl, if_pos rfl⟩

Premises used: if_pos, And.intro, rfl
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : α) → ℕ) a : ℕ) ((y : (a : α) → ℕ) a : ℕ) = if a = a then n else 0
⊢ Eq (α := ℕ) (if a = a then (x : (a : α) → ℕ) a else 0 : ℕ) ((x : (a : α) → ℕ) a : ℕ) ∧
    Eq (α := ℕ) (if a = a then (y : (a : α) → ℕ) a else 0 : ℕ) ((y : (a : α) → ℕ) a : ℕ)

Tactic:
exact ⟨if_pos rfl, if_pos rfl⟩
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : HAdd.hAdd (α := ℕ) (β := ℕ) ((x : (a : α) → ℕ) i : ℕ) ((y : (a : α) → ℕ) i : ℕ) = if a = i then n else 0
hai : a ≠ i
h₁ :
  ∀ (h : Eq (α := ℕ) ((x : (a : α) → ℕ) i : ℕ) (0 : ℕ) ∧ Eq (α := ℕ) ((y : (a : α) → ℕ) i : ℕ) (0 : ℕ)),
    Eq (α := ℕ) (0 : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧ Eq (α := ℕ) (0 : ℕ) ((y : (a : α) → ℕ) i : ℕ)
⊢ Eq (α := ℕ) (if a = i then (x : (a : α) → ℕ) a else 0 : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧
    Eq (α := ℕ) (if a = i then (y : (a : α) → ℕ) a else 0 : ℕ) ((y : (a : α) → ℕ) i : ℕ)

Tactic:
simp_rw [if_neg hai, add_eq_zero] at h ⊢

Premises used: add_eq_zero, if_neg
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
hai : a ≠ i
h : Eq (α := ℕ) ((x : (a : α) → ℕ) i : ℕ) (0 : ℕ) ∧ Eq (α := ℕ) ((y : (a : α) → ℕ) i : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (0 : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧ Eq (α := ℕ) (0 : ℕ) ((y : (a : α) → ℕ) i : ℕ)

Tactic:
h.imp Eq.symm Eq.symm

Premises used: And.imp, Eq.symm
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
hai : a ≠ i
h : Eq (α := ℕ) ((x : (a : α) → ℕ) i : ℕ) (0 : ℕ) ∧ Eq (α := ℕ) ((y : (a : α) → ℕ) i : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (0 : ℕ) ((x : (a : α) → ℕ) i : ℕ) ∧ Eq (α := ℕ) (0 : ℕ) ((y : (a : α) → ℕ) i : ℕ)

Tactic:
exact h.imp Eq.symm Eq.symm

Premises used: And.imp, Eq.symm
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a_1 : α
a b : ℕ
⊢ HAdd.hAdd (α := α →₀ ℕ) (single a_1 a) (single a_1 b) = single a_1 (a + b)

Tactic:
(single_add _ _ _).symm

Premises used: Finsupp.single_add, Eq.symm
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
a_1 : α
a b : ℕ
⊢ HAdd.hAdd (α := α →₀ ℕ) (single a_1 a) (single a_1 b) = single a_1 (a + b)

Tactic:
exact (single_add _ _ _).symm

Premises used: Finsupp.single_add, Eq.symm
-- Module: Mathlib.Data.Finsupp.Antidiagonal
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
h :
  ∀ (u v : β →₀ ℕ),
    (u, v) ∈ image (Prod.map (embDomain f) (embDomain f)) (@antidiagonal _ instAddMonoid _ y) ↔
      (u, v) ∈ @antidiagonal _ instAddMonoid _ (embDomain f y)
⊢ image (Prod.map (embDomain f) (embDomain f)) (@antidiagonal _ instAddMonoid _ y) =
    @antidiagonal _ instAddMonoid _ (embDomain f y)

Tactic:
ext ⟨u, v⟩
-- 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) ↔ u + v = embDomain f y
⊢ (u, v) ∈ image (Prod.map (embDomain f) (embDomain f)) (@antidiagonal _ instAddMonoid _ y) ↔
    (u, v) ∈ @antidiagonal _ instAddMonoid _ (embDomain f y)

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

Premises used: Finset.mem_image, Finset.HasAntidiagonal.mem_antidiagonal, Prod.mk.injEq, Prod.map_apply, Prod.exists