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 : Fintype α
inst_1 : Fintype β
h : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
x x_1 : V
hr :
  ∃ (a : β),
    Membership.mem (γ := Finset β) univ a ∧
      ({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := ⋯ : β ↪ V } : (a : β) → V) a = x_1
w : α
left : Membership.mem (γ := Finset α) univ w
hl : ({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := ⋯ : α ↪ V } : (a : α) → V) w = x
⊢ G.Adj x x_1
have replace : ∀ (w : β),
  Membership.mem (γ := Finset β) univ w →
    ∀
      (hr :
        ({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := sorry : β ↪ V } : (a : β) → V) w =
          x_1),
      G.Adj x x_1
Tactic: replace ⟨_, _, hr⟩ := hr
Cleared hypotheses: 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 : Fintype α
inst_1 : Fintype β
h : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
x x_1 : V
w : α
left : Membership.mem (γ := Finset α) univ w
hl : ({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := ⋯ : α ↪ V } : (a : α) → V) w = x
w_1 : β
left_1 : Membership.mem (γ := Finset β) univ w_1
hr : ({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := ⋯ : β ↪ V } : (a : β) → V) w_1 = x_1
⊢ G.Adj x x_1
have rw : G.Adj (({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := sorry : α ↪ V } : (a : α) → V) w)
  (({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := sorry : β ↪ V } : (a : β) → V) w_1)
Tactic: rw [← hl, ← hr]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v_1 w_1 : V
G_1 : SimpleGraph V
s_1 t_1 s t : Set V
G : SimpleGraph V
v w : V
⊢ (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) v w →
    (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) w v
have inl : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v_1 w_1 : V
G_1 : SimpleGraph V
s_1 t_1 s t : Set V
G : SimpleGraph V
v w : V
inl : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
⊢ (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) v w →
    (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) w v
have inr : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v_1 w_1 : V
G_1 : SimpleGraph V
s_1 t_1 s t : Set V
G : SimpleGraph V
v w : V
inl : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₁ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr₁ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
⊢ (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) v w →
    (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) w v
have inl₂ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v_1 w_1 : V
G_1 : SimpleGraph V
s_1 t_1 s t : Set V
G : SimpleGraph V
v w : V
inl : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₁ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr₁ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₂ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
⊢ (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) v w →
    (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) w v
have inl₃ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v_1 w_1 : V
G_1 : SimpleGraph V
s_1 t_1 s t : Set V
G : SimpleGraph V
v w : V
inl : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₁ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr₁ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₂ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₃ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
⊢ (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) v w →
    (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) w v
have inr₂ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v_1 w_1 : V
G_1 : SimpleGraph V
s_1 t_1 s t : Set V
G : SimpleGraph V
v w : V
inl : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₁ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr₁ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₂ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₃ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inr₂ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
⊢ (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) v w →
    (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) w v
have inr₃ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v_1 w_1 : V
G_1 : SimpleGraph V
s_1 t_1 s t : Set V
G : SimpleGraph V
v w : V
inl : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₁ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr₁ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₂ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₃ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inr₂ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₃ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₄ inl₅ inl₆ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₇ inl₈ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
⊢ (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) v w →
    (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) w v
have inl₉ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → w ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v_1 w_1 : V
G_1 : SimpleGraph V
s_1 t_1 s t : Set V
G : SimpleGraph V
v w : V
inl : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₁ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr₁ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₂ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₃ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inr₂ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₃ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₄ inl₅ inl₆ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₇ inl₈ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₉ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → w ∈ t
⊢ (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) v w →
    (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) w v
have inl₁₀ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → v ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v_1 w_1 : V
G_1 : SimpleGraph V
s_1 t_1 s t : Set V
G : SimpleGraph V
v w : V
inl : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₁ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr₁ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₂ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₃ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inr₂ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₃ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₄ inl₅ inl₆ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₇ inl₈ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₉ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → w ∈ t
inl₁₀ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → v ∈ s
inr₄ inr₅ inr₆ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₇ inr₈ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
⊢ (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) v w →
    (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) w v
have inr₉ : G.Adj v w → v ∈ t → w ∈ s → ¬(w ∈ s ∧ v ∈ t) → w ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v_1 w_1 : V
G_1 : SimpleGraph V
s_1 t_1 s t : Set V
G : SimpleGraph V
v w : V
inl : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₁ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr₁ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₂ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₃ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inr₂ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₃ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₄ inl₅ inl₆ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₇ inl₈ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₉ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → w ∈ t
inl₁₀ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → v ∈ s
inr₄ inr₅ inr₆ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₇ inr₈ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inr₉ : G.Adj v w → v ∈ t → w ∈ s → ¬(w ∈ s ∧ v ∈ t) → w ∈ t
⊢ (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) v w →
    (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) w v
have inr₁₀ : G.Adj v w → v ∈ t → w ∈ s → ¬(w ∈ s ∧ v ∈ t) → v ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v_1 w_1 : V
G_1 : SimpleGraph V
s_1 t_1 s t : Set V
G : SimpleGraph V
v w : V
inl : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₁ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr₁ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₂ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₃ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inr₂ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₃ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₄ inl₅ inl₆ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₇ inl₈ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₉ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → w ∈ t
inl₁₀ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → v ∈ s
inr₄ inr₅ inr₆ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₇ inr₈ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inr₉ : G.Adj v w → v ∈ t → w ∈ s → ¬(w ∈ s ∧ v ∈ t) → w ∈ t
inr₁₀ : G.Adj v w → v ∈ t → w ∈ s → ¬(w ∈ s ∧ v ∈ t) → v ∈ s
inl₁₁ inl₁₂ inl₁₃ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inr₁₁ inr₁₂ inr₁₃ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
⊢ (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) v w →
    (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) w v
have inr₁₄ : G.Adj v w → v ∈ t → w ∈ s → w ∉ s → w ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v_1 w_1 : V
G_1 : SimpleGraph V
s_1 t_1 s t : Set V
G : SimpleGraph V
v w : V
inl : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₁ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr₁ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₂ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₃ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inr₂ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₃ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₄ inl₅ inl₆ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₇ inl₈ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₉ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → w ∈ t
inl₁₀ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → v ∈ s
inr₄ inr₅ inr₆ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₇ inr₈ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inr₉ : G.Adj v w → v ∈ t → w ∈ s → ¬(w ∈ s ∧ v ∈ t) → w ∈ t
inr₁₀ : G.Adj v w → v ∈ t → w ∈ s → ¬(w ∈ s ∧ v ∈ t) → v ∈ s
inl₁₁ inl₁₂ inl₁₃ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inr₁₁ inr₁₂ inr₁₃ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₁₄ : G.Adj v w → v ∈ t → w ∈ s → w ∉ s → w ∈ t
⊢ (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) v w →
    (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) w v
have inr₁₅ : G.Adj v w → v ∈ t → w ∈ s → v ∉ t → w ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v_1 w_1 : V
G_1 : SimpleGraph V
s_1 t_1 s t : Set V
G : SimpleGraph V
v w : V
inl : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₁ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr₁ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₂ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₃ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inr₂ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₃ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₄ inl₅ inl₆ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₇ inl₈ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₉ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → w ∈ t
inl₁₀ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → v ∈ s
inr₄ inr₅ inr₆ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₇ inr₈ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inr₉ : G.Adj v w → v ∈ t → w ∈ s → ¬(w ∈ s ∧ v ∈ t) → w ∈ t
inr₁₀ : G.Adj v w → v ∈ t → w ∈ s → ¬(w ∈ s ∧ v ∈ t) → v ∈ s
inl₁₁ inl₁₂ inl₁₃ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inr₁₁ inr₁₂ inr₁₃ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₁₄ : G.Adj v w → v ∈ t → w ∈ s → w ∉ s → w ∈ t
inr₁₅ : G.Adj v w → v ∈ t → w ∈ s → v ∉ t → w ∈ t
⊢ (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) v w →
    (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) w v
have inr₁₆ : G.Adj v w → v ∈ t → w ∈ s → w ∉ s → v ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v_1 w_1 : V
G_1 : SimpleGraph V
s_1 t_1 s t : Set V
G : SimpleGraph V
v w : V
inl : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₁ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inr₁ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v ∧ (w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s)
inl₂ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₃ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inr₂ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₃ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₄ inl₅ inl₆ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inl₇ inl₈ : G.Adj v w → v ∈ s → w ∈ t → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inl₉ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → w ∈ t
inl₁₀ : G.Adj v w → v ∈ s → w ∈ t → ¬(w ∈ s ∧ v ∈ t) → v ∈ s
inr₄ inr₅ inr₆ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₇ inr₈ : G.Adj v w → v ∈ t → w ∈ s → w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
inr₉ : G.Adj v w → v ∈ t → w ∈ s → ¬(w ∈ s ∧ v ∈ t) → w ∈ t
inr₁₀ : G.Adj v w → v ∈ t → w ∈ s → ¬(w ∈ s ∧ v ∈ t) → v ∈ s
inl₁₁ inl₁₂ inl₁₃ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
inr₁₁ inr₁₂ inr₁₃ : G.Adj v w → v ∈ t → w ∈ s → G.Adj w v
inr₁₄ : G.Adj v w → v ∈ t → w ∈ s → w ∉ s → w ∈ t
inr₁₅ : G.Adj v w → v ∈ t → w ∈ s → v ∉ t → w ∈ t
inr₁₆ : G.Adj v w → v ∈ t → w ∈ s → w ∉ s → v ∈ s
⊢ (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) v w →
    (fun (v w : V) ↦ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)) w v
have inr₁₇ : G.Adj v w → v ∈ t → w ∈ s → v ∉ t → v ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s
have pos : ∀ (hw : w ∈ s), G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s
Tactic: by_cases hw : w ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
pos : ∀ (hw : w ∈ s), G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s
have neg : ∀ (hw : w ∉ s), G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s
Tactic: by_cases hw : w ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ
have pos : ∀ (hv : v ∈ s), G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ
Tactic: by_cases hv : v ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
pos : ∀ (hv : v ∈ s), G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ
have neg : ∀ (hv : v ∉ s), G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ
Tactic: by_cases hv : v ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
v : V
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
s : Finset V
inst_2 : DecidableRel G.Adj
hv : v ∈ s
⊢ G.degree v ≤ (between (↑s : Set V) (↑s : Set V)ᶜ G).degree v + #s
have h_bipartite : (between (↑s : Set V) (↑s : Set V)ᶜ G).IsBipartiteWith (↑s : Set V) (↑sᶜ : Set V)
Tactic: have h_bipartite : (G.between s sᶜ).IsBipartiteWith s ↑(sᶜ) := by
    simpa using between_isBipartiteWith disjoint_compl_right
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v : V
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
s : Finset V
inst_2 : DecidableRel G.Adj
hv : v ∈ s
h_bipartite : (between (↑s : Set V) (↑s : Set V)ᶜ G).IsBipartiteWith (↑s : Set V) (↑sᶜ : Set V)
⊢ G.degree v ≤ (between (↑s : Set V) (↑s : Set V)ᶜ G).degree v + #s
have simp_rw : #(G.neighborFinset v) ≤ #((between (↑s : Set V) (↑s : Set V)ᶜ G).neighborFinset v ∪ s)
Tactic: simp_rw [← card_neighborFinset_eq_degree,
    ← card_union_of_disjoint (isBipartiteWith_neighborFinset_disjoint h_bipartite hv)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
w : V
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
s : Finset V
inst_2 : DecidableRel G.Adj
hw : w ∈ sᶜ
⊢ G.degree w ≤ (between (↑s : Set V) (↑s : Set V)ᶜ G).degree w + #sᶜ
have h_bipartite : (between (↑s : Set V) (↑s : Set V)ᶜ G).IsBipartiteWith (↑s : Set V) (↑sᶜ : Set V)
Tactic: have h_bipartite : (G.between s sᶜ).IsBipartiteWith s ↑(sᶜ) := by
    simpa using between_isBipartiteWith disjoint_compl_right
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
w : V
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
s : Finset V
inst_2 : DecidableRel G.Adj
hw : w ∈ sᶜ
h_bipartite : (between (↑s : Set V) (↑s : Set V)ᶜ G).IsBipartiteWith (↑s : Set V) (↑sᶜ : Set V)
⊢ G.degree w ≤ (between (↑s : Set V) (↑s : Set V)ᶜ G).degree w + #sᶜ
have simp_rw : #(G.neighborFinset w) ≤ #((between (↑s : Set V) (↑s : Set V)ᶜ G).neighborFinset w ∪ sᶜ)
Tactic: simp_rw [← card_neighborFinset_eq_degree,
    ← card_union_of_disjoint (isBipartiteWith_neighborFinset_disjoint' h_bipartite hw)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
W₁ : Type u_2
W₂ : Type u_3
⊢ (completeBipartiteGraph W₁ W₂).edgeSet = Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2)
have refine_1 : ∀ (u v : W₁ ⊕ W₂) (h : s(u, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet),
  Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2)) s(u, v)
Tactic: refine Set.ext <| Sym2.ind fun u v ↦ ⟨fun h ↦ ?_, fun ⟨⟨a, b⟩, z⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
W₁ : Type u_2
W₂ : Type u_3
refine_1 :
  ∀ (u v : W₁ ⊕ W₂) (h : s(u, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet),
    Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2)) s(u, v)
⊢ (completeBipartiteGraph W₁ W₂).edgeSet = Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2)
have refine_2 : ∀ (u v : W₁ ⊕ W₂),
  Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2)) s(u, v) →
    ∀ (a : W₁) (b : W₂) (z : (fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2)) (a, b) = s(u, v)),
      s(u, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
Tactic: refine Set.ext <| Sym2.ind fun u v ↦ ⟨fun h ↦ ?_, fun ⟨⟨a, b⟩, z⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
W₁ : Type u_2
W₂ : Type u_3
u v : W₁ ⊕ W₂
h : s(u, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2)) s(u, v)
have refine_1 : ∀ (val : W₁) (h : s(Sum.inl val, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet),
  Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2))
    s(Sum.inl val, v)
Tactic: cases u
Cleared hypotheses: u, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
W₁ : Type u_2
W₂ : Type u_3
u v : W₁ ⊕ W₂
h : s(u, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
refine_1 :
  ∀ (val : W₁) (h : s(Sum.inl val, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet),
    Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2))
      s(Sum.inl val, v)
⊢ Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2)) s(u, v)
have refine_1₁ : ∀ (val : W₂) (h : s(Sum.inr val, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet),
  Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2))
    s(Sum.inr val, v)
Tactic: cases u
Cleared hypotheses: u, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
W₁ : Type u_2
W₂ : Type u_3
v : W₁ ⊕ W₂
val : W₁
h : s(Sum.inl val, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2))
    s(Sum.inl val, v)
have refine_1 : ∀ (val_1 : W₁) (h : s(Sum.inl val, Sum.inl val_1) ∈ (completeBipartiteGraph W₁ W₂).edgeSet),
  Membership.mem (γ := Set (Sym2 (W₁ ⊕ W₂))) (Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2))
    s(Sum.inl val, Sum.inl val_1)
Tactic: cases v
Cleared hypotheses: v, h