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))
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
    (Sum.isLeft (β := V) (Sum.inl l) = true → l'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl l) = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V} (hr' : r' ∈ right),
    (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)
refine_1 : #left.toLeft = #left
⊢ ∃ (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₁ : #right.toRight = #right
Tactic: refine ⟨left.toLeft, right.toRight, ?_, ?_, fun i hi j hj ↦ ?_⟩
-- 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)
refine_1 : #left.toLeft = #left
refine_1₁ : #right.toRight = #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 refine_1₂ : ∀ (i : V) (hi : i ∈ (↑left.toLeft : Set V)) (j : V) (hj : j ∈ (↑right.toRight : Set V)), G.Adj i j
Tactic: refine ⟨left.toLeft, right.toRight, ?_, ?_, fun i hi j hj ↦ ?_⟩
-- 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)
i : V
hi : i ∈ (↑left.toLeft : Set V)
j : V
hj : j ∈ (↑right.toRight : Set V)
⊢ G.Adj i j
have refine_1 : ∀ (hi : Sum.inl i ∈ left) (j : V) (hj : j ∈ (↑right.toRight : Set V)), G.Adj i j
Tactic: rw [mem_coe, mem_toLeft] at hi
Cleared hypotheses: hi, j, hj
-- 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
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)
⊢ G.Adj i j
have hj₁ : Sum.inr j ∈ right
Tactic: rw [mem_coe, mem_toRight] at hj
Cleared hypotheses: hj
-- 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.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)
have refine_1 : #left.toRight = #left
Tactic: refine ⟨left.toRight, right.toLeft, ?_, ?_, fun i hi j hj ↦ ?_⟩
-- 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.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
⊢ ∃ (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₁ : #right.toLeft = #right
Tactic: refine ⟨left.toRight, right.toLeft, ?_, ?_, fun i hi j hj ↦ ?_⟩
-- 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.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
⊢ ∃ (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₂ : ∀ (i : V) (hi : i ∈ (↑left.toRight : Set V)) (j : V) (hj : j ∈ (↑right.toLeft : Set V)), G.Adj i j
Tactic: refine ⟨left.toRight, right.toLeft, ?_, ?_, fun i hi j hj ↦ ?_⟩
-- 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.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 : Set V)
j : V
hj : j ∈ (↑right.toLeft : Set V)
⊢ G.Adj i j
have refine_1 : ∀ (hi : Sum.inr i ∈ left) (j : V) (hj : j ∈ (↑right.toLeft : Set V)), G.Adj i j
Tactic: rw [mem_coe, mem_toRight] at hi
Cleared hypotheses: hi, j, hj
-- 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
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 : Sum.inr i ∈ left
j : V
hj : j ∈ (↑right.toLeft : Set V)
⊢ G.Adj i j
have hj₁ : Sum.inl j ∈ right
Tactic: rw [mem_coe, mem_toLeft] at hj
Cleared hypotheses: hj
-- 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) (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))
have refine_2 : ∃ (left_1 : Finset (V ⊕ V)) (right_1 : Finset (V ⊕ V)),
  #left_1 = #left ∧
    #right_1 = #right ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left_1 : Set (V ⊕ V)) (↑right_1 : Set (V ⊕ V))
Tactic: simp_rw [← card_left, ← card_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) (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_1 : Finset (V ⊕ V)) (right_1 : Finset (V ⊕ V)),
    #left_1 = #left ∧
      #right_1 = #right ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left_1 : Set (V ⊕ V)) (↑right_1 : Set (V ⊕ V))
have refine_2 : ∀ (i : V ⊕ V) (hi : i ∈ (↑(map Function.Embedding.inl left) : Set (V ⊕ V))) (j : V ⊕ V)
  (hj : j ∈ (↑(map Function.Embedding.inr right) : Set (V ⊕ V))), G.bipartiteDoubleCover.Adj i j
Tactic: refine ⟨left.map .inl, right.map .inr, card_map _, card_map _, fun i hi j hj ↦ ?_⟩
-- 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) (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)
i : V ⊕ V
hi : i ∈ (↑(map Function.Embedding.inl left) : Set (V ⊕ V))
j : V ⊕ V
hj : j ∈ (↑(map Function.Embedding.inr right) : Set (V ⊕ V))
⊢ G.bipartiteDoubleCover.Adj i j
have hi₁ : ∃ a ∈ left, Sum.inl a = i
Tactic: simp_rw [mem_coe, mem_map, Function.Embedding.inl_apply,
      Function.Embedding.inr_apply] at hi hj
Cleared hypotheses: hi, hj
-- 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) (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)
i : V ⊕ V
hi : i ∈ (↑(map Function.Embedding.inl left) : Set (V ⊕ V))
j : V ⊕ V
hj : j ∈ (↑(map Function.Embedding.inr right) : Set (V ⊕ V))
hi₁ : ∃ a ∈ left, Sum.inl a = i
⊢ G.bipartiteDoubleCover.Adj i j
have hj₁ : ∃ a ∈ right, Sum.inr a = j
Tactic: simp_rw [mem_coe, mem_map, Function.Embedding.inl_apply,
      Function.Embedding.inr_apply] at hi hj
Cleared hypotheses: hi, hj
-- 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) (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)
i j : V ⊕ V
hi : ∃ a ∈ left, Sum.inl a = i
hj : ∃ a ∈ right, Sum.inr a = j
⊢ G.bipartiteDoubleCover.Adj i j
have refine_2 : ∀ (i' : V) (hi' : i' ∈ left) (hi : Sum.inl i' = i), G.bipartiteDoubleCover.Adj i j
Tactic: obtain ⟨i', hi', hi⟩ := hi
Cleared hypotheses: hi
-- 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) (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)
i j : V ⊕ V
hj : ∃ a ∈ right, Sum.inr a = j
i' : V
hi' : i' ∈ left
hi : Sum.inl i' = i
⊢ G.bipartiteDoubleCover.Adj i j
have refine_2 : ∀ (j' : V) (hj' : j' ∈ right) (hj : Sum.inr j' = j), G.bipartiteDoubleCover.Adj i j
Tactic: obtain ⟨j', hj', hj⟩ := hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Cayley (goal)
Goal:
M : Type u_1
s : Set M
inst : Mul M
G : SimpleGraph M
⊢ (∀ (v w : M), (mulCayley s).Adj v w → G.Adj v w) ↔ ∀ g ∈ s, ∀ (a : M), a * g ≠ a → G.Adj (a * g) a
have simp : (∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w) ↔ ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a
Tactic: simp only [mulCayley_adj', ne_eq, and_imp, forall_exists_index]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Cayley (goal)
Goal:
M : Type u_1
s : Set M
inst : Mul M
G : SimpleGraph M
⊢ (∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w) ↔ ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a
have mp : (∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w) → ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Cayley (goal)
Goal:
M : Type u_1
s : Set M
inst : Mul M
G : SimpleGraph M
mp :
  (∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w) → ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a
⊢ (∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w) ↔ ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a
have mpr : (∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a) → ∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Cayley (goal)
Goal:
M : Type u_1
s : Set M
inst : MulOneClass M
⊢ mulCayley (s \ {1}) = mulCayley s
have nth_rw : mulCayley (s \ {1}) = mulCayley (s \ {1} ∪ s ∩ {1})
Tactic: nth_rw 2 [← Set.diff_union_inter s {1}]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Cayley (goal)
Goal:
M : Type u_1
s : Set M
inst : MulOneClass M
⊢ mulCayley (s \ {1}) = mulCayley (s \ {1} ∪ s ∩ {1})
have rw : mulCayley (s \ {1}) = mulCayley (s \ {1}) ⊔ mulCayley (s ∩ {1})
Tactic: rw [mulCayley_union]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Cayley (goal)
Goal:
M : Type u_1
s : Set M
inst : MulOneClass M
⊢ mulCayley (s \ {1}) = mulCayley (s \ {1}) ⊔ mulCayley (s ∩ {1})
have Adj : ∀ (u v : M), (mulCayley (s \ {1})).Adj u v ↔ (mulCayley (s \ {1}) ⊔ mulCayley (s ∩ {1})).Adj u v
Tactic: ext u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Cayley (goal)
Goal:
M : Type u_1
inst : MulOneClass M
⊢ Eq (α := SimpleGraph M) (mulCayley {1}) ⊥
have rw : Eq (α := SimpleGraph M) (mulCayley ({1} \ {1})) ⊥
Tactic: rw [← mulCayley_erase_one, Set.diff_self, mulCayley_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Cayley (goal)
Goal:
M : Type u_1
inst : MulOneClass M
rw : Eq (α := SimpleGraph M) (mulCayley ({1} \ {1})) ⊥
⊢ Eq (α := SimpleGraph M) (mulCayley {1}) ⊥
have rw₁ : Eq.{u_1 + 1} (α := SimpleGraph M) (mulCayley ∅) ⊥
Tactic: rw [← mulCayley_erase_one, Set.diff_self, mulCayley_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Cayley (goal)
Goal:
M : Type u_1
inst : MulOneClass M
rw : Eq (α := SimpleGraph M) (mulCayley ({1} \ {1})) ⊥
rw₁ : Eq.{u_1 + 1} (α := SimpleGraph M) (mulCayley ∅) ⊥
⊢ Eq (α := SimpleGraph M) (mulCayley {1}) ⊥
have rw₂ : Eq.{u_1 + 1} (α := SimpleGraph M) ⊥ ⊥
Tactic: rw [← mulCayley_erase_one, Set.diff_self, mulCayley_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Cayley (goal)
Goal:
M : Type u_1
s : Set M
inst : Group M
⊢ mulCayley s⁻¹ = mulCayley s
have Adj : ∀ (u v : M), (mulCayley s⁻¹).Adj u v ↔ (mulCayley s).Adj u v
Tactic: ext u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Cayley (goal)
Goal:
M : Type u_1
inst : Group M
⊢ Eq.{u_1 + 1} (α := SimpleGraph M) (mulCayley Set.univ) ⊤
have Adj : ∀ (x x_1 : M), Adj (mulCayley Set.univ) x x_1 ↔ Adj ⊤ x x_1
Tactic: ext _ _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
⊢ circulantGraph s = circulantGraph (s \ {0})
have Adj : ∀ (u v : G), (circulantGraph s).Adj u v ↔ (circulantGraph (s \ {0})).Adj u v
Tactic: ext (u v : G)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
u v : G
⊢ (circulantGraph s).Adj u v ↔ (circulantGraph (s \ {0})).Adj u v
have Adj : u ≠ v → (u - v ∈ s ∨ v - u ∈ s ↔ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0})
Tactic: simp only [circulantGraph, fromRel_adj, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
u v : G
h : u ≠ v
⊢ u - v ∈ s ∨ v - u ∈ s ↔ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
have Adj : u - v ∈ s ∨ v - u ∈ s → u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
u v : G
h : u ≠ v
Adj : u - v ∈ s ∨ v - u ∈ s → u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
⊢ u - v ∈ s ∨ v - u ∈ s ↔ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
have Adj₁ : u - v ∈ s \ {0} ∨ v - u ∈ s \ {0} → u - v ∈ s ∨ v - u ∈ s
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s ∨ v - u ∈ s
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
have Adj : ∀ (h1 : u - v ∈ s), u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
Tactic: cases h1 with
      | inl h1 => exact Or.inl ⟨h1, sub_ne_zero_of_ne h⟩
      | inr h1 => exact Or.inr ⟨h1, sub_ne_zero_of_ne h.symm⟩
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s ∨ v - u ∈ s
Adj : ∀ (h1 : u - v ∈ s), u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
have Adj₁ : ∀ (h1 : v - u ∈ s), u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
Tactic: cases h1 with
      | inl h1 => exact Or.inl ⟨h1, sub_ne_zero_of_ne h⟩
      | inr h1 => exact Or.inr ⟨h1, sub_ne_zero_of_ne h.symm⟩
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Circulant (goal)
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
⊢ u - v ∈ s ∨ v - u ∈ s
have Adj : ∀ (h1 : u - v ∈ s \ {0}), u - v ∈ s ∨ v - u ∈ s
Tactic: cases h1 with
      | inl h1 => exact Or.inl h1.left
      | inr h1 => exact Or.inr h1.left
Cleared hypotheses: h1