-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
lemma ConnectedComponent.odd_card_supp_iff_odd_subcomponents [Finite V] {G'}
    (h : G ≤ G') (c' : ConnectedComponent G') :
    Odd c'.supp.ncard ↔
      Odd {c : ConnectedComponent G | c.supp ⊆ c'.supp ∧ Odd c.supp.ncard}.ncard

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd (∑ x ∈ filter (fun c => c.supp ⊆ c'.supp) univ, Fintype.card ↑x.supp) ↔
    Odd (Nat.card ↑{c | c.supp ⊆ c'.supp ∧ Odd (Nat.card ↑c.supp)})

Tactic:
rw [Finset.odd_sum_iff_odd_card_odd, Nat.card_eq_fintype_card, Fintype.card_ofFinset]

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd #(filter (fun x => Odd (Fintype.card ↑x.supp)) (filter (fun c => c.supp ⊆ c'.supp) univ)) ↔
    Odd #(filter (Membership.mem {c | c.supp ⊆ c'.supp ∧ Odd (Nat.card ↑c.supp)}) univ)

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd #((filter (fun c => c.supp ⊆ c'.supp) univ).disjiUnion (fun c => c.supp.toFinset) ⋯) ↔
    Odd (Nat.card ↑{c | c.supp ⊆ c'.supp ∧ Odd (Nat.card ↑c.supp)})

Tactic:
simp only [Finset.card_disjiUnion, Set.toFinset_card]

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd (∑ x ∈ filter (fun c => c.supp ⊆ c'.supp) univ, Fintype.card ↑x.supp) ↔
    Odd (Nat.card ↑{c | c.supp ⊆ c'.supp ∧ Odd (Nat.card ↑c.supp)})

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd #(filter (fun a => a.supp ⊆ c'.supp ∧ Odd (Fintype.card ↑a.supp)) univ) ↔
    Odd #(filter (Membership.mem {c | c.supp ⊆ c'.supp ∧ Odd (Fintype.card ↑c.supp)}) univ)

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
⊢ Odd (Nat.card ↑c'.supp) ↔ Odd (Nat.card ↑{c | c.supp ⊆ c'.supp ∧ Odd (Nat.card ↑c.supp)})

Tactic:
classical
cases nonempty_fintype V
rw [Nat.card_eq_card_toFinset, ← disjiUnion_supp_toFinset_eq_supp_toFinset h]
simp only [Finset.card_disjiUnion, Set.toFinset_card]
rw [Finset.odd_sum_iff_odd_card_odd, Nat.card_eq_fintype_card, Fintype.card_ofFinset]
simp only [Nat.card_eq_fintype_card, Finset.filter_filter]
rfl

Result:
no goals

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd #(filter (fun x => Odd (Fintype.card ↑x.supp)) (filter (fun c => c.supp ⊆ c'.supp) univ)) ↔
    Odd #(filter (Membership.mem {c | c.supp ⊆ c'.supp ∧ Odd (Nat.card ↑c.supp)}) univ)

Tactic:
simp only [Nat.card_eq_fintype_card, Finset.filter_filter]

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd #(filter (fun a => a.supp ⊆ c'.supp ∧ Odd (Fintype.card ↑a.supp)) univ) ↔
    Odd #(filter (Membership.mem {c | c.supp ⊆ c'.supp ∧ Odd (Fintype.card ↑c.supp)}) univ)

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
⊢ Odd c'.supp.ncard ↔ Odd {c | c.supp ⊆ c'.supp ∧ Odd c.supp.ncard}.ncard

Tactic:
simp_rw [← Set.Nat.card_coe_set_eq]

Result:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
⊢ Odd (Nat.card ↑c'.supp) ↔ Odd (Nat.card ↑{c | c.supp ⊆ c'.supp ∧ Odd (Nat.card ↑c.supp)})

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd (Nat.card ↑c'.supp) ↔ Odd (Nat.card ↑{c | c.supp ⊆ c'.supp ∧ Odd (Nat.card ↑c.supp)})

Tactic:
rw [Nat.card_eq_card_toFinset, ← disjiUnion_supp_toFinset_eq_supp_toFinset h]

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd #((filter (fun c => c.supp ⊆ c'.supp) univ).disjiUnion (fun c => c.supp.toFinset) ⋯) ↔
    Odd (Nat.card ↑{c | c.supp ⊆ c'.supp ∧ Odd (Nat.card ↑c.supp)})

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
⊢ Odd (Nat.card ↑c'.supp) ↔ Odd (Nat.card ↑{c | c.supp ⊆ c'.supp ∧ Odd (Nat.card ↑c.supp)})

Tactic:
cases nonempty_fintype V

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd (Nat.card ↑c'.supp) ↔ Odd (Nat.card ↑{c | c.supp ⊆ c'.supp ∧ Odd (Nat.card ↑c.supp)})