awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : G.LocallyFinite
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
conv_lhs :
  Eq (α := ℕ) (∑ v ∈ s.attach, #(bipartiteAbove G.Adj t (↑v : V))) (∑ x ∈ t.attach, #(G.neighborFinset (↑x : V)))
⊢ Eq (α := ℕ) (∑ x ∈ s.attach, #(G.neighborFinset (↑x : V))) (∑ x ∈ t.attach, #(G.neighborFinset (↑x : V)))

Tactic:
conv_lhs =>
    rhs; intro v
    rw [isBipartiteWith_bipartiteAbove h v.prop]
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : G.LocallyFinite
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
rhs : fun (x : ↥t) ↦ #(G.neighborFinset (↑x : V))
| ∑ x ∈ t.attach, #(G.neighborFinset (↑x : V))

Tactic:
rhs
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : G.LocallyFinite
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
w : ↥t
h₁ : #(bipartiteBelow G.Adj s (↑w : V))
| #(G.neighborFinset (↑w : V))

Tactic:
rw [isBipartiteWith_bipartiteBelow h w.prop]

Premises used: SimpleGraph.isBipartiteWith_bipartiteBelow, Subtype.prop
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : G.LocallyFinite
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
h₁ : ∀ (w : ↥t), #(bipartiteBelow G.Adj s (↑w : V))
| ∑ x ∈ t.attach, #(G.neighborFinset (↑x : V))

Tactic:
rhs; intro w
    rw [isBipartiteWith_bipartiteBelow h w.prop]
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : G.LocallyFinite
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
conv_rhs :
  Eq (α := ℕ) (∑ v ∈ s.attach, #(bipartiteAbove G.Adj t (↑v : V))) (∑ w ∈ t.attach, #(bipartiteBelow G.Adj s (↑w : V)))
⊢ Eq (α := ℕ) (∑ v ∈ s.attach, #(bipartiteAbove G.Adj t (↑v : V))) (∑ x ∈ t.attach, #(G.neighborFinset (↑x : V)))

Tactic:
conv_rhs =>
    rhs; intro w
    rw [isBipartiteWith_bipartiteBelow h w.prop]
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : G.LocallyFinite
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
simp_rw : Eq (α := ℕ) (∑ x ∈ s, #(bipartiteAbove G.Adj t x)) (∑ x ∈ t, #(bipartiteBelow G.Adj s x))
⊢ Eq (α := ℕ) (∑ v ∈ s.attach, #(bipartiteAbove G.Adj t (↑v : V))) (∑ w ∈ t.attach, #(bipartiteBelow G.Adj s (↑w : V)))

Tactic:
simp_rw [sum_attach s fun w ↦ #(bipartiteAbove G.Adj t w),
    sum_attach t fun v ↦ #(bipartiteBelow G.Adj s v)]

Premises used: SimpleGraph.Adj, Finset.bipartiteAbove, Finset.sum_attach, Finset.card, Finset.bipartiteBelow
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : G.LocallyFinite
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
⊢ Eq (α := ℕ) (∑ x ∈ s, #(bipartiteAbove G.Adj t x)) (∑ x ∈ t, #(bipartiteBelow G.Adj s x))

Tactic:
sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow G.Adj

Premises used: Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow, SimpleGraph.Adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : G.LocallyFinite
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
⊢ Eq (α := ℕ) (∑ x ∈ s, #(bipartiteAbove G.Adj t x)) (∑ x ∈ t, #(bipartiteBelow G.Adj s x))

Tactic:
exact sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow G.Adj

Premises used: Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow, SimpleGraph.Adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : G.LocallyFinite
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
simp_rw : Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ x ∈ t.attach, G.degree (↑x : V))
simp_rw₁ : Eq (α := ℕ) (∑ x ∈ s.attach, G.degree (↑x : V)) (∑ x ∈ t.attach, G.degree (↑x : V))
simp_rw₂ : Eq (α := ℕ) (∑ x ∈ s.attach, #(G.neighborFinset (↑x : V))) (∑ x ∈ t.attach, #(G.neighborFinset (↑x : V)))
simp_rw₃ :
  Eq (α := ℕ) (∑ v ∈ s.attach, #(bipartiteAbove G.Adj t (↑v : V))) (∑ x ∈ t.attach, #(G.neighborFinset (↑x : V)))
simp_rw₄ :
  Eq (α := ℕ) (∑ v ∈ s.attach, #(bipartiteAbove G.Adj t (↑v : V))) (∑ w ∈ t.attach, #(bipartiteBelow G.Adj s (↑w : V)))
simp_rw₅ : Eq (α := ℕ) (∑ x ∈ s, #(bipartiteAbove G.Adj t x)) (∑ x ∈ t, #(bipartiteBelow G.Adj s x))
⊢ Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ w ∈ t, G.degree w)

Tactic:
classical
  simp_rw [← sum_attach t, ← sum_attach s, ← card_neighborFinset_eq_degree]
  conv_lhs =>
    rhs; intro v
    rw [isBipartiteWith_bipartiteAbove h v.prop]
  conv_rhs =>
    rhs; intro w
    rw [isBipartiteWith_bipartiteBelow h w.prop]
  simp_rw [sum_attach s fun w ↦ #(bipartiteAbove G.Adj t w),
    sum_attach t fun v ↦ #(bipartiteBelow G.Adj s v)]
  exact sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow G.Adj

Premises used: Finset.sum_attach, SimpleGraph.card_neighborFinset_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
⊢ G.support ⊆ (↑s : Set V) ∪ (↑t : Set V)

Tactic:
have hsub : G.support ⊆ ↑s ∪ ↑t := isBipartiteWith_support_subset h
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hsub : G.support ⊆ (↑s : Set V) ∪ (↑t : Set V)
⊢ G.support.toFinset ⊆ s ∪ t

Tactic:
rw [← coe_union, ← Set.toFinset_subset] at hsub

Premises used: Set.toFinset_subset, Finset.coe_union
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hsub : G.support.toFinset ⊆ s ∪ t
rw : ∀ x ∈ s ∪ t, x ∉ G.support.toFinset → G.degree x = 0
⊢ ∑ v ∈ s ∪ t, G.degree v = 2 * #G.edgeFinset

Tactic:
rw [← Finset.sum_subset hsub, ← sum_degrees_support_eq_twice_card_edges]

Premises used: SimpleGraph.sum_degrees_support_eq_twice_card_edges, Finset.sum_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hsub : G.support.toFinset ⊆ s ∪ t
v : V
_ : v ∈ s ∪ t → v ∉ G.support.toFinset → G.degree v = 0
⊢ v ∈ s ∪ t → v ∉ G.support.toFinset → G.degree v = 0

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hsub : G.support.toFinset ⊆ s ∪ t
v : V
h_1 : v ∈ s ∪ t
hv : v ∉ G.support.toFinset
rwa : ∀ (hv : v ∉ G.support), G.degree v = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hv : G.degree v = 0), G.degree v = 0
⊢ G.degree v = 0

Tactic:
rwa [Set.mem_toFinset, ← degree_eq_zero_iff_notMem_support] at hv

Premises used: SimpleGraph.degree_eq_zero_iff_notMem_support, Set.mem_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
rw : Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ x ∈ t, G.degree x)
⊢ ∑ v ∈ s, G.degree v = #G.edgeFinset

Tactic:
rw [← Nat.mul_left_cancel_iff zero_lt_two, ← isBipartiteWith_sum_degrees_eq_twice_card_edges h,
    sum_union (disjoint_coe.mp h.disjoint), two_mul, add_right_inj]

Premises used: Nat.mul_left_cancel_iff, Finset.disjoint_coe, two_mul, Finset.sum_union, SimpleGraph.IsBipartiteWith.disjoint, Iff.mp, zero_lt_two, add_right_inj, SimpleGraph.isBipartiteWith_sum_degrees_eq_twice_card_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
⊢ Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ x ∈ t, G.degree x)

Tactic:
isBipartiteWith_sum_degrees_eq h

Premises used: SimpleGraph.isBipartiteWith_sum_degrees_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
⊢ Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ x ∈ t, G.degree x)

Tactic:
exact isBipartiteWith_sum_degrees_eq h

Premises used: SimpleGraph.isBipartiteWith_sum_degrees_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
rw : HMul.hMul (α := ℕ) 2 (∑ v ∈ s, G.degree v) = 2 * #G.edgeFinset
rw₁ : HMul.hMul (α := ℕ) 2 (∑ v ∈ s, G.degree v) = ∑ v ∈ s ∪ t, G.degree v
rw₂ : HMul.hMul (α := ℕ) 2 (∑ v ∈ s, G.degree v) = HAdd.hAdd (α := ℕ) (∑ x ∈ s, G.degree x) (∑ x ∈ t, G.degree x)
rw₃ :
  HAdd.hAdd (α := ℕ) (∑ v ∈ s, G.degree v) (∑ v ∈ s, G.degree v) =
    HAdd.hAdd (α := ℕ) (∑ x ∈ s, G.degree x) (∑ x ∈ t, G.degree x)
rw₄ rw₅ rw₆ : Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ x ∈ t, G.degree x)
⊢ ∑ v ∈ s, G.degree v = #G.edgeFinset

Tactic:
classical
  rw [← Nat.mul_left_cancel_iff zero_lt_two, ← isBipartiteWith_sum_degrees_eq_twice_card_edges h,
    sum_union (disjoint_coe.mp h.disjoint), two_mul, add_right_inj]
  exact isBipartiteWith_sum_degrees_eq h

Premises used: Nat.mul_left_cancel_iff, two_mul, zero_lt_two, add_right_inj, SimpleGraph.isBipartiteWith_sum_degrees_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
⊢ ∑ v ∈ t, G.degree v = #G.edgeFinset

Tactic:
isBipartiteWith_sum_degrees_eq_card_edges h.symm

Premises used: SimpleGraph.isBipartiteWith_sum_degrees_eq_card_edges, SimpleGraph.IsBipartiteWith.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
h : G.IsBipartite
obtain :
  ∀ (c : V → Fin 2) (hc : ∀ {a b : V}, G.Adj a b → Adj (completeGraph (Fin 2)) (c a) (c b)),
    ∃ (s : Set V) (t : Set V), G.IsBipartiteWith s t
⊢ ∃ (s : Set V) (t : Set V), G.IsBipartiteWith s t

Tactic:
obtain ⟨c, hc⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
c : V → Fin 2
hc : ∀ {a b : V}, G.Adj a b → Adj (completeGraph (Fin 2)) (c a) (c b)
⊢ Disjoint.{u_1} (α := Set V) {v : V | c v = 0} {v : V | c v = 1}

Tactic:
aesop (add simp [Set.disjoint_left])

Premises used: Set.disjoint_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
c : V → Fin 2
hc : ∀ {a b : V}, G.Adj a b → Adj (completeGraph (Fin 2)) (c a) (c b)
refine :
  ∀ ⦃v w : V⦄,
    G.Adj v w →
      Membership.mem (γ := Set V) {v : V | c v = 0} v ∧ Membership.mem (γ := Set V) {v : V | c v = 1} w ∨
        Membership.mem (γ := Set V) {v : V | c v = 1} v ∧ Membership.mem (γ := Set V) {v : V | c v = 0} w
⊢ ∃ (s : Set V) (t : Set V), G.IsBipartiteWith s t

Tactic:
refine ⟨{v | c v = 0}, {v | c v = 1}, by aesop (add simp [Set.disjoint_left]), ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
c : V → Fin 2
hc : ∀ {a b : V}, G.Adj a b → Adj (completeGraph (Fin 2)) (c a) (c b)
v w : V
hvw : G.Adj v w
⊢ Adj (completeGraph (Fin 2)) (c v) (c w)

Tactic:
apply hc at hvw
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
c : V → Fin 2
hc : ∀ {a b : V}, G.Adj a b → Adj (completeGraph (Fin 2)) (c a) (c b)
v w : V
hvw : Adj (completeGraph (Fin 2)) (c v) (c w)
⊢ ¬c v = c w

Tactic:
simp [Set.mem_setOf_eq] at hvw ⊢

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
c : V → Fin 2
hc : ∀ {a b : V}, G.Adj a b → Adj (completeGraph (Fin 2)) (c a) (c b)
v w : V
hvw : ¬c v = c w
⊢ c v = 0 ∧ c w = 1 ∨ c v = 1 ∧ c w = 0

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
⊢ G.IsBipartite

Tactic:
⟨s.indicator 1, fun {v w} hw ↦ ?_⟩

Premises used: Set.indicator, Nonempty.intro, RelHom.mk, SimpleGraph.Colorable, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
refine : ∀ {v w : V} (hw : G.Adj v w), Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
⊢ G.IsBipartite

Tactic:
refine ⟨s.indicator 1, fun {v w} hw ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
inl : ∀ (hs : v ∈ s) (ht : w ∈ t), Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
inr : ∀ (ht : v ∈ t) (hs : w ∈ s), Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
⊢ Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)

Tactic:
obtain (⟨hs, ht⟩ | ⟨ht, hs⟩) := h.2 hw

Premises used: SimpleGraph.IsBipartiteWith.mem_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
hs : v ∈ s
ht : w ∈ t
⊢ w ∉ s

Tactic:
replace ht : _ ∉ s := h.1.subset_compl_left ht
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
hs : v ∈ s
ht : w ∉ s
⊢ Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)

Tactic:
simp [hs, ht]
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
hs : v ∈ s
ht : w ∈ t
inl inl₁ inl₂ inl₃ : ∀ (ht : w ∉ s), Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
⊢ Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)

Tactic:
{ replace ht : _ ∉ s := h.1.subset_compl_left ht; simp [hs, ht] }
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
ht : v ∈ t
hs : w ∈ s
⊢ v ∉ s

Tactic:
replace ht : _ ∉ s := h.1.subset_compl_left ht
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
hs : w ∈ s
ht : v ∉ s
⊢ Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)

Tactic:
simp [hs, ht]
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hw : G.Adj v w
ht : v ∈ t
hs : w ∈ s
inr inr₁ inr₂ inr₃ : ∀ (ht : v ∉ s), Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)
⊢ Adj (V := Fin 2) (completeGraph (Fin 2)) (s.indicator 1 v) (s.indicator 1 w)

Tactic:
{ replace ht : _ ∉ s := h.1.subset_compl_left ht; simp [hs, ht] }
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsBipartite ↔ ∃ (s : Set V) (t : Set V), G.IsBipartiteWith s t

Tactic:
⟨IsBipartite.exists_isBipartiteWith, fun ⟨_, _, h⟩ ↦ h.isBipartite⟩

Premises used: SimpleGraph.IsBipartite, SimpleGraph.IsBipartiteWith.isBipartite, _private.0.SimpleGraph.isBipartite_iff_exists_isBipartiteWith.match_1, Iff.intro, SimpleGraph.IsBipartite.exists_isBipartiteWith
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.chromaticNumber ≤ 2 ↔ G.IsBipartite

Tactic:
chromaticNumber_le_iff_colorable

Premises used: SimpleGraph.chromaticNumber_le_iff_colorable
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
h : G.chromaticNumber = 2
⊢ G.chromaticNumber ≤ 2

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
h : G.chromaticNumber = 2
⊢ 2 ≤ G.chromaticNumber

Tactic:
simp [h]
-- 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)
⊢ Fintype.card.{u_1} ↥left = Fintype.card α

Tactic:
rw [← card_coe] at card_left

Premises used: Fintype.card_coe
-- 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)
card_left₁ : Fintype.card.{u_1} ↥left = Fintype.card α
⊢ #right = Fintype.card β

Tactic:
rw [← card_coe] at card_left

Premises used: Fintype.card_coe
-- 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)
card_left₁ : Fintype.card.{u_1} ↥left = Fintype.card α
card_right₁ : #right = Fintype.card β
⊢ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)

Tactic:
rw [← card_coe] at card_left

Premises used: Fintype.card_coe
-- 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 : Fintype.card.{u_1} ↥left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
⊢ Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)

Tactic:
Function.Embedding.nonempty_of_card_le card_left.symm.le

Premises used: Eq.le, Eq.symm, Function.Embedding.nonempty_of_card_le
-- 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 : Fintype.card.{u_1} ↥left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
⊢ Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)

Tactic:
exact Function.Embedding.nonempty_of_card_le card_left.symm.le

Premises used: Eq.le, Eq.symm, Function.Embedding.nonempty_of_card_le
-- 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)
⊢ Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)

Tactic:
have : Nonempty (α ↪ left) := by
    rw [← card_coe] at card_left
    exact Function.Embedding.nonempty_of_card_le card_left.symm.le
-- 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 : 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)
⊢ Fintype.card.{u_1} ↥right = Fintype.card β

Tactic:
rw [← card_coe] at card_right

Premises used: Fintype.card_coe
-- 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 : 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)
card_right₁ : Fintype.card.{u_1} ↥right = Fintype.card β
⊢ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)

Tactic:
rw [← card_coe] at card_right

Premises used: Fintype.card_coe
-- 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 : 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)
card_right₁ : Fintype.card.{u_1} ↥right = Fintype.card β
h₁ : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
⊢ Nonempty (Function.Embedding.{u_2 + 1, u_1 + 1} α ↥left)

Tactic:
rw [← card_coe] at card_right

Premises used: Fintype.card_coe
-- 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 : Fintype.card.{u_1} ↥right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
this : 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)
⊢ Nonempty (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)

Tactic:
Function.Embedding.nonempty_of_card_le card_right.symm.le

Premises used: Eq.le, Eq.symm, Function.Embedding.nonempty_of_card_le
-- 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 : Fintype.card.{u_1} ↥right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
this : 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)
⊢ Nonempty (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)

Tactic:
exact Function.Embedding.nonempty_of_card_le card_right.symm.le

Premises used: Eq.le, Eq.symm, Function.Embedding.nonempty_of_card_le
-- 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 : 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)
⊢ Nonempty (Function.Embedding.{u_3 + 1, u_1 + 1} β ↥right)

Tactic:
have : Nonempty (β ↪ right) := by
    rw [← card_coe] at card_right
    exact Function.Embedding.nonempty_of_card_le card_right.symm.le