awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst : DecidableEq α
n : ℕ
h : a ∉ s
x : (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))
i : Fin (n + 1)
m : Sym α (n - (↑i : ℕ))
hm : Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) m
⊢ a ∉
    (Sigma.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))
        (Sigma.map (β₁ := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) (β₂ := fun (i : Fin (n + 1)) ↦
          Sym α (n - (↑i : ℕ))) id
          (fun (i : Fin (n + 1)) (a : ↥(s.sym (n - (↑i : ℕ)))) ↦ (↑a : Sym α (n - (↑(id i) : ℕ))))
          (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) i
            (Subtype.mk (p := fun (x : Sym α (n - (↑i : ℕ))) ↦
              Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) x) m hm))) :
      Sym α
        (n -
          (↑(Sigma.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))
                (Sigma.map (β₁ := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) (β₂ := fun (i : Fin (n + 1)) ↦
                  Sym α (n - (↑i : ℕ))) id
                  (fun (i : Fin (n + 1)) (a : ↥(s.sym (n - (↑i : ℕ)))) ↦ (↑a : Sym α (n - (↑(id i) : ℕ))))
                  (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) i
                    (Subtype.mk (p := fun (x : Sym α (n - (↑i : ℕ))) ↦
                      Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) x) m hm)))) :
            ℕ)))

Tactic:
h ∘ mem_sym_iff.1 hm a

Premises used: Finset.mem_sym_iff, Function.comp, Iff.mp, Not
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
rw : Eq (α := α) (∏ i ∈ s, i ^ Multiset.count i (↑k : Multiset α)) (∏ d ∈ s, d ^ Multiset.count d (↑k : Multiset α))
rw₁ : (↑k : Multiset α).toFinset ⊆ s
⊢ (↑k : Multiset α).prod = ∏ d ∈ s, d ^ Multiset.count d (↑k : Multiset α)

Tactic:
rw [Finset.prod_multiset_count_of_subset _ s]

Premises used: Finset.prod_multiset_count_of_subset
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ ∀ x ∈ s, x ^ Multiset.count x (↑k : Multiset α) = x ^ Multiset.count x (↑k : Multiset α)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ Eq (α := α) (∏ i ∈ s, i ^ Multiset.count i (↑k : Multiset α)) (∏ d ∈ s, d ^ Multiset.count d (↑k : Multiset α))

Tactic:
apply Finset.prod_congr rfl (by simp)

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
x : α
hx : x ∈ (↑k : Multiset α).toFinset
⊢ x ∈ k

Tactic:
simp only [Sym.val_eq_coe, Multiset.mem_toFinset, Sym.mem_coe] at hx

Premises used: Sym.val_eq_coe, Sym.mem_coe, Multiset.mem_toFinset
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
x : α
hx : x ∈ k
⊢ ∀ a ∈ k, a ∈ s

Tactic:
simp only [Finset.mem_sym_iff] at hk

Premises used: Finset.mem_sym_iff
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
x : α
hx : x ∈ k
hk : ∀ a ∈ k, a ∈ s
⊢ x ∈ s

Tactic:
hk x hx
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
x : α
hx : x ∈ k
hk : ∀ a ∈ k, a ∈ s
⊢ x ∈ s

Tactic:
exact hk x hx
-- Module: Mathlib.Data.Finset.SymmDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
simp_rw : a ∈ s \ t ⊔ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
simp_rw₁ : a ∈ s \ t ∪ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
simp_rw₂ : a ∈ s \ t ∨ a ∈ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
⊢ a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

Tactic:
simp_rw [symmDiff, sup_eq_union, mem_union, mem_sdiff]

Premises used: Finset.mem_sdiff, Finset.mem_union, Finset.sup_eq_union, symmDiff
-- Module: Mathlib.Data.Finset.SymmDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
x : α
⊢ x ∈ (↑(s ∆ t) : Set α) ↔ x ∈ (↑s : Set α) ∆ (↑t : Set α)

Tactic:
simp [mem_symmDiff, Set.mem_symmDiff]

Premises used: Set.mem_symmDiff, Finset.mem_symmDiff
-- Module: Mathlib.Data.Finset.SymmDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∆ t = ∅ ↔ s = t

Tactic:
symmDiff_eq_bot

Premises used: symmDiff_eq_bot
-- Module: Mathlib.Data.Finset.SymmDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ (s ∆ t).Nonempty ↔ s ≠ t

Tactic:
nonempty_iff_ne_empty.trans symmDiff_eq_empty.not

Premises used: Iff.not, Finset.nonempty_iff_ne_empty, Iff.trans, Finset.symmDiff_eq_empty
-- Module: Mathlib.Data.Finset.SymmDiff
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
s t : Finset α
hf : Injective f
⊢ image f (s ∆ t) = image f s ∆ image f t

Tactic:
mod_cast Set.image_symmDiff hf s t

Premises used: Set.image_symmDiff, congrArg, SetLike.coe_set_eq._simp_1, cast, Finset.coe_image._simp_1, SetLike.coe, Finset.coe_symmDiff._simp_3, congr, Set.image, Eq, symmDiff, Eq.trans
-- Module: Mathlib.Data.Finset.SymmDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s \ t ⊆ s ∆ t

Tactic:
subset_union_left

Premises used: Set.Mem, setOf, Finset.subset_union_left
-- Module: Mathlib.Data.Finset.SymmDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ t \ s ⊆ s ∆ t

Tactic:
subset_union_right

Premises used: Set.Mem, setOf, Finset.subset_union_right
-- Module: Mathlib.Data.Finset.SymmDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∆ t ⊆ s ∪ t

Tactic:
symmDiff_le_sup (α := Finset α)

Premises used: Set.Mem, setOf, symmDiff_le_sup
-- Module: Mathlib.Data.Finset.SymmDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∆ t = s ∪ t ↔ Disjoint s t

Tactic:
symmDiff_eq_sup s t

Premises used: symmDiff_eq_sup
-- Module: Mathlib.Data.Finset.SymmDiff
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
h : Disjoint s t
⊢ s ∆ t = s ∪ t

Tactic:
Disjoint.symmDiff_eq_sup h

Premises used: Disjoint.symmDiff_eq_sup
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
h : (↑s : Set α).PairwiseDisjoint t
⊢ (s.disjiUnion t h).val = s.val.bind fun (a : α) ↦ (t a).val

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Multiset.join, Multiset.bind, rfl
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t_1 t₁ t₂ t : α → Finset β
⊢ (↑∅ : Set α).PairwiseDisjoint t

Tactic:
simp
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
t : α → Finset β
⊢ disjiUnion ∅ t ⋯ = ∅

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finset.disjiUnion, Finset.empty, Multiset.join, List.foldr, Multiset.bind, rfl
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
b : β
h : (↑s : Set α).PairwiseDisjoint t
⊢ b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a

Tactic:
simp only [mem_def, disjiUnion_val, Multiset.mem_bind]

Premises used: Multiset.mem_bind, Finset.disjiUnion_val, Finset.mem_def
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
h : (↑s : Set α).PairwiseDisjoint t
⊢ (↑(s.disjiUnion t h) : Set β) = ⋃ x ∈ (↑s : Set α), (↑(t x) : Set β)

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

Premises used: Set.mem_iUnion, Finset.mem_disjiUnion, Set.ext_iff
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
a : α
s : Finset α
ha : a ∉ s
f : α → Finset β
H : (↑(cons a s ha) : Set α).PairwiseDisjoint f
⊢ (cons a s ha).disjiUnion f H = (f a).disjUnion (s.disjiUnion f ⋯) ⋯

Tactic:
eq_of_veq <| Multiset.cons_bind _ _ _

Premises used: Finset.eq_of_veq, Multiset.cons_bind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
t : α → Finset β
a : α
h : (↑{a} : Set α).PairwiseDisjoint t
⊢ disjiUnion {a} t h = t a

Tactic:
eq_of_veq <| Multiset.singleton_bind _ _

Premises used: Finset.eq_of_veq, Multiset.singleton_bind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s : Set α).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1) : Set β).PairwiseDisjoint g
a : ↥s
h : a ∈ (↑s.attach : Set ↥s)
b : ↥s
h_1 : b ∈ (↑s.attach : Set ↥s)
hab : a ≠ b
x : γ
hxa : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) a) x
hxb : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) b) x
obtain : ∀ (xa : β) (hfa : xa ∈ f (↑a : α)) (hga : x ∈ g xa), False
⊢ False

Tactic:
obtain ⟨xa, hfa, hga⟩ := mem_disjiUnion.mp hxa

Premises used: Finset.mem_disjiUnion, Iff.mp
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s : Set α).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1) : Set β).PairwiseDisjoint g
a : ↥s
h : a ∈ (↑s.attach : Set ↥s)
b : ↥s
h_1 : b ∈ (↑s.attach : Set ↥s)
hab : a ≠ b
x : γ
hxa : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) a) x
hxb : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) b) x
xa : β
hfa : xa ∈ f (↑a : α)
hga : x ∈ g xa
obtain : ∀ (xb : β) (hfb : xb ∈ f (↑b : α)) (hgb : x ∈ g xb), False
⊢ False

Tactic:
obtain ⟨xb, hfb, hgb⟩ := mem_disjiUnion.mp hxb

Premises used: Finset.mem_disjiUnion, Iff.mp
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s : Set α).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1) : Set β).PairwiseDisjoint g
a : ↥s
h : a ∈ (↑s.attach : Set ↥s)
b : ↥s
h_1 : b ∈ (↑s.attach : Set ↥s)
hab : a ≠ b
x : γ
hxa : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) a) x
hxb : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) b) x
xa : β
hfa : xa ∈ f (↑a : α)
hga : x ∈ g xa
xb : β
hfb : xb ∈ f (↑b : α)
hgb : x ∈ g xb
⊢ False

Tactic:
disjoint_left.mp
            (h2 (mem_disjiUnion.mpr ⟨_, a.prop, hfa⟩) (mem_disjiUnion.mpr ⟨_, b.prop, hfb⟩) ?_) hga
            hgb

Premises used: Iff.mpr, Finset.mem_disjiUnion, Subtype.prop, And.intro, Exists.intro, Iff.mp, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s : Set α).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1) : Set β).PairwiseDisjoint g
a : ↥s
h : a ∈ (↑s.attach : Set ↥s)
b : ↥s
h_1 : b ∈ (↑s.attach : Set ↥s)
hab : a ≠ b
x : γ
hxa : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) a) x
hxb : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) b) x
xa : β
hfa : xa ∈ f (↑a : α)
hga : x ∈ g xa
xb : β
hfb : xb ∈ f (↑b : α)
hgb : x ∈ g xb
refine : xa ≠ xb
⊢ False

Tactic:
refine disjoint_left.mp
            (h2 (mem_disjiUnion.mpr ⟨_, a.prop, hfa⟩) (mem_disjiUnion.mpr ⟨_, b.prop, hfb⟩) ?_) hga
            hgb

Premises used: Iff.mpr, Finset.mem_disjiUnion, Subtype.prop, And.intro, Exists.intro, Iff.mp, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s : Set α).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1) : Set β).PairwiseDisjoint g
a : ↥s
h : a ∈ (↑s.attach : Set ↥s)
b : ↥s
h_1 : b ∈ (↑s.attach : Set ↥s)
hab : a ≠ b
x : γ
hxa : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) a) x
hxb : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) b) x
xa : β
hfa : xa ∈ f (↑a : α)
hga : x ∈ g xa
hfb : xa ∈ f (↑b : α)
hgb : x ∈ g xa
⊢ False

Tactic:
disjoint_left.mp (h1 a.prop b.prop <| Subtype.coe_injective.ne hab) hfa hfb

Premises used: Function.Injective.ne, Subtype.coe_injective, Subtype.prop, Iff.mp, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s : Set α).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1) : Set β).PairwiseDisjoint g
a : ↥s
h : a ∈ (↑s.attach : Set ↥s)
b : ↥s
h_1 : b ∈ (↑s.attach : Set ↥s)
hab : a ≠ b
x : γ
hxa : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) a) x
hxb : Membership.mem (γ := Finset γ) ((fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) b) x
xa : β
hfa : xa ∈ f (↑a : α)
hga : x ∈ g xa
hfb : xa ∈ f (↑b : α)
hgb : x ∈ g xa
⊢ False

Tactic:
exact disjoint_left.mp (h1 a.prop b.prop <| Subtype.coe_injective.ne hab) hfa hfb

Premises used: Function.Injective.ne, Subtype.coe_injective, Subtype.prop, Iff.mp, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s : Set α).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1) : Set β).PairwiseDisjoint g
⊢ (s.disjiUnion f h1).disjiUnion g h2 = s.attach.disjiUnion (fun (a : ↥s) ↦ (f (↑a : α)).disjiUnion g ⋯) ⋯

Tactic:
eq_of_veq <| Multiset.bind_assoc.trans (Multiset.attach_bind_coe _ _).symm

Premises used: Finset.eq_of_veq, Multiset.bind_assoc, Multiset.attach_bind_coe, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
h :
  ∀ (x : β),
    x ∈ ⋃₀ (↑(I.disjiUnion f hf) : Set (Set β)) ↔ Membership.mem (γ := Set β) (⋃ a ∈ I, ⋃₀ (↑(f a) : Set (Set β))) x
⊢ ⋃₀ (↑(I.disjiUnion f hf) : Set (Set β)) = ⋃ a ∈ I, ⋃₀ (↑(f a) : Set (Set β))

Tactic:
ext
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
⊢ x ∈ ⋃₀ (↑(I.disjiUnion f hf) : Set (Set β)) ↔ Membership.mem (γ := Set β) (⋃ a ∈ I, ⋃₀ (↑(f a) : Set (Set β))) x

Tactic:
simp only [coe_disjiUnion, Set.mem_sUnion, Set.mem_iUnion, mem_coe, exists_prop]

Premises used: Set.mem_iUnion, exists_prop, Finset.coe_disjiUnion, Set.mem_sUnion, Finset.mem_coe
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I : Set α).PairwiseDisjoint f
x : β
h : (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁ : (∃ i ∈ I, ∃ t ∈ f i, x ∈ t) → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₂ h₃ h₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₅ h₆ h₇ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₈ h₉ h₁₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₁ h₁₂ h₁₃ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₁₄ h₁₅ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ i ∈ I, ∃ t ∈ f i, x ∈ t
h₁₆ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
h₁₇ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₁₈ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I ∧ ∃ t ∈ f w_1, x ∈ t
h₁₉ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₀ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I
h₂₁ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₂ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₃ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → w_1 ∈ I
h₂₄ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₅ : (w : Set β) → x ∈ w → (w_1 : α) → w_1 ∈ I → w ∈ f w_1 → α
h₂₆ h₂₇ : ∀ (w : Set β), x ∈ w → ∀ w_1 ∈ I, w ∈ f w_1 → ∃ t ∈ f w_1, x ∈ t
h₂₈ h₂₉ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t
h₃₀ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → (∃ i ∈ I, w_1 ∈ f i) ∧ x ∈ w_1
h₃₁ : (w : α) → w ∈ I → (w_1 : Set β) → w_1 ∈ f w → x ∈ w_1 → Set β
h₃₂ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → (∃ i ∈ I, w_1 ∈ f i) ∧ x ∈ w_1
h₃₃ : (w : α) → w ∈ I → (w_1 : Set β) → w_1 ∈ f w → x ∈ w_1 → Set β
h₃₄ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ i ∈ I, w_1 ∈ f i
h₃₅ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → x ∈ w_1
h₃₆ : (w : α) → w ∈ I → (w_1 : Set β) → w_1 ∈ f w → x ∈ w_1 → Set β
h₃₇ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → ∃ i ∈ I, w_1 ∈ f i
h₃₈ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → x ∈ w_1
h₃₉ : (w : α) → w ∈ I → (w_1 : Set β) → w_1 ∈ f w → x ∈ w_1 → Set β
h₄₀ h₄₁ : ∀ w ∈ I, ∀ w_1 ∈ f w, x ∈ w_1 → x ∈ w_1
⊢ (∃ (t : Set β), (∃ i ∈ I, t ∈ f i) ∧ x ∈ t) ↔ ∃ i ∈ I, ∃ t ∈ f i, x ∈ t

Tactic:
tauto
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
x' : β
hx : x' ∈ (↑t : Set β)
y' : β
hy : y' ∈ (↑t : Set β)
hne : x' ≠ y'
simp_rw : ∀ ⦃a : α⦄, a ∈ s ∧ f a = x' → ¬(a ∈ s ∧ f a = y')
⊢ Function.onFun.{u_2 + 1, u_1 + 1, 1} (β := Finset α) Disjoint (fun (a : β) ↦ {x ∈ s | f x = a}) x' y'

Tactic:
simp_rw [disjoint_left, mem_filter]

Premises used: Finset.mem_filter, Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
i : α
left : i ∈ s
hx : f i ∈ (↑t : Set β)
left_1 : i ∈ s
hy : f i ∈ (↑t : Set β)
hne : f i ≠ f i
⊢ False

Tactic:
hne rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
i : α
left : i ∈ s
hx : f i ∈ (↑t : Set β)
left_1 : i ∈ s
hy : f i ∈ (↑t : Set β)
hne : f i ≠ f i
⊢ False

Tactic:
exact hne rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : α
⊢ Membership.mem (γ := Finset α) (t.disjiUnion (fun (a : β) ↦ {x ∈ s | f x = a}) ⋯) b ↔ b ∈ {c ∈ s | f c ∈ t}

Tactic:
simpa using and_comm

Premises used: and_comm
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
t : Finset β
f : α → β
h : ∀ x ∈ s, f x ∈ t
⊢ t.disjiUnion (fun (a : β) ↦ {x ∈ s | f x = a}) ⋯ = s

Tactic:
simpa [filter_eq_self]

Premises used: Finset.filter_eq_self
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
t : β → Finset γ
h : (↑(map f s) : Set β).PairwiseDisjoint t
⊢ (map f s).disjiUnion t h = s.disjiUnion (fun (a : α) ↦ t ((f : (a : α) → β) a)) ⋯

Tactic:
eq_of_veq <| Multiset.bind_map _ _ _

Premises used: Finset.eq_of_veq, Multiset.bind_map
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : α → Finset β
f : β ↪ γ
h : (↑s : Set α).PairwiseDisjoint t
⊢ map f (s.disjiUnion t h) = s.disjiUnion (fun (a : α) ↦ map f (t a)) ⋯

Tactic:
eq_of_veq <| Multiset.map_bind _ _ _

Premises used: Finset.eq_of_veq, Multiset.map_bind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s_1 s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
x : α
h : x ∈ (↑s : Set α)
⊢ ∀ ⦃y : α⦄, y ∈ (↑s : Set α) → x ≠ y → Function.onFun (β := Finset α) Disjoint singleton x y

Tactic:
simp
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
s : Finset α
⊢ s.disjiUnion singleton ⋯ = s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
f : α → β
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
s : Finset ι
t : ι → Finset α
b : ι → β
b₀ : β
h : (↑s : Set ι).PairwiseDisjoint t
⊢ fold op (fold op b₀ b s) f (s.disjiUnion t h) = fold op b₀ (fun (i : ι) ↦ fold op (b i) f (t i)) s

Tactic:
(congr_arg _ <| Multiset.map_bind _ _ _).trans (Multiset.fold_bind _ _ _ _ _)

Premises used: Multiset.sum, Multiset.foldr, Multiset.map_bind, Finset.fold, congr_arg, Multiset.fold_bind, Multiset.join, Multiset.bind, Eq.trans
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → Finset β
h : (↑s : Set α).PairwiseDisjoint f
p : β → Prop
inst : DecidablePred p
⊢ Set.PairwiseDisjoint.{u_2, u_1} (α := Finset β) (↑s : Set α) fun (a : α) ↦ filter p (f a)

Tactic:
fun _ h₁ _ h₂ hne ↦ Finset.disjoint_filter_filter (h h₁ h₂ hne)

Premises used: Set.PairwiseDisjoint, Set.Pairwise, Finset.disjoint_filter_filter
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → Finset β
h : (↑s : Set α).PairwiseDisjoint f
p : β → Prop
inst : DecidablePred p
⊢ filter p (s.disjiUnion f h) = s.disjiUnion (fun (a : α) ↦ filter p (f a)) ⋯

Tactic:
grind
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
hf : Function.Injective f
h :
  ∀ (a : β),
    Membership.mem (γ := Finset β) (s.disjiUnion (fun (a : α) ↦ {f a}) ⋯) a ↔
      a ∈ map { toFun := f, inj' := hf : α ↪ β } s
⊢ s.disjiUnion (fun (a : α) ↦ {f a}) ⋯ = map { toFun := f, inj' := hf : α ↪ β } s

Tactic:
ext
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
hf : Function.Injective f
a : β
⊢ Membership.mem (γ := Finset β) (s.disjiUnion (fun (a : α) ↦ {f a}) ⋯) a ↔ a ∈ map { toFun := f, inj' := hf : α ↪ β } s

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → Finset β
hf : (↑s : Set α).PairwiseDisjoint f
t : Finset β
empty :
  ∀ (hf : (↑∅ : Set α).PairwiseDisjoint f),
    Disjoint (disjiUnion ∅ f hf) t ↔ ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Disjoint (f i) t
cons :
  ∀ (a : α) (s : Finset α) (h : a ∉ s),
    (∀ (hf : (↑s : Set α).PairwiseDisjoint f), Disjoint (s.disjiUnion f hf) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
      ∀ (hf : (↑(Finset.cons a s h) : Set α).PairwiseDisjoint f),
        Disjoint ((Finset.cons a s h).disjiUnion f hf) t ↔ ∀ i ∈ Finset.cons a s h, Disjoint (f i) t
⊢ Disjoint (s.disjiUnion f hf) t ↔ ∀ i ∈ s, Disjoint (f i) t

Tactic:
induction s using Finset.cons_induction
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
f : α → Finset β
t : Finset β
hf : (↑∅ : Set α).PairwiseDisjoint f
⊢ Disjoint (disjiUnion ∅ f hf) t ↔ ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Disjoint (f i) t

Tactic:
simp_all
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
f : α → Finset β
t : Finset β
a : α
s : Finset α
h : a ∉ s
h_1 : ∀ (hf : (↑s : Set α).PairwiseDisjoint f), Disjoint (s.disjiUnion f hf) t ↔ ∀ i ∈ s, Disjoint (f i) t
hf : (↑(cons a s h) : Set α).PairwiseDisjoint f
⊢ Disjoint ((cons a s h).disjiUnion f hf) t ↔ ∀ i ∈ cons a s h, Disjoint (f i) t

Tactic:
simp_all
-- Module: Mathlib.Data.Finset.Union
Goal:
α : Type u_1
β : Type u_2
s : Finset β
t : Finset α
f : α → Finset β
hf : (↑t : Set α).PairwiseDisjoint f
⊢ Disjoint s (t.disjiUnion f hf) ↔ ∀ i ∈ t, Disjoint s (f i)

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

Premises used: disjoint_comm, Finset.disjoint_disjiUnion_left
-- 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
i : α
hi : i ∈ (↑s : Set α)
j : α
hj : j ∈ (↑s : Set α)
hij : i ≠ j
⊢ Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Finset β) Disjoint (fun (a : α) ↦ (f a).disjUnion (g a) ⋯) i j

Tactic:
simp [hf hi hj hij, hg hi hj hij, hfg' hi hj hij, (hfg' hj hi hij.symm).symm]

Premises used: Ne.symm, Disjoint.symm
-- 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
simp_rw : ∀ i ∈ s, ∀ i_1 ∈ s, Disjoint (f i) (g i_1)
⊢ Disjoint (s.disjiUnion f hf) (s.disjiUnion g hg)

Tactic:
simp_rw [disjoint_disjiUnion_left, disjoint_disjiUnion_right]

Premises used: Finset.disjoint_disjiUnion_right, Finset.disjoint_disjiUnion_left