awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
refine : ∀ (h : Subsingleton.{u + 1} (SimpleGraph V)), Subsingleton V
⊢ Subsingleton.{u + 1} (SimpleGraph V) ↔ Subsingleton V

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ Unique.instSubsingleton⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
h : Subsingleton.{u + 1} (SimpleGraph V)
contrapose! : ∀ (h : Nontrivial V), Nontrivial.{u} (SimpleGraph V)
⊢ Subsingleton V

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
h : Nontrivial V
⊢ Nontrivial.{u} (SimpleGraph V)

Tactic:
instNontrivial

Premises used: SimpleGraph.instNontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
h : Nontrivial V
⊢ Nontrivial.{u} (SimpleGraph V)

Tactic:
exact instNontrivial

Premises used: SimpleGraph.instNontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
⊢ Nontrivial.{u} (SimpleGraph V) ↔ Nontrivial V

Tactic:
⟨fun h ↦ ?_, fun _ ↦ instNontrivial⟩

Premises used: Iff.intro, SimpleGraph.instNontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
refine : ∀ (h : Nontrivial.{u} (SimpleGraph V)), Nontrivial V
⊢ Nontrivial.{u} (SimpleGraph V) ↔ Nontrivial V

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ instNontrivial⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
h : Nontrivial.{u} (SimpleGraph V)
contrapose! : ∀ (h : Subsingleton V), Subsingleton.{u + 1} (SimpleGraph V)
⊢ Nontrivial V

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
h : Subsingleton V
⊢ Subsingleton.{u + 1} (SimpleGraph V)

Tactic:
Unique.instSubsingleton

Premises used: Unique.instSubsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
h : Subsingleton V
⊢ Subsingleton.{u + 1} (SimpleGraph V)

Tactic:
exact Unique.instSubsingleton

Premises used: Unique.instSubsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ G.neighborSet v = ∅ ↔ G.IsIsolated v

Tactic:
simp [neighborSet, IsIsolated, Set.ext_iff]

Premises used: SimpleGraph.neighborSet, Set.ext_iff, SimpleGraph.IsIsolated
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ (G.neighborSet v).Nonempty ↔ ¬G.IsIsolated v

Tactic:
simp [Set.nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Basic
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ v ∈ G.support ↔ ¬G.IsIsolated v

Tactic:
simp [mem_support, IsIsolated]

Premises used: SimpleGraph.mem_support, SimpleGraph.IsIsolated
-- 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
hadj : G.Adj v w
rw : w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
⊢ v ∈ t ∧ w ∈ s ∨ v ∈ s ∧ w ∈ t

Tactic:
rw [@and_comm (v ∈ t) (w ∈ s), @and_comm (v ∈ s) (w ∈ t)]

Premises used: and_comm
-- 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
hadj : G.Adj v w
⊢ w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s

Tactic:
h.mem_of_adj hadj.symm

Premises used: SimpleGraph.Adj.symm, 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
hadj : G.Adj v w
⊢ w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s

Tactic:
exact h.mem_of_adj hadj.symm

Premises used: SimpleGraph.Adj.symm, SimpleGraph.IsBipartiteWith.mem_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
⊢ G.IsBipartiteWith s t ↔ G.IsBipartiteWith t s

Tactic:
⟨IsBipartiteWith.symm, IsBipartiteWith.symm⟩

Premises used: Iff.intro, SimpleGraph.IsBipartiteWith.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
hadj : G.Adj v w
⊢ v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s

Tactic:
apply h.mem_of_adj at hadj

Premises used: SimpleGraph.IsBipartiteWith.mem_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
hadj : v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s
⊢ v ∉ t

Tactic:
have nhv : v ∉ t := Set.disjoint_left.mp h.disjoint hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
hadj : v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s
nhv : v ∉ t
⊢ w ∈ t

Tactic:
simpa [hv, nhv] using hadj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
h₁ : ∀ (w : V), w ∈ G.neighborSet v ↔ Membership.mem (γ := Set V) {w : V | w ∈ t ∧ G.Adj v w} w
⊢ G.neighborSet v = {w : V | w ∈ t ∧ G.Adj v w}

Tactic:
ext w
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
w : V
h₁ : G.Adj v w → w ∈ t
⊢ w ∈ G.neighborSet v ↔ Membership.mem (γ := Set V) {w : V | w ∈ t ∧ G.Adj v w} w

Tactic:
rw [mem_neighborSet, Set.mem_setOf_eq, iff_and_self]

Premises used: Set.mem_setOf_eq, SimpleGraph.mem_neighborSet, iff_and_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
w : V
⊢ G.Adj v w → w ∈ t

Tactic:
h.mem_of_mem_adj hv

Premises used: SimpleGraph.IsBipartiteWith.mem_of_mem_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
w : V
⊢ G.Adj v w → w ∈ t

Tactic:
exact h.mem_of_mem_adj hv

Premises used: SimpleGraph.IsBipartiteWith.mem_of_mem_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
rw : {w : V | w ∈ t ∧ G.Adj v w} ⊆ t
⊢ G.neighborSet v ⊆ t

Tactic:
rw [isBipartiteWith_neighborSet h hv]

Premises used: SimpleGraph.isBipartiteWith_neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
⊢ {w : V | w ∈ t ∧ G.Adj v w} ⊆ t

Tactic:
Set.sep_subset t (G.Adj v ·)

Premises used: SimpleGraph.Adj, Set.sep_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
⊢ {w : V | w ∈ t ∧ G.Adj v w} ⊆ t

Tactic:
exact Set.sep_subset t (G.Adj v ·)

Premises used: SimpleGraph.Adj, Set.sep_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
⊢ Disjoint (G.neighborSet v) s

Tactic:
Set.disjoint_of_subset_left (isBipartiteWith_neighborSet_subset h hv) h.disjoint.symm

Premises used: Set.disjoint_of_subset_left, SimpleGraph.IsBipartiteWith.disjoint, Disjoint.symm, SimpleGraph.isBipartiteWith_neighborSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
hadj : G.Adj v w
⊢ v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s

Tactic:
apply h.mem_of_adj at hadj

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

Tactic:
have nhw : w ∉ s := Set.disjoint_right.mp h.disjoint hw
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
hadj : v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s
nhw : w ∉ s
⊢ v ∈ s

Tactic:
simpa [hw, nhw] using hadj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
h₁ : ∀ (v : V), v ∈ G.neighborSet w ↔ Membership.mem (γ := Set V) {v : V | v ∈ s ∧ G.Adj v w} v
⊢ G.neighborSet w = {v : V | v ∈ s ∧ G.Adj v w}

Tactic:
ext v
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
v : V
h₁ : G.Adj v w → v ∈ s
⊢ v ∈ G.neighborSet w ↔ Membership.mem (γ := Set V) {v : V | v ∈ s ∧ G.Adj v w} v

Tactic:
rw [mem_neighborSet, adj_comm, Set.mem_setOf_eq, iff_and_self]

Premises used: Set.mem_setOf_eq, SimpleGraph.mem_neighborSet, iff_and_self, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
v : V
⊢ G.Adj v w → v ∈ s

Tactic:
h.mem_of_mem_adj' hw

Premises used: SimpleGraph.IsBipartiteWith.mem_of_mem_adj'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
v : V
⊢ G.Adj v w → v ∈ s

Tactic:
exact h.mem_of_mem_adj' hw

Premises used: SimpleGraph.IsBipartiteWith.mem_of_mem_adj'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
rw : {v : V | v ∈ s ∧ G.Adj v w} ⊆ s
⊢ G.neighborSet w ⊆ s

Tactic:
rw [isBipartiteWith_neighborSet' h hw]

Premises used: SimpleGraph.isBipartiteWith_neighborSet'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
⊢ {v : V | v ∈ s ∧ G.Adj v w} ⊆ s

Tactic:
Set.sep_subset s (G.Adj · w)

Premises used: SimpleGraph.Adj, Set.sep_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
⊢ {v : V | v ∈ s ∧ G.Adj v w} ⊆ s

Tactic:
exact Set.sep_subset s (G.Adj · w)

Premises used: SimpleGraph.Adj, Set.sep_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v : V
this :
  ∀ (w : V)
    (hadj :
      Membership.mem (γ := SetRel V V)
        {x : V × V |
          match (motive := V × V → Prop) x with
          | (u, v) => G.Adj u v}
        (v, w)),
    v ∈ s ∪ t
⊢ v ∈ G.support → v ∈ s ∪ t

Tactic:
⟨w, hadj⟩
-- 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
hadj :
  Membership.mem (γ := SetRel V V)
    {x : V × V |
      match (motive := V × V → Prop) x with
      | (u, v) => G.Adj u v}
    (v, w)
⊢ v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s

Tactic:
apply h.mem_of_adj at hadj

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
hadj : v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s
inl : v ∈ s → w ∈ t → v ∈ s ∪ t
inr : v ∈ t → w ∈ s → v ∈ s ∪ t
inl₁ : v ∈ s → w ∈ t → v ∈ s ∪ t
inr₁ : v ∈ t → w ∈ s → v ∈ s ∪ t
inl₂ : v ∈ s → w ∈ t → v ∉ s → v ∈ t
inr₂ : v ∈ t → w ∈ s → v ∉ s → v ∈ t
inl₃ : v ∈ s → w ∈ t → v ∉ s → v ∈ t
⊢ v ∈ s ∪ t

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
⊢ Disjoint (G.neighborSet w) t

Tactic:
Set.disjoint_of_subset_left (isBipartiteWith_neighborSet_subset' h hw) h.disjoint

Premises used: Set.disjoint_of_subset_left, SimpleGraph.IsBipartiteWith.disjoint, SimpleGraph.isBipartiteWith_neighborSet_subset'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hv : v ∈ s
h₁ : ∀ (w : V), w ∈ G.neighborFinset v ↔ w ∈ {w ∈ t | G.Adj v w}
⊢ G.neighborFinset v = {w ∈ t | G.Adj v w}

Tactic:
ext w
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hv : v ∈ s
w : V
h₁ : G.Adj v w → w ∈ t
⊢ w ∈ G.neighborFinset v ↔ w ∈ {w ∈ t | G.Adj v w}

Tactic:
rw [mem_neighborFinset, mem_filter, iff_and_self]

Premises used: SimpleGraph.mem_neighborFinset, Finset.mem_filter, iff_and_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hv : v ∈ s
w : V
⊢ G.Adj v w → w ∈ t

Tactic:
h.mem_of_mem_adj hv

Premises used: SimpleGraph.IsBipartiteWith.mem_of_mem_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hv : v ∈ s
w : V
⊢ G.Adj v w → w ∈ t

Tactic:
exact h.mem_of_mem_adj hv

Premises used: SimpleGraph.IsBipartiteWith.mem_of_mem_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet w) : Type u_1)
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hw : w ∈ t
h₁ : ∀ (v : V), v ∈ G.neighborFinset w ↔ v ∈ {v ∈ s | G.Adj v w}
⊢ G.neighborFinset w = {v ∈ s | G.Adj v w}

Tactic:
ext v
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet w) : Type u_1)
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hw : w ∈ t
v : V
h₁ : G.Adj v w → v ∈ s
⊢ v ∈ G.neighborFinset w ↔ v ∈ {v ∈ s | G.Adj v w}

Tactic:
rw [mem_neighborFinset, adj_comm, mem_filter, iff_and_self]

Premises used: SimpleGraph.mem_neighborFinset, Finset.mem_filter, iff_and_self, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet w) : Type u_1)
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hw : w ∈ t
v : V
⊢ G.Adj v w → v ∈ s

Tactic:
h.mem_of_mem_adj' hw

Premises used: SimpleGraph.IsBipartiteWith.mem_of_mem_adj'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet w) : Type u_1)
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hw : w ∈ t
v : V
⊢ G.Adj v w → v ∈ s

Tactic:
exact h.mem_of_mem_adj' hw

Premises used: SimpleGraph.IsBipartiteWith.mem_of_mem_adj'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hv : v ∈ s
rw : {w ∈ t | G.Adj v w} = bipartiteAbove G.Adj t v
rw₁ rw₂ : {w ∈ t | G.Adj v w} = {b ∈ t | G.Adj v b}
⊢ G.neighborFinset v = bipartiteAbove G.Adj t v

Tactic:
rw [isBipartiteWith_neighborFinset h hv, bipartiteAbove]

Premises used: Finset.bipartiteAbove, SimpleGraph.isBipartiteWith_neighborFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet w) : Type u_1)
inst_1 : DecidableRel G.Adj
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hw : w ∈ t
rw : {v ∈ s | G.Adj v w} = bipartiteBelow G.Adj s w
rw₁ rw₂ : {v ∈ s | G.Adj v w} = {a ∈ s | G.Adj a w}
⊢ G.neighborFinset w = bipartiteBelow G.Adj s w

Tactic:
rw [isBipartiteWith_neighborFinset' h hw, bipartiteBelow]

Premises used: Finset.bipartiteBelow, SimpleGraph.isBipartiteWith_neighborFinset'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hv : v ∈ s
rw : {w ∈ t | G.Adj v w} ⊆ t
⊢ G.neighborFinset v ⊆ t

Tactic:
rw [isBipartiteWith_neighborFinset h hv]

Premises used: SimpleGraph.isBipartiteWith_neighborFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hv : v ∈ s
⊢ {w ∈ t | G.Adj v w} ⊆ t

Tactic:
filter_subset (G.Adj v ·) t

Premises used: SimpleGraph.Adj, Finset.filter_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hv : v ∈ s
⊢ {w ∈ t | G.Adj v w} ⊆ t

Tactic:
exact filter_subset (G.Adj v ·) t

Premises used: SimpleGraph.Adj, Finset.filter_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hv : v ∈ s
rw rw₁ rw₂ : {w ∈ t | G.Adj v w} ⊆ t
⊢ G.neighborFinset v ⊆ t

Tactic:
classical
  rw [isBipartiteWith_neighborFinset h hv]
  exact filter_subset (G.Adj v ·) t
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hv : v ∈ s
rw : Disjoint (G.neighborSet v) (↑s : Set V)
⊢ Disjoint (G.neighborFinset v) s

Tactic:
rw [neighborFinset_def, ← disjoint_coe, Set.coe_toFinset]

Premises used: Finset.disjoint_coe, SimpleGraph.neighborFinset_def, Set.coe_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hv : v ∈ s
⊢ Disjoint (G.neighborSet v) (↑s : Set V)

Tactic:
isBipartiteWith_neighborSet_disjoint h hv

Premises used: SimpleGraph.isBipartiteWith_neighborSet_disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hv : v ∈ s
⊢ Disjoint (G.neighborSet v) (↑s : Set V)

Tactic:
exact isBipartiteWith_neighborSet_disjoint h hv

Premises used: SimpleGraph.isBipartiteWith_neighborSet_disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hv : v ∈ s
⊢ #(G.neighborFinset v) ≤ #t

Tactic:
card_le_card (isBipartiteWith_neighborFinset_subset h hv)

Premises used: Finset.card_le_card, SimpleGraph.isBipartiteWith_neighborFinset_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hv : v ∈ s
⊢ #(G.neighborFinset v) ≤ #t

Tactic:
exact card_le_card (isBipartiteWith_neighborFinset_subset h hv)

Premises used: Finset.card_le_card, SimpleGraph.isBipartiteWith_neighborFinset_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet w) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hw : w ∈ t
rw : {v ∈ s | G.Adj v w} ⊆ s
⊢ G.neighborFinset w ⊆ s

Tactic:
rw [isBipartiteWith_neighborFinset' h hw]

Premises used: SimpleGraph.isBipartiteWith_neighborFinset'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet w) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hw : w ∈ t
⊢ {v ∈ s | G.Adj v w} ⊆ s

Tactic:
filter_subset (G.Adj · w) s

Premises used: SimpleGraph.Adj, Finset.filter_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet w) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hw : w ∈ t
⊢ {v ∈ s | G.Adj v w} ⊆ s

Tactic:
exact filter_subset (G.Adj · w) s

Premises used: SimpleGraph.Adj, Finset.filter_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet w) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hw : w ∈ t
rw rw₁ rw₂ : {v ∈ s | G.Adj v w} ⊆ s
⊢ G.neighborFinset w ⊆ s

Tactic:
classical
  rw [isBipartiteWith_neighborFinset' h hw]
  exact filter_subset (G.Adj · w) s
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet w) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hw : w ∈ t
rw : Disjoint (G.neighborSet w) (↑t : Set V)
⊢ Disjoint (G.neighborFinset w) t

Tactic:
rw [neighborFinset_def, ← disjoint_coe, Set.coe_toFinset]

Premises used: Finset.disjoint_coe, SimpleGraph.neighborFinset_def, Set.coe_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet w) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hw : w ∈ t
⊢ Disjoint (G.neighborSet w) (↑t : Set V)

Tactic:
isBipartiteWith_neighborSet_disjoint' h hw

Premises used: SimpleGraph.isBipartiteWith_neighborSet_disjoint'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet w) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hw : w ∈ t
⊢ Disjoint (G.neighborSet w) (↑t : Set V)

Tactic:
exact isBipartiteWith_neighborSet_disjoint' h hw

Premises used: SimpleGraph.isBipartiteWith_neighborSet_disjoint'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet w) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hw : w ∈ t
⊢ #(G.neighborFinset w) ≤ #s

Tactic:
card_le_card (isBipartiteWith_neighborFinset_subset' h hw)

Premises used: Finset.card_le_card, SimpleGraph.isBipartiteWith_neighborFinset_subset'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst : Fintype (↑(G.neighborSet w) : Type u_1)
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
hw : w ∈ t
⊢ #(G.neighborFinset w) ≤ #s

Tactic:
exact card_le_card (isBipartiteWith_neighborFinset_subset' h hw)

Premises used: Finset.card_le_card, SimpleGraph.isBipartiteWith_neighborFinset_subset'
-- 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.attach, #(G.neighborFinset (↑x : V))) (∑ x ∈ t.attach, #(G.neighborFinset (↑x : V)))
⊢ Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ w ∈ t, G.degree w)

Tactic:
simp_rw [← sum_attach t, ← sum_attach s, ← card_neighborFinset_eq_degree]

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 : G.LocallyFinite
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
rhs : fun (x : ↥s) ↦ #(G.neighborFinset (↑x : V))
| ∑ x ∈ s.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)
v : ↥s
h₁ : #(bipartiteAbove G.Adj t (↑v : V))
| #(G.neighborFinset (↑v : V))

Tactic:
rw [isBipartiteWith_bipartiteAbove h v.prop]

Premises used: Subtype.prop, SimpleGraph.isBipartiteWith_bipartiteAbove
-- 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₁ : ∀ (v : ↥s), #(bipartiteAbove G.Adj t (↑v : V))
| ∑ x ∈ s.attach, #(G.neighborFinset (↑x : V))

Tactic:
rhs; intro v
    rw [isBipartiteWith_bipartiteAbove h v.prop]