awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
u v x y : V
w : G.Walk u v
hw : w.IsTrail
huv : G.IsEdgeReachable 2 u v
hx : x ∈ w.support
hy : y ∈ w.support
⊢ G.IsEdgeReachable 2 x y

Tactic:
(hw.isEdgeReachable_two_of_isEdgeReachable_two_aux huv hx).symm.trans
    (hw.isEdgeReachable_two_of_isEdgeReachable_two_aux huv hy)

Premises used: SimpleGraph.IsEdgeReachable.trans, _private.0.SimpleGraph.Walk.IsTrail.isEdgeReachable_two_of_isEdgeReachable_two_aux, SimpleGraph.IsEdgeReachable.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
huv : G.IsEdgeReachable 2 u v
huy : ¬G.IsEdgeReachable 2 u x
⊢ x ∉ w.support

Tactic:
mt (hw.isEdgeReachable_two_of_isEdgeReachable_two_aux huv) huy

Premises used: mt, _private.0.SimpleGraph.Walk.IsTrail.isEdgeReachable_two_of_isEdgeReachable_two_aux
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
Goal:
V : Type u_1
G : SimpleGraph V
u x y : V
w : G.Walk u u
hw : w.IsTrail
hx : x ∈ w.support
hy : y ∈ w.support
⊢ G.IsEdgeReachable 2 x y

Tactic:
hw.isEdgeReachable_two_of_isEdgeReachable_two .rfl hx hy

Premises used: SimpleGraph.IsEdgeReachable.rfl, SimpleGraph.Walk.IsTrail.isEdgeReachable_two_of_isEdgeReachable_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
inst : Finite V
G G' : SimpleGraph V
h : G ≤ G'
⊢ Nat.card.{u} G'.ConnectedComponent ≤ Nat.card.{u} G.ConnectedComponent

Tactic:
Nat.card_le_card_of_surjective _ <| ConnectedComponent.surjective_map_ofLE h

Premises used: Nat.card_le_card_of_surjective, SimpleGraph.ConnectedComponent.surjective_map_ofLE
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
mp : G.Reachable u v → ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty
mpr : (∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty) → G.Reachable u v
⊢ G.Reachable u v ↔ ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
r : G.Reachable u v
⊢ ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty

Tactic:
r.elim_path fun p => ?_

Premises used: SimpleGraph.Reachable.elim_path
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
r : G.Reachable u v
mp : ∀ (p : G.Path u v), ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty
⊢ ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty

Tactic:
refine r.elim_path fun p => ?_

Premises used: SimpleGraph.Reachable.elim_path
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
r : G.Reachable u v
p : G.Path u v
⊢ ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty

Tactic:
⟨⟨_, p.isPath.length_lt⟩, p, ?_⟩

Premises used: Fin.mk, SimpleGraph.Path.isPath, Exists.intro, Subtype.val, SimpleGraph.Walk.IsPath.length_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
r : G.Reachable u v
p : G.Path u v
mp : (↑p : G.Walk u v) ∈ G.finsetWalkLength (↑(⟨(↑p : G.Walk u v).length, ⋯⟩ : Fin (Fintype.card V)) : ℕ) u v
⊢ ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n : ℕ) u v).Nonempty

Tactic:
refine ⟨⟨_, p.isPath.length_lt⟩, p, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
r : G.Reachable u v
p : G.Path u v
⊢ (↑p : G.Walk u v) ∈ G.finsetWalkLength (↑(⟨(↑p : G.Walk u v).length, ⋯⟩ : Fin (Fintype.card V)) : ℕ) u v

Tactic:
simp [mem_finsetWalkLength_iff]

Premises used: SimpleGraph.mem_finsetWalkLength_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
w : Fin (Fintype.card V)
p : G.Walk u v
h : p ∈ G.finsetWalkLength (↑w : ℕ) u v
⊢ G.Reachable u v

Tactic:
⟨p⟩

Premises used: Nonempty.intro, SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
w : Fin (Fintype.card V)
p : G.Walk u v
h : p ∈ G.finsetWalkLength (↑w : ℕ) u v
⊢ G.Reachable u v

Tactic:
exact ⟨p⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
rw : G.Preconnected ∧ Finset.Nonempty.{u} (α := V) univ ↔ G.Preconnected ∧ Nonempty V
rw₁ rw₂ : G.Preconnected ∧ Finset.Nonempty.{u} (α := V) univ ↔ G.Preconnected ∧ Finset.Nonempty.{u} (α := V) univ
⊢ G.Preconnected ∧ Finset.Nonempty.{u} (α := V) univ ↔ G.Connected

Tactic:
rw [connected_iff, ← Finset.univ_nonempty_iff]

Premises used: SimpleGraph.connected_iff, Finset.univ_nonempty_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
c : G.ConnectedComponent
v w : V
⊢ G.Reachable v w ↔ v ∈ (G.connectedComponentMk w).supp

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
inst_3 : Fintype (↑c'.supp : Type u)
inst_4 : DecidablePred fun (c : G.ConnectedComponent) ↦ c.supp ⊆ c'.supp
x : G.ConnectedComponent
h_1 : x ∈ (↑{c : G.ConnectedComponent | c.supp ⊆ c'.supp} : Set G.ConnectedComponent)
y : G.ConnectedComponent
h_2 : y ∈ (↑{c : G.ConnectedComponent | c.supp ⊆ c'.supp} : Set G.ConnectedComponent)
hxy : x ≠ y
⊢ onFun (β := Finset V) Disjoint (fun (c : G.ConnectedComponent) ↦ c.supp.toFinset) x y

Tactic:
simpa using pairwise_disjoint_supp_connectedComponent _ hxy

Premises used: SimpleGraph.pairwise_disjoint_supp_connectedComponent
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
inst_3 : Fintype (↑c'.supp : Type u)
inst_4 : DecidablePred fun (c : G.ConnectedComponent) ↦ c.supp ⊆ c'.supp
⊢ (↑(disjiUnion {c : G.ConnectedComponent | c.supp ⊆ c'.supp} (fun (c : G.ConnectedComponent) ↦ c.supp.toFinset) ⋯) :
      Set V) =
    (↑c'.supp.toFinset : Set V)

Tactic:
simpa using ConnectedComponent.biUnion_supp_eq_supp h _

Premises used: SimpleGraph.ConnectedComponent.biUnion_supp_eq_supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
intro :
  ∀ (val : Fintype V),
    Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
      Odd (Nat.card.{u} (↑c'.supp : Type u))
⊢ Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd (Nat.card.{u} (↑c'.supp : Type u))

Tactic:
cases nonempty_fintype V

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val : Fintype V
intro :
  Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd
      (card.{u} (α := V)
        (disjiUnion {c : G.ConnectedComponent | c.supp ⊆ c'.supp} (fun (c : G.ConnectedComponent) ↦ c.supp.toFinset) ⋯))
⊢ Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd (Nat.card.{u} (↑c'.supp : Type u))

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

Premises used: SimpleGraph.disjiUnion_supp_toFinset_eq_supp_toFinset, Nat.card_eq_card_toFinset, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val : Fintype V
intro :
  Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd (α := ℕ) (∑ x : G.ConnectedComponent with x.supp ⊆ c'.supp, #(filter (Membership.mem x.supp) univ))
⊢ Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd
      (card.{u} (α := V)
        (disjiUnion {c : G.ConnectedComponent | c.supp ⊆ c'.supp} (fun (c : G.ConnectedComponent) ↦ c.supp.toFinset) ⋯))

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

Premises used: Fintype.card_ofFinset, Finset.card_disjiUnion, Set.toFinset_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val : Fintype V
intro :
  Odd #({a ∈ G.oddComponents.toFinset | (fun (c : G.ConnectedComponent) ↦ c.supp ⊆ c'.supp) a}) ↔
    Odd
      (card.{u} (α := G.ConnectedComponent)
        ({x ∈ {c : G.ConnectedComponent | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}))
⊢ Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd (α := ℕ) (∑ x : G.ConnectedComponent with x.supp ⊆ c'.supp, #(filter (Membership.mem x.supp) univ))

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

Premises used: Fintype.card_ofFinset, Finset.odd_sum_iff_odd_card_odd, Nat.card_eq_fintype_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val : Fintype V
intro :
  {a ∈ G.oddComponents.toFinset | (fun (c : G.ConnectedComponent) ↦ c.supp ⊆ c'.supp) a} =
    {x ∈ {c : G.ConnectedComponent | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}
⊢ Odd #({a ∈ G.oddComponents.toFinset | (fun (c : G.ConnectedComponent) ↦ c.supp ⊆ c'.supp) a}) ↔
    Odd
      (card.{u} (α := G.ConnectedComponent)
        ({x ∈ {c : G.ConnectedComponent | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}))

Tactic:
congr! 2
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val : Fintype V
intro :
  ∀ (c : G.ConnectedComponent),
    c ∈ {a ∈ G.oddComponents.toFinset | (fun (c : G.ConnectedComponent) ↦ c.supp ⊆ c'.supp) a} ↔
      Membership.mem (γ := Finset G.ConnectedComponent)
        ({x ∈ {c : G.ConnectedComponent | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}) c
⊢ {a ∈ G.oddComponents.toFinset | (fun (c : G.ConnectedComponent) ↦ c.supp ⊆ c'.supp) a} =
    {x ∈ {c : G.ConnectedComponent | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}

Tactic:
ext c
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val : Fintype V
c : G.ConnectedComponent
intro intro₁ :
  c ∈ {x ∈ G.oddComponents.toFinset | x.supp ⊆ c'.supp} ↔
    Membership.mem (γ := Finset G.ConnectedComponent)
      ({x ∈ {c : G.ConnectedComponent | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}) c
intro₂ :
  Membership.mem (γ := Finset G.ConnectedComponent)
      ({x ∈ {x : G.ConnectedComponent | Odd x.supp.ncard} | x.supp ⊆ c'.supp}) c ↔
    Membership.mem (γ := Finset G.ConnectedComponent)
      ({x ∈ {c : G.ConnectedComponent | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}) c
intro₃ :
  (Membership.mem (γ := Finset G.ConnectedComponent) univ c ∧ Odd c.supp.ncard) ∧ c.supp ⊆ c'.supp ↔
    (Membership.mem (γ := Finset G.ConnectedComponent) univ c ∧ c.supp ⊆ c'.supp) ∧
      Odd #(filter (Membership.mem c.supp) univ)
intro₄ :
  (Membership.mem (γ := Finset G.ConnectedComponent) univ c ∧ Odd c.supp.ncard) ∧ c.supp ⊆ c'.supp ↔
    (Membership.mem (γ := Finset G.ConnectedComponent) univ c ∧ c.supp ⊆ c'.supp) ∧
      Odd (↑(filter (Membership.mem c.supp) univ) : Set V).ncard
intro₅ :
  (Membership.mem (γ := Finset G.ConnectedComponent) univ c ∧ Odd c.supp.ncard) ∧ c.supp ⊆ c'.supp ↔
    (Membership.mem (γ := Finset G.ConnectedComponent) univ c ∧ c.supp ⊆ c'.supp) ∧
      Odd (Set.ncard.{u} (α := V) {x : V | Membership.mem (γ := Finset V) univ x ∧ x ∈ c.supp})
intro₆ :
  (Membership.mem (γ := Finset G.ConnectedComponent) univ c ∧ Odd c.supp.ncard) ∧ c.supp ⊆ c'.supp ↔
    (Membership.mem (γ := Finset G.ConnectedComponent) univ c ∧ c.supp ⊆ c'.supp) ∧
      Odd (Set.ncard.{u} (α := V) {x : V | Membership.mem (γ := Finset V) univ x ∧ G.connectedComponentMk x = c})
intro₇ :
  (True ∧ Odd c.supp.ncard) ∧ c.supp ⊆ c'.supp ↔
    (True ∧ c.supp ⊆ c'.supp) ∧ Odd (Set.ncard.{u} (α := V) {x : V | True ∧ G.connectedComponentMk x = c})
intro₈ :
  Odd c.supp.ncard ∧ c.supp ⊆ c'.supp ↔
    c.supp ⊆ c'.supp ∧ Odd (Set.ncard.{u} (α := V) {x : V | G.connectedComponentMk x = c})
intro₉ :
  Odd (Set.ncard.{u} (α := V) {v : V | G.connectedComponentMk v = c}) ∧
      Subset.{u} (α := Set V) {v : V | G.connectedComponentMk v = c} {v : V | G'.connectedComponentMk v = c'} ↔
    Subset.{u} (α := Set V) {v : V | G.connectedComponentMk v = c} {v : V | G'.connectedComponentMk v = c'} ∧
      Odd (Set.ncard.{u} (α := V) {v : V | G.connectedComponentMk v = c})
⊢ c ∈ {a ∈ G.oddComponents.toFinset | (fun (c : G.ConnectedComponent) ↦ c.supp ⊆ c'.supp) a} ↔
    Membership.mem (γ := Finset G.ConnectedComponent)
      ({x ∈ {c : G.ConnectedComponent | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}) c

Tactic:
simp_rw [Set.toFinset_setOf, mem_filter, ← Set.ncard_coe_finset, coe_filter,
    mem_supp_iff, mem_univ, true_and, supp, and_comm]

Premises used: Finset.mem_univ, Finset.coe_filter, and_comm, SimpleGraph.ConnectedComponent.mem_supp_iff, Finset.mem_filter, Set.toFinset_setOf, true_and, SimpleGraph.ConnectedComponent.supp, Set.ncard_coe_finset
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
intro :
  ∀ (val : Fintype V),
    Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
      Odd (Nat.card.{u} (↑c'.supp : Type u))
intro₁ :
  ∀ (val : Fintype V),
    Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
      Odd
        (card.{u} (α := V)
          (disjiUnion {c : G.ConnectedComponent | c.supp ⊆ c'.supp} (fun (c : G.ConnectedComponent) ↦ c.supp.toFinset)
            ⋯))
intro₂ :
  ∀ (val : Fintype V),
    Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
      Odd (α := ℕ) (∑ x : G.ConnectedComponent with x.supp ⊆ c'.supp, #(filter (Membership.mem x.supp) univ))
intro₃ :
  ∀ (val : Fintype V),
    Odd #({a ∈ G.oddComponents.toFinset | (fun (c : G.ConnectedComponent) ↦ c.supp ⊆ c'.supp) a}) ↔
      Odd
        (card.{u} (α := G.ConnectedComponent)
          ({x ∈ {c : G.ConnectedComponent | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}))
intro₄ :
  ∀ (val : Fintype V),
    {a ∈ G.oddComponents.toFinset | (fun (c : G.ConnectedComponent) ↦ c.supp ⊆ c'.supp) a} =
      {x ∈ {c : G.ConnectedComponent | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}
intro₅ :
  ∀ (val : Fintype V) (c : G.ConnectedComponent),
    c ∈ {a ∈ G.oddComponents.toFinset | (fun (c : G.ConnectedComponent) ↦ c.supp ⊆ c'.supp) a} ↔
      Membership.mem (γ := Finset G.ConnectedComponent)
        ({x ∈ {c : G.ConnectedComponent | c.supp ⊆ c'.supp} | Odd #(filter (Membership.mem x.supp) univ)}) c
⊢ Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd (Nat.card.{u} (↑c'.supp : Type u))

Tactic:
classical
  cases nonempty_fintype V
  rw [Nat.card_eq_card_toFinset c'.supp, ← disjiUnion_supp_toFinset_eq_supp_toFinset h]
  simp only [Finset.card_disjiUnion, Set.toFinset_card, Fintype.card_ofFinset]
  rw [Finset.odd_sum_iff_odd_card_odd, Nat.card_eq_fintype_card, Fintype.card_ofFinset]
  congr! 2
  ext c
  simp_rw [Set.toFinset_setOf, mem_filter, ← Set.ncard_coe_finset, coe_filter,
    mem_supp_iff, mem_univ, true_and, supp, and_comm]

Premises used: Finset.mem_univ, Fintype.card_ofFinset, Finset.coe_filter, Finset.card_disjiUnion, and_comm, Set.toFinset_card, Finset.odd_sum_iff_odd_card_odd, nonempty_fintype, SimpleGraph.ConnectedComponent.mem_supp_iff, Finset.mem_filter, Set.toFinset_setOf, true_and, SimpleGraph.ConnectedComponent.supp, Set.ncard_coe_finset, Nat.card_eq_fintype_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
intro : ∀ (val : Fintype V), Odd G.oddComponents.ncard ↔ Odd (Nat.card V)
⊢ Odd G.oddComponents.ncard ↔ Odd (Nat.card V)

Tactic:
cases nonempty_fintype V

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
val : Fintype V
intro : Odd G.oddComponents.ncard ↔ Odd (Fintype.card V)
⊢ Odd G.oddComponents.ncard ↔ Odd (Nat.card V)

Tactic:
rw [Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
val : Fintype V
intro :
  Odd G.oddComponents.ncard ↔
    Odd (card.{u} (α := V) (Finset.biUnion univ fun (x : G.ConnectedComponent) ↦ x.supp.toFinset))
⊢ Odd G.oddComponents.ncard ↔ Odd (Fintype.card V)

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

Premises used: Iff.mpr, SimpleGraph.iUnion_connectedComponentSupp, set_fintype_card_eq_univ_iff, Set.toFinset_card, Set.toFinset_iUnion, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
val : Fintype V
intro : Odd G.oddComponents.ncard ↔ Odd (α := ℕ) (∑ u : G.ConnectedComponent, #u.supp.toFinset)
⊢ Odd G.oddComponents.ncard ↔
    Odd (card.{u} (α := V) (Finset.biUnion univ fun (x : G.ConnectedComponent) ↦ x.supp.toFinset))

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

Premises used: Iff.mpr, Set.disjoint_toFinset, Finset.card_biUnion, SimpleGraph.pairwise_disjoint_supp_connectedComponent
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
val : Fintype V
intro :
  Odd (card.{u} (α := G.ConnectedComponent) {x : G.ConnectedComponent | Odd x.supp.ncard}) ↔
    Odd (α := ℕ) (∑ x : G.ConnectedComponent, x.supp.ncard)
⊢ Odd G.oddComponents.ncard ↔ Odd (α := ℕ) (∑ u : G.ConnectedComponent, #u.supp.toFinset)

Tactic:
simp_rw [← Set.ncard_eq_toFinset_card', ← Finset.coe_filter_univ, Set.ncard_coe_finset]

Premises used: Set.ncard_eq_toFinset_card', Finset.coe_filter_univ, Set.ncard_coe_finset
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
val : Fintype V
⊢ Odd (card.{u} (α := G.ConnectedComponent) {x : G.ConnectedComponent | Odd x.supp.ncard}) ↔
    Odd (α := ℕ) (∑ x : G.ConnectedComponent, x.supp.ncard)

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

Premises used: Finset.odd_sum_iff_odd_card_odd, Set.ncard, Iff.symm, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
val : Fintype V
⊢ Odd (card.{u} (α := G.ConnectedComponent) {x : G.ConnectedComponent | Odd x.supp.ncard}) ↔
    Odd (α := ℕ) (∑ x : G.ConnectedComponent, x.supp.ncard)

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

Premises used: Finset.odd_sum_iff_odd_card_odd, Set.ncard, Iff.symm, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
intro : ∀ (val : Fintype V), Odd G.oddComponents.ncard ↔ Odd (Nat.card V)
intro₁ : ∀ (val : Fintype V), Odd G.oddComponents.ncard ↔ Odd (Fintype.card V)
intro₂ :
  ∀ (val : Fintype V),
    Odd G.oddComponents.ncard ↔
      Odd (card.{u} (α := V) (Finset.biUnion univ fun (x : G.ConnectedComponent) ↦ x.supp.toFinset))
intro₃ : ∀ (val : Fintype V), Odd G.oddComponents.ncard ↔ Odd (α := ℕ) (∑ u : G.ConnectedComponent, #u.supp.toFinset)
intro₄ :
  ∀ (val : Fintype V),
    Odd (card.{u} (α := G.ConnectedComponent) {x : G.ConnectedComponent | Odd x.supp.ncard}) ↔
      Odd (α := ℕ) (∑ x : G.ConnectedComponent, x.supp.ncard)
⊢ Odd G.oddComponents.ncard ↔ Odd (Nat.card V)

Tactic:
classical
  cases nonempty_fintype V
  rw [Nat.card_eq_fintype_card]
  simp only [← (set_fintype_card_eq_univ_iff _).mpr G.iUnion_connectedComponentSupp,
    ← 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.ncard_eq_toFinset_card', ← Finset.coe_filter_univ, Set.ncard_coe_finset]
  exact (Finset.odd_sum_iff_odd_card_odd (fun x : G.ConnectedComponent ↦ x.supp.ncard)).symm

Premises used: Iff.mpr, SimpleGraph.iUnion_connectedComponentSupp, set_fintype_card_eq_univ_iff, Set.disjoint_toFinset, Finset.card_biUnion, Set.toFinset_card, SimpleGraph.pairwise_disjoint_supp_connectedComponent, Set.ncard_eq_toFinset_card', Finset.odd_sum_iff_odd_card_odd, nonempty_fintype, Set.toFinset_iUnion, Finset.coe_filter_univ, Set.ncard, Iff.symm, SimpleGraph.ConnectedComponent.supp, Set.ncard_coe_finset, Nat.card_eq_fintype_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c : G'.ConnectedComponent
hc : Odd c.supp.ncard
⊢ Set.Nonempty.{u} (α := G.ConnectedComponent) {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}

Tactic:
Set.nonempty_of_ncard_ne_zero fun h' ↦ ?_

Premises used: Set.nonempty_of_ncard_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c : G'.ConnectedComponent
hc : Odd c.supp.ncard
refine :
  ∀
    (h' :
      Set.ncard.{u} (α := G.ConnectedComponent) {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp} = 0),
    False
⊢ Set.Nonempty.{u} (α := G.ConnectedComponent) {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}

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

Premises used: Set.nonempty_of_ncard_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c : G'.ConnectedComponent
hc : Odd c.supp.ncard
h' : Set.ncard.{u} (α := G.ConnectedComponent) {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp} = 0
⊢ False

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

Premises used: Iff.mpr, Set.coe_setOf, SimpleGraph.ConnectedComponent.odd_oddComponents_ncard_subset_supp, Nat.card_eq_fintype_card