awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
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 ∪ t
have hadj₁ : v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s
Tactic: apply h.mem_of_adj at hadj
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ v ∈ s ∪ t
have inl : v ∈ s → w ∈ t → v ∈ s ∪ t
Tactic: tauto
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ v ∈ s ∪ t
have inr : v ∈ t → w ∈ s → v ∈ s ∪ t
Tactic: tauto
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ v ∈ s ∪ t
have inl₂ : v ∈ s → w ∈ t → v ∉ s → v ∈ t
Tactic: tauto
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ v ∈ s ∪ t
have inr₂ : v ∈ t → w ∈ s → v ∉ s → v ∈ t
Tactic: tauto
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ G.neighborFinset v = {w ∈ t | G.Adj v w}
have h₁ : ∀ (w : V), w ∈ G.neighborFinset v ↔ w ∈ {w ∈ t | G.Adj v w}
Tactic: ext w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ w ∈ G.neighborFinset v ↔ w ∈ {w ∈ t | G.Adj v w}
have h₁ : G.Adj v w → w ∈ t
Tactic: rw [mem_neighborFinset, mem_filter, iff_and_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ G.neighborFinset w = {v ∈ s | G.Adj v w}
have h₁ : ∀ (v : V), v ∈ G.neighborFinset w ↔ v ∈ {v ∈ s | G.Adj v w}
Tactic: ext v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ v ∈ G.neighborFinset w ↔ v ∈ {v ∈ s | G.Adj v w}
have h₁ : G.Adj v w → v ∈ s
Tactic: rw [mem_neighborFinset, adj_comm, mem_filter, iff_and_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ G.neighborFinset v = bipartiteAbove G.Adj t v
have rw : {w ∈ t | G.Adj v w} = bipartiteAbove G.Adj t v
Tactic: rw [isBipartiteWith_neighborFinset h hv, bipartiteAbove]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ G.neighborFinset v = bipartiteAbove G.Adj t v
have rw₁ : {w ∈ t | G.Adj v w} = {b ∈ t | G.Adj v b}
Tactic: rw [isBipartiteWith_neighborFinset h hv, bipartiteAbove]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ G.neighborFinset w = bipartiteBelow G.Adj s w
have rw : {v ∈ s | G.Adj v w} = bipartiteBelow G.Adj s w
Tactic: rw [isBipartiteWith_neighborFinset' h hw, bipartiteBelow]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ G.neighborFinset w = bipartiteBelow G.Adj s w
have rw₁ : {v ∈ s | G.Adj v w} = {a ∈ s | G.Adj a w}
Tactic: rw [isBipartiteWith_neighborFinset' h hw, bipartiteBelow]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
have rw : {w ∈ t | G.Adj v w} ⊆ t
Tactic: rw [isBipartiteWith_neighborFinset h hv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
have rw : {w ∈ t | G.Adj v w} ⊆ t
Tactic: classical
  rw [isBipartiteWith_neighborFinset h hv]
  exact filter_subset (G.Adj v ·) t
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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.neighborFinset v) s
have rw : Disjoint (G.neighborSet v) (↑s : Set V)
Tactic: rw [neighborFinset_def, ← disjoint_coe, Set.coe_toFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
have rw : {v ∈ s | G.Adj v w} ⊆ s
Tactic: rw [isBipartiteWith_neighborFinset' h hw]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
have rw : {v ∈ s | G.Adj v w} ⊆ s
Tactic: classical
  rw [isBipartiteWith_neighborFinset' h hw]
  exact filter_subset (G.Adj · w) s
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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.neighborFinset w) t
have rw : Disjoint (G.neighborSet w) (↑t : Set V)
Tactic: rw [neighborFinset_def, ← disjoint_coe, Set.coe_toFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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 (α := ℕ) (∑ v ∈ s, G.degree v) (∑ w ∈ t, G.degree w)
have simp_rw : Eq (α := ℕ) (∑ x ∈ s.attach, #(G.neighborFinset (↑x : V))) (∑ x ∈ t.attach, #(G.neighborFinset (↑x : V)))
Tactic: simp_rw [← sum_attach t, ← sum_attach s, ← card_neighborFinset_eq_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : G.LocallyFinite
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
| ∑ x ∈ s.attach, #(G.neighborFinset (↑x : V))
have rhs : fun (x : ↥s) ↦ #(G.neighborFinset (↑x : V))
Tactic: rhs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
| #(G.neighborFinset (↑v : V))
have h₁ : #(bipartiteAbove G.Adj t (↑v : V))
Tactic: rw [isBipartiteWith_bipartiteAbove h v.prop]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : G.LocallyFinite
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
| ∑ x ∈ s.attach, #(G.neighborFinset (↑x : V))
have h₁ : ∀ (v : ↥s), #(bipartiteAbove G.Adj t (↑v : V))
Tactic: rhs; intro v
    rw [isBipartiteWith_bipartiteAbove h v.prop]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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.attach, #(G.neighborFinset (↑x : V))) (∑ x ∈ t.attach, #(G.neighborFinset (↑x : V)))
have conv_lhs : Eq (α := ℕ) (∑ v ∈ s.attach, #(bipartiteAbove G.Adj t (↑v : V))) (∑ x ∈ t.attach, #(G.neighborFinset (↑x : V)))
Tactic: conv_lhs =>
    rhs; intro v
    rw [isBipartiteWith_bipartiteAbove h v.prop]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : G.LocallyFinite
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
| ∑ x ∈ t.attach, #(G.neighborFinset (↑x : V))
have rhs : fun (x : ↥t) ↦ #(G.neighborFinset (↑x : V))
Tactic: rhs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
| #(G.neighborFinset (↑w : V))
have h₁ : #(bipartiteBelow G.Adj s (↑w : V))
Tactic: rw [isBipartiteWith_bipartiteBelow h w.prop]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst : G.LocallyFinite
h : G.IsBipartiteWith (↑s : Set V) (↑t : Set V)
| ∑ x ∈ t.attach, #(G.neighborFinset (↑x : V))
have h₁ : ∀ (w : ↥t), #(bipartiteBelow G.Adj s (↑w : V))
Tactic: rhs; intro w
    rw [isBipartiteWith_bipartiteBelow h w.prop]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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 (α := ℕ) (∑ v ∈ s.attach, #(bipartiteAbove G.Adj t (↑v : V))) (∑ x ∈ t.attach, #(G.neighborFinset (↑x : V)))
have conv_rhs : Eq (α := ℕ) (∑ v ∈ s.attach, #(bipartiteAbove G.Adj t (↑v : V))) (∑ w ∈ t.attach, #(bipartiteBelow G.Adj s (↑w : V)))
Tactic: conv_rhs =>
    rhs; intro w
    rw [isBipartiteWith_bipartiteBelow h w.prop]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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 (α := ℕ) (∑ v ∈ s.attach, #(bipartiteAbove G.Adj t (↑v : V))) (∑ w ∈ t.attach, #(bipartiteBelow G.Adj s (↑w : V)))
have simp_rw : Eq (α := ℕ) (∑ x ∈ s, #(bipartiteAbove G.Adj t x)) (∑ x ∈ t, #(bipartiteBelow G.Adj s x))
Tactic: simp_rw [sum_attach s fun w ↦ #(bipartiteAbove G.Adj t w),
    sum_attach t fun v ↦ #(bipartiteBelow G.Adj s v)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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 (α := ℕ) (∑ v ∈ s, G.degree v) (∑ w ∈ t, G.degree w)
have simp_rw : Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ x ∈ t.attach, G.degree (↑x : V))
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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))
⊢ Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ w ∈ t, G.degree w)
have simp_rw₁ : Eq (α := ℕ) (∑ x ∈ s.attach, G.degree (↑x : V)) (∑ x ∈ t.attach, G.degree (↑x : V))
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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))
⊢ Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ w ∈ t, G.degree w)
have simp_rw₂ : Eq (α := ℕ) (∑ x ∈ s.attach, #(G.neighborFinset (↑x : V))) (∑ x ∈ t.attach, #(G.neighborFinset (↑x : V)))
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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)))
⊢ Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ w ∈ t, G.degree w)
have simp_rw₃ : Eq (α := ℕ) (∑ v ∈ s.attach, #(bipartiteAbove G.Adj t (↑v : V))) (∑ x ∈ t.attach, #(G.neighborFinset (↑x : V)))
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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)))
⊢ Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ w ∈ t, G.degree w)
have simp_rw₄ : Eq (α := ℕ) (∑ v ∈ s.attach, #(bipartiteAbove G.Adj t (↑v : V))) (∑ w ∈ t.attach, #(bipartiteBelow G.Adj s (↑w : V)))
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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)))
⊢ Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ w ∈ t, G.degree w)
have simp_rw₅ : Eq (α := ℕ) (∑ x ∈ s, #(bipartiteAbove G.Adj t x)) (∑ x ∈ t, #(bipartiteBelow G.Adj s x))
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
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)
⊢ ∑ v ∈ s ∪ t, G.degree v = 2 * #G.edgeFinset
have hsub : G.support ⊆ (↑s : Set V) ∪ (↑t : Set V)
Tactic: have hsub : G.support ⊆ ↑s ∪ ↑t := isBipartiteWith_support_subset h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
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)
⊢ ∑ v ∈ s ∪ t, G.degree v = 2 * #G.edgeFinset
have hsub₁ : G.support.toFinset ⊆ s ∪ t
Tactic: rw [← coe_union, ← Set.toFinset_subset] at hsub
Cleared hypotheses: hsub
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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 ∈ s ∪ t, G.degree v = 2 * #G.edgeFinset
have rw : ∀ x ∈ s ∪ t, x ∉ G.support.toFinset → G.degree x = 0
Tactic: rw [← Finset.sum_subset hsub, ← sum_degrees_support_eq_twice_card_edges]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ G.degree v = 0
have rwa : ∀ (hv : v ∉ G.support), G.degree v = 0
Tactic: rwa [Set.mem_toFinset, ← degree_eq_zero_iff_notMem_support] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ G.degree v = 0
have rwa₁ : ∀ (hv : G.degree v = 0), G.degree v = 0
Tactic: rwa [Set.mem_toFinset, ← degree_eq_zero_iff_notMem_support] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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 ∈ s, G.degree v = #G.edgeFinset
have rw : Eq (α := ℕ) (∑ v ∈ s, G.degree v) (∑ x ∈ t, G.degree x)
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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 ∈ s, G.degree v = #G.edgeFinset
have rw : HMul.hMul (α := ℕ) 2 (∑ v ∈ s, G.degree v) = 2 * #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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ ∑ v ∈ s, G.degree v = #G.edgeFinset
have rw₁ : HMul.hMul (α := ℕ) 2 (∑ v ∈ s, G.degree v) = ∑ v ∈ s ∪ t, G.degree v
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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
⊢ ∑ v ∈ s, G.degree v = #G.edgeFinset
have rw₂ : HMul.hMul (α := ℕ) 2 (∑ v ∈ s, G.degree v) = HAdd.hAdd (α := ℕ) (∑ x ∈ s, G.degree x) (∑ x ∈ t, G.degree x)
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
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)
⊢ ∑ v ∈ s, G.degree v = #G.edgeFinset
have 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)
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