awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
d : G.Dart
⊢ ∃ (x : V) (h : x ∈ G.neighborSet d.toProd.1),
    G.dartOfNeighborSet d.toProd.1 (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet d.toProd.1) x h) = d

Tactic:
exact ⟨_, d.adj, by ext <;> rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
v e : V
he : e ∈ G.neighborSet v
⊢ (G.dartOfNeighborSet v (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) e he)).toProd.1 = v

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
v : V
⊢ card.{u} (α := G.Dart) {d : G.Dart | d.toProd.1 = v} = G.degree v

Tactic:
simpa only [dart_fst_fiber, Finset.card_univ, card_neighborSet_eq_degree] using
    card_image_of_injective univ (G.dartOfNeighborSet_injective v)

Premises used: Finset.card_univ, Finset.univ, SimpleGraph.card_neighborSet_eq_degree, Finset.card_image_of_injective, SimpleGraph.dartOfNeighborSet_injective, SimpleGraph.dart_fst_fiber
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
haveI : ∀ (this : DecidableEq V), Fintype.card.{u} G.Dart = ∑ v : V, G.degree v
⊢ Fintype.card.{u} G.Dart = ∑ v : V, G.degree v

Tactic:
haveI := Classical.decEq V
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
this : DecidableEq V
simp : card.{u} (α := G.Dart) univ = ∑ x : V, card.{u} (α := G.Dart) {d : G.Dart | d.toProd.1 = x}
⊢ Fintype.card.{u} G.Dart = ∑ v : V, G.degree v

Tactic:
simp only [← card_univ, ← dart_fst_fiber_card_eq_degree]

Premises used: Finset.card_univ, SimpleGraph.dart_fst_fiber_card_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
this : DecidableEq V
⊢ Set.MapsTo (fun (d : G.Dart) ↦ d.toProd.1) (↑univ : Set G.Dart) (↑univ : Set V)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
this : DecidableEq V
⊢ card.{u} (α := G.Dart) univ = ∑ x : V, card.{u} (α := G.Dart) {d : G.Dart | d.toProd.1 = x}

Tactic:
exact card_eq_sum_card_fiberwise (by simp)

Premises used: Finset.card_eq_sum_card_fiberwise
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
d d' : G.Dart
⊢ Membership.mem (γ := Finset G.Dart) {d' : G.Dart | d'.edge = d.edge} d' ↔
    Membership.mem (γ := Finset G.Dart) {d, d.symm} d'

Tactic:
simpa using dart_edge_eq_iff d' d

Premises used: SimpleGraph.dart_edge_eq_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
e : Sym2 V
h : e ∈ G.edgeSet
mk :
  ∀ (v w : V) (h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet),
    card.{u} (α := G.Dart) {d : G.Dart | d.edge = Quot.mk (Sym2.Rel V) (v, w)} = 2
⊢ card.{u} (α := G.Dart) {d : G.Dart | d.edge = e} = 2

Tactic:
obtain ⟨v, w⟩ := e
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ card.{u} (α := G.Dart) {d' : G.Dart | d'.edge = d.edge} = card (α := G.Dart) {d, d.symm}

Tactic:
congr_arg card d.edge_fiber

Premises used: SimpleGraph.Dart.edge_fiber, congr_arg, Finset.card
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
h₁ : 2 = card (α := G.Dart) {d, d.symm}
⊢ card.{u} (α := G.Dart) {d : G.Dart | d.edge = Quot.mk (Sym2.Rel V) (v, w)} = 2

Tactic:
convert! congr_arg card d.edge_fiber

Premises used: SimpleGraph.Dart.edge_fiber, congr_arg, Finset.card
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
h₁ : d ∉ {d.symm}
⊢ 2 = card (α := G.Dart) {d, d.symm}

Tactic:
rw [card_insert_of_notMem, card_singleton]

Premises used: Finset.card_insert_of_notMem, Finset.card_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
h₁ : ¬d = d.symm
⊢ d ∉ {d.symm}

Tactic:
rw [mem_singleton]

Premises used: Finset.mem_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ ¬d = d.symm

Tactic:
d.symm_ne.symm

Premises used: SimpleGraph.Dart.symm_ne, Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ ¬d = d.symm

Tactic:
exact d.symm_ne.symm

Premises used: SimpleGraph.Dart.symm_ne, Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
d : G.Dart
_h : d ∈ (↑univ : Set G.Dart)
rw : d.edge ∈ G.edgeSet
⊢ d.edge ∈ (↑G.edgeFinset : Set (Sym2 V))

Tactic:
rw [mem_coe, mem_edgeFinset]

Premises used: SimpleGraph.mem_edgeFinset, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
d : G.Dart
_h : d ∈ (↑univ : Set G.Dart)
⊢ d.edge ∈ G.edgeSet

Tactic:
apply Dart.edge_mem

Premises used: SimpleGraph.Dart.edge_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
rw : ∑ b ∈ G.edgeFinset, card.{u} (α := G.Dart) {a : G.Dart | a.edge = b} = 2 * #G.edgeFinset
⊢ card.{u} (α := G.Dart) univ = 2 * #G.edgeFinset

Tactic:
rw [@card_eq_sum_card_fiberwise _ _ _ Dart.edge _ G.edgeFinset fun d _h =>
      by rw [mem_coe, mem_edgeFinset]; apply Dart.edge_mem]

Premises used: Finset.card_eq_sum_card_fiberwise
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
rw : ∀ x ∈ G.edgeFinset, card.{u} (α := G.Dart) {a : G.Dart | a.edge = x} = 2
⊢ ∑ b ∈ G.edgeFinset, card.{u} (α := G.Dart) {a : G.Dart | a.edge = b} = 2 * #G.edgeFinset

Tactic:
rw [← mul_comm, sum_const_nat]

Premises used: Finset.sum_const_nat, mul_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
e : Sym2 V
h : e ∈ G.edgeFinset
apply : e ∈ G.edgeSet
⊢ card.{u} (α := G.Dart) {a : G.Dart | a.edge = e} = 2

Tactic:
apply G.dart_edge_fiber_card e

Premises used: SimpleGraph.dart_edge_fiber_card
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
e : Sym2 V
h rwa rwa₁ rwa₂ rwa₃ : e ∈ G.edgeFinset
⊢ e ∈ G.edgeSet

Tactic:
rwa [← mem_edgeFinset]

Premises used: SimpleGraph.mem_edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
rw rw₁ rw₂ : card.{u} (α := G.Dart) univ = 2 * #G.edgeFinset
rw₃ : ∑ b ∈ G.edgeFinset, card.{u} (α := G.Dart) {a : G.Dart | a.edge = b} = 2 * #G.edgeFinset
rw₄ rw₅ : ∀ (e : Sym2 V) (h : e ∈ G.edgeFinset), card.{u} (α := G.Dart) {a : G.Dart | a.edge = e} = 2
rw₆ : ∀ (e : Sym2 V) (h : e ∈ G.edgeFinset), e ∈ G.edgeSet
⊢ Fintype.card.{u} G.Dart = 2 * #G.edgeFinset

Tactic:
classical
  rw [← card_univ]
  rw [@card_eq_sum_card_fiberwise _ _ _ Dart.edge _ G.edgeFinset fun d _h =>
      by rw [mem_coe, mem_edgeFinset]; apply Dart.edge_mem]
  rw [← mul_comm, sum_const_nat]
  intro e h
  apply G.dart_edge_fiber_card e
  rwa [← mem_edgeFinset]

Premises used: Finset.card_univ, Finset.sum_const_nat, SimpleGraph.mem_edgeFinset, mul_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ ∑ v : V, G.degree v = 2 * #G.edgeFinset

Tactic:
G.dart_card_eq_sum_degrees.symm.trans G.dart_card_eq_twice_card_edges

Premises used: SimpleGraph.dart_card_eq_twice_card_edges, SimpleGraph.dart_card_eq_sum_degrees, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
rw :
  card.{u} (α := G.Dart) univ =
    card.{u} (α := V × V)
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y}
⊢ 2 * #G.edgeFinset =
    card.{u} (α := V × V)
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y}

Tactic:
rw [← dart_card_eq_twice_card_edges, ← card_univ]

Premises used: Finset.card_univ, SimpleGraph.dart_card_eq_twice_card_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ card.{u} (α := G.Dart) univ =
    card.{u} (α := V × V)
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y}

Tactic:
card_bij' (fun d _ ↦ (d.fst, d.snd)) (fun xy h ↦ ⟨xy, (mem_filter.1 h).2⟩) ?_ ?_ ?_ ?_

Premises used: Prod.mk, Prod.fst, SimpleGraph.Dart.toProd, And.right, Finset.card_bij', Iff.mp, Finset.mem_filter, Prod.snd, SimpleGraph.Dart.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
refine_1 :
  ∀ (a : G.Dart) (ha : Membership.mem (γ := Finset G.Dart) univ a),
    Membership.mem (γ := Finset (V × V))
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y}
      ((fun (d : G.Dart) (x : Membership.mem (γ := Finset G.Dart) univ d) ↦ (d.toProd.1, d.toProd.2)) a ha)
refine_2 :
  ∀ (a : V × V)
    (ha :
      Membership.mem (γ := Finset (V × V))
        {x : V × V |
          match (motive := V × V → Prop) x with
          | (x, y) => G.Adj x y}
        a),
    Membership.mem (γ := Finset G.Dart) univ
      ((fun (xy : V × V)
            (h :
              Membership.mem (γ := Finset (V × V))
                {x : V × V |
                  match (motive := V × V → Prop) x with
                  | (x, y) => G.Adj x y}
                xy) ↦
          { toProd := xy, adj := ⋯ : G.Dart })
        a ha)
refine_3 :
  ∀ (a : G.Dart) (ha : Membership.mem (γ := Finset G.Dart) univ a),
    (fun (xy : V × V)
            (h :
              Membership.mem (γ := Finset (V × V))
                {x : V × V |
                  match (motive := V × V → Prop) x with
                  | (x, y) => G.Adj x y}
                xy) ↦
          { toProd := xy, adj := ⋯ : G.Dart })
        ((fun (d : G.Dart) (x : Membership.mem (γ := Finset G.Dart) univ d) ↦ (d.toProd.1, d.toProd.2)) a ha) ⋯ =
      a
refine_4 :
  ∀ (a : V × V)
    (ha :
      Membership.mem (γ := Finset (V × V))
        {x : V × V |
          match (motive := V × V → Prop) x with
          | (x, y) => G.Adj x y}
        a),
    (fun (d : G.Dart) (x : Membership.mem (γ := Finset G.Dart) univ d) ↦ (d.toProd.1, d.toProd.2))
        ((fun (xy : V × V)
              (h :
                Membership.mem (γ := Finset (V × V))
                  {x : V × V |
                    match (motive := V × V → Prop) x with
                    | (x, y) => G.Adj x y}
                  xy) ↦
            { toProd := xy, adj := ⋯ : G.Dart })
          a ha)
        ⋯ =
      a
⊢ card.{u} (α := G.Dart) univ =
    card.{u} (α := V × V)
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y}

Tactic:
refine card_bij' (fun d _ ↦ (d.fst, d.snd)) (fun xy h ↦ ⟨xy, (mem_filter.1 h).2⟩) ?_ ?_ ?_ ?_

Premises used: Prod.mk, Finset.card_bij'
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ ∀ (a : G.Dart) (ha : Membership.mem (γ := Finset G.Dart) univ a),
    Membership.mem (γ := Finset (V × V))
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y}
      ((fun (d : G.Dart) (x : Membership.mem (γ := Finset G.Dart) univ d) ↦ (d.toProd.1, d.toProd.2)) a ha)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ ∀ (a : V × V)
    (ha :
      Membership.mem (γ := Finset (V × V))
        {x : V × V |
          match (motive := V × V → Prop) x with
          | (x, y) => G.Adj x y}
        a),
    Membership.mem (γ := Finset G.Dart) univ
      ((fun (xy : V × V)
            (h :
              Membership.mem (γ := Finset (V × V))
                {x : V × V |
                  match (motive := V × V → Prop) x with
                  | (x, y) => G.Adj x y}
                xy) ↦
          { toProd := xy, adj := ⋯ : G.Dart })
        a ha)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ ∀ (a : G.Dart) (ha : Membership.mem (γ := Finset G.Dart) univ a),
    (fun (xy : V × V)
            (h :
              Membership.mem (γ := Finset (V × V))
                {x : V × V |
                  match (motive := V × V → Prop) x with
                  | (x, y) => G.Adj x y}
                xy) ↦
          { toProd := xy, adj := ⋯ : G.Dart })
        ((fun (d : G.Dart) (x : Membership.mem (γ := Finset G.Dart) univ d) ↦ (d.toProd.1, d.toProd.2)) a ha) ⋯ =
      a

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ ∀ (a : V × V)
    (ha :
      Membership.mem (γ := Finset (V × V))
        {x : V × V |
          match (motive := V × V → Prop) x with
          | (x, y) => G.Adj x y}
        a),
    (fun (d : G.Dart) (x : Membership.mem (γ := Finset G.Dart) univ d) ↦ (d.toProd.1, d.toProd.2))
        ((fun (xy : V × V)
              (h :
                Membership.mem (γ := Finset (V × V))
                  {x : V × V |
                    match (motive := V × V → Prop) x with
                    | (x, y) => G.Adj x y}
                  xy) ↦
            { toProd := xy, adj := ⋯ : G.Dart })
          a ha)
        ⋯ =
      a

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
simp_rw : Eq (α := ℕ) (∑ v ∈ G.support.toFinsetᶜ, G.degree v) 0
⊢ ∑ v ∈ G.support.toFinset, G.degree v = 2 * #G.edgeFinset

Tactic:
simp_rw [← sum_degrees_eq_twice_card_edges,
    ← sum_add_sum_compl G.support.toFinset, left_eq_add]

Premises used: SimpleGraph.sum_degrees_eq_twice_card_edges, left_eq_add, Set.toFinset, SimpleGraph.support, Finset.sum_add_sum_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : ∀ x ∈ G.support.toFinsetᶜ, G.degree x = 0
⊢ Eq (α := ℕ) (∑ v ∈ G.support.toFinsetᶜ, G.degree v) 0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
hv : v ∈ G.support.toFinsetᶜ
h : v ∉ G.support
⊢ G.degree v = 0

Tactic:
rw [degree_eq_zero_iff_notMem_support]

Premises used: SimpleGraph.degree_eq_zero_iff_notMem_support
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
hv : v ∈ G.support.toFinsetᶜ
h : ∀ (hv : v ∉ G.support.toFinset), v ∉ G.support
h₁ h₂ h₃ h₄ : ∀ (hv : v ∉ G.support), v ∉ G.support
⊢ v ∉ G.support

Tactic:
rwa [mem_compl, Set.mem_toFinset] at hv

Premises used: Finset.mem_compl, Set.mem_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
simp_rw : Eq (α := ℕ) (∑ v ∈ G.support.toFinset, G.degree v) (∑ v : V, G.degree v)
simp_rw₁ :
  ∑ v ∈ G.support.toFinset, G.degree v =
    HAdd.hAdd (α := ℕ) (∑ v ∈ G.support.toFinset, G.degree v) (∑ v ∈ G.support.toFinsetᶜ, G.degree v)
simp_rw₂ : Eq (α := ℕ) (∑ v ∈ G.support.toFinsetᶜ, G.degree v) 0
h h₁ : ∀ (v : V) (hv : v ∈ G.support.toFinsetᶜ), G.degree v = 0
h₂ : ∀ (v : V) (hv : v ∈ G.support.toFinsetᶜ), v ∉ G.support
⊢ ∑ v ∈ G.support.toFinset, G.degree v = 2 * #G.edgeFinset

Tactic:
classical
  simp_rw [← sum_degrees_eq_twice_card_edges,
    ← sum_add_sum_compl G.support.toFinset, left_eq_add]
  apply Finset.sum_eq_zero
  intro v hv
  rw [degree_eq_zero_iff_notMem_support]
  rwa [mem_compl, Set.mem_toFinset] at hv

Premises used: SimpleGraph.sum_degrees_eq_twice_card_edges, left_eq_add, SimpleGraph.degree_eq_zero_iff_notMem_support, Finset.sum_eq_zero, Finset.mem_compl, Set.mem_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ Eq (α := ZMod 2) ((fun (n : ℕ) ↦ ((↑n : ZMod 2) : ZMod 2)) (∑ v : V, G.degree v))
    ((fun (n : ℕ) ↦ ((↑n : ZMod 2) : ZMod 2)) (2 * #G.edgeFinset))

Tactic:
have h := congr_arg (fun n => ↑n : ℕ → ZMod 2) G.sum_degrees_eq_twice_card_edges
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h :
  Eq (α := ZMod 2) ((fun (n : ℕ) ↦ ((↑n : ZMod 2) : ZMod 2)) (∑ v : V, G.degree v))
    ((fun (n : ℕ) ↦ ((↑n : ZMod 2) : ZMod 2)) (2 * #G.edgeFinset))
⊢ Eq (α := ZMod 2) (↑(∑ v : V, G.degree v) : ZMod 2) 0

Tactic:
simp only [ZMod.natCast_self, zero_mul, Nat.cast_mul] at h

Premises used: ZMod.natCast_self, MulZeroClass.zero_mul, Nat.cast_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : Eq (α := ZMod 2) (↑(∑ v : V, G.degree v) : ZMod 2) 0
⊢ Eq (α := ZMod 2) (∑ x : V with Ne (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0, (↑(G.degree x) : ZMod 2)) 0

Tactic:
rw [Nat.cast_sum, ← sum_filter_ne_zero] at h

Premises used: Finset.sum_filter_ne_zero, Nat.cast_sum
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : Eq (α := ZMod 2) (∑ x : V with Ne (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0, (↑(G.degree x) : ZMod 2)) 0
rw :
  ∀ (h : Eq (α := ZMod 2) (∑ _v : V with Ne (α := ZMod 2) (↑(G.degree _v) : ZMod 2) 0, 1) 0),
    Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
rw₁ :
  ∀ (x : V),
    Membership.mem (γ := Finset V) {x : V | Ne (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0} x →
      Eq (α := ZMod 2) (↑(G.degree x) : ZMod 2) 1
⊢ Even (card.{u} (α := V) {v : V | Odd (G.degree v)})

Tactic:
rw [sum_congr (g := fun _v ↦ (1 : ZMod 2)) rfl] at h

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : Eq (α := ZMod 2) (∑ _v : V with Ne (α := ZMod 2) (↑(G.degree _v) : ZMod 2) 0, 1) 0
⊢ Eq (α := ZMod 2) (↑(card.{u} (α := V) {x : V | ¬Eq (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0}) : ZMod 2) 0

Tactic:
simp only [mul_one, nsmul_eq_mul, sum_const, Ne] at h

Premises used: Ne, nsmul_eq_mul, mul_one, Finset.sum_const
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : Eq (α := ZMod 2) (↑(card.{u} (α := V) {x : V | ¬Eq (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0}) : ZMod 2) 0
rw : Eq (α := ZMod 2) (↑(card.{u} (α := V) {v : V | Odd (G.degree v)}) : ZMod 2) 0
⊢ Even (card.{u} (α := V) {v : V | Odd (G.degree v)})

Tactic:
rw [← ZMod.natCast_eq_zero_iff_even]

Premises used: ZMod.natCast_eq_zero_iff_even
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : Eq (α := ZMod 2) (↑(card.{u} (α := V) {x : V | ¬Eq (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0}) : ZMod 2) 0
⊢ Eq (α := ZMod 2) (↑(card.{u} (α := V) {x : V | ¬Eq (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0}) : ZMod 2) 0

Tactic:
h
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : Eq (α := ZMod 2) (↑(card.{u} (α := V) {x : V | ¬Eq (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0}) : ZMod 2) 0
h₁ :
  ∀ (x : V), Membership.mem (γ := Finset V) univ x → (Odd (G.degree x) ↔ ¬Eq (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0)
⊢ Eq (α := ZMod 2) (↑(card.{u} (α := V) {v : V | Odd (G.degree v)}) : ZMod 2) 0

Tactic:
convert! h
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : Eq (α := ZMod 2) (↑(card.{u} (α := V) {x : V | ¬Eq (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0}) : ZMod 2) 0
x : V
h_1 : Membership.mem (γ := Finset V) univ x
⊢ Odd (G.degree x) ↔ ¬Eq (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0

Tactic:
ZMod.natCast_ne_zero_iff_odd.symm

Premises used: ZMod.natCast_ne_zero_iff_odd, Iff.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : Eq (α := ZMod 2) (↑(card.{u} (α := V) {x : V | ¬Eq (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0}) : ZMod 2) 0
x : V
h_1 : Membership.mem (γ := Finset V) univ x
⊢ Odd (G.degree x) ↔ ¬Eq (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0

Tactic:
exact ZMod.natCast_ne_zero_iff_odd.symm

Premises used: ZMod.natCast_ne_zero_iff_odd, Iff.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : Eq (α := ZMod 2) (∑ x : V with Ne (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0, (↑(G.degree x) : ZMod 2)) 0
v : V
rw : ¬Even (G.degree v) → ¬Even (G.degree v)
⊢ Membership.mem (γ := Finset V) {x : V | Ne (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0} v →
    Eq (α := ZMod 2) (↑(G.degree v) : ZMod 2) 1

Tactic:
rw [mem_filter_univ, Ne, ZMod.natCast_eq_zero_iff_even, ZMod.natCast_eq_one_iff_odd,
        ← Nat.not_even_iff_odd]

Premises used: ZMod.natCast_eq_one_iff_odd, Finset.mem_filter_univ, Nat.not_even_iff_odd, Ne, ZMod.natCast_eq_zero_iff_even
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : Eq (α := ZMod 2) (∑ x : V with Ne (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0, (↑(G.degree x) : ZMod 2)) 0
v : V
tauto tauto₁ : ¬Even (G.degree v) → ¬Even (G.degree v)
tauto₂ tauto₃ : ¬Even (G.degree v) → Even (G.degree v) → False
⊢ ¬Even (G.degree v) → ¬Even (G.degree v)

Tactic:
tauto