awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
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)}
have 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
Tactic: ext c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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
⊢ 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
have 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
Tactic: simp_rw [Set.toFinset_setOf, mem_filter, ← Set.ncard_coe_finset, coe_filter,
    mem_supp_iff, mem_univ, true_and, supp, and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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
⊢ 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
have 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)
Tactic: simp_rw [Set.toFinset_setOf, mem_filter, ← Set.ncard_coe_finset, coe_filter,
    mem_supp_iff, mem_univ, true_and, supp, and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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)
⊢ 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
have 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
Tactic: simp_rw [Set.toFinset_setOf, mem_filter, ← Set.ncard_coe_finset, coe_filter,
    mem_supp_iff, mem_univ, true_and, supp, and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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
⊢ 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
have 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})
Tactic: simp_rw [Set.toFinset_setOf, mem_filter, ← Set.ncard_coe_finset, coe_filter,
    mem_supp_iff, mem_univ, true_and, supp, and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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})
⊢ 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
have 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})
Tactic: simp_rw [Set.toFinset_setOf, mem_filter, ← Set.ncard_coe_finset, coe_filter,
    mem_supp_iff, mem_univ, true_and, supp, and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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})
⊢ 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
have 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})
Tactic: simp_rw [Set.toFinset_setOf, mem_filter, ← Set.ncard_coe_finset, coe_filter,
    mem_supp_iff, mem_univ, true_and, supp, and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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})
⊢ 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
have intro₈ : Odd c.supp.ncard ∧ c.supp ⊆ c'.supp ↔
  c.supp ⊆ c'.supp ∧ Odd (Set.ncard.{u} (α := V) {x : V | G.connectedComponentMk x = 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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})
⊢ 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
have 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})
Tactic: simp_rw [Set.toFinset_setOf, mem_filter, ← Set.ncard_coe_finset, coe_filter,
    mem_supp_iff, mem_univ, true_and, supp, and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
⊢ Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd (Nat.card.{u} (↑c'.supp : Type u))
have 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))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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))
have 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) sorry))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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)
            ⋯))
⊢ Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd (Nat.card.{u} (↑c'.supp : Type u))
have 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))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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))
⊢ Odd (Nat.card.{u} (↑{c : G.ConnectedComponent | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp} : Type u)) ↔
    Odd (Nat.card.{u} (↑c'.supp : Type u))
have 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)}))
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]