awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
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
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
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

Tactic:
Nat.card_le_card_of_injective f fun c c' fcc' ↦ ?_

Premises used: Nat.card_le_card_of_injective, Set.encard, Nat.card, dite, Function.extend, ENat.toNat, WithTop.untopD, Set.ncard, WithTop.recTopCoe, ENat.card, Cardinal.toENatAux
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
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})
          ⋯)
        ⋯
refine : ∀ (c c' : (↑G'.oddComponents : Type u)) (fcc' : f c = f c'), c = c'
⊢ G'.oddComponents.ncard ≤ G.oddComponents.ncard

Tactic:
refine Nat.card_le_card_of_injective f fun c c' fcc' ↦ ?_

Premises used: Nat.card_le_card_of_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
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'
⊢ Exists.choose (p :=
      Membership.mem (γ := Set G.ConnectedComponent)
        {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ (↑c : G'.ConnectedComponent).supp})
      ⋯ =
    Exists.choose (p :=
      Membership.mem (γ := Set G.ConnectedComponent)
        {c'_1 : G.ConnectedComponent | Odd c'_1.supp.ncard ∧ c'_1.supp ⊆ (↑c' : G'.ConnectedComponent).supp})
      ⋯

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

Premises used: Subtype.mk.injEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
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' :
  Exists.choose (p :=
      Membership.mem (γ := Set G.ConnectedComponent)
        {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ (↑c : G'.ConnectedComponent).supp})
      ⋯ =
    Exists.choose (p :=
      Membership.mem (γ := Set G.ConnectedComponent)
        {c'_1 : G.ConnectedComponent | Odd c'_1.supp.ncard ∧ c'_1.supp ⊆ (↑c' : G'.ConnectedComponent).supp})
      ⋯
⊢ c = c'

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

Premises used: Exists.choose_spec, Subtype.val_injective, Set.Nonempty.some_mem, And.right, SimpleGraph.ConnectedComponent.eq_of_common_vertex, Subtype.val, Subtype.property, SimpleGraph.ConnectedComponent.nonempty_supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
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' :
  Exists.choose (p :=
      Membership.mem (γ := Set G.ConnectedComponent)
        {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ (↑c : G'.ConnectedComponent).supp})
      ⋯ =
    Exists.choose (p :=
      Membership.mem (γ := Set G.ConnectedComponent)
        {c'_1 : G.ConnectedComponent | Odd c'_1.supp.ncard ∧ c'_1.supp ⊆ (↑c' : G'.ConnectedComponent).supp})
      ⋯
⊢ c = c'

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

Premises used: Exists.choose_spec, Subtype.val_injective, Set.Nonempty.some_mem, And.right, SimpleGraph.ConnectedComponent.eq_of_common_vertex, Subtype.val, Subtype.property, SimpleGraph.ConnectedComponent.nonempty_supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
x : Quot G.Reachable
hx : x ∈ C
⊢ G.connectedComponentMk (x.out (r := G.Reachable)) ∈ C

Tactic:
simp_all [connectedComponentMk]

Premises used: SimpleGraph.connectedComponentMk
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
c : Quot G.Reachable
hc : c ∈ C
d : Quot G.Reachable
hd : d ∈ C
hxy : Quot.mk G.Reachable (c.out (r := G.Reachable)) = Quot.mk G.Reachable (d.out (r := G.Reachable))
⊢ c.out (r := G.Reachable) = d.out (r := G.Reachable)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
x : G.ConnectedComponent
h : x ∈ C
⊢ x ∈ G.connectedComponentMk '' Quot.out (r := G.Reachable) '' C

Tactic:
simpa [connectedComponentMk]

Premises used: SimpleGraph.connectedComponentMk
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
obtain :
  ∀ (x : V) (hx : x ∈ s) (h : G.connectedComponentMk x ∈ C), ∃! x_1 : V, x_1 ∈ s ∩ (G.connectedComponentMk x).supp
⊢ ∃! x : V, x ∈ s ∩ c.supp

Tactic:
obtain ⟨x, ⟨hx, rfl⟩⟩ := hrep.2.2 h

Premises used: And.right, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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
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
⊢ ∃! x_1 : V, x_1 ∈ s ∩ (G.connectedComponentMk x).supp

Tactic:
use x
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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
h₁ : ∀ y ∈ s, G.connectedComponentMk y = G.connectedComponentMk x → y = x
⊢ (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:
simp only [Set.mem_inter_iff, hx, mem_supp_iff, and_self, and_imp, true_and]

Premises used: and_self, and_imp, Set.mem_inter_iff, SimpleGraph.ConnectedComponent.mem_supp_iff, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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
⊢ ∀ y ∈ s, G.connectedComponentMk y = G.connectedComponentMk x → y = x

Tactic:
fun y hy hyx ↦ hrep.2.1 hy hx hyx

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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
⊢ ∀ y ∈ s, G.connectedComponentMk y = G.connectedComponentMk x → y = x

Tactic:
exact fun y hy hyx ↦ hrep.2.1 hy hx hyx

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
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}
⊢ ∃ (x : V), s ∩ c.supp = {x}

Tactic:
obtain ⟨a, ha⟩ := existsUnique_rep hrep h

Premises used: SimpleGraph.ConnectedComponent.Represents.existsUnique_rep
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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 : (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:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
rw : ∀ ⦃a : V⦄, a ∈ s → a ∉ c.supp
⊢ Disjoint s c.supp

Tactic:
rw [Set.disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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
⊢ G.connectedComponentMk a = c

Tactic:
simp only [mem_supp_iff] at hc

Premises used: SimpleGraph.ConnectedComponent.mem_supp_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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
⊢ G.connectedComponentMk a ∉ C

Tactic:
subst hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
a : V
ha : a ∈ s
h : G.connectedComponentMk a ∉ C
⊢ False

Tactic:
h (hrep.1 ha)

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
a : V
ha : a ∈ s
h : G.connectedComponentMk a ∉ C
⊢ False

Tactic:
exact h (hrep.1 ha)

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
rw : ∃ (a : V), s ∩ c.supp = {a}
⊢ (s ∩ c.supp).ncard = 1

Tactic:
rw [Set.ncard_eq_one]

Premises used: Set.ncard_eq_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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), s ∩ c.supp = {a}

Tactic:
exists_inter_eq_singleton hrep h

Premises used: SimpleGraph.ConnectedComponent.Represents.exists_inter_eq_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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), s ∩ c.supp = {a}

Tactic:
exact exists_inter_eq_singleton hrep h

Premises used: SimpleGraph.ConnectedComponent.Represents.exists_inter_eq_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
⊢ s.ncard = C.ncard

Tactic:
hrep.image_eq ▸ hrep.injOn.ncard_image.symm

Premises used: Eq.rec, Set.BijOn.image_eq, Set.BijOn.injOn, Set.InjOn.ncard_image, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
obtain : ∀ (a : V) (ha : s ∩ c.supp = {a}), (c.supp \ s).ncard = c.supp.ncard - 1
⊢ (c.supp \ s).ncard = c.supp.ncard - 1

Tactic:
obtain ⟨a, ha⟩ := exists_inter_eq_singleton hrep h

Premises used: SimpleGraph.ConnectedComponent.Represents.exists_inter_eq_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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}
rw : {a} ⊆ c.supp
⊢ (c.supp \ s).ncard = c.supp.ncard - 1

Tactic:
rw [← Set.diff_inter_self_eq_diff, ha, Set.ncard_diff, Set.ncard_singleton]

Premises used: Set.diff_inter_self_eq_diff, Set.ncard_diff, Set.ncard_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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}
⊢ {a} ⊆ c.supp

Tactic:
simp [← ha]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
Goal:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
rw rw₁ : c.supp.ncard = c.supp.ncard
⊢ (c.supp \ s).ncard = c.supp.ncard

Tactic:
rw [(disjoint_supp_of_notMem hrep h).sdiff_eq_right]

Premises used: Disjoint.sdiff_eq_right, SimpleGraph.ConnectedComponent.Represents.disjoint_supp_of_notMem
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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
neg : ∀ (h : ¬Even K.supp.ncard), Even (K.supp \ s).ncard
⊢ Even (K.supp \ s).ncard

Tactic:
by_cases h : Even K.supp.ncard

Premises used: Even, Set.ncard, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
Goal:
V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
h : Even K.supp.ncard
⊢ K ∉ G.oddComponents

Tactic:
simpa [Set.ncard_image_of_injective, ← Nat.not_odd_iff_even] using h

Premises used: Nat.not_odd_iff_even, Set.ncard_image_of_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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

Tactic:
simpa [hrep.ncard_sdiff_of_notMem
      (by simpa [Set.ncard_image_of_injective, ← Nat.not_odd_iff_even] using h)] using h

Premises used: SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_notMem
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
Goal:
V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
h : ¬Even K.supp.ncard
⊢ K.supp.ncard ≠ 0

Tactic:
have : K.supp.ncard ≠ 0 := Nat.ne_of_odd_add (Nat.not_even_iff_odd.mp h)
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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
⊢ 1 ≤ K.supp.ncard

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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
neg : Even K.supp.ncard ↔ Even (α := ℕ) 1
⊢ Even (K.supp \ s).ncard

Tactic:
rw [hrep.ncard_sdiff_of_mem (Nat.not_even_iff_odd.mp h), Nat.even_sub (by lia)]

Premises used: SimpleGraph.ConnectedComponent.Represents.ncard_sdiff_of_mem, Nat.not_even_iff_odd, Iff.mp, Nat.even_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
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.ncard ↔ Even (α := ℕ) 1

Tactic:
simpa [Nat.even_sub] using Nat.not_even_iff_odd.mp h

Premises used: Nat.not_even_iff_odd, Iff.mp, Nat.even_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Preconnected ↔ H.coe.Preconnected

Tactic:
⟨fun ⟨h⟩ => h, .mk⟩

Premises used: _private.0.SimpleGraph.Subgraph.preconnected_iff.match_1, SimpleGraph.Preconnected, SimpleGraph.Subgraph.coe, Iff.intro, SimpleGraph.Subgraph.Preconnected.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Connected ↔ H.coe.Connected

Tactic:
⟨fun ⟨h⟩ => h, .mk⟩

Premises used: _private.0.SimpleGraph.Subgraph.connected_iff'.match_1, SimpleGraph.Subgraph.Connected.mk, SimpleGraph.Connected, SimpleGraph.Subgraph.coe, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
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
rw₃ rw₄ : H.coe.Preconnected ∧ H.verts.Nonempty ↔ H.coe.Preconnected ∧ H.verts.Nonempty
⊢ H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty

Tactic:
rw [H.connected_iff', connected_iff, H.preconnected_iff, Set.nonempty_coe_sort]

Premises used: Set.nonempty_coe_sort, SimpleGraph.Subgraph.preconnected_iff, SimpleGraph.Subgraph.connected_iff', SimpleGraph.connected_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ H.Preconnected ∧ H.verts.Nonempty

Tactic:
rw [H.connected_iff] at h

Premises used: SimpleGraph.Subgraph.connected_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.Preconnected

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.Preconnected

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.verts.Nonempty

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.verts.Nonempty

Tactic:
exact h.2

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ (G.singletonSubgraph v).Connected

Tactic:
⟨⟨Preconnected.of_subsingleton⟩⟩

Premises used: SimpleGraph.Connected.mk, SimpleGraph.Preconnected.of_subsingleton, SimpleGraph.Subgraph.Connected.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).Connected

Tactic:
⟨⟨?_⟩⟩

Premises used: SimpleGraph.Connected.mk, SimpleGraph.Subgraph.Connected.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
refine : (G.subgraphOfAdj hvw).coe.Preconnected
⊢ (G.subgraphOfAdj hvw).Connected

Tactic:
refine ⟨⟨?_⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ a = v ∨ a = w

Tactic:
simp only [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb

Premises used: Set.mem_singleton_iff, SimpleGraph.subgraphOfAdj_verts, Set.mem_insert_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb : b ∈ (G.subgraphOfAdj hvw).verts
ha₁ : a = v ∨ a = w
⊢ b = v ∨ b = w

Tactic:
simp only [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb

Premises used: Set.mem_singleton_iff, SimpleGraph.subgraphOfAdj_verts, Set.mem_insert_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha_1 : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb_1 : b ∈ (G.subgraphOfAdj hvw).verts
ha : a = v ∨ a = w
hb : b = v ∨ b = w
inl :
  ∀ (hvw : G.Adj a w) (ha : a ∈ (G.subgraphOfAdj hvw).verts) (hb : b ∈ (G.subgraphOfAdj hvw).verts)
    (hb_2 : b = a ∨ b = w),
    (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
inr :
  ∀ (hvw : G.Adj v a) (ha : a ∈ (G.subgraphOfAdj hvw).verts) (hb : b ∈ (G.subgraphOfAdj hvw).verts)
    (hb_2 : b = v ∨ b = a),
    (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb)
⊢ (G.subgraphOfAdj hvw).coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) a ha_1)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (G.subgraphOfAdj hvw).verts) b hb_1)

Tactic:
obtain rfl | rfl := ha

Premises used: rfl