Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V ⊕ V
hl : l ∈ left
r : V ⊕ V
hr : r ∈ right
hmem_left : ∀ {l' : V ⊕ V}, l' ∈ left → (l.isLeft = true → l'.isLeft = true) ∧ (l.isRight = true → l'.isRight = true)
r' : V ⊕ V
hr' : r' ∈ right
⊢ (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)

Tactic:
rcases l with l | l <;> rcases r with r | r

Goal state after:
case inl.inl
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
r' : V ⊕ V
hr' : r' ∈ right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
⊢ ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)

case inl.inr
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
r' : V ⊕ V
hr' : r' ∈ right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
⊢ ((Sum.inr r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inr r).isRight = true → r'.isRight = true)

case inr.inl
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
r' : V ⊕ V
hr' : r' ∈ right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
⊢ ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)

case inr.inr
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
r' : V ⊕ V
hr' : r' ∈ right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
⊢ ((Sum.inr r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inr r).isRight = true → r'.isRight = true)