awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
d : G.Dart
⊢ G.dartOfNeighborSet d.toProd.1 (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet d.toProd.1) d.toProd.2 ⋯) = d
have h : (G.dartOfNeighborSet d.toProd.1 (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet d.toProd.1) d.toProd.2 sorry)).toProd.1 =
  d.toProd.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableEq V
d : G.Dart
h :
  (G.dartOfNeighborSet d.toProd.1
          (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet d.toProd.1) d.toProd.2 ⋯)).toProd.1 =
    d.toProd.1
⊢ G.dartOfNeighborSet d.toProd.1 (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet d.toProd.1) d.toProd.2 ⋯) = d
have h₁ : (G.dartOfNeighborSet d.toProd.1 (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet d.toProd.1) d.toProd.2 sorry)).toProd.2 =
  d.toProd.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ Fintype.card.{u} G.Dart = ∑ v : V, G.degree v
have haveI : ∀ (this : DecidableEq V), Fintype.card.{u} G.Dart = ∑ v : V, G.degree v
Tactic: haveI := Classical.decEq V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
this : DecidableEq V
⊢ Fintype.card.{u} G.Dart = ∑ v : V, G.degree v
have simp : card.{u} (α := G.Dart) univ = ∑ x : V, card.{u} (α := G.Dart) {d : G.Dart | d.toProd.1 = x}
Tactic: simp only [← card_univ, ← dart_fst_fiber_card_eq_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
⊢ card.{u} (α := G.Dart) {d : G.Dart | d.edge = e} = 2
have 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
Tactic: obtain ⟨v, w⟩ := e
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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 = Quot.mk (Sym2.Rel V) (v, w)} = 2
have h₁ : 2 = card (α := G.Dart) {d, d.symm}
Tactic: convert! congr_arg card d.edge_fiber
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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 }
⊢ 2 = card (α := G.Dart) {d, d.symm}
have h₁ : d ∉ {d.symm}
Tactic: rw [card_insert_of_notMem, card_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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}
have h₁ : ¬d = d.symm
Tactic: rw [mem_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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.edgeFinset : Set (Sym2 V))
have rw : d.edge ∈ G.edgeSet
Tactic: rw [mem_coe, mem_edgeFinset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ card.{u} (α := G.Dart) univ = 2 * #G.edgeFinset
have rw : ∑ b ∈ G.edgeFinset, card.{u} (α := G.Dart) {a : G.Dart | a.edge = b} = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ ∑ b ∈ G.edgeFinset, card.{u} (α := G.Dart) {a : G.Dart | a.edge = b} = 2 * #G.edgeFinset
have rw : ∀ x ∈ G.edgeFinset, card.{u} (α := G.Dart) {a : G.Dart | a.edge = x} = 2
Tactic: rw [← mul_comm, sum_const_nat]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
e : Sym2 V
h : e ∈ G.edgeFinset
⊢ card.{u} (α := G.Dart) {a : G.Dart | a.edge = e} = 2
have apply : e ∈ G.edgeSet
Tactic: apply G.dart_edge_fiber_card e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ Fintype.card.{u} G.Dart = 2 * #G.edgeFinset
have rw : card.{u} (α := G.Dart) univ = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
⊢ Fintype.card.{u} G.Dart = 2 * #G.edgeFinset
have rw₃ : ∑ b ∈ G.edgeFinset, card.{u} (α := G.Dart) {a : G.Dart | a.edge = b} = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
⊢ Fintype.card.{u} G.Dart = 2 * #G.edgeFinset
have rw₄ : ∀ x ∈ G.edgeFinset, card.{u} (α := G.Dart) {a : G.Dart | a.edge = x} = 2
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
⊢ Fintype.card.{u} G.Dart = 2 * #G.edgeFinset
have rw₆ : ∀ (e : Sym2 V) (h : e ∈ G.edgeFinset), e ∈ G.edgeSet
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ 2 * #G.edgeFinset =
    card.{u} (α := V × V)
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (x, y) => G.Adj x y}
have 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}
Tactic: rw [← dart_card_eq_twice_card_edges, ← card_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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}
have 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)
Tactic: refine card_bij' (fun d _ ↦ (d.fst, d.snd)) (fun xy h ↦ ⟨xy, (mem_filter.1 h).2⟩) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)
⊢ 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}
have 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 := sorry : G.Dart })
      a ha)
Tactic: refine card_bij' (fun d _ ↦ (d.fst, d.snd)) (fun xy h ↦ ⟨xy, (mem_filter.1 h).2⟩) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)
⊢ 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}
have 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 := sorry : G.Dart })
      ((fun (d : G.Dart) (x : Membership.mem (γ := Finset G.Dart) univ d) ↦ (d.toProd.1, d.toProd.2)) a ha) sorry =
    a
Tactic: refine card_bij' (fun d _ ↦ (d.fst, d.snd)) (fun xy h ↦ ⟨xy, (mem_filter.1 h).2⟩) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
⊢ 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}
have 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 := sorry : G.Dart })
        a ha)
      sorry =
    a
Tactic: refine card_bij' (fun d _ ↦ (d.fst, d.snd)) (fun xy h ↦ ⟨xy, (mem_filter.1 h).2⟩) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ ∑ v ∈ G.support.toFinset, G.degree v = 2 * #G.edgeFinset
have simp_rw : Eq (α := ℕ) (∑ v ∈ G.support.toFinsetᶜ, G.degree v) 0
Tactic: simp_rw [← sum_degrees_eq_twice_card_edges,
    ← sum_add_sum_compl G.support.toFinset, left_eq_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ Eq (α := ℕ) (∑ v ∈ G.support.toFinsetᶜ, G.degree v) 0
have h : ∀ x ∈ G.support.toFinsetᶜ, G.degree x = 0
Tactic: apply Finset.sum_eq_zero
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
hv : v ∈ G.support.toFinsetᶜ
⊢ G.degree v = 0
have h : v ∉ G.support
Tactic: rw [degree_eq_zero_iff_notMem_support]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
hv : v ∈ G.support.toFinsetᶜ
⊢ v ∉ G.support
have h : ∀ (hv : v ∉ G.support.toFinset), v ∉ G.support
Tactic: rwa [mem_compl, Set.mem_toFinset] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
⊢ v ∉ G.support
have h₁ : ∀ (hv : v ∉ G.support), v ∉ G.support
Tactic: rwa [mem_compl, Set.mem_toFinset] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ ∑ v ∈ G.support.toFinset, G.degree v = 2 * #G.edgeFinset
have simp_rw : Eq (α := ℕ) (∑ v ∈ G.support.toFinset, G.degree v) (∑ v : V, G.degree v)
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)
⊢ ∑ v ∈ G.support.toFinset, G.degree v = 2 * #G.edgeFinset
have 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)
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)
⊢ ∑ v ∈ G.support.toFinset, G.degree v = 2 * #G.edgeFinset
have simp_rw₂ : Eq (α := ℕ) (∑ v ∈ G.support.toFinsetᶜ, G.degree v) 0
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
⊢ ∑ v ∈ G.support.toFinset, G.degree v = 2 * #G.edgeFinset
have h : ∀ x ∈ G.support.toFinsetᶜ, G.degree x = 0
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
⊢ ∑ v ∈ G.support.toFinset, G.degree v = 2 * #G.edgeFinset
have h₂ : ∀ (v : V) (hv : v ∈ G.support.toFinsetᶜ), v ∉ G.support
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
have 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))
Tactic: have h := congr_arg (fun n => ↑n : ℕ → ZMod 2) G.sum_degrees_eq_twice_card_edges
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (hypothesis)
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))
⊢ Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
have h₁ : Eq (α := ZMod 2) (↑(∑ v : V, G.degree v) : ZMod 2) 0
Tactic: simp only [ZMod.natCast_self, zero_mul, Nat.cast_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (hypothesis)
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
⊢ Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
⊢ Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
have 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)})
Tactic: rw [sum_congr (g := fun _v ↦ (1 : ZMod 2)) rfl] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)})
⊢ Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
have 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
Tactic: rw [sum_congr (g := fun _v ↦ (1 : ZMod 2)) rfl] at h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (hypothesis)
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
⊢ Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
⊢ Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
have rw : Eq (α := ZMod 2) (↑(card.{u} (α := V) {v : V | Odd (G.degree v)}) : ZMod 2) 0
Tactic: rw [← ZMod.natCast_eq_zero_iff_even]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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) {v : V | Odd (G.degree v)}) : ZMod 2) 0
have h₁ : ∀ (x : V), Membership.mem (γ := Finset V) univ x → (Odd (G.degree x) ↔ ¬Eq (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0)
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
⊢ 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
have rw : ¬Even (G.degree v) → ¬Even (G.degree v)
Tactic: rw [mem_filter_univ, Ne, ZMod.natCast_eq_zero_iff_even, ZMod.natCast_eq_one_iff_odd,
        ← Nat.not_even_iff_odd]