awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
pos :
  ∀ (his : i ∈ s),
    updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
      updateFinset (π := π) x (s ∪ t)
        ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
          (y, z))
        i
neg :
  ∀ (his : i ∉ s),
    updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
      updateFinset (π := π) x (s ∪ t)
        ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
          (y, z))
        i
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i

Tactic:
by_cases his : i ∈ s
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
pos :
  ∀ (hit : i ∈ t),
    updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
      updateFinset (π := π) x (s ∪ t)
        ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
          (y, z))
        i
neg :
  ∀ (hit : i ∉ t),
    updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
      updateFinset (π := π) x (s ∪ t)
        ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
          (y, z))
        i
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i

Tactic:
by_cases hit : i ∈ t
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
pos :
  ∀ (hit : i ∈ t),
    updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
      updateFinset (π := π) x (s ∪ t)
        ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
          (y, z))
        i
neg :
  ∀ (hit : i ∉ t),
    updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
      updateFinset (π := π) x (s ∪ t)
        ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
          (y, z))
        i
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i

Tactic:
by_cases hit : i ∈ t
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∈ t
pos :
  Eq (α := π i) (z (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ⋯) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ⋯) : ι))
    (if h : True ∨ True then
      (piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i ⋯)
    else x i)
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i

Tactic:
simp only [updateFinset, his, hit, dif_pos, dif_neg, Finset.mem_union, false_or, not_false_iff]

Premises used: Function.updateFinset, dif_pos, false_or, dif_neg, Finset.mem_union, not_false_iff
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∉ t
neg :
  Eq (α := π i) (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : ι))
    (if h : True ∨ False then
      (piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i ⋯)
    else x i)
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i

Tactic:
simp only [updateFinset, his, hit, dif_pos, dif_neg, Finset.mem_union, false_or, not_false_iff]

Premises used: Function.updateFinset, dif_pos, false_or, dif_neg, Finset.mem_union, not_false_iff
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
hit : i ∈ t
pos :
  Eq (α := π i) (z (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ⋯) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ⋯) : ι))
    ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
      (y, z) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i ⋯))
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i

Tactic:
simp only [updateFinset, his, hit, dif_pos, dif_neg, Finset.mem_union, false_or, not_false_iff]

Premises used: Function.updateFinset, dif_pos, false_or, dif_neg, Finset.mem_union, not_false_iff
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
hit : i ∉ t
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i

Tactic:
simp only [updateFinset, his, hit, dif_pos, dif_neg, Finset.mem_union, false_or, not_false_iff]

Premises used: Function.updateFinset, dif_pos, false_or, dif_neg, Finset.mem_union, not_false_iff
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∈ t
pos : False
⊢ Eq (α := π i) (z (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ⋯) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ⋯) : ι))
    (if h : True ∨ True then
      (piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i ⋯)
    else x i)

Tactic:
exfalso
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∈ t
⊢ False

Tactic:
Finset.disjoint_left.mp hst his hit

Premises used: Iff.mp, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∈ t
⊢ False

Tactic:
exact Finset.disjoint_left.mp hst his hit

Premises used: Iff.mp, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∉ t
⊢ Eq (α := π i) (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : ι))
    (if h : True ∨ False then
      (piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i ⋯)
    else x i)

Tactic:
piCongrLeft_sumInl (fun b : ↥(s ∪ t) => π b) e y z ⟨i, his⟩ |>.symm

Premises used: Set.Mem, Equiv.trans, setOf, Equiv.setCongr, Equiv.subtypeEquiv, Equiv.piCongrLeft_sumInl, dite, Subtype.mk, Equiv.subtypeEquivProp, Equiv.symm, Eq.symm, Subtype.val, Set
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∉ t
⊢ Eq (α := π i) (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯) : ι))
    (if h : True ∨ False then
      (piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i ⋯)
    else x i)

Tactic:
exact piCongrLeft_sumInl (fun b : ↥(s ∪ t) => π b) e y z ⟨i, his⟩ |>.symm

Premises used: Equiv.piCongrLeft_sumInl, Subtype.mk, Eq.symm, Subtype.val
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
hit : i ∈ t
⊢ Eq (α := π i) (z (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ⋯) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ⋯) : ι))
    ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
      (y, z) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i ⋯))

Tactic:
piCongrLeft_sumInr (fun b : ↥(s ∪ t) => π b) e y z ⟨i, hit⟩ |>.symm

Premises used: Set.Mem, Equiv.trans, setOf, Equiv.setCongr, Equiv.subtypeEquiv, Subtype.mk, Equiv.subtypeEquivProp, Equiv.piCongrLeft_sumInr, Equiv.symm, Eq.symm, Subtype.val, Set
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
hit : i ∈ t
⊢ Eq (α := π i) (z (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ⋯) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ⋯) : ι))
    ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
      (y, z) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i ⋯))

Tactic:
exact piCongrLeft_sumInr (fun b : ↥(s ∪ t) => π b) e y z ⟨i, hit⟩ |>.symm

Premises used: Subtype.mk, Equiv.piCongrLeft_sumInr, Eq.symm, Subtype.val
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
inst : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z = updateFinset (π := π) x t z

Tactic:
grind [updateFinset]

Premises used: Function.updateFinset
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
inst : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : ↥t) → π (↑i : ι)
h : ∀ (i : ↥s), s.restrict (π := π) (updateFinset (π := π) x t y) i = restrict₂ (π := π) hst y i
⊢ s.restrict (π := π) (updateFinset (π := π) x t y) = restrict₂ (π := π) hst y

Tactic:
ext i
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
inst : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : ↥t) → π (↑i : ι)
i : ↥s
⊢ s.restrict (π := π) (updateFinset (π := π) x t y) i = restrict₂ (π := π) hst y i

Tactic:
simp [updateFinset, dif_pos (hst i.2)]

Premises used: Function.updateFinset, dif_pos, Subtype.property
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
inst : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
y : (i : ↥s) → π (↑i : ι)
rw : restrict₂ (π := π) ⋯ y = y
⊢ s.restrict (π := π) (updateFinset (π := π) x s y) = y

Tactic:
rw [restrict_updateFinset_of_subset subset_rfl]

Premises used: Function.restrict_updateFinset_of_subset, subset_rfl
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
inst : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
y : (i : ↥s) → π (↑i : ι)
⊢ restrict₂ (π := π) ⋯ y = y

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
inst : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
h : ∀ (i : ι), updateFinset (π := π) x s (s.restrict (π := π) x) i = x i
⊢ updateFinset (π := π) x s (s.restrict (π := π) x) = x

Tactic:
ext i
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
inst : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
i : ι
⊢ updateFinset (π := π) x s (s.restrict (π := π) x) i = x i

Tactic:
simp [updateFinset]

Premises used: Function.updateFinset
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s : Finset ι
y : (i : ↥s) → π (↑i : ι)
i : ι
z : π i
hi : i ∉ s
rw :
  updateFinset (π := π) (updateFinset (π := π) x s y) {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z) =
    updateFinset (π := π) x (s ∪ {i})
      ((piFinsetUnion π ⋯ :
          (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
        (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z))
rw₁ :
  updateFinset (π := π) x (s ∪ {i})
      ((piFinsetUnion π ⋯ :
          (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
        (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z)) =
    updateFinset (π := π) x (s ∪ {i})
      ((piFinsetUnion π ⋯ :
          (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
        (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z))
rw₂ : Disjoint s {i}
rw₃ :
  updateFinset (π := π) x (s ∪ {i})
      ((piFinsetUnion π ⋯ :
          (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
        (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z)) =
    updateFinset (π := π) x (s ∪ {i})
      ((piFinsetUnion π ⋯ :
          (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
        (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z))
rw₄ : Disjoint s {i}
⊢ update (β := π) (updateFinset (π := π) x s y) i z =
    updateFinset (π := π) x (s ∪ {i})
      ((piFinsetUnion π ⋯ :
          (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
        (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z))

Tactic:
rw [update_eq_updateFinset, updateFinset_updateFinset]

Premises used: Function.update_eq_updateFinset, Function.updateFinset_updateFinset
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
s : Finset ι
y : (i : ↥s) → π (↑i : ι)
i_1 : ι
z : (i : ↥s) → π (↑i : ι)
i : ↥s
⊢ (↑i : ι) ∈ s

Tactic:
i.prop

Premises used: Subtype.prop
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
h : s = t
subst :
  ∀ {z : (i : ↥s) → π (↑i : ι)},
    updateFinset (π := π) x s y =
      updateFinset (π := π) x s fun (i : ↥s) ↦ y (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑i : ι) ⋯)
⊢ updateFinset (π := π) x s y =
    updateFinset (π := π) x t fun (i : ↥t) ↦ y (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑i : ι) ⋯)

Tactic:
subst h
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
s : Finset ι
y z : (i : ↥s) → π (↑i : ι)
⊢ updateFinset (π := π) x s y =
    updateFinset (π := π) x s fun (i : ↥s) ↦ y (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑i : ι) ⋯)

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
inst_1 : Fintype ι
y : (i : ↥univ) → π (↑i : ι)
⊢ updateFinset (π := π) x univ y = fun (i : ι) ↦
    y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯)

Tactic:
simp [updateFinset_def]

Premises used: Function.updateFinset_def
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
inst_1 : Fintype ι
y : (i : ↥univ) → π (↑i : ι)
i : ι
⊢ updateFinset (π := π) x univ y i = y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) univ x) i ⋯)

Tactic:
simp [updateFinset_def]

Premises used: Function.updateFinset_def
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
rw : ∀ x ∈ f.graph.toList, ∀ y ∈ f.graph.toList, x.1 = y.1 → x = y
rw₁ : f.graph.toList.Nodup
⊢ (List.map Prod.toSigma f.graph.toList).NodupKeys (β := fun (_x : α) ↦ M)

Tactic:
rw [List.NodupKeys, List.keys, List.map_map, Prod.fst_comp_toSigma, List.nodup_map_iff_inj_on]

Premises used: Prod.fst_comp_toSigma, List.keys, List.map_map, List.nodup_map_iff_inj_on, List.NodupKeys
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
b : α
m : M
hb : (b, m) ∈ f.graph.toList
n : M
hc : (b, n) ∈ f.graph.toList
rw :
  ∀ (hb : (f : (a : α) → M) (b, m).1 = (b, m).2 ∧ (b, m).2 ≠ 0) (n : M)
    (hc : (f : (a : α) → M) (b, n).1 = (b, n).2 ∧ (b, n).2 ≠ 0), (b, m) = (b, n)
⊢ (b, m) = (b, n)

Tactic:
rw [Finset.mem_toList, Finsupp.mem_graph_iff] at hb hc

Premises used: Finsupp.mem_graph_iff, Finset.mem_toList
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
b : α
m : M
hb : (f : (a : α) → M) b = m ∧ ¬m = 0
n : M
hc : (f : (a : α) → M) b = n ∧ ¬n = 0
rw : (b, m) = (b, (f : (a : α) → M) b)
rw₁ rw₂ : (b, m) = (b, m)
⊢ (b, m) = (b, n)

Tactic:
rw [← hc.1, hb.1]

Premises used: And.left
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
⊢ f.graph.toList.Nodup

Tactic:
apply Finset.nodup_toList

Premises used: Finset.nodup_toList
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
h : ∀ (a : α), a ∈ f.toAList.keys (β := fun (_x : α) ↦ M).toFinset ↔ a ∈ f.support
⊢ f.toAList.keys (β := fun (_x : α) ↦ M).toFinset = f.support

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
a : α
⊢ a ∈ f.toAList.keys (β := fun (_x : α) ↦ M).toFinset ↔ a ∈ f.support

Tactic:
simp [toAList, AList.keys, List.keys]

Premises used: List.keys, Finsupp.toAList, AList.keys
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
x : α
rw : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M) ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
rw₁ : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M).toFinset ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
rw₂ : x ∈ f.support ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
rw₃ rw₄ :
  Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M) ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
⊢ x ∈ f.toAList ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)

Tactic:
rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]

Premises used: List.mem_toFinset, Finsupp.mem_support_iff, AList.mem_keys, Finsupp.toAList_keys_toFinset
-- Module: Mathlib.Data.Finsupp.AList
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
x : α
classical : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M) ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
classical₁ :
  x ∈ f.toAList.keys (β := fun (_x : α) ↦ M).toFinset ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
classical₂ : x ∈ f.support ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
classical₃ classical₄ :
  Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M) ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
⊢ x ∈ f.toAList ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)

Tactic:
classical rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]

Premises used: List.mem_toFinset, Finsupp.mem_support_iff, AList.mem_keys, Finsupp.toAList_keys_toFinset
-- 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
haveI : (this : DecidableEq α) → Finset α
⊢ Finset α

Tactic:
haveI := Classical.decEq α
-- 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
this : DecidableEq α
haveI : (this : DecidableEq M) → Finset α
⊢ Finset α

Tactic:
haveI := Classical.decEq M
-- 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
this_1 : DecidableEq α
this : DecidableEq M
⊢ Finset α

Tactic:
exact (l.1.filter fun x => Sigma.snd x ≠ 0).keys.toFinset

Premises used: List.keys, List.toFinset, List.filter, AList.entries
-- 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 :
  (∃ 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:
simp_rw [mem_toFinset, List.mem_keys, List.mem_filter, ← mem_lookup_iff]

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
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
none :
  (∃ (b : M), Membership.mem (γ := Option M) Option.none b ∧ decide (b ≠ 0) = true) ↔
    Ne.{u_2 + 1} (α := M) (Option.getD Option.none 0) 0
some : ∀ (val : M), (∃ b ∈ Option.some val, decide (b ≠ 0) = true) ↔ (Option.some val).getD 0 ≠ 0
⊢ (∃ b ∈ lookup (β := fun (_x : α) ↦ M) a l, decide (b ≠ 0) = true) ↔ (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0

Tactic:
cases lookup a l

Premises used: AList.lookup
-- 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 : α
⊢ (∃ (b : M), Membership.mem (γ := Option M) none b ∧ decide (b ≠ 0) = true) ↔
    Ne.{u_2 + 1} (α := M) (Option.getD none 0) 0

Tactic:
simp
-- 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 : α
val : M
⊢ (∃ b ∈ some val, decide (b ≠ 0) = true) ↔ (some val).getD 0 ≠ 0

Tactic:
simp