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
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)
⊢ (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.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: 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.inr r ∈ right
⊢ (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)
have 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)
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.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)
⊢ (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)
have 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)
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.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
⊢ (Sum.isLeft (β := V) (Sum.inl r) = true → r'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl r) = true → r'.isRight = true)
have 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)
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.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)
⊢ (Sum.isLeft (β := V) (Sum.inl r) = true → r'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl r) = true → r'.isRight = true)
have 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)
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.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
⊢ (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)
have 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)
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.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)
⊢ (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)
have 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)
Tactic: rcases r' with r' | r'
Cleared hypotheses: r', hr'
-- 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
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left), (l.isLeft = true → l'.isLeft = true) ∧ (l.isRight = 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)
have hmem_right : ∀ {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'
-- 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)
hmem_right :
  ∀ {r' : V ⊕ V} (hr' : r' ∈ right), (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = 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)
have 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)
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)
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)
⊢ ∃ (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 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)
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
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)
⊢ ∃ (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 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)
Tactic: rcases r with r | r
Cleared hypotheses: r, hr, hmem_right
-- 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
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)
⊢ ∃ (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 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)
Tactic: rcases r with r | r
Cleared hypotheses: r, hr, hmem_right
-- 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
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)
⊢ ∃ (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 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)
Tactic: rcases r with r | r
Cleared hypotheses: r, hr, hmem_right
-- 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
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)
⊢ ∃ (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 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)
Tactic: rcases r with r | r
Cleared hypotheses: r, hr, hmem_right
-- 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
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)
have refine_1 : #left.toLeft = #left
Tactic: refine ⟨left.toLeft, right.toRight, ?_, ?_, fun i hi j hj ↦ ?_⟩