awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inl l ∈ left
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ (Sum.isLeft (β := V) (Sum.inl l) = true → Sum.isLeft (β := V) (Sum.inl l') = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → Sum.isRight (β := V) (Sum.inl l') = true)

Tactic:
solve | simp | simpa using h hl hr | simpa using h hl' hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inl l ∈ left
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ (Sum.isLeft (β := V) (Sum.inl l) = true → Sum.isLeft (α := V) (Sum.inr l') = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → Sum.isRight (α := V) (Sum.inr l') = true)

Tactic:
simpa using h hl hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inl l ∈ left
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ (Sum.isLeft (β := V) (Sum.inl l) = true → Sum.isLeft (β := V) (Sum.inl l') = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → Sum.isRight (β := V) (Sum.inl l') = true)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inl l ∈ left
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ (Sum.isLeft (β := V) (Sum.inl l) = true → Sum.isLeft (β := V) (Sum.inl l') = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → Sum.isRight (β := V) (Sum.inl l') = true)

Tactic:
solve | simp | simpa using h hl hr | simpa using h hl' hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inl l ∈ left
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ (Sum.isLeft (β := V) (Sum.inl l) = true → Sum.isLeft (α := V) (Sum.inr l') = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → Sum.isRight (α := V) (Sum.inr l') = true)

Tactic:
simpa using h hl' hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ (Sum.isLeft (α := V) (Sum.inr l) = true → Sum.isLeft (β := V) (Sum.inl l') = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → Sum.isRight (β := V) (Sum.inl l') = true)

Tactic:
simpa using h hl' hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ (Sum.isLeft (α := V) (Sum.inr l) = true → Sum.isLeft (α := V) (Sum.inr l') = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → Sum.isRight (α := V) (Sum.inr l') = true)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inl r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ (Sum.isLeft (α := V) (Sum.inr l) = true → Sum.isLeft (α := V) (Sum.inr l') = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → Sum.isRight (α := V) (Sum.inr l') = true)

Tactic:
solve | simp | simpa using h hl hr | simpa using h hl' hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inl l' ∈ left
⊢ (Sum.isLeft (α := V) (Sum.inr l) = true → Sum.isLeft (β := V) (Sum.inl l') = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → Sum.isRight (β := V) (Sum.inl l') = true)

Tactic:
simpa using h hl hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ (Sum.isLeft (α := V) (Sum.inr l) = true → Sum.isLeft (α := V) (Sum.inr l') = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → Sum.isRight (α := V) (Sum.inr l') = true)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inr r ∈ right
l' : V
hl' : Sum.inr l' ∈ left
⊢ (Sum.isLeft (α := V) (Sum.inr l) = true → Sum.isLeft (α := V) (Sum.inr l') = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → Sum.isRight (α := V) (Sum.inr l') = true)

Tactic:
solve | simp | simpa using h hl hr | simpa using h hl' hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V ⊕ V
hl : l ∈ left
r : V ⊕ V
hr : r ∈ right
⊢ ∀ {l' : V ⊕ V} (hl' : l' ∈ left), (l.isLeft = true → l'.isLeft = true) ∧ (l.isRight = true → l'.isRight = true)

Tactic:
have hmem_left {l'} (hl' : l' ∈ left) :
        (l.isLeft → l'.isLeft) ∧ (l.isRight → l'.isRight) := by
      rcases l with l | l <;> rcases r with r | r <;> rcases l' with l' | l'
      all_goals solve | simp | simpa using h hl hr | simpa using h hl' hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V ⊕ V
hl : l ∈ left
r : V ⊕ V
hr : r ∈ right
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left), (l.isLeft = true → l'.isLeft = true) ∧ (l.isRight = true → l'.isRight = true)
r' : V ⊕ V
hr' : r' ∈ right
inl :
  ∀ (l : V) (hl : Sum.inl l ∈ left)
    (hmem_left :
      ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
        (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
          (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)),
    (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)
inr :
  ∀ (l : V) (hl : Sum.inr l ∈ left)
    (hmem_left :
      ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
        (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
          (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)),
    (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)
⊢ (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)

Tactic:
rcases l with l | l
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
r : V ⊕ V
hr : r ∈ right
r' : V ⊕ V
hr' : r' ∈ right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
    (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
inl :
  ∀ (r : V) (hr : Sum.inl r ∈ right),
    (Sum.isLeft (β := V) (Sum.inl r) = true → r'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl r) = true → r'.isRight = true)
inl₁ :
  ∀ (r : V) (hr : Sum.inr r ∈ right),
    (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)
⊢ (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)

Tactic:
rcases r with r | r
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
r : V ⊕ V
hr : r ∈ right
r' : V ⊕ V
hr' : r' ∈ right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
    (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
inr :
  ∀ (r : V) (hr : Sum.inl r ∈ right),
    (Sum.isLeft (β := V) (Sum.inl r) = true → r'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl r) = true → r'.isRight = true)
inr₁ :
  ∀ (r : V) (hr : Sum.inr r ∈ right),
    (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)
⊢ (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)

Tactic:
rcases r with r | r
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
r' : V ⊕ V
hr' : r' ∈ right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
    (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
inl :
  ∀ (r' : V) (hr' : Sum.inl r' ∈ right),
    (Sum.isLeft (β := V) (Sum.inl r) = true → Sum.isLeft (β := V) (Sum.inl r') = true) ∧
      (Sum.isRight (β := V) (Sum.inl r) = true → Sum.isRight (β := V) (Sum.inl r') = true)
inl₁ :
  ∀ (r' : V) (hr' : Sum.inr r' ∈ right),
    (Sum.isLeft (β := V) (Sum.inl r) = true → Sum.isLeft (α := V) (Sum.inr r') = true) ∧
      (Sum.isRight (β := V) (Sum.inl r) = true → Sum.isRight (α := V) (Sum.inr r') = true)
⊢ (Sum.isLeft (β := V) (Sum.inl r) = true → r'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl r) = true → r'.isRight = true)

Tactic:
rcases r' with r' | r'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
r' : V ⊕ V
hr' : r' ∈ right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
    (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
inl :
  ∀ (r' : V) (hr' : Sum.inl r' ∈ right),
    (Sum.isLeft (α := V) (Sum.inr r) = true → Sum.isLeft (β := V) (Sum.inl r') = true) ∧
      (Sum.isRight (α := V) (Sum.inr r) = true → Sum.isRight (β := V) (Sum.inl r') = true)
inl₁ :
  ∀ (r' : V) (hr' : Sum.inr r' ∈ right),
    (Sum.isLeft (α := V) (Sum.inr r) = true → Sum.isLeft (α := V) (Sum.inr r') = true) ∧
      (Sum.isRight (α := V) (Sum.inr r) = true → Sum.isRight (α := V) (Sum.inr r') = true)
⊢ (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)

Tactic:
rcases r' with r' | r'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
r' : V ⊕ V
hr' : r' ∈ right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
    (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
inr :
  ∀ (r' : V) (hr' : Sum.inl r' ∈ right),
    (Sum.isLeft (β := V) (Sum.inl r) = true → Sum.isLeft (β := V) (Sum.inl r') = true) ∧
      (Sum.isRight (β := V) (Sum.inl r) = true → Sum.isRight (β := V) (Sum.inl r') = true)
inr₁ :
  ∀ (r' : V) (hr' : Sum.inr r' ∈ right),
    (Sum.isLeft (β := V) (Sum.inl r) = true → Sum.isLeft (α := V) (Sum.inr r') = true) ∧
      (Sum.isRight (β := V) (Sum.inl r) = true → Sum.isRight (α := V) (Sum.inr r') = true)
⊢ (Sum.isLeft (β := V) (Sum.inl r) = true → r'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl r) = true → r'.isRight = true)

Tactic:
rcases r' with r' | r'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
r' : V ⊕ V
hr' : r' ∈ right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
    (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
inr :
  ∀ (r' : V) (hr' : Sum.inl r' ∈ right),
    (Sum.isLeft (α := V) (Sum.inr r) = true → Sum.isLeft (β := V) (Sum.inl r') = true) ∧
      (Sum.isRight (α := V) (Sum.inr r) = true → Sum.isRight (β := V) (Sum.inl r') = true)
inr₁ :
  ∀ (r' : V) (hr' : Sum.inr r' ∈ right),
    (Sum.isLeft (α := V) (Sum.inr r) = true → Sum.isLeft (α := V) (Sum.inr r') = true) ∧
      (Sum.isRight (α := V) (Sum.inr r) = true → Sum.isRight (α := V) (Sum.inr r') = true)
⊢ (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)

Tactic:
rcases r' with r' | r'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
    (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
r' : V
hr' : Sum.inl r' ∈ right
⊢ (Sum.isLeft (β := V) (Sum.inl r) = true → Sum.isLeft (β := V) (Sum.inl r') = true) ∧
    (Sum.isRight (β := V) (Sum.inl r) = true → Sum.isRight (β := V) (Sum.inl r') = true)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
    (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
r' : V
hr' : Sum.inl r' ∈ right
⊢ (Sum.isLeft (β := V) (Sum.inl r) = true → Sum.isLeft (β := V) (Sum.inl r') = true) ∧
    (Sum.isRight (β := V) (Sum.inl r) = true → Sum.isRight (β := V) (Sum.inl r') = true)

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