case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
m : Sym α Nat.zero
⊢ m ∈ Finset.sym s Nat.zero ↔ ∀ (a : α), a ∈ m → a ∈ s

case succ
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
⊢ m ∈ Finset.sym s (Nat.succ n) ↔ ∀ (a : α), a ∈ m → a ∈ s
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
induction' n with n ih
case succ.refine'_1
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
⊢ (∃ v, v ∈ s ∧ m ∈ image (Sym.cons v) (Finset.sym s n)) → ∀ (a : α), a ∈ m → a ∈ s

case succ.refine'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
h : ∀ (a : α), a ∈ m → a ∈ s
⊢ ∃ v, v ∈ s ∧ m ∈ image (Sym.cons v) (Finset.sym s n)
case succ
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
⊢ m ∈ Finset.sym s (Nat.succ n) ↔ ∀ (a : α), a ∈ m → a ∈ s
refine' mem_sup.trans ⟨_, fun h ↦ _⟩
case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
m : Sym α Nat.zero
⊢ m = ∅ → ∀ (a : α), a ∈ m → a ∈ s
case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
m : Sym α Nat.zero
⊢ m ∈ Finset.sym s Nat.zero ↔ ∀ (a : α), a ∈ m → a ∈ s
refine' mem_singleton.trans ⟨_, fun _ ↦ Sym.eq_nil_of_card_zero _⟩
case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ ∀ (a : α), a ∈ ∅ → a ∈ s
case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
m : Sym α Nat.zero
⊢ m = ∅ → ∀ (a : α), a ∈ m → a ∈ s
rintro rfl
no goals
case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ ∀ (a : α), a ∈ ∅ → a ∈ s
exact fun a ha ↦ (Finset.not_mem_empty _ ha).elim
case succ.refine'_1.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
a : α
ha : a ∈ s
he : m ∈ image (Sym.cons a) (Finset.sym s n)
b : α
hb : b ∈ m
⊢ b ∈ s
case succ.refine'_1
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
⊢ (∃ v, v ∈ s ∧ m ∈ image (Sym.cons v) (Finset.sym s n)) → ∀ (a : α), a ∈ m → a ∈ s
rintro ⟨a, ha, he⟩ b hb
case succ.refine'_1.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
a : α
ha : a ∈ s
he : ∃ a_1, a_1 ∈ Finset.sym s n ∧ a ::ₛ a_1 = m
b : α
hb : b ∈ m
⊢ b ∈ s
case succ.refine'_1.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
a : α
ha : a ∈ s
he : m ∈ image (Sym.cons a) (Finset.sym s n)
b : α
hb : b ∈ m
⊢ b ∈ s
rw [mem_image] at he
case succ.refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
hb : b ∈ a ::ₛ m
⊢ b ∈ s
case succ.refine'_1.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
a : α
ha : a ∈ s
he : ∃ a_1, a_1 ∈ Finset.sym s n ∧ a ::ₛ a_1 = m
b : α
hb : b ∈ m
⊢ b ∈ s
obtain ⟨m, he, rfl⟩ := he
case succ.refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
hb : b = a ∨ b ∈ m
⊢ b ∈ s
case succ.refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
hb : b ∈ a ::ₛ m
⊢ b ∈ s
rw [Sym.mem_cons] at hb
case succ.refine'_1.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
ha : b ∈ s
⊢ b ∈ s

case succ.refine'_1.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
hb : b ∈ m
⊢ b ∈ s
case succ.refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
hb : b = a ∨ b ∈ m
⊢ b ∈ s
obtain rfl | hb := hb
no goals
case succ.refine'_1.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
ha : b ∈ s
⊢ b ∈ s
exact ha
no goals
case succ.refine'_1.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
hb : b ∈ m
⊢ b ∈ s
exact ih.1 he _ hb
case succ.refine'_2.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
m : Sym α n
h : ∀ (a_1 : α), a_1 ∈ a ::ₛ m → a_1 ∈ s
⊢ ∃ v, v ∈ s ∧ a ::ₛ m ∈ image (Sym.cons v) (Finset.sym s n)
case succ.refine'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
h : ∀ (a : α), a ∈ m → a ∈ s
⊢ ∃ v, v ∈ s ∧ m ∈ image (Sym.cons v) (Finset.sym s n)
obtain ⟨a, m, rfl⟩ := m.exists_eq_cons_of_succ
no goals
case succ.refine'_2.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
m : Sym α n
h : ∀ (a_1 : α), a_1 ∈ a ::ₛ m → a_1 ∈ s
⊢ ∃ v, v ∈ s ∧ a ::ₛ m ∈ image (Sym.cons v) (Finset.sym s n)
exact
  ⟨a, h _ <| Sym.mem_cons_self _ _,
    mem_image_of_mem _ <| ih.2 fun b hb ↦ h _ <| Sym.mem_cons_of_mem hb⟩