Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case inl.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
l : V
hl : Sum.inl l ∈ left
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ ((Sum.inl l).isLeft = true → (Sum.inl l').isLeft = true) ∧ ((Sum.inl l).isRight = true → (Sum.inl l').isRight = true)

pp: case inl.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
l : V
hl : Sum.inl l ∈ left
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ ((Sum.inl l).isLeft = true → (Sum.inr l').isLeft = true) ∧ ((Sum.inl l).isRight = true → (Sum.inr l').isRight = true)

pp: case inl.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
l : V
hl : Sum.inl l ∈ left
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ ((Sum.inl l).isLeft = true → (Sum.inl l').isLeft = true) ∧ ((Sum.inl l).isRight = true → (Sum.inl l').isRight = true)

pp: case inl.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
l : V
hl : Sum.inl l ∈ left
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ ((Sum.inl l).isLeft = true → (Sum.inr l').isLeft = true) ∧ ((Sum.inl l).isRight = true → (Sum.inr l').isRight = true)

pp: case inr.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
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ ((Sum.inr l).isLeft = true → (Sum.inl l').isLeft = true) ∧ ((Sum.inr l).isRight = true → (Sum.inl l').isRight = true)

pp: case inr.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
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ ((Sum.inr l).isLeft = true → (Sum.inr l').isLeft = true) ∧ ((Sum.inr l).isRight = true → (Sum.inr l').isRight = true)

pp: case inr.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
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ ((Sum.inr l).isLeft = true → (Sum.inl l').isLeft = true) ∧ ((Sum.inr l).isRight = true → (Sum.inl l').isRight = true)

pp: case inr.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
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ ((Sum.inr l).isLeft = true → (Sum.inr l').isLeft = true) ∧ ((Sum.inr l).isRight = true → (Sum.inr l').isRight = true)

Tactic:
all_goals solve | simp | simpa using h hl hr | simpa using h hl' hr

Goal state after: