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.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
j : V
hj : j ∈ left.toLeft
⊢ Eq.{u_1 + 1} (α := V ⊕ V) ((fun (i : V) (x : i ∈ left.toLeft) ↦ (Sum.inl i : V ⊕ V)) i hi)
      ((fun (i : V) (x : i ∈ left.toLeft) ↦ (Sum.inl i : V ⊕ V)) j hj) →
    i = j

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
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 ⊕ V
hi : i ∈ left
⊢ ∃ (ha : i.getLeft ⋯ ∈ left.toLeft), (fun (i : V) (x : i ∈ left.toLeft) ↦ (Sum.inl i : V ⊕ V)) (i.getLeft ⋯) ha = i

Tactic:
simp [hi]
-- 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.toLeft = #left

Tactic:
exact card_bij (fun i _ ↦ .inl i) (fun i hi ↦ by simpa using hi) (fun i hi j hj ↦ by simp)
          (fun i hi ↦ ⟨i.getLeft <| (hmem_left hi).left Sum.isLeft_inl, by simp [hi]⟩)

Premises used: Finset.card_bij, 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)
j : V
hj : j ∈ right.toRight
⊢ (fun (j : V) (hj : j ∈ right.toRight) ↦ (Sum.inr j : V ⊕ V)) j hj ∈ right

Tactic:
simpa using 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 ∈ right.toRight
j : V
hj : j ∈ right.toRight
⊢ Eq.{u_1 + 1} (α := V ⊕ V) ((fun (j : V) (hj : j ∈ right.toRight) ↦ (Sum.inr j : V ⊕ V)) i hi)
      ((fun (j : V) (hj : j ∈ right.toRight) ↦ (Sum.inr j : V ⊕ V)) j hj) →
    i = j

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
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)
j : V ⊕ V
hj : j ∈ right
⊢ ∃ (ha : j.getRight ⋯ ∈ right.toRight),
    (fun (j : V) (hj : j ∈ right.toRight) ↦ (Sum.inr j : V ⊕ V)) (j.getRight ⋯) ha = j

Tactic:
simp [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)
⊢ #right.toRight = #right

Tactic:
exact card_bij (fun j hj ↦ .inr j) (fun j hj ↦ by simpa using hj) (fun i hi j hj ↦ by simp)
          (fun j hj ↦ ⟨j.getRight <| (hmem_right hj).right Sum.isRight_inr, by simp [hj]⟩)

Premises used: Finset.card_bij, 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)
i : V
hi : i ∈ (↑left.toLeft : Set V)
j : V
hj : j ∈ (↑right.toRight : Set V)
refine_1 : ∀ (hi : Sum.inl i ∈ left) (j : V) (hj : j ∈ (↑right.toRight : Set V)), G.Adj i j
⊢ G.Adj i j

Tactic:
rw [mem_coe, mem_toLeft] at hi

Premises used: Finset.mem_toLeft, Finset.mem_coe
-- 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 : Sum.inl i ∈ left
j : V
hj : j ∈ (↑right.toRight : Set V)
⊢ Sum.inr j ∈ right

Tactic:
rw [mem_coe, mem_toRight] at hj

Premises used: Finset.mem_toRight, Finset.mem_coe
-- 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 : Sum.inl i ∈ left
j : V
hj : Sum.inr j ∈ right
⊢ G.Adj i j

Tactic:
simpa using h hi 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.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
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:
⟨left.toRight, right.toLeft, ?_, ?_, 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.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
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)
refine_1 : #left.toRight = #left
refine_1₁ : #right.toLeft = #right
refine_1₂ : ∀ (i : V) (hi : i ∈ (↑left.toRight : Set V)) (j : V) (hj : j ∈ (↑right.toLeft : 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.toRight, right.toLeft, ?_, ?_, 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.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
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)
i : V
hi : i ∈ left.toRight
⊢ (fun (i : V) (x : i ∈ left.toRight) ↦ (Sum.inr i : V ⊕ V)) i hi ∈ left

Tactic:
simpa using hi
-- 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
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)
i : V
hi : i ∈ left.toRight
j : V
hj : j ∈ left.toRight
⊢ Eq.{u_1 + 1} (α := V ⊕ V) ((fun (i : V) (x : i ∈ left.toRight) ↦ (Sum.inr i : V ⊕ V)) i hi)
      ((fun (i : V) (x : i ∈ left.toRight) ↦ (Sum.inr i : V ⊕ V)) j hj) →
    i = j

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
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)
i : V ⊕ V
hi : i ∈ left
⊢ ∃ (ha : i.getRight ⋯ ∈ left.toRight), (fun (i : V) (x : i ∈ left.toRight) ↦ (Sum.inr i : V ⊕ V)) (i.getRight ⋯) ha = i

Tactic:
simp [hi]
-- 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
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.toRight = #left

Tactic:
exact card_bij (fun i _ ↦ .inr i) (fun i hi ↦ by simpa using hi) (fun i hi j hj ↦ by simp)
          (fun i hi ↦ ⟨i.getRight <| (hmem_left hi).right Sum.isRight_inr, by simp [hi]⟩)

Premises used: Finset.card_bij, 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.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
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)
j : V
hj : j ∈ right.toLeft
⊢ (fun (j : V) (hj : j ∈ right.toLeft) ↦ (Sum.inl j : V ⊕ V)) j hj ∈ right

Tactic:
simpa using 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.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
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)
i : V
hi : i ∈ right.toLeft
j : V
hj : j ∈ right.toLeft
⊢ Eq.{u_1 + 1} (α := V ⊕ V) ((fun (j : V) (hj : j ∈ right.toLeft) ↦ (Sum.inl j : V ⊕ V)) i hi)
      ((fun (j : V) (hj : j ∈ right.toLeft) ↦ (Sum.inl j : V ⊕ V)) j hj) →
    i = j

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
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)
j : V ⊕ V
hj : j ∈ right
⊢ ∃ (ha : j.getLeft ⋯ ∈ right.toLeft), (fun (j : V) (hj : j ∈ right.toLeft) ↦ (Sum.inl j : V ⊕ V)) (j.getLeft ⋯) ha = j

Tactic:
simp [hj]