awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f_1 : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s : Set α).Pairwise fun (a₁ a₂ : α) ↦ Disjoint (f a₁) (g a₂)
hf : (↑s : Set α).PairwiseDisjoint f
hg : (↑s : Set α).PairwiseDisjoint g
i : α
hi : i ∈ s
j : α
hj : j ∈ s
⊢ i ≠ j → (fun (a₁ a₂ : α) ↦ Disjoint (f a₁) (g a₂)) i j

Tactic:
specialize hfg' hi hj
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
f_1 : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hf : (↑s : Set α).PairwiseDisjoint f
hg : (↑s : Set α).PairwiseDisjoint g
i : α
hi : i ∈ s
j : α
hj : j ∈ s
hfg' : i ≠ j → (fun (a₁ a₂ : α) ↦ Disjoint (f a₁) (g a₂)) i j
⊢ Disjoint (f i) (g j)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s : Set α).Pairwise fun (a₁ a₂ : α) ↦ Disjoint (f a₁) (g a₂)
hf : (↑s : Set α).PairwiseDisjoint f
hg : (↑s : Set α).PairwiseDisjoint g
⊢ s.disjiUnion (fun (a : α) ↦ (f a).disjUnion (g a) ⋯) ⋯ = (s.disjiUnion f hf).disjUnion (s.disjiUnion g hg) ⋯

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
t : α → Finset β
⊢ (s.biUnion t).val = Multiset.dedup (s.val.bind fun (a : α) ↦ (t a).val)

Tactic:
rfl

Premises used: Multiset.dedup, rfl
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
t : α → Finset β
inst : DecidableEq β
⊢ Finset.biUnion ∅ t = ∅

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, List.dedup, Multiset.zero, Finset.empty, Finset.biUnion, Multiset.ofList, List.pwFilter, List.foldr, rfl
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst : DecidableEq β
b : β
⊢ b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a

Tactic:
simp only [mem_def, biUnion_val, Multiset.mem_dedup, Multiset.mem_bind]

Premises used: Finset.biUnion_val, Multiset.mem_dedup, Multiset.mem_bind, Finset.mem_def
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst : DecidableEq β
⊢ (↑(s.biUnion t) : Set β) = ⋃ x ∈ (↑s : Set α), (↑(t x) : Set β)

Tactic:
simp [Set.ext_iff, mem_biUnion, Set.mem_iUnion]

Premises used: Set.mem_iUnion, Set.ext_iff, Finset.mem_biUnion
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst : DecidableEq β
inst_1 : DecidableEq α
a : α
⊢ (insert a s).biUnion t = t a ∪ s.biUnion t

Tactic:
aesop
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t₁ t₂ : α → Finset β
inst : DecidableEq β
hs : s₁ = s₂
ht : ∀ a ∈ s₁, t₁ a = t₂ a
⊢ s₁.biUnion t₁ = s₂.biUnion t₂

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → Finset β
hf : (↑s : Set α).PairwiseDisjoint f
⊢ s.disjiUnion f hf = s.biUnion f

Tactic:
eq_of_veq (s.disjiUnion f hf).nodup.dedup.symm

Premises used: Finset.eq_of_veq, Finset.disjiUnion, Finset.nodup, Multiset.Nodup.dedup, Eq.symm
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst : DecidableEq β
s' : Finset β
⊢ s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s'

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
t : α → Finset β
inst : DecidableEq β
a : α
⊢ Finset.biUnion {a} t = t a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ s.biUnion f ∩ t = s.biUnion fun (x : α) ↦ f x ∩ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
t : Finset β
s : Finset α
f : α → Finset β
⊢ t ∩ s.biUnion f = s.biUnion fun (x : α) ↦ t ∩ f x

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
inst_1 : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
⊢ (s.biUnion f).biUnion g = s.biUnion fun (a : α) ↦ (f a).biUnion g

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
s : Multiset α
t : α → Multiset β
x : β
⊢ x ∈ (s.bind t).toFinset ↔ Membership.mem (γ := Finset β) (s.toFinset.biUnion fun (a : α) ↦ (t a).toFinset) x

Tactic:
simp only [Multiset.mem_toFinset, mem_biUnion, Multiset.mem_bind]

Premises used: Multiset.mem_bind, Multiset.mem_toFinset, Finset.mem_biUnion
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t₁ t₂ : α → Finset β
inst : DecidableEq β
h : ∀ a ∈ s, t₁ a ⊆ t₂ a
⊢ s.biUnion t₁ ⊆ s.biUnion t₂

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
inst : DecidableEq β
t : α → Finset β
h : s₁ ⊆ s₂
⊢ s₁.biUnion t ⊆ s₂.biUnion t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
inst : DecidableEq β
u : α → Finset β
x : α
xs : x ∈ s
⊢ u x ⊆ s.biUnion u

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_4
β : Type u_5
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → Finset β
⊢ s.biUnion f ⊆ t ↔ ∀ x ∈ s, f x ⊆ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ s.biUnion singleton = s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst_1 : DecidablePred p
⊢ filter p (s.biUnion f) = s.biUnion fun (a : α) ↦ filter p (f a)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
s : Finset α
t : Finset β
f : α → β
h : ∀ x ∈ s, f x ∈ t
⊢ (t.biUnion fun (a : β) ↦ {c ∈ s | f c = a}) = s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → Finset β
s : Finset α
b : β
⊢ (s.biUnion f).erase b = s.biUnion fun (x : α) ↦ (f x).erase b

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst : DecidableEq β
simp : (∃ (x : β), ∃ a ∈ s, x ∈ t a) ↔ ∃ x ∈ s, ∃ (x_1 : β), x_1 ∈ t x
⊢ (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty

Tactic:
simp only [Finset.Nonempty, mem_biUnion]

Premises used: Finset.Nonempty, Finset.mem_biUnion
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst : DecidableEq β
rw : (∃ (b : α) (a : β), b ∈ s ∧ a ∈ t b) ↔ ∃ x ∈ s, ∃ (x_1 : β), x_1 ∈ t x
⊢ (∃ (x : β), ∃ a ∈ s, x ∈ t a) ↔ ∃ x ∈ s, ∃ (x_1 : β), x_1 ∈ t x

Tactic:
rw [exists_comm]

Premises used: exists_comm
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst : DecidableEq β
⊢ (∃ (b : α) (a : β), b ∈ s ∧ a ∈ t b) ↔ ∃ x ∈ s, ∃ (x_1 : β), x_1 ∈ t x

Tactic:
simp [exists_and_left]

Premises used: exists_and_left
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst : DecidableEq β
hs : s.Nonempty
ht : ∀ x ∈ s, (t x).Nonempty
⊢ (s.biUnion t).Nonempty

Tactic:
biUnion_nonempty.2 <| hs.imp fun x hx ↦ ⟨hx, ht x hx⟩

Premises used: Iff.mpr, Finset.biUnion_nonempty, Exists.imp, And.intro
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t

Tactic:
s.induction ?_ ?_

Premises used: Finset.induction
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
refine_1 : Disjoint (Finset.biUnion ∅ f) t ↔ ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Disjoint (f i) t
refine_2 :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      (Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
        (Disjoint ((insert a s).biUnion f) t ↔ ∀ i ∈ insert a s, Disjoint (f i) t)
⊢ Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t

Tactic:
refine s.induction ?_ ?_
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Disjoint (Finset.biUnion ∅ f) t ↔ ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Disjoint (f i) t

Tactic:
simp
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s_1 : Finset α
f : α → Finset β
t : Finset β
i : α
s : Finset α
his : i ∉ s
ih : Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t
⊢ Disjoint ((insert i s).biUnion f) t ↔ ∀ i_1 ∈ insert i s, Disjoint (f i_1) t

Tactic:
simp only [disjoint_union_left, biUnion_insert, forall_mem_insert, ih]

Premises used: Finset.forall_mem_insert, Finset.biUnion_insert, Finset.disjoint_union_left
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
refine_1 : Disjoint (Finset.biUnion ∅ f) t ↔ ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Disjoint (f i) t
refine_2 refine_2₁ :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      (Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
        (Disjoint ((insert a s).biUnion f) t ↔ ∀ i ∈ insert a s, Disjoint (f i) t)
⊢ Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t

Tactic:
classical
  refine s.induction ?_ ?_
  · simp
  · intro i s his ih
    simp only [disjoint_union_left, biUnion_insert, forall_mem_insert, ih]

Premises used: Finset.forall_mem_insert, Finset.biUnion_insert, Finset.disjoint_union_left
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset β
t : Finset α
f : α → Finset β
⊢ Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i)

Tactic:
simpa only [_root_.disjoint_comm] using disjoint_biUnion_left t f s

Premises used: disjoint_comm, Finset.disjoint_biUnion_left
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
inst_1 : DecidableEq γ
f : α → β
s_1 : Finset α
t : β → Finset γ
this : DecidableEq α
a : α
s : Finset α
h : a ∉ s
ih : (image f s).biUnion t = s.biUnion fun (a : α) ↦ t (f a)
⊢ (image f (insert a s)).biUnion t = (insert a s).biUnion fun (a : α) ↦ t (f a)

Tactic:
simp only [image_insert, biUnion_insert, ih]

Premises used: Finset.biUnion_insert, Finset.image_insert
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
inst_1 : DecidableEq γ
s_1 : Finset α
t : α → Finset β
f : β → γ
this : DecidableEq α
a : α
s : Finset α
h : a ∉ s
ih : image f (s.biUnion t) = s.biUnion fun (a : α) ↦ image f (t a)
⊢ image f ((insert a s).biUnion t) = (insert a s).biUnion fun (a : α) ↦ image f (t a)

Tactic:
simp only [biUnion_insert, image_union, ih]

Premises used: Finset.image_union, Finset.biUnion_insert
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
s : Finset β
g : β → α
⊢ ((image g s).biUnion fun (a : α) ↦ {c ∈ s | g c = a}) = s

Tactic:
biUnion_filter_eq_of_maps_to fun _ => mem_image_of_mem g

Premises used: Finset.biUnion_filter_eq_of_maps_to, Finset.mem_image_of_mem
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Finset α
t : α → Finset β
inst : DecidableEq β
inst_1 : DecidableEq α
⊢ (s₁ ∪ s₂).biUnion t = s₁.biUnion t ∪ s₂.biUnion t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t₁ t₂ : α → Finset β
inst : DecidableEq β
⊢ (s.biUnion fun (x : α) ↦ t₁ x ∪ t₂ x) = s.biUnion t₁ ∪ s.biUnion t₂

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
inst : DecidableEq β
f : α → β
⊢ (s.biUnion fun (a : α) ↦ {f a}) = image f s

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

Tactic:
rfl

Premises used: Function.updateFinset, rfl
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
y : (i : ↥∅) → π (↑i : ι)
⊢ updateFinset (π := π) x ∅ y = x

Tactic:
rfl

Premises used: Function.updateFinset, Multiset.zero, dite, Multiset.ofList, rfl
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π (↑i_1 : ι)
h :
  ∀ (j : ι),
    updateFinset (π := π) x {i} y j =
      update (β := π) x i
        (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
          π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
        j
⊢ updateFinset (π := π) x {i} y =
    update (β := π) x i
      (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
        π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))

Tactic:
congr with j
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π (↑i_1 : ι)
j : ι
pos :
  ∀ (hj : j = i),
    updateFinset (π := π) x {i} y j =
      update (β := π) x i
        (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
          π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
        j
neg :
  ∀ (hj : ¬j = i),
    updateFinset (π := π) x {i} y j =
      update (β := π) x i
        (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
          π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
        j
⊢ updateFinset (π := π) x {i} y j =
    update (β := π) x i
      (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
        π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
      j

Tactic:
by_cases hj : j = i
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π (↑i_1 : ι)
j : ι
hj : j = i
pos :
  updateFinset (π := π) x {i} y i =
    update (β := π) x i
      (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
        π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
      i
⊢ updateFinset (π := π) x {i} y j =
    update (β := π) x i
      (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
        π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
      j

Tactic:
cases hj
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π (↑i_1 : ι)
⊢ updateFinset (π := π) x {i} y i =
    update (β := π) x i
      (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
        π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
      i

Tactic:
simp only [dif_pos, Finset.mem_singleton, update_self, updateFinset]

Premises used: Finset.mem_singleton, Function.updateFinset, dif_pos, Function.update_self
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π (↑i_1 : ι)
j : ι
hj : ¬j = i
⊢ updateFinset (π := π) x {i} y j =
    update (β := π) x i
      (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
        π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
      j

Tactic:
simp [hj, updateFinset]

Premises used: Function.updateFinset
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : π i
h :
  ∀ (j : ι),
    update (β := π) x i y j = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) j
⊢ update (β := π) x i y = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y)

Tactic:
congr with j
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : π i
j : ι
pos :
  ∀ (hj : j = i),
    update (β := π) x i y j = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) j
neg :
  ∀ (hj : ¬j = i),
    update (β := π) x i y j = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) j
⊢ update (β := π) x i y j = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) j

Tactic:
by_cases hj : j = i
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : π i
j : ι
hj : j = i
pos : update (β := π) x i y i = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) i
⊢ update (β := π) x i y j = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) j

Tactic:
cases hj
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : π i
pos :
  y =
    uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y
      (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)
⊢ update (β := π) x i y i = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) i

Tactic:
simp only [dif_pos, Finset.mem_singleton, update_self, updateFinset]

Premises used: Finset.mem_singleton, Function.updateFinset, dif_pos, Function.update_self
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : π i
⊢ y =
    uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y
      (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)

Tactic:
uniqueElim_default (α := fun j : ({i} : Finset ι) => π j) y

Premises used: Eq.mpr, uniqueElim, uniqueElim_default
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : π i
⊢ y =
    uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y
      (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯)

Tactic:
exact uniqueElim_default (α := fun j : ({i} : Finset ι) => π j) y

Premises used: uniqueElim_default
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : π i
j : ι
hj : ¬j = i
⊢ update (β := π) x i y j = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) j

Tactic:
simp [hj, updateFinset]

Premises used: Function.updateFinset
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_2
π : ι → Type u_3
inst : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn (α := π) f s
t : Finset ι
y : (i : ↥t) → π (↑i : ι)
⊢ DependsOn.{u_2, u_3, u_1} (α := π) (β := α) (fun (x : (i : ι) → π i) ↦ f (updateFinset (π := π) x t y))
    (s \ (↑t : Set ι))

Tactic:
fun x₁ x₂ h ↦ hf (fun i hi ↦ ?_)

Premises used: DependsOn
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_2
π : ι → Type u_3
inst : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn (α := π) f s
t : Finset ι
y : (i : ↥t) → π (↑i : ι)
refine :
  ∀ (x₁ x₂ : (i : ι) → π i) (h : ∀ i ∈ s \ (↑t : Set ι), x₁ i = x₂ i) (i : ι) (hi : i ∈ s),
    Function.updateFinset (π := π) x₁ t y i = Function.updateFinset (π := π) x₂ t y i
⊢ DependsOn.{u_2, u_3, u_1} (α := π) (β := α) (fun (x : (i : ι) → π i) ↦ f (Function.updateFinset (π := π) x t y))
    (s \ (↑t : Set ι))

Tactic:
refine fun x₁ x₂ h ↦ hf (fun i hi ↦ ?_)
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_2
π : ι → Type u_3
inst : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn (α := π) f s
t : Finset ι
y : (i : ↥t) → π (↑i : ι)
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ (↑t : Set ι), x₁ i = x₂ i
i : ι
hi : i ∈ s
pos :
  ∀ (h : i ∈ t),
    Eq (α := π i) (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i h) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i h) : ι))
      (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i h))
neg : i ∉ t → x₁ i = x₂ i
⊢ Eq.{u_3 + 1} (α := π i) (if hi : i ∈ t then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) else x₁ i)
    (if hi : i ∈ t then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) else x₂ i)

Tactic:
split_ifs
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_2
π : ι → Type u_3
inst : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn (α := π) f s
t : Finset ι
y : (i : ↥t) → π (↑i : ι)
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ (↑t : Set ι), x₁ i = x₂ i
i : ι
hi : i ∈ s
h_1 : i ∈ t
⊢ Eq (α := π i)
    (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i h_1) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i h_1) : ι))
    (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i h_1))

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_2
π : ι → Type u_3
inst : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn (α := π) f s
t : Finset ι
y : (i : ↥t) → π (↑i : ι)
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ (↑t : Set ι), x₁ i = x₂ i
i : ι
hi : i ∈ s
h_1 : i ∉ t
⊢ x₁ i = x₂ i

Tactic:
simp_all
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_2
π : ι → Type u_3
inst : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Finset ι
hf : DependsOn (α := π) f (↑s : Set ι)
i : ι
y : π i
simp_rw :
  DependsOn.{u_2, u_3, u_1} (α := π) (β := α)
    (fun (x : (i : ι) → π i) ↦ f (updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y)))
    ((↑s : Set ι) \ (↑{i} : Set ι))
⊢ DependsOn.{u_2, u_3, u_1} (α := π) (β := α) (fun (x : (i : ι) → π i) ↦ f (Function.update (β := π) x i y))
    (↑(s.erase i) : Set ι)

Tactic:
simp_rw [Function.update_eq_updateFinset, erase_eq, coe_sdiff]

Premises used: Function.update_eq_updateFinset, Finset.erase_eq, Finset.coe_sdiff
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_2
π : ι → Type u_3
inst : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Finset ι
hf : DependsOn (α := π) f (↑s : Set ι)
i : ι
y : π i
⊢ DependsOn.{u_2, u_3, u_1} (α := π) (β := α)
    (fun (x : (i : ι) → π i) ↦ f (updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y)))
    ((↑s : Set ι) \ (↑{i} : Set ι))

Tactic:
hf.updateFinset _

Premises used: DependsOn.updateFinset
-- Module: Mathlib.Data.Finset.Update
Goal:
ι : Type u_2
π : ι → Type u_3
inst : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Finset ι
hf : DependsOn (α := π) f (↑s : Set ι)
i : ι
y : π i
⊢ DependsOn.{u_2, u_3, u_1} (α := π) (β := α)
    (fun (x : (i : ι) → π i) ↦ f (updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y)))
    ((↑s : Set ι) \ (↑{i} : Set ι))

Tactic:
exact hf.updateFinset _

Premises used: DependsOn.updateFinset
-- 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
h :
  ∀ (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
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))

Tactic:
ext i