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
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)}))
⊢ 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),
  {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: 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))
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)}
⊢ 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) (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: 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
⊢ Odd G.oddComponents.ncard ↔ Odd (Nat.card V)
have intro : ∀ (val : Fintype V), Odd G.oddComponents.ncard ↔ Odd (Nat.card V)
Tactic: cases nonempty_fintype V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
val : Fintype V
⊢ Odd G.oddComponents.ncard ↔ Odd (Nat.card V)
have intro : Odd G.oddComponents.ncard ↔ Odd (Fintype.card V)
Tactic: rw [Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
val : Fintype V
⊢ Odd G.oddComponents.ncard ↔ Odd (Fintype.card V)
have intro : Odd G.oddComponents.ncard ↔
  Odd (card.{u} (α := V) (Finset.biUnion univ fun (x : G.ConnectedComponent) ↦ x.supp.toFinset))
Tactic: simp only [← (set_fintype_card_eq_univ_iff _).mpr G.iUnion_connectedComponentSupp,
    ← Set.toFinset_card, Set.toFinset_iUnion ConnectedComponent.supp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
val : Fintype V
⊢ Odd G.oddComponents.ncard ↔
    Odd (card.{u} (α := V) (Finset.biUnion univ fun (x : G.ConnectedComponent) ↦ x.supp.toFinset))
have intro : Odd G.oddComponents.ncard ↔ Odd (α := ℕ) (∑ u : G.ConnectedComponent, #u.supp.toFinset)
Tactic: rw [Finset.card_biUnion
    (fun x _ y _ hxy ↦ Set.disjoint_toFinset.mpr (pairwise_disjoint_supp_connectedComponent _ hxy))]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
val : Fintype V
⊢ Odd G.oddComponents.ncard ↔ Odd (α := ℕ) (∑ u : G.ConnectedComponent, #u.supp.toFinset)
have intro : Odd (card.{u} (α := G.ConnectedComponent) {x : G.ConnectedComponent | Odd x.supp.ncard}) ↔
  Odd (α := ℕ) (∑ x : G.ConnectedComponent, x.supp.ncard)
Tactic: simp_rw [← Set.ncard_eq_toFinset_card', ← Finset.coe_filter_univ, Set.ncard_coe_finset]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
⊢ Odd G.oddComponents.ncard ↔ Odd (Nat.card V)
have intro : ∀ (val : Fintype V), 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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)
have intro₁ : ∀ (val : Fintype V), Odd G.oddComponents.ncard ↔ Odd (Fintype.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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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)
⊢ Odd G.oddComponents.ncard ↔ Odd (Nat.card V)
have intro₂ : ∀ (val : Fintype V),
  Odd G.oddComponents.ncard ↔
    Odd (card.{u} (α := V) (Finset.biUnion univ fun (x : G.ConnectedComponent) ↦ x.supp.toFinset))
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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))
⊢ Odd G.oddComponents.ncard ↔ Odd (Nat.card V)
have intro₃ : ∀ (val : Fintype V), Odd G.oddComponents.ncard ↔ Odd (α := ℕ) (∑ u : G.ConnectedComponent, #u.supp.toFinset)
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (goal)
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)
⊢ Odd G.oddComponents.ncard ↔ Odd (Nat.card V)
have intro₄ : ∀ (val : Fintype V),
  Odd (card.{u} (α := G.ConnectedComponent) {x : G.ConnectedComponent | Odd x.supp.ncard}) ↔
    Odd (α := ℕ) (∑ x : G.ConnectedComponent, x.supp.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,
    ← 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
-- 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
hc : Odd c.supp.ncard
⊢ Set.Nonempty.{u} (α := G.ConnectedComponent) {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}
have refine : ∀
  (h' :
    Set.ncard.{u} (α := G.ConnectedComponent) {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp} = 0),
  False
Tactic: refine Set.nonempty_of_ncard_ne_zero fun h' ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
⊢ G'.oddComponents.ncard ≤ G.oddComponents.ncard
have aux : ∀ (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: have aux (c : G'.ConnectedComponent) (hc : Odd c.supp.ncard) :
      {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}.Nonempty := by
    refine Set.nonempty_of_ncard_ne_zero fun h' ↦ ?_
    simpa [-Nat.card_eq_fintype_card, -Set.coe_setOf, h']
      using (c.odd_oddComponents_ncard_subset_supp _ h).2 hc
-- 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'
aux :
  ∀ (c : G'.ConnectedComponent) (hc : Odd c.supp.ncard),
    Set.Nonempty.{u} (α := G.ConnectedComponent) {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}
f : (↑G'.oddComponents : Type u) → (↑G.oddComponents : Type u) :=
  fun (x : (↑G'.oddComponents : Type u)) ↦
    match (motive := (↑G'.oddComponents : Type u) → (↑G.oddComponents : Type u)) x with
    | ⟨c, hc⟩ =>
      Subtype.mk (p := fun (x : G.ConnectedComponent) ↦ x ∈ G.oddComponents)
        (Exists.choose (p :=
          Membership.mem (γ := Set G.ConnectedComponent)
            {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp})
          ⋯)
        ⋯
⊢ G'.oddComponents.ncard ≤ G.oddComponents.ncard
have refine : ∀ (c c' : (↑G'.oddComponents : Type u)) (fcc' : f c = f c'), c = c'
Tactic: refine Nat.card_le_card_of_injective f fun c c' fcc' ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : Finite V
G' : SimpleGraph V
h : G ≤ G'
aux :
  ∀ (c : G'.ConnectedComponent) (hc : Odd c.supp.ncard),
    Set.Nonempty.{u} (α := G.ConnectedComponent) {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}
f : (↑G'.oddComponents : Type u) → (↑G.oddComponents : Type u) :=
  fun (x : (↑G'.oddComponents : Type u)) ↦
    match (motive := (↑G'.oddComponents : Type u) → (↑G.oddComponents : Type u)) x with
    | ⟨c, hc⟩ =>
      Subtype.mk (p := fun (x : G.ConnectedComponent) ↦ x ∈ G.oddComponents)
        (Exists.choose (p :=
          Membership.mem (γ := Set G.ConnectedComponent)
            {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp})
          ⋯)
        ⋯
c c' : (↑G'.oddComponents : Type u)
fcc' : f c = f c'
⊢ c = c'
have fcc'₁ : Exists.choose (p :=
    Membership.mem (γ := Set G.ConnectedComponent)
      {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ (↑c : G'.ConnectedComponent).supp})
    sorry =
  Exists.choose (p :=
    Membership.mem (γ := Set G.ConnectedComponent)
      {c'_1 : G.ConnectedComponent | Odd c'_1.supp.ncard ∧ c'_1.supp ⊆ (↑c' : G'.ConnectedComponent).supp})
    sorry
Tactic: simp only [Subtype.mk.injEq, f] at fcc'
Cleared hypotheses: fcc'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (goal)
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ ∃! x : V, x ∈ s ∩ c.supp
have obtain : ∀ (x : V) (hx : x ∈ s) (h : G.connectedComponentMk x ∈ C), ∃! x_1 : V, x_1 ∈ s ∩ (G.connectedComponentMk x).supp
Tactic: obtain ⟨x, ⟨hx, rfl⟩⟩ := hrep.2.2 h
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (goal)
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
x : V
hx : x ∈ s
h : G.connectedComponentMk x ∈ C
⊢ ∃! x_1 : V, x_1 ∈ s ∩ (G.connectedComponentMk x).supp
have h₁ : (fun (x_1 : V) ↦ x_1 ∈ s ∩ (G.connectedComponentMk x).supp) x ∧
  ∀ (y : V), (fun (x_1 : V) ↦ x_1 ∈ s ∩ (G.connectedComponentMk x).supp) y → y = x
Tactic: use x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (goal)
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
x : V
hx : x ∈ s
h : G.connectedComponentMk x ∈ C
⊢ (fun (x_1 : V) ↦ x_1 ∈ s ∩ (G.connectedComponentMk x).supp) x ∧
    ∀ (y : V), (fun (x_1 : V) ↦ x_1 ∈ s ∩ (G.connectedComponentMk x).supp) y → y = x
have h₁ : ∀ y ∈ s, G.connectedComponentMk y = G.connectedComponentMk x → y = x
Tactic: simp only [Set.mem_inter_iff, hx, mem_supp_iff, and_self, and_imp, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (goal)
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ ∃ (x : V), s ∩ c.supp = {x}
have obtain : ∀ (a : V) (ha : (fun (x : V) ↦ x ∈ s ∩ c.supp) a ∧ ∀ (y : V), (fun (x : V) ↦ x ∈ s ∩ c.supp) y → y = a),
  ∃ (x : V), s ∩ c.supp = {x}
Tactic: obtain ⟨a, ha⟩ := existsUnique_rep hrep h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (goal)
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
⊢ Disjoint s c.supp
have rw : ∀ ⦃a : V⦄, a ∈ s → a ∉ c.supp
Tactic: rw [Set.disjoint_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
a : V
ha : a ∈ s
hc : a ∈ c.supp
⊢ False
have hc₁ : G.connectedComponentMk a = c
Tactic: simp only [mem_supp_iff] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
a : V
ha : a ∈ s
hc : G.connectedComponentMk a = c
⊢ False
have h₁ : G.connectedComponentMk a ∉ C
Tactic: subst hc
Cleared hypotheses: c, h, hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (goal)
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ (s ∩ c.supp).ncard = 1
have rw : ∃ (a : V), s ∩ c.supp = {a}
Tactic: rw [Set.ncard_eq_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (goal)
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ (c.supp \ s).ncard = c.supp.ncard - 1
have obtain : ∀ (a : V) (ha : s ∩ c.supp = {a}), (c.supp \ s).ncard = c.supp.ncard - 1
Tactic: obtain ⟨a, ha⟩ := exists_inter_eq_singleton hrep h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (goal)
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
a : V
ha : s ∩ c.supp = {a}
⊢ (c.supp \ s).ncard = c.supp.ncard - 1
have rw : {a} ⊆ c.supp
Tactic: rw [← Set.diff_inter_self_eq_diff, ha, Set.ncard_diff, Set.ncard_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (goal)
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
⊢ (c.supp \ s).ncard = c.supp.ncard
have rw : c.supp.ncard = c.supp.ncard
Tactic: rw [(disjoint_supp_of_notMem hrep h).sdiff_eq_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
⊢ Even (K.supp \ s).ncard
have pos : ∀ (h : Even K.supp.ncard), Even (K.supp \ s).ncard
Tactic: by_cases h : Even K.supp.ncard
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
pos : ∀ (h : Even K.supp.ncard), Even (K.supp \ s).ncard
⊢ Even (K.supp \ s).ncard
have neg : ∀ (h : ¬Even K.supp.ncard), Even (K.supp \ s).ncard
Tactic: by_cases h : Even K.supp.ncard
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
h : ¬Even K.supp.ncard
⊢ Even (K.supp \ s).ncard
have this : K.supp.ncard ≠ 0
Tactic: have : K.supp.ncard ≠ 0 := Nat.ne_of_odd_add (Nat.not_even_iff_odd.mp h)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
h : ¬Even K.supp.ncard
this : K.supp.ncard ≠ 0
⊢ Even (K.supp \ s).ncard
have neg : Even K.supp.ncard ↔ Even (α := ℕ) 1
Tactic: rw [hrep.ncard_sdiff_of_mem (Nat.not_even_iff_odd.mp h), Nat.even_sub (by lia)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty
have rw : H.coe.Connected ↔ H.Preconnected ∧ H.verts.Nonempty
Tactic: rw [H.connected_iff', connected_iff, H.preconnected_iff, Set.nonempty_coe_sort]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
rw : H.coe.Connected ↔ H.Preconnected ∧ H.verts.Nonempty
⊢ H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty
have rw₁ : H.coe.Preconnected ∧ Nonempty.{u + 1} (↑H.verts : Type u) ↔ H.Preconnected ∧ H.verts.Nonempty
Tactic: rw [H.connected_iff', connected_iff, H.preconnected_iff, Set.nonempty_coe_sort]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
rw : H.coe.Connected ↔ H.Preconnected ∧ H.verts.Nonempty
rw₁ : H.coe.Preconnected ∧ Nonempty.{u + 1} (↑H.verts : Type u) ↔ H.Preconnected ∧ H.verts.Nonempty
⊢ H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty
have rw₂ : H.coe.Preconnected ∧ Nonempty.{u + 1} (↑H.verts : Type u) ↔ H.coe.Preconnected ∧ H.verts.Nonempty
Tactic: rw [H.connected_iff', connected_iff, H.preconnected_iff, Set.nonempty_coe_sort]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
rw : H.coe.Connected ↔ H.Preconnected ∧ H.verts.Nonempty
rw₁ : H.coe.Preconnected ∧ Nonempty.{u + 1} (↑H.verts : Type u) ↔ H.Preconnected ∧ H.verts.Nonempty
rw₂ : H.coe.Preconnected ∧ Nonempty.{u + 1} (↑H.verts : Type u) ↔ H.coe.Preconnected ∧ H.verts.Nonempty
⊢ H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty
have rw₃ : H.coe.Preconnected ∧ H.verts.Nonempty ↔ H.coe.Preconnected ∧ H.verts.Nonempty
Tactic: rw [H.connected_iff', connected_iff, H.preconnected_iff, Set.nonempty_coe_sort]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ H.Preconnected
have h₁ : H.Preconnected ∧ H.verts.Nonempty
Tactic: rw [H.connected_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ H.verts.Nonempty
have h₁ : H.Preconnected ∧ H.verts.Nonempty
Tactic: rw [H.connected_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).Connected
have refine : (G.subgraphOfAdj hvw).coe.Preconnected
Tactic: refine ⟨⟨?_⟩⟩