-- Mathlib/Data/Finset/Sym.lean
theorem mem_sym_iff {m : Sym α n} : m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s

Proof state:
case succ.refine_1.intro.intro
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ 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
⊢ b ∈ s

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

Result:
case succ.refine_1.intro.intro.intro.intro
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ 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 ∈ s

Proof state:
case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
⊢ m ∈ s.sym (n + 1) ↔ ∀ a ∈ m, a ∈ s

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

Result:
case succ.refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
⊢ (∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)) → ∀ a ∈ m, a ∈ s

case succ.refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
h : ∀ a ∈ m, a ∈ s
⊢ ∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
m : Sym α n
⊢ m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s

Tactic:
induction' n with n ih

Result:
case zero
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
m : Sym α 0
⊢ m ∈ s.sym 0 ↔ ∀ a ∈ m, a ∈ s

case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
⊢ m ∈ s.sym (n + 1) ↔ ∀ a ∈ m, a ∈ s

Proof state:
case succ.refine_1.intro.intro.intro.intro
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ 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 ∈ s

Tactic:
rw [Sym.mem_cons] at hb

Result:
case succ.refine_1.intro.intro.intro.intro
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ 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
⊢ b ∈ s

Proof state:
case succ.refine_1.intro.intro
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ 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
⊢ b ∈ s

Tactic:
rw [mem_image] at he

Result:
case succ.refine_1.intro.intro
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ 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
⊢ b ∈ s

Proof state:
case succ.refine_1.intro.intro.intro.intro.inr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ 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

Result:
no goals

Proof state:
case zero
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
m : Sym α 0
⊢ m = ∅ → ∀ a ∈ m, a ∈ s

Tactic:
rintro rfl

Result:
case zero
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ ∀ a ∈ ∅, a ∈ s

Proof state:
case zero
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ ∀ a ∈ ∅, a ∈ s

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

Result:
no goals

Proof state:
case succ.refine_1.intro.intro.intro.intro
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ 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
⊢ b ∈ s

Tactic:
obtain rfl | hb := hb

Result:
case succ.refine_1.intro.intro.intro.intro.inl
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ 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

case succ.refine_1.intro.intro.intro.intro.inr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ 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

Proof state:
case succ.refine_1.intro.intro.intro.intro.inl
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ 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

Result:
no goals

Proof state:
case succ.refine_2.intro.intro
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ 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⟩

Result:
no goals

Proof state:
case succ.refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
h : ∀ a ∈ m, a ∈ s
⊢ ∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)

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

Result:
case succ.refine_2.intro.intro
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ 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)

Proof state:
case succ.refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
⊢ (∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)) → ∀ a ∈ m, a ∈ s

Tactic:
rintro ⟨a, ha, he⟩ b hb

Result:
case succ.refine_1.intro.intro
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ 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
⊢ b ∈ s

Proof state:
case zero
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
m : Sym α 0
⊢ m ∈ s.sym 0 ↔ ∀ a ∈ m, a ∈ s

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

Result:
case zero
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
m : Sym α 0
⊢ m = ∅ → ∀ a ∈ m, a ∈ s