awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Sups
Goal:
α : Type u_4
inst : DecidableEq α
inst_1 : Fintype α
𝒜 : Finset (Finset α)
n : ℕ
hn : n ≤ Fintype.card α
h𝒜 : Set.Sized (Fintype.card α - n) (↑𝒜 : Set (Finset α))
⊢ Set.Sized n (↑𝒜ᶜˢ : Set (Finset α))

Tactic:
simpa only [Nat.sub_sub_self hn] using h𝒜.compls

Premises used: Nat.sub_sub_self, Set.Sized.compls
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
a b : α
rw : s(a, b) ∈ s.sym2.val ↔ a ∈ s ∧ b ∈ s
rw₁ : s(a, b) ∈ s.val.sym2 ↔ a ∈ s ∧ b ∈ s
rw₂ : a ∈ s.val ∧ b ∈ s.val ↔ a ∈ s ∧ b ∈ s
rw₃ : a ∈ s.val ∧ b ∈ s.val ↔ a ∈ s.val ∧ b ∈ s
rw₄ rw₅ : a ∈ s.val ∧ b ∈ s.val ↔ a ∈ s.val ∧ b ∈ s.val
⊢ s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s

Tactic:
rw [mem_mk, sym2_val, Multiset.mk_mem_sym2_iff, mem_mk, mem_mk]

Premises used: Finset.mem_mk, Multiset.mk_mem_sym2_iff, Finset.sym2_val
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
m : Sym2 α
rw : (∀ y ∈ m, y ∈ s.val) ↔ ∀ a ∈ m, a ∈ s
⊢ m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s

Tactic:
rw [mem_mk, sym2_val, Multiset.mem_sym2_iff]

Premises used: Finset.mem_mk, Multiset.mem_sym2_iff, Finset.sym2_val
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
m : Sym2 α
⊢ (∀ y ∈ m, y ∈ s.val) ↔ ∀ a ∈ m, a ∈ s

Tactic:
simp only [mem_val]

Premises used: Finset.mem_val
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
m : Finset α
z : Sym2 α
a b : α
⊢ s(a, b) ∈ (↑m.sym2 : Set (Sym2 α)) ↔ s(a, b) ∈ (↑m : Set α).sym2

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
s_1 t : Finset α
a_1 b a : α
s : Finset α
ha : a ∉ s
⊢ Disjoint (map (Sym2.mkEmbedding a) (cons a s ha)) s.sym2

Tactic:
simp [Finset.disjoint_left, ha]

Premises used: Finset.disjoint_left
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
a : α
s : Finset α
ha : a ∉ s
⊢ (cons a s ha).sym2 = (map (Sym2.mkEmbedding a) (cons a s ha)).disjUnion s.sym2 ⋯

Tactic:
val_injective <| Multiset.sym2_cons _ _

Premises used: Finset.val_injective, Multiset.sym2_cons
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
inl : ∀ (ha : a ∈ s), (insert a s).sym2 = image (fun (b : α) ↦ s(a, b)) (insert a s) ∪ s.sym2
inr : ∀ (ha : a ∉ s), (insert a s).sym2 = image (fun (b : α) ↦ s(a, b)) (insert a s) ∪ s.sym2
⊢ (insert a s).sym2 = image (fun (b : α) ↦ s(a, b)) (insert a s) ∪ s.sym2

Tactic:
obtain ha | ha := Decidable.em (a ∈ s)

Premises used: Membership.mem, Decidable.em
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∈ s
inl : ∀ x ∈ s, s(a, x) ∈ s.sym2
⊢ (insert a s).sym2 = image (fun (b : α) ↦ s(a, b)) (insert a s) ∪ s.sym2

Tactic:
simp only [insert_eq_of_mem ha, right_eq_union, image_subset_iff]

Premises used: Finset.right_eq_union, Finset.image_subset_iff, Finset.insert_eq_of_mem
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∈ s
⊢ ∀ x ∈ s, s(a, x) ∈ s.sym2

Tactic:
simp_all
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
⊢ (insert a s).sym2 = image (fun (b : α) ↦ s(a, b)) (insert a s) ∪ s.sym2

Tactic:
simpa [map_eq_image] using sym2_cons a s ha

Premises used: Finset.sym2_cons, Finset.map_eq_image
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ (map f s).sym2 = map f.sym2Map s.sym2

Tactic:
val_injective <| s.val.sym2_map _

Premises used: Finset.val, Finset.val_injective, Multiset.sym2_map
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
a : (image f s).sym2.val = (image (Sym2.map f) s.sym2).val
⊢ (image f s).sym2 = image (Sym2.map f) s.sym2

Tactic:
apply val_injective

Premises used: Finset.val_injective
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
a : (Multiset.map f s.val).dedup.sym2 = (Multiset.map (Sym2.map f) s.val.sym2).dedup
⊢ (image f s).sym2.val = (image (Sym2.map f) s.sym2).val

Tactic:
dsimp [Finset.sym2]

Premises used: Finset.sym2
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
a : (Multiset.map f s.val).sym2.dedup = (Multiset.map (Sym2.map f) s.val.sym2).dedup
a₁ a₂ : (Multiset.map (Sym2.map f) s.val.sym2).dedup = (Multiset.map (Sym2.map f) s.val.sym2).dedup
⊢ (Multiset.map f s.val).dedup.sym2 = (Multiset.map (Sym2.map f) s.val.sym2).dedup

Tactic:
rw [← Multiset.dedup_sym2, Multiset.sym2_map]

Premises used: Multiset.dedup_sym2, Multiset.sym2_map
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst : Fintype α
x : Sym2 α
rw : ∀ a ∈ x, Membership.mem (γ := Finset α) univ a
⊢ Membership.mem (γ := Finset (Sym2 α)) (Finset.sym2 univ) x

Tactic:
rw [mem_sym2_iff]

Premises used: Finset.mem_sym2_iff
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst : Fintype α
x : Sym2 α
⊢ ∀ a ∈ x, Membership.mem (γ := Finset α) univ a

Tactic:
(fun a _ ↦ mem_univ a)

Premises used: Finset.mem_univ
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst : Fintype α
x : Sym2 α
⊢ ∀ a ∈ x, Membership.mem (γ := Finset α) univ a

Tactic:
exact (fun a _ ↦ mem_univ a)

Premises used: Finset.mem_univ
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst_1 : Fintype α
inst : Fintype (Sym2 α)
h :
  ∀ (a : Sym2 α),
    Membership.mem (γ := Finset (Sym2 α)) (Finset.sym2 univ) a ↔ Membership.mem (γ := Finset (Sym2 α)) univ a
⊢ Eq.{u_1 + 1} (α := Finset (Sym2 α)) (Finset.sym2 univ) univ

Tactic:
ext
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst_1 : Fintype α
inst : Fintype (Sym2 α)
a : Sym2 α
⊢ Membership.mem (γ := Finset (Sym2 α)) (Finset.sym2 univ) a ↔ Membership.mem (γ := Finset (Sym2 α)) univ a

Tactic:
simp only [mem_sym2_iff, mem_univ, implies_true]

Premises used: Finset.mem_univ, Finset.mem_sym2_iff, implies_true
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s t : Finset α
h : s ⊆ t
⊢ s.sym2 ⊆ t.sym2

Tactic:
grind
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
⊢ Monotone.{u_1, u_1} (α := Finset α) Finset.sym2

Tactic:
fun _ _ => sym2_mono

Premises used: Monotone, Finset.sym2_mono
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s t : Finset α
h : s.sym2 = t.sym2
h₁ : ∀ (x : α), x ∈ s ↔ x ∈ t
⊢ s = t

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s t : Finset α
h : s.sym2 = t.sym2
x : α
⊢ x ∈ s ↔ x ∈ t

Tactic:
simpa using congr(s(x, x) ∈ $h)
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
⊢ StrictMono.{u_1, u_1} (α := Finset α) Finset.sym2

Tactic:
monotone_sym2.strictMono_of_injective injective_sym2

Premises used: Finset.injective_sym2, Monotone.strictMono_of_injective, Finset.monotone_sym2
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
h : ∀ (z : Sym2 α), z ∈ m.toFinset.sym2 ↔ z ∈ m.sym2.toFinset
⊢ m.toFinset.sym2 = m.sym2.toFinset

Tactic:
ext z
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
z : Sym2 α
⊢ z ∈ m.toFinset.sym2 ↔ z ∈ m.sym2.toFinset

Tactic:
z.ind fun x y ↦ ?_

Premises used: Sym2.ind
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
z : Sym2 α
h : ∀ (x y : α), s(x, y) ∈ m.toFinset.sym2 ↔ s(x, y) ∈ m.sym2.toFinset
⊢ z ∈ m.toFinset.sym2 ↔ z ∈ m.sym2.toFinset

Tactic:
refine z.ind fun x y ↦ ?_
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
m : Multiset α
z : Sym2 α
x y : α
⊢ s(x, y) ∈ m.toFinset.sym2 ↔ s(x, y) ∈ m.sym2.toFinset

Tactic:
simp only [mk_mem_sym2_iff, Multiset.mem_toFinset, Multiset.mk_mem_sym2_iff]

Premises used: Finset.mk_mem_sym2_iff, Multiset.mk_mem_sym2_iff, Multiset.mem_toFinset
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Finset (Sym2 α)) (Finset.sym2 ∅) ∅

Tactic:
rfl

Premises used: Multiset.zero, Finset.empty, Multiset.ofList, List.sym2, Multiset.sym2, Finset.sym2, rfl
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
rw : s.sym2.val = 0 ↔ s = ∅
rw₁ : s.val.sym2 = 0 ↔ s = ∅
rw₂ : s.val = 0 ↔ s = ∅
rw₃ rw₄ : s = ∅ ↔ s = ∅
⊢ s.sym2 = ∅ ↔ s = ∅

Tactic:
rw [← val_eq_zero, sym2_val, Multiset.sym2_eq_zero_iff, val_eq_zero]

Premises used: Finset.val_eq_zero, Multiset.sym2_eq_zero_iff, Finset.sym2_val
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
contrapose! : s.sym2 = ∅ ↔ s = ∅
⊢ s.sym2.Nonempty ↔ s.Nonempty

Tactic:
contrapose!
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
⊢ s.sym2 = ∅ ↔ s = ∅

Tactic:
sym2_eq_empty

Premises used: Finset.sym2_eq_empty
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
⊢ s.sym2 = ∅ ↔ s = ∅

Tactic:
exact sym2_eq_empty

Premises used: Finset.sym2_eq_empty
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
a : α
⊢ Eq (α := Finset (Sym2 α)) (Finset.sym2 {a}) {Sym2.diag a}

Tactic:
rfl

Premises used: Multiset.cons, List.append, Multiset.ofList, List.sym2, Multiset.sym2, Finset.sym2, rfl, Sym2.diag
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
rw : s.sym2.val.card = (#s + 1).choose 2
rw₁ : s.val.sym2.card = (#s + 1).choose 2
rw₂ : (s.val.card + 1).choose 2 = (#s + 1).choose 2
rw₃ rw₄ : (#s + 1).choose 2 = (#s + 1).choose 2
⊢ #s.sym2 = (#s + 1).choose 2

Tactic:
rw [card_def, sym2_val, Multiset.card_sym2, ← card_def]

Premises used: Finset.card_def, Finset.sym2_val, Multiset.card_sym2
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
h :
  ∀ (a : Sym2 α) (a b : α),
    Quot.mk (Sym2.Rel α) (a, b) ∈ s.sym2 ↔ Quot.mk (Sym2.Rel α) (a, b) ∈ image (Function.uncurry Sym2.mk) (s ×ˢ s)
⊢ s.sym2 = image (Function.uncurry Sym2.mk) (s ×ˢ s)

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a_1 : Sym2 α
a b : α
h : a ∈ s ∧ b ∈ s ↔ ∃ (a_2 : α) (b_1 : α), (a_2 ∈ s ∧ b_1 ∈ s) ∧ (a_2 = a ∧ b_1 = b ∨ a_2 = b ∧ b_1 = a)
⊢ Quot.mk (Sym2.Rel α) (a, b) ∈ s.sym2 ↔ Quot.mk (Sym2.Rel α) (a, b) ∈ image (Function.uncurry Sym2.mk) (s ×ˢ s)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a_1 : Sym2 α
a b : α
⊢ a ∈ s ∧ b ∈ s ↔ ∃ (a_2 : α) (b_1 : α), (a_2 ∈ s ∧ b_1 ∈ s) ∧ (a_2 = a ∧ b_1 = b ∨ a_2 = b ∧ b_1 = a)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
a b : α
h : (a, b) ∈ s.diag
simp : ∀ (h : a ∈ s ∧ a = b), a = b
⊢ s(a, b).IsDiag

Tactic:
simp at *
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
a b : α
h : a ∈ s ∧ a = b
⊢ a = b

Tactic:
grind
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
a b : α
h : (a, b) ∈ s.offDiag
simp : ∀ (h : a ∈ s ∧ b ∈ s ∧ ¬a = b), ¬a = b
⊢ ¬s(a, b).IsDiag

Tactic:
simp at *
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
a b : α
h : a ∈ s ∧ b ∈ s ∧ ¬a = b
⊢ ¬a = b

Tactic:
grind
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
a : α
rw : Sym2.diag a ∈ s.sym2 ↔ a ∈ s
⊢ (∀ b ∈ Sym2.diag a, b ∈ s) ↔ a ∈ s

Tactic:
rw [← mem_sym2_iff]

Premises used: Finset.mem_sym2_iff
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
a : α
⊢ Sym2.diag a ∈ s.sym2 ↔ a ∈ s

Tactic:
mk_mem_sym2_iff.trans <| and_self_iff

Premises used: Finset.mk_mem_sym2_iff, Set.Mem, setOf, Iff.trans, and_self_iff, Sym2.diag
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
a : α
⊢ Sym2.diag a ∈ s.sym2 ↔ a ∈ s

Tactic:
exact mk_mem_sym2_iff.trans <| and_self_iff

Premises used: Finset.mk_mem_sym2_iff, Iff.trans, and_self_iff
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
a : α
⊢ Sym2.diag a ∈ s.sym2 ↔ a ∈ s

Tactic:
simp [diag_mem_sym2_mem_iff]

Premises used: Finset.diag_mem_sym2_mem_iff
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
rw : image (Function.uncurry Sym2.mk) (s.diag ∪ s.offDiag) = s.sym2
rw₁ : image (Function.uncurry Sym2.mk) (s ×ˢ s) = s.sym2
rw₂ rw₃ : image (Function.uncurry Sym2.mk) (s ×ˢ s) = image (Function.uncurry Sym2.mk) (s ×ˢ s)
⊢ image (Function.uncurry Sym2.mk) s.diag ∪ image (Function.uncurry Sym2.mk) s.offDiag = s.sym2

Tactic:
rw [← image_union, diag_union_offDiag, sym2_eq_image]

Premises used: Finset.diag_union_offDiag, Finset.image_union, Finset.sym2_eq_image
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ Eq (α := Finset (Sym α 0)) (s.sym 0) {∅}

Tactic:
rfl

Premises used: Finset.sym, rfl
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
⊢ Eq (α := Finset (Sym α (n + 1))) (s.sym (n + 1)) (s.sup fun (a : α) ↦ image (Sym.cons a) (s.sym n))

Tactic:
rfl

Premises used: Finset.sym, rfl
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
m : Sym α 0
⊢ Membership.mem (γ := Finset (Sym α 0)) (s.sym 0) m ↔ ∀ a ∈ m, a ∈ s

Tactic:
mem_singleton.trans ⟨?_, fun _ ↦ Sym.eq_nil_of_card_zero _⟩

Premises used: Finset.mem_singleton, Set.Mem, setOf, Sym.eq_nil_of_card_zero, Iff.intro, Iff.trans
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
m : Sym α 0
zero : m = ∅ → ∀ a ∈ m, a ∈ s
⊢ Membership.mem (γ := Finset (Sym α 0)) (s.sym 0) m ↔ ∀ a ∈ m, a ∈ s

Tactic:
refine mem_singleton.trans ⟨?_, fun _ ↦ Sym.eq_nil_of_card_zero _⟩

Premises used: Finset.mem_singleton, Sym.eq_nil_of_card_zero, Iff.intro, Iff.trans
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
⊢ ∀ (a : α), Membership.mem (γ := Sym α 0) ∅ a → a ∈ s

Tactic:
fun a ha ↦ (Finset.notMem_empty _ ha).elim

Premises used: False.elim, Finset.notMem_empty
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
⊢ ∀ (a : α), Membership.mem (γ := Sym α 0) ∅ a → a ∈ s

Tactic:
exact fun a ha ↦ (Finset.notMem_empty _ ha).elim

Premises used: False.elim, Finset.notMem_empty
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
⊢ Membership.mem (γ := Finset (Sym α (n + 1))) (s.sym (n + 1)) m ↔ ∀ a ∈ m, a ∈ s

Tactic:
?_
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
m : Sym α n
succ :
  ∀ (n : ℕ) (ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s) {m : Sym α (n + 1)},
    Membership.mem (γ := Finset (Sym α (n + 1))) (s.sym (n + 1)) m ↔ ∀ a ∈ m, a ∈ s
⊢ m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s

Tactic:
induction n with
  | zero =>
    refine mem_singleton.trans ⟨?_, fun _ ↦ Sym.eq_nil_of_card_zero _⟩
    rintro rfl
    exact fun a ha ↦ (Finset.notMem_empty _ ha).elim
  | succ n ih => ?_

Premises used: Finset.mem_singleton, False.elim, Finset.notMem_empty, Sym.eq_nil_of_card_zero, Iff.intro, Iff.trans, rfl
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
⊢ Membership.mem (γ := Finset (Sym α (n + 1))) (s.sym (n + 1)) m ↔ ∀ a ∈ m, a ∈ s

Tactic:
mem_sup.trans ⟨?_, fun h ↦ ?_⟩

Premises used: Finset.mem_sup, Set.Mem, setOf, Iff.intro, Iff.trans
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
succ : (∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)) → ∀ a ∈ m, a ∈ s
succ₁ : ∀ (h : ∀ a ∈ m, a ∈ s), ∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)
⊢ Membership.mem (γ := Finset (Sym α (n + 1))) (s.sym (n + 1)) m ↔ ∀ a ∈ m, a ∈ s

Tactic:
refine mem_sup.trans ⟨?_, fun h ↦ ?_⟩

Premises used: Finset.mem_sup, Iff.intro, Iff.trans
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
a : α
ha : a ∈ s
he : m ∈ image (Sym.cons a) (s.sym n)
b : α
hb : b ∈ m
succ : ∀ (he : ∃ a_1 ∈ s.sym n, a ::ₛ a_1 = m) (b : α) (hb : b ∈ m), b ∈ s
⊢ b ∈ s

Tactic:
rw [mem_image] at he

Premises used: Finset.mem_image
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
a : α
ha : a ∈ s
he : ∃ a_1 ∈ s.sym n, a ::ₛ a_1 = m
b : α
hb : b ∈ m
succ : ∀ (m : Sym α n) (he : m ∈ s.sym n) (hb : b ∈ a ::ₛ m), b ∈ s
⊢ b ∈ s

Tactic:
obtain ⟨m, he, rfl⟩ := he

Premises used: rfl
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ s.sym n
hb : b ∈ a ::ₛ m
⊢ b = a ∨ b ∈ m

Tactic:
rw [Sym.mem_cons] at hb

Premises used: Sym.mem_cons
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ s.sym n
hb : b = a ∨ b ∈ m
succ : ∀ (ha : b ∈ s), b ∈ s
succ₁ : ∀ (hb : b ∈ m), b ∈ s
⊢ b ∈ s

Tactic:
obtain rfl | hb := hb

Premises used: rfl
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
b : α
m : Sym α n
he : m ∈ s.sym n
ha : b ∈ s
⊢ b ∈ s

Tactic:
ha
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
b : α
m : Sym α n
he : m ∈ s.sym n
ha : b ∈ s
⊢ b ∈ s

Tactic:
exact ha
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ s.sym n
hb : b ∈ m
⊢ b ∈ s

Tactic:
ih.1 he _ hb

Premises used: Iff.mp
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ s.sym n
hb : b ∈ m
⊢ b ∈ s

Tactic:
exact ih.1 he _ hb

Premises used: Iff.mp
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
h : ∀ a ∈ m, a ∈ s
succ : ∀ (a : α) (m : Sym α n) (h : ∀ a_1 ∈ a ::ₛ m, a_1 ∈ s), ∃ i ∈ s, a ::ₛ m ∈ image (Sym.cons i) (s.sym n)
⊢ ∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)

Tactic:
obtain ⟨a, m, rfl⟩ := m.exists_eq_cons_of_succ

Premises used: Sym.exists_eq_cons_of_succ, rfl
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
m : Sym α n
h : ∀ a_1 ∈ a ::ₛ m, a_1 ∈ s
⊢ ∃ i ∈ s, a ::ₛ m ∈ image (Sym.cons i) (s.sym n)

Tactic:
⟨a, h _ <| Sym.mem_cons_self _ _,
        mem_image_of_mem _ <| ih.2 fun b hb ↦ h _ <| Sym.mem_cons_of_mem hb⟩

Premises used: Iff.mpr, Sym.mem_cons_self, And.intro, Exists.intro, Sym.mem_cons_of_mem, Finset.mem_image_of_mem
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
m : Sym α n
h : ∀ a_1 ∈ a ::ₛ m, a_1 ∈ s
⊢ ∃ i ∈ s, a ::ₛ m ∈ image (Sym.cons i) (s.sym n)

Tactic:
exact
      ⟨a, h _ <| Sym.mem_cons_self _ _,
        mem_image_of_mem _ <| ih.2 fun b hb ↦ h _ <| Sym.mem_cons_of_mem hb⟩
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
h :
  ∀ (d : Sym β n),
    d ∈ (map g s).sym n ↔
      d ∈
        map
          { toFun := Sym.map (⇑g : (a : α) → β), inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Sym α n) (Sym β n) }
          (s.sym n)
⊢ (map g s).sym n =
    map { toFun := Sym.map (⇑g : (a : α) → β), inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Sym α n) (Sym β n) }
      (s.sym n)

Tactic:
ext d
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
h :
  (∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a) ↔
    ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
⊢ d ∈ (map g s).sym n ↔
    d ∈
      map { toFun := Sym.map (⇑g : (a : α) → β), inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Sym α n) (Sym β n) }
        (s.sym n)

Tactic:
simp only [mem_sym_iff, mem_map, Function.Embedding.coeFn_mk]

Premises used: Finset.mem_sym_iff, Function.Embedding.coeFn_mk, Finset.mem_map
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
⊢ (∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a) ↔
    ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d

Tactic:
⟨fun hd ↦ ?_, fun ⟨b, hb, hd'⟩ d' hd ↦ ?_⟩

Premises used: Membership.mem, Exists, And, Iff.intro, _private.0.Finset.sym_map.match_1, Eq, DFunLike.coe
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
h :
  ∀ (hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a),
    ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
h₁ :
  (∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d) →
    ∀ (d' : β) (hd : d' ∈ d) (b : Sym α n) (hb : ∀ a ∈ b, a ∈ s) (hd' : Sym.map (⇑g : (a : α) → β) b = d),
      ∃ a ∈ s, (g : (a : α) → β) a = d'
⊢ (∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a) ↔
    ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d

Tactic:
refine ⟨fun hd ↦ ?_, fun ⟨b, hb, hd'⟩ d' hd ↦ ?_⟩
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
⊢ ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d

Tactic:
⟨(fun p ↦ Sym.map g' p) d.attach, ?_, ?_⟩

Premises used: Sym.attach, And.intro, Exists.intro, Sym.map
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
h : ∀ (a : α), Membership.mem (γ := Sym α n) ((fun (p : Sym { x : β // x ∈ d } n) ↦ Sym.map g' p) d.attach) a → a ∈ s
h₁ : Sym.map.{u_1, u_2} (α := α) (⇑g : (a : α) → β) ((fun (p : Sym { x : β // x ∈ d } n) ↦ Sym.map g' p) d.attach) = d
⊢ ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d

Tactic:
refine ⟨(fun p ↦ Sym.map g' p) d.attach, ?_, ?_⟩
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
h : ∀ (a : α) (x : β) (x_1 : x ∈ d) (h : ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x) = a), a ∈ s
⊢ ∀ (a : α), Membership.mem (γ := Sym α n) ((fun (p : Sym { x : β // x ∈ d } n) ↦ Sym.map g' p) d.attach) a → a ∈ s

Tactic:
simp only [Sym.mem_map, Sym.mem_attach, true_and, Subtype.exists, forall_exists_index, g']

Premises used: Sym.mem_map, Subtype.exists, forall_exists_index, Sym.mem_attach, true_and