-- Mathlib/Order/Partition/Finpartition.lean
theorem mem_part_ofSetoid_iff_rel {s : Setoid α} [DecidableRel s.r] {b : α} :
    b ∈ (ofSetoid s).part a ↔ s.r a b

Proof state:
α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
H : ∃! a_1, a_1 ∈ image (fun a => filter (fun b => s a b) univ) univ ∧ a ∈ a_1
this :
  choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H ∈
      image (fun a => filter (fun b => s a b) univ) univ ∧
    a ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H
⊢ b ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H ↔ s a b

Tactic:
simp only [mem_univ, mem_image, true_and] at this

Result:
α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
H : ∃! a_1, a_1 ∈ image (fun a => filter (fun b => s a b) univ) univ ∧ a ∈ a_1
this :
  (∃ a_1,
      filter (fun b => s a_1 b) univ =
        choose (fun a_2 => a ∈ a_2) (image (fun a => filter (fun b => s a b) univ) univ) H) ∧
    a ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H
⊢ b ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H ↔ s a b

Proof state:
α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
H : ∃! a_1, a_1 ∈ image (fun a => filter (fun b => s a b) univ) univ ∧ a ∈ a_1
⊢ b ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H ↔ s a b

Tactic:
have := choose_spec _ _ H

Result:
α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
H : ∃! a_1, a_1 ∈ image (fun a => filter (fun b => s a b) univ) univ ∧ a ∈ a_1
this :
  choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H ∈
      image (fun a => filter (fun b => s a b) univ) univ ∧
    a ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H
⊢ b ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H ↔ s a b

Proof state:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
H : ∃! a_1, a_1 ∈ image (fun a => filter (fun b => s a b) univ) univ ∧ a ∈ a_1
w✝ : α
hc : filter (fun b => s w✝ b) univ = choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H
this : s w✝ a
⊢ s w✝ b ↔ s a b

Tactic:
exact ⟨s.trans (s.symm this), s.trans this⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
H : ∃! a_1, a_1 ∈ image (fun a => filter (fun b => s a b) univ) univ ∧ a ∈ a_1
this : a ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H
w✝ : α
hc : filter (fun b => s w✝ b) univ = choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H
⊢ b ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H ↔ s a b

Tactic:
simp only [← hc, mem_univ, mem_filter, true_and] at this ⊢

Result:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
H : ∃! a_1, a_1 ∈ image (fun a => filter (fun b => s a b) univ) univ ∧ a ∈ a_1
w✝ : α
hc : filter (fun b => s w✝ b) univ = choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H
this : s w✝ a
⊢ s w✝ b ↔ s a b

Proof state:
α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
H : ∃! a_1, a_1 ∈ image (fun a => filter (fun b => s a b) univ) univ ∧ a ∈ a_1
this :
  (∃ a_1,
      filter (fun b => s a_1 b) univ =
        choose (fun a_2 => a ∈ a_2) (image (fun a => filter (fun b => s a b) univ) univ) H) ∧
    a ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H
⊢ b ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H ↔ s a b

Tactic:
obtain ⟨⟨_, hc⟩, this⟩ := this

Result:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
H : ∃! a_1, a_1 ∈ image (fun a => filter (fun b => s a b) univ) univ ∧ a ∈ a_1
this : a ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H
w✝ : α
hc : filter (fun b => s w✝ b) univ = choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H
⊢ b ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H ↔ s a b

Proof state:
α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
⊢ b ∈ (ofSetoid s).part a ↔ s a b

Tactic:
simp_rw [part, ofSetoid, mem_univ, reduceDIte]

Result:
α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
⊢ b ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) ⋯ ↔ s a b

Proof state:
α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
⊢ b ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) ⋯ ↔ s a b

Tactic:
generalize_proofs H

Result:
α : Type u_1
inst✝² : DecidableEq α
a : α
inst✝¹ : Fintype α
s : Setoid α
inst✝ : DecidableRel ⇑s
b : α
H : ∃! a_1, a_1 ∈ image (fun a => filter (fun b => s a b) univ) univ ∧ a ∈ a_1
⊢ b ∈ choose (fun a_1 => a ∈ a_1) (image (fun a => filter (fun b => s a b) univ) univ) H ↔ s a b