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
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.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)

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
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
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)

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
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
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)

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.inr r ∈ right
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)

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
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
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.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
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'
-- 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
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
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)

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
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
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)

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
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
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)

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
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
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)

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
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), (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)

Tactic:
have hmem_right {r'} (hr' : r' ∈ right) :
        (r.isLeft → r'.isLeft) ∧ (r.isRight → r'.isRight) := by
      rcases l with l | l <;> rcases r with r | r <;> rcases r' with r' | r'
      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)
hmem_right :
  ∀ {r' : V ⊕ V} (hr' : r' ∈ right), (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)
refine_1 :
  ∀ (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)),
    ∃ (left_1 : Finset V) (right_1 : Finset V),
      #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)
refine_1₁ :
  ∀ (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)),
    ∃ (left_1 : Finset V) (right_1 : Finset V),
      #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)
⊢ ∃ (left_1 : Finset V) (right_1 : Finset V),
    #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)

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
hmem_right :
  ∀ {r' : V ⊕ V} (hr' : r' ∈ right), (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)
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)
refine_1 :
  ∀ (r : V) (hr : Sum.inl r ∈ right)
    (hmem_right :
      ∀ {r' : V ⊕ V} (hr' : r' ∈ right),
        (Sum.isLeft (β := V) (Sum.inl r) = true → r'.isLeft = true) ∧
          (Sum.isRight (β := V) (Sum.inl r) = true → r'.isRight = true)),
    ∃ (left_1 : Finset V) (right_1 : Finset V),
      #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)
refine_1₁ :
  ∀ (r : V) (hr : Sum.inr r ∈ right)
    (hmem_right :
      ∀ {r' : V ⊕ V} (hr' : r' ∈ right),
        (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
          (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)),
    ∃ (left_1 : Finset V) (right_1 : Finset V),
      #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)
⊢ ∃ (left_1 : Finset V) (right_1 : Finset V),
    #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)

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
hmem_right :
  ∀ {r' : V ⊕ V} (hr' : r' ∈ right), (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)
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)
refine_1 :
  ∀ (r : V) (hr : Sum.inl r ∈ right)
    (hmem_right :
      ∀ {r' : V ⊕ V} (hr' : r' ∈ right),
        (Sum.isLeft (β := V) (Sum.inl r) = true → r'.isLeft = true) ∧
          (Sum.isRight (β := V) (Sum.inl r) = true → r'.isRight = true)),
    ∃ (left_1 : Finset V) (right_1 : Finset V),
      #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)
refine_1₁ :
  ∀ (r : V) (hr : Sum.inr r ∈ right)
    (hmem_right :
      ∀ {r' : V ⊕ V} (hr' : r' ∈ right),
        (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
          (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)),
    ∃ (left_1 : Finset V) (right_1 : Finset V),
      #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)
⊢ ∃ (left_1 : Finset V) (right_1 : Finset V),
    #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)

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
hmem_right :
  ∀ {r' : V ⊕ V} (hr' : r' ∈ right),
    (Sum.isLeft (β := V) (Sum.inl r) = true → r'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl r) = true → r'.isRight = true)
⊢ ∃ (left_1 : Finset V) (right_1 : Finset V),
    #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)

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
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
hmem_right :
  ∀ {r' : V ⊕ V} (hr' : r' ∈ right),
    (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)
⊢ ∃ (left_1 : Finset V) (right_1 : Finset V),
    #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)

Tactic:
⟨left.toLeft, right.toRight, ?_, ?_, fun i hi j hj ↦ ?_⟩

Premises used: Finset.toLeft, Finset.toRight, And.intro, Exists.intro
-- 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.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V} (hr' : r' ∈ right),
    (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)
refine_1 : #left.toLeft = #left
refine_1₁ : #right.toRight = #right
refine_1₂ : ∀ (i : V) (hi : i ∈ (↑left.toLeft : Set V)) (j : V) (hj : j ∈ (↑right.toRight : Set V)), G.Adj i j
⊢ ∃ (left_1 : Finset V) (right_1 : Finset V),
    #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)

Tactic:
refine ⟨left.toLeft, right.toRight, ?_, ?_, fun i hi j hj ↦ ?_⟩
-- 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.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V} (hr' : r' ∈ right),
    (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)
i : V
hi : i ∈ left.toLeft
⊢ (fun (i : V) (x : i ∈ left.toLeft) ↦ (Sum.inl i : V ⊕ V)) i hi ∈ left

Tactic:
simpa using hi