-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
lemma odd_card_iff_odd_components [Finite V] : Odd (Nat.card V) ↔
    Odd {c : ConnectedComponent G | Odd c.supp.ncard}.ncard

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd (∑ u : G.ConnectedComponent, #u.supp.toFinset) ↔ Odd {c | Odd c.supp.ncard}.ncard

Tactic:
simp_rw [Set.toFinset_card, ← Nat.card_eq_fintype_card, ← Finset.coe_filter_univ,
  Set.ncard_coe_Finset, Set.Nat.card_coe_set_eq]

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd (∑ x : G.ConnectedComponent, x.supp.ncard) ↔ Odd #(filter (fun x => Odd x.supp.ncard) univ)

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
⊢ Odd (Nat.card V) ↔ Odd {c | Odd c.supp.ncard}.ncard

Tactic:
classical
cases nonempty_fintype V
rw [Nat.card_eq_fintype_card]
simp only [← (set_fintype_card_eq_univ_iff _).mpr G.iUnion_connectedComponentSupp,
  ConnectedComponent.mem_supp_iff, Fintype.card_subtype_compl,
  ← Set.toFinset_card, Set.toFinset_iUnion ConnectedComponent.supp]
rw [Finset.card_biUnion
  (fun x _ y _ hxy ↦ Set.disjoint_toFinset.mpr (pairwise_disjoint_supp_connectedComponent _ hxy))]
simp_rw [Set.toFinset_card, ← Nat.card_eq_fintype_card, ← Finset.coe_filter_univ,
  Set.ncard_coe_Finset, Set.Nat.card_coe_set_eq]
exact (Finset.odd_sum_iff_odd_card_odd (fun x : G.ConnectedComponent ↦ x.supp.ncard))

Result:
no goals

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd (Fintype.card V) ↔ Odd {c | Odd c.supp.ncard}.ncard

Tactic:
simp only [← (set_fintype_card_eq_univ_iff _).mpr G.iUnion_connectedComponentSupp,
  ConnectedComponent.mem_supp_iff, Fintype.card_subtype_compl,
  ← Set.toFinset_card, Set.toFinset_iUnion ConnectedComponent.supp]

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd #(univ.biUnion fun x => x.supp.toFinset) ↔ Odd {c | Odd c.supp.ncard}.ncard

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
⊢ Odd (Nat.card V) ↔ Odd {c | Odd c.supp.ncard}.ncard

Tactic:
cases nonempty_fintype V

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd (Nat.card V) ↔ Odd {c | Odd c.supp.ncard}.ncard

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd (∑ x : G.ConnectedComponent, x.supp.ncard) ↔ Odd #(filter (fun x => Odd x.supp.ncard) univ)

Tactic:
exact (Finset.odd_sum_iff_odd_card_odd (fun x : G.ConnectedComponent ↦ x.supp.ncard))

Result:
no goals

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd #(univ.biUnion fun x => x.supp.toFinset) ↔ Odd {c | Odd c.supp.ncard}.ncard

Tactic:
rw [Finset.card_biUnion
  (fun x _ y _ hxy ↦ Set.disjoint_toFinset.mpr (pairwise_disjoint_supp_connectedComponent _ hxy))]

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd (∑ u : G.ConnectedComponent, #u.supp.toFinset) ↔ Odd {c | Odd c.supp.ncard}.ncard

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd (Nat.card V) ↔ Odd {c | Odd c.supp.ncard}.ncard

Tactic:
rw [Nat.card_eq_fintype_card]

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd (Fintype.card V) ↔ Odd {c | Odd c.supp.ncard}.ncard