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

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
aux : ∀ (c : G'.ConnectedComponent), Odd c.supp.ncard → {c' | c'.supp ⊆ c.supp ∧ Odd c'.supp.ncard}.Nonempty
f : ↑{c | Odd (Nat.card ↑c.supp)} → ↑{c | Odd (Nat.card ↑c.supp)} :=
  fun x =>
    match x with
    | ⟨c, hc⟩ => ⟨Exists.choose ⋯, ⋯⟩
c c' : ↑{c | Odd c.supp.ncard}
fcc' : Exists.choose ⋯ = Exists.choose ⋯
⊢ c = c'

Tactic:
exact Subtype.val_injective (ConnectedComponent.eq_of_common_vertex
  ((fcc' ▸ (aux c.1 c.2).choose_spec.1) (ConnectedComponent.nonempty_supp _).some_mem)
    ((aux c'.1 c'.2).choose_spec.1 (ConnectedComponent.nonempty_supp _).some_mem))

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
aux : ∀ (c : G'.ConnectedComponent), Odd c.supp.ncard → {c' | c'.supp ⊆ c.supp ∧ Odd c'.supp.ncard}.Nonempty
f : ↑{c | Odd (Nat.card ↑c.supp)} → ↑{c | Odd (Nat.card ↑c.supp)} :=
  fun x =>
    match x with
    | ⟨c, hc⟩ => ⟨Exists.choose ⋯, ⋯⟩
c c' : ↑{c | Odd c.supp.ncard}
fcc' : f c = f c'
⊢ c = c'

Tactic:
simp only [Subtype.mk.injEq, f] at fcc'

Result:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
aux : ∀ (c : G'.ConnectedComponent), Odd c.supp.ncard → {c' | c'.supp ⊆ c.supp ∧ Odd c'.supp.ncard}.Nonempty
f : ↑{c | Odd (Nat.card ↑c.supp)} → ↑{c | Odd (Nat.card ↑c.supp)} :=
  fun x =>
    match x with
    | ⟨c, hc⟩ => ⟨Exists.choose ⋯, ⋯⟩
c c' : ↑{c | Odd c.supp.ncard}
fcc' : Exists.choose ⋯ = Exists.choose ⋯
⊢ c = c'

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

Tactic:
simpa [-Nat.card_eq_fintype_card, -Set.coe_setOf, h']
  using (c.odd_card_supp_iff_odd_subcomponents _ h).mp hc

Result:
no goals

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

Tactic:
refine Set.nonempty_of_ncard_ne_zero fun h' ↦ ?_

Result:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c : G'.ConnectedComponent
hc : Odd c.supp.ncard
h' : {c' | c'.supp ⊆ c.supp ∧ Odd c'.supp.ncard}.ncard = 0
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
aux : ∀ (c : G'.ConnectedComponent), Odd c.supp.ncard → {c' | c'.supp ⊆ c.supp ∧ Odd c'.supp.ncard}.Nonempty
⊢ {c | Odd c.supp.ncard}.ncard ≤ {c | Odd c.supp.ncard}.ncard

Tactic:
let f : {c : ConnectedComponent G' | Odd (Nat.card c.supp)} →
    {c : ConnectedComponent G | Odd (Nat.card c.supp)} :=
  fun ⟨c, hc⟩ ↦ ⟨(aux c hc).choose, (aux c hc).choose_spec.2⟩

Result:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
aux : ∀ (c : G'.ConnectedComponent), Odd c.supp.ncard → {c' | c'.supp ⊆ c.supp ∧ Odd c'.supp.ncard}.Nonempty
f : ↑{c | Odd (Nat.card ↑c.supp)} → ↑{c | Odd (Nat.card ↑c.supp)} :=
  fun x =>
    match x with
    | ⟨c, hc⟩ => ⟨Exists.choose ⋯, ⋯⟩
⊢ {c | Odd c.supp.ncard}.ncard ≤ {c | Odd c.supp.ncard}.ncard

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
aux : ∀ (c : G'.ConnectedComponent), Odd c.supp.ncard → {c' | c'.supp ⊆ c.supp ∧ Odd c'.supp.ncard}.Nonempty
f : ↑{c | Odd (Nat.card ↑c.supp)} → ↑{c | Odd (Nat.card ↑c.supp)} :=
  fun x =>
    match x with
    | ⟨c, hc⟩ => ⟨Exists.choose ⋯, ⋯⟩
⊢ {c | Odd c.supp.ncard}.ncard ≤ {c | Odd c.supp.ncard}.ncard

Tactic:
refine Finite.card_le_of_injective f fun c c' fcc' ↦ ?_

Result:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
aux : ∀ (c : G'.ConnectedComponent), Odd c.supp.ncard → {c' | c'.supp ⊆ c.supp ∧ Odd c'.supp.ncard}.Nonempty
f : ↑{c | Odd (Nat.card ↑c.supp)} → ↑{c | Odd (Nat.card ↑c.supp)} :=
  fun x =>
    match x with
    | ⟨c, hc⟩ => ⟨Exists.choose ⋯, ⋯⟩
c c' : ↑{c | Odd c.supp.ncard}
fcc' : f c = f c'
⊢ c = c'

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

Tactic:
have aux (c : G'.ConnectedComponent) (hc : Odd c.supp.ncard) :
    {c' : G.ConnectedComponent | c'.supp ⊆ c.supp ∧ Odd c'.supp.ncard}.Nonempty := by
  refine Set.nonempty_of_ncard_ne_zero fun h' ↦ ?_
  simpa [-Nat.card_eq_fintype_card, -Set.coe_setOf, h']
    using (c.odd_card_supp_iff_odd_subcomponents _ h).mp hc

Result:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
aux : ∀ (c : G'.ConnectedComponent), Odd c.supp.ncard → {c' | c'.supp ⊆ c.supp ∧ Odd c'.supp.ncard}.Nonempty
⊢ {c | Odd c.supp.ncard}.ncard ≤ {c | Odd c.supp.ncard}.ncard