awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v w : V ⊕ V
val val_1 : V
he : G.bipartiteDoubleCover.Adj (Sum.inr val) (Sum.inl val_1)
⊢ ∃ (a : V × V) (ha :
    Membership.mem (γ := Finset (V × V))
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y}
      a),
    (fun (x : V × V)
            (x_1 :
              Membership.mem (γ := Finset (V × V))
                {x : V × V |
                  match (motive := V × V → Prop) x with
                  | (x, y) => G.Adj x y}
                x) ↦
          (match (motive :=
              (x : V × V) →
                Membership.mem (γ := Finset (V × V))
                    {x : V × V |
                      match (motive := V × V → Prop) x with
                      | (x, y) => G.Adj x y}
                    x →
                  Sym2 (V ⊕ V))
              x, x_1 with
            | (v, w), x => s(Sum.inl v, Sum.inr w) :
            Sym2 (V ⊕ V)))
        a ha =
      s(Sum.inr val, Sum.inl val_1)

Tactic:
simpa using he.symm

Premises used: SimpleGraph.Adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v w : V ⊕ V
val val_1 : V
he : G.bipartiteDoubleCover.Adj (Sum.inl val) (Sum.inl val_1)
⊢ ∃ (a : V × V) (ha :
    Membership.mem (γ := Finset (V × V))
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y}
      a),
    Eq (α := Sym2 (V ⊕ V))
      ((fun (x : V × V)
            (x_1 :
              Membership.mem (γ := Finset (V × V))
                {x : V × V |
                  match (motive := V × V → Prop) x with
                  | (x, y) => G.Adj x y}
                x) ↦
          (match (motive :=
              (x : V × V) →
                Membership.mem (γ := Finset (V × V))
                    {x : V × V |
                      match (motive := V × V → Prop) x with
                      | (x, y) => G.Adj x y}
                    x →
                  Sym2 (V ⊕ V))
              x, x_1 with
            | (v, w), x => s(Sum.inl v, Sum.inr w) :
            Sym2 (V ⊕ V)))
        a ha)
      s(Sum.inl val, Sum.inl val_1)

Tactic:
simp at he
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v w : V ⊕ V
val val_1 : V
he : G.bipartiteDoubleCover.Adj (Sum.inr val) (Sum.inr val_1)
⊢ ∃ (a : V × V) (ha :
    Membership.mem (γ := Finset (V × V))
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y}
      a),
    Eq (α := Sym2 (V ⊕ V))
      ((fun (x : V × V)
            (x_1 :
              Membership.mem (γ := Finset (V × V))
                {x : V × V |
                  match (motive := V × V → Prop) x with
                  | (x, y) => G.Adj x y}
                x) ↦
          (match (motive :=
              (x : V × V) →
                Membership.mem (γ := Finset (V × V))
                    {x : V × V |
                      match (motive := V × V → Prop) x with
                      | (x, y) => G.Adj x y}
                    x →
                  Sym2 (V ⊕ V))
              x, x_1 with
            | (v, w), x => s(Sum.inl v, Sum.inr w) :
            Sym2 (V ⊕ V)))
        a ha)
      s(Sum.inr val, Sum.inr val_1)

Tactic:
simp at he
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v w : V ⊕ V
he : G.bipartiteDoubleCover.Adj v w
⊢ ∃ (a : V × V) (ha :
    Membership.mem (γ := Finset (V × V))
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y}
      a),
    (fun (x : V × V)
            (x_1 :
              Membership.mem (γ := Finset (V × V))
                {x : V × V |
                  match (motive := V × V → Prop) x with
                  | (x, y) => G.Adj x y}
                x) ↦
          (match (motive :=
              (x : V × V) →
                Membership.mem (γ := Finset (V × V))
                    {x : V × V |
                      match (motive := V × V → Prop) x with
                      | (x, y) => G.Adj x y}
                    x →
                  Sym2 (V ⊕ V))
              x, x_1 with
            | (v, w), x => s(Sum.inl v, Sum.inr w) :
            Sym2 (V ⊕ V)))
        a ha =
      s(v, w)

Tactic:
match v, w with
  | .inl _, .inr _ => simpa using he
  | .inr _, .inl _ => simpa using he.symm
  | .inl _, .inl _ | .inr _, .inr _ => simp at he
-- 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 β
have : ∀ (this : Fintype α), completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G
⊢ completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G

Tactic:
have : Fintype α := .ofFinite α
-- 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 : Fintype α
have : ∀ (this : Fintype β), completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G
⊢ completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G

Tactic:
have : Fintype β := .ofFinite β
-- 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 β
simp_rw :
  (∃ (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 : Finset V) (right : Finset V),
      #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
⊢ completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G

Tactic:
simp_rw [completeBipartiteGraph_isContained_iff]

Premises used: SimpleGraph.completeBipartiteGraph_isContained_iff
-- 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 β
⊢ (∃ (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 : Finset V) (right : Finset V),
      #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)

Tactic:
⟨fun ⟨left, right, card_left, card_right, h⟩ ↦ ?_,
    fun ⟨left, right, card_left, card_right, h⟩ ↦ ?_⟩

Premises used: SimpleGraph.bipartiteDoubleCover, _private.0.SimpleGraph.completeBipartiteGraph_isContained_bipartiteDoubleCover.match_1, Exists, Fintype.card, SimpleGraph.IsCompleteBetween, And, SetLike.coe, Iff.intro, Finset.card, _private.0.SimpleGraph.completeBipartiteGraph_isContained_iff.match_1, Eq
-- 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 β
refine_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))),
      ∃ (left : Finset V) (right : Finset V),
        #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
refine_2 :
  (∃ (left : Finset V) (right : Finset V),
      #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)) →
    ∀ (left right : Finset V) (card_left : #left = Fintype.card α) (card_right : #right = Fintype.card β)
      (h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)),
      ∃ (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 : 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 : Finset V) (right : Finset V),
      #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)

Tactic:
refine ⟨fun ⟨left, right, card_left, card_right, h⟩ ↦ ?_,
    fun ⟨left, right, card_left, card_right, h⟩ ↦ ?_⟩
-- 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))
refine_1 :
  ∃ (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 : Finset V) (right : Finset V),
    #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)

Tactic:
simp_rw [← card_left, ← card_right]
-- 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))
⊢ left.Nonempty

Tactic:
card_pos.mp <| card_pos.trans_le card_left.ge

Premises used: Eq.ge, LT.lt.trans_le, Iff.mp, Finset.card_pos, Fintype.card_pos
-- 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))
refine_1 :
  ∀ (l : V ⊕ V) (hl : l ∈ left),
    ∃ (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:
obtain ⟨l, hl⟩ : left.Nonempty := card_pos.mp <| card_pos.trans_le card_left.ge

Premises used: Eq.ge, LT.lt.trans_le, Iff.mp, Finset.Nonempty, Finset.card_pos, Fintype.card_pos
-- 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
⊢ right.Nonempty

Tactic:
card_pos.mp <| card_pos.trans_le card_right.ge

Premises used: Eq.ge, LT.lt.trans_le, Iff.mp, Finset.card_pos, Fintype.card_pos
-- 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
refine_1 :
  ∀ (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)
⊢ ∃ (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:
obtain ⟨r, hr⟩ : right.Nonempty := card_pos.mp <| card_pos.trans_le card_right.ge

Premises used: Eq.ge, LT.lt.trans_le, Iff.mp, Finset.Nonempty, Finset.card_pos, Fintype.card_pos
-- 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
inl :
  ∀ (l : V) (hl : Sum.inl l ∈ left),
    (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
inr :
  ∀ (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)
⊢ (l.isLeft = true → l'.isLeft = true) ∧ (l.isRight = true → l'.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
l' : V ⊕ V
hl' : l' ∈ left
l : V
hl : Sum.inl l ∈ left
inl :
  ∀ (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)
inl₁ :
  ∀ (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)
⊢ (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → l'.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 ⊕ 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)
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)
⊢ (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
-- 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
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)
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)
⊢ (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → l'.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))
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)
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)
⊢ (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
    (Sum.isRight (β := V) (Sum.inl l) = true → l'.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))
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)
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)
⊢ (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → l'.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))
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)
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)
⊢ (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
    (Sum.isRight (α := V) (Sum.inr l) = true → l'.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))
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:
simp