awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
this_1 : Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
fα : Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left :=
  Classical.arbitrary (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)
this : Nonempty (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
fβ : Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right :=
  Classical.arbitrary (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)
f : α ⊕ β ↪ V :=
  {
    toFun :=
      Sum.elim (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left))
        (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)),
    inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isRight = true
hs₂ : s₂.isLeft = true
⊢ G.Adj
    (Function.comp (β := ↥left) (Subtype.val (p := fun (x : V) ↦ x ∈ left)) (⇑fα : (a : α) → ↥left) (s₂.getLeft hs₂))
    (Function.comp (β := ↥right) (Subtype.val (p := fun (x : V) ↦ x ∈ right)) (⇑fβ : (a : β) → ↥right)
      (s₁.getRight hs₁))

Tactic:
exact h (by simp) (by simp)
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
⊢ #(map { toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := ⋯ : α ↪ V } univ) = Fintype.card α

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
⊢ #(map { toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := ⋯ : β ↪ V } univ) = Fintype.card β

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Fintype α
inst_1 : Fintype β
refine :
  completeBipartiteGraph α β ⊑ G →
    ∀ (f : (completeBipartiteGraph α β).Copy G) (x : V)
      (hl :
        x ∈
          (↑(map { toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := ⋯ : α ↪ V } univ) :
            Set V))
      (x_1 : V)
      (hr :
        x_1 ∈
          (↑(map { toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := ⋯ : β ↪ V } univ) :
            Set V)),
      G.Adj x x_1
⊢ completeBipartiteGraph α β ⊑ G →
    ∃ (left : Finset V) (right : Finset V),
      #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)

Tactic:
refine fun ⟨f⟩ ↦ ⟨univ.map ⟨f ∘ Sum.inl, f.injective.comp Sum.inl_injective⟩,
      univ.map ⟨f ∘ Sum.inr, f.injective.comp Sum.inr_injective⟩, by simp, by simp,
      fun _ hl _ hr ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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 : V
hl : x ∈ (↑(map { toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := ⋯ : α ↪ V } univ) : Set V)
x_1 : V
hr :
  x_1 ∈ (↑(map { toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := ⋯ : β ↪ V } univ) : Set V)
rw :
  ∀
    (hl :
      ∃ (a : α),
        Membership.mem (γ := Finset α) univ a ∧
          ({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := ⋯ : α ↪ V } : (a : α) → V) a =
            x)
    (x_2 : V)
    (hr :
      ∃ (a : β),
        Membership.mem (γ := Finset β) univ a ∧
          ({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := ⋯ : β ↪ V } : (a : β) → V) a =
            x_2),
    G.Adj x x_2
⊢ G.Adj x x_1

Tactic:
rw [mem_coe, mem_map] at hl hr

Premises used: Finset.mem_map, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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 : V
hl :
  ∃ (a : α),
    Membership.mem (γ := Finset α) univ a ∧
      ({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := ⋯ : α ↪ V } : (a : α) → V) a = 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
replace :
  ∀ (w : α),
    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
⊢ G.Adj x x_1

Tactic:
replace ⟨_, _, hl⟩ := hl
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
replace :
  ∀ (w : β),
    Membership.mem (γ := Finset β) univ w →
      ∀
        (hr :
          ({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := ⋯ : β ↪ V } : (a : β) → V) w =
            x_1),
        G.Adj x x_1
⊢ G.Adj x x_1

Tactic:
replace ⟨_, _, hr⟩ := hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
rw :
  G.Adj (({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := ⋯ : α ↪ V } : (a : α) → V) w)
    (({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := ⋯ : β ↪ V } : (a : β) → V) w_1)
⊢ G.Adj x x_1

Tactic:
rw [← hl, ← hr]
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
⊢ (completeBipartiteGraph α β).Adj (Sum.inl w) (Sum.inr w_1)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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 (({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inl, inj' := ⋯ : α ↪ V } : (a : α) → V) w)
    (({ toFun := Function.comp (β := α ⊕ β) (⇑f : (a : α ⊕ β) → V) Sum.inr, inj' := ⋯ : β ↪ V } : (a : β) → V) w_1)

Tactic:
exact f.toHom.map_adj (by simp)

Premises used: SimpleGraph.Hom.map_adj, SimpleGraph.Copy.toHom
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
H : G.Subgraph
⊢ Disjoint.{u_1} (α := Set (↑H.verts : Type u_1)) {x : (↑H.verts : Type u_1) | (↑x : V) ∈ s}
    {x : (↑H.verts : Type u_1) | (↑x : V) ∈ t}

Tactic:
grind [h.disjoint]

Premises used: SimpleGraph.IsBipartiteWith.disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsBipartite
H : G.Subgraph
⊢ H.coe.IsBipartite

Tactic:
let ⟨_, _, hst⟩ := isBipartite_iff_exists_isBipartiteWith.mp h
  isBipartite_iff_exists_isBipartiteWith.mpr ⟨_, _, IsBipartiteWith.subgraph hst H⟩

Premises used: Iff.mpr, setOf, Membership.mem, SimpleGraph.IsBipartiteWith.subgraph, SimpleGraph.IsBipartite, SimpleGraph.Subgraph.coe, _private.0.SimpleGraph.isBipartite_iff_exists_isBipartiteWith.match_1, Exists.intro, Iff.mp, Subtype.val, SimpleGraph.isBipartite_iff_exists_isBipartiteWith
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
inr₁₇ : G.Adj v w → v ∈ t → 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
inl₁₇ inl₁₈ : G.Adj v w → v ∈ s → w ∈ t → G.Adj w v
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

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
⊢ (between s t G).Adj v w ↔ G.Adj v w ∧ (v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
⊢ between s t G ≤ G

Tactic:
fun _ _ h ↦ h.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
⊢ between s t G = between t s G

Tactic:
simp [between, or_comm]

Premises used: SimpleGraph.between, or_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
⊢ (between s t G).IsBipartite

Tactic:
(between_isBipartiteWith h).isBipartite

Premises used: SimpleGraph.IsBipartiteWith.isBipartite, SimpleGraph.between_isBipartiteWith
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
neg : ∀ (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

Tactic:
by_cases hw : w ∈ s
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
hw : w ∈ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s

Tactic:
Or.inr hw

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
hw : w ∈ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s

Tactic:
exact Or.inr hw

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
hw : w ∉ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s

Tactic:
Or.inl ⟨hadj, Or.inl ⟨hv, hw⟩⟩

Premises used: And.intro, Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
hw : w ∉ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s

Tactic:
exact Or.inl ⟨hadj, Or.inl ⟨hv, hw⟩⟩

Premises used: Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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ᶜ
neg : ∀ (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ᶜ

Tactic:
by_cases hv : v ∈ s
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∈ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ

Tactic:
Or.inl ⟨hadj, Or.inr ⟨hw, hv⟩⟩

Premises used: And.intro, Or.inl, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∈ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ

Tactic:
exact Or.inl ⟨hadj, Or.inr ⟨hw, hv⟩⟩

Premises used: Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∉ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ

Tactic:
Or.inr hv

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∉ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ

Tactic:
exact Or.inr hv

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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.neighborFinset v ⊆ (between (↑s : Set V) (↑s : Set V)ᶜ G).neighborFinset v ∪ s

Tactic:
simpa [neighborFinset_def] using neighborSet_subset_between_union hv

Premises used: SimpleGraph.neighborSet_subset_between_union, SimpleGraph.neighborFinset_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
⊢ (between (↑s : Set V) (↑s : Set V)ᶜ G).IsBipartiteWith (↑s : Set V) (↑sᶜ : Set V)

Tactic:
simpa using between_isBipartiteWith disjoint_compl_right

Premises used: SimpleGraph.between_isBipartiteWith, disjoint_compl_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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
⊢ (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
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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)
simp_rw : #(G.neighborFinset v) ≤ #((between (↑s : Set V) (↑s : Set V)ᶜ G).neighborFinset v ∪ s)
⊢ G.degree v ≤ (between (↑s : Set V) (↑s : Set V)ᶜ G).degree v + #s

Tactic:
simp_rw [← card_neighborFinset_eq_degree,
    ← card_union_of_disjoint (isBipartiteWith_neighborFinset_disjoint h_bipartite hv)]

Premises used: SimpleGraph.isBipartiteWith_neighborFinset_disjoint, SimpleGraph.card_neighborFinset_eq_degree, Finset.card_union_of_disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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.neighborFinset v) ≤ #((between (↑s : Set V) (↑s : Set V)ᶜ G).neighborFinset v ∪ s)

Tactic:
card_le_card (neighborFinset_subset_between_union hv)

Premises used: Finset.card_le_card, SimpleGraph.neighborFinset_subset_between_union
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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.neighborFinset v) ≤ #((between (↑s : Set V) (↑s : Set V)ᶜ G).neighborFinset v ∪ s)

Tactic:
exact card_le_card (neighborFinset_subset_between_union hv)

Premises used: Finset.card_le_card, SimpleGraph.neighborFinset_subset_between_union
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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ᶜ
⊢ w ∈ (↑s : Set V)ᶜ

Tactic:
simpa using hw
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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.neighborFinset w ⊆ (between (↑s : Set V) (↑s : Set V)ᶜ G).neighborFinset w ∪ sᶜ

Tactic:
simpa [neighborFinset_def] using G.neighborSet_subset_between_union_compl (by simpa using hw)

Premises used: SimpleGraph.neighborSet_subset_between_union_compl, SimpleGraph.neighborFinset_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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ᶜ
⊢ (between (↑s : Set V) (↑s : Set V)ᶜ G).IsBipartiteWith (↑s : Set V) (↑sᶜ : Set V)

Tactic:
simpa using between_isBipartiteWith disjoint_compl_right

Premises used: SimpleGraph.between_isBipartiteWith, disjoint_compl_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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ᶜ
⊢ (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
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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)
simp_rw : #(G.neighborFinset w) ≤ #((between (↑s : Set V) (↑s : Set V)ᶜ G).neighborFinset w ∪ sᶜ)
⊢ G.degree w ≤ (between (↑s : Set V) (↑s : Set V)ᶜ G).degree w + #sᶜ

Tactic:
simp_rw [← card_neighborFinset_eq_degree,
    ← card_union_of_disjoint (isBipartiteWith_neighborFinset_disjoint' h_bipartite hw)]

Premises used: SimpleGraph.isBipartiteWith_neighborFinset_disjoint', SimpleGraph.card_neighborFinset_eq_degree, Finset.card_union_of_disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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.neighborFinset w) ≤ #((between (↑s : Set V) (↑s : Set V)ᶜ G).neighborFinset w ∪ sᶜ)

Tactic:
card_le_card (neighborFinset_subset_between_union_compl hw)

Premises used: Finset.card_le_card, SimpleGraph.neighborFinset_subset_between_union_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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.neighborFinset w) ≤ #((between (↑s : Set V) (↑s : Set V)ᶜ G).neighborFinset w ∪ sᶜ)

Tactic:
exact card_le_card (neighborFinset_subset_between_union_compl hw)

Premises used: Finset.card_le_card, SimpleGraph.neighborFinset_subset_between_union_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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)

Tactic:
Set.ext <| Sym2.ind fun u v ↦ ⟨fun h ↦ ?_, fun ⟨⟨a, b⟩, z⟩ ↦ ?_⟩

Premises used: Set.ext, Sym2.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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)
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
⊢ (completeBipartiteGraph W₁ W₂).edgeSet = Set.range fun (x : W₁ × W₂) ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
refine Set.ext <| Sym2.ind fun u v ↦ ⟨fun h ↦ ?_, fun ⟨⟨a, b⟩, z⟩ ↦ ?_⟩

Premises used: Set.ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
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)
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)
⊢ 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:
cases u
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
W₁ : Type u_2
W₂ : Type u_3
v : W₁ ⊕ W₂
val : W₁
h : s(Sum.inl val, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
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)
refine_1₁ :
  ∀ (val_1 : W₂) (h : s(Sum.inl val, Sum.inr 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.inr val_1)
⊢ 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 v