awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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 ⊕ V
hl' : l' ∈ left
l : V
hl : Sum.inr l ∈ left
⊢ (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
have inr : ∀ (r : V) (hr : Sum.inl r ∈ right),
  (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
Tactic: rcases r with r | r
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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 ⊕ V
hl' : l' ∈ left
l : V
hl : Sum.inr l ∈ left
inr :
  ∀ (r : V) (hr : Sum.inl r ∈ right),
    (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
⊢ (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
have inr₁ : ∀ (r : V) (hr : Sum.inr r ∈ right),
  (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
Tactic: rcases r with r | r
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
l : V
hl : Sum.inl l ∈ left
r : V
hr : Sum.inl r ∈ right
⊢ (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
have inl : ∀ (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: rcases l' with l' | l'
Cleared hypotheses: l', hl'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
l : V
hl : Sum.inl l ∈ left
r : V
hr : Sum.inl r ∈ right
inl :
  ∀ (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)
⊢ (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
have inl₁ : ∀ (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: rcases l' with l' | l'
Cleared hypotheses: l', hl'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
l : V
hl : Sum.inl l ∈ left
r : V
hr : Sum.inr r ∈ right
⊢ (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
have inl : ∀ (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: rcases l' with l' | l'
Cleared hypotheses: l', hl'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
l : V
hl : Sum.inl l ∈ left
r : V
hr : Sum.inr r ∈ right
inl :
  ∀ (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)
⊢ (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
have inl₁ : ∀ (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: rcases l' with l' | l'
Cleared hypotheses: l', hl'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inl r ∈ right
⊢ (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
have inr : ∀ (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: rcases l' with l' | l'
Cleared hypotheses: l', hl'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inl r ∈ right
inr :
  ∀ (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)
⊢ (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
have inr₁ : ∀ (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: rcases l' with l' | l'
Cleared hypotheses: l', hl'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inr r ∈ right
⊢ (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
have inr : ∀ (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: rcases l' with l' | l'
Cleared hypotheses: l', hl'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
l : V
hl : Sum.inr l ∈ left
r : V
hr : Sum.inr r ∈ right
inr :
  ∀ (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)
⊢ (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
have inr₁ : ∀ (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: rcases l' with l' | l'
Cleared hypotheses: l', hl'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
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
⊢ ∃ (left_1 : Finset V) (right_1 : Finset V),
    #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)
have hmem_left : ∀ {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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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)
have 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)
Tactic: rcases l with l | l
Cleared hypotheses: l, hl, hmem_left
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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)
⊢ (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)
have 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)
Tactic: rcases l with l | l
Cleared hypotheses: l, hl, hmem_left
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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)
⊢ (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)
have 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)
Tactic: rcases r with r | r
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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)
⊢ (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)
have 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)
Tactic: rcases r with r | r
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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)
⊢ (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)
have 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)
Tactic: rcases r with r | r
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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)
⊢ (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)
have 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)
Tactic: rcases r with r | r
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ (Sum.isLeft (β := V) (Sum.inl r) = true → r'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl r) = true → r'.isRight = true)
have 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)
Tactic: rcases r' with r' | r'
Cleared hypotheses: r', hr'