Theorem: Finpartition.multipartiteGraph_adj_of_mem_parts (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Multipartite.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s t : Finset α
a b : α
hs : s ∈ P.parts
ht : t ∈ P.parts
ha : a ∈ s
hb : b ∈ t
⊢ P.multipartiteGraph.Adj a b ↔ s ≠ t
Tactic:
refine' ⟨_, fun hst u hu hau hbu => hst _⟩
State after:
case refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s t : Finset α
a b : α
hs : s ∈ P.parts
ht : t ∈ P.parts
ha : a ∈ s
hb : b ∈ t
⊢ P.multipartiteGraph.Adj a b → s ≠ t

case refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s t : Finset α
a b : α
hs : s ∈ P.parts
ht : t ∈ P.parts
ha : a ∈ s
hb : b ∈ t
hst : s ≠ t
u : Finset α
hu : u ∈ P.parts
hau : a ∈ u
hbu : b ∈ u
⊢ s = t

State before:
case refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s t : Finset α
a b : α
hs : s ∈ P.parts
ht : t ∈ P.parts
ha : a ∈ s
hb : b ∈ t
⊢ P.multipartiteGraph.Adj a b → s ≠ t
Tactic:
rintro hab rfl
State after:
case refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s : Finset α
a b : α
hs : s ∈ P.parts
ha : a ∈ s
hab : P.multipartiteGraph.Adj a b
ht : s ∈ P.parts
hb : b ∈ s
⊢ False

State before:
case refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s : Finset α
a b : α
hs : s ∈ P.parts
ha : a ∈ s
hab : P.multipartiteGraph.Adj a b
ht : s ∈ P.parts
hb : b ∈ s
⊢ False
Tactic:
exact hab hs ha hb
State after:
no goals

State before:
case refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
P : Finpartition univ
s t : Finset α
a b : α
hs : s ∈ P.parts
ht : t ∈ P.parts
ha : a ∈ s
hb : b ∈ t
hst : s ≠ t
u : Finset α
hu : u ∈ P.parts
hau : a ∈ u
hbu : b ∈ u
⊢ s = t
Tactic:
rw [P.eq_of_mem_parts hs hu ha hau, P.eq_of_mem_parts ht hu hb hbu]
State after:
no goals