awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
w : V
a : w ∈ C
w_1 : V
w_2 : w_1 ∈ C
h₁ : C.toSimpleGraph.Adj (Subtype.mk (p := fun (a : V) ↦ a ∈ C) w a) (Subtype.mk (p := fun (a : V) ↦ a ∈ C) w_1 w_2)
⊢ G.connectedComponentMk
        ((Embedding.subtype fun (x : V) ↦ x ∈ (↑C : Set V) : (a : ↥C) → V)
          (Subtype.mk (p := fun (a : V) ↦ a ∈ C) w a)) =
      C ∧
    G.Adj
      ((Embedding.subtype fun (x : V) ↦ x ∈ (↑C : Set V) : (a : ↥C) → V) (Subtype.mk (p := fun (a : V) ↦ a ∈ C) w a))
      ((Embedding.subtype fun (x : V) ↦ x ∈ (↑C : Set V) : (a : ↥C) → V)
        (Subtype.mk (p := fun (a : V) ↦ a ∈ C) w_1 w_2))

Tactic:
exact ⟨a, h₁⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
mpr :
  v ∈ C.supp →
    G.Adj v w → ∃ (a : V) (_ : a ∈ (↑C : Set V)) (a_1 : V), G.Adj a a_1 ∧ a = v ∧ ∃ (_ : a_1 ∈ (↑C : Set V)), a_1 = w
⊢ v ∈ C.supp ∧ G.Adj v w → C.toSimpleGraph.spanningCoe (s := (↑C : Set V)).Adj v w

Tactic:
simp only [toSimpleGraph, map_adj, comap_adj, Embedding.subtype_apply, Subtype.exists,
      exists_and_left, and_imp]

Premises used: and_imp, Subtype.exists, exists_and_left, SimpleGraph.map_adj, SimpleGraph.ConnectedComponent.toSimpleGraph, SimpleGraph.comap_adj, Function.Embedding.subtype_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
h : v ∈ C.supp
hadj : G.Adj v w
⊢ ∃ (a : V) (_ : a ∈ (↑C : Set V)) (a_1 : V), G.Adj a a_1 ∧ a = v ∧ ∃ (_ : a_1 ∈ (↑C : Set V)), a_1 = w

Tactic:
⟨v, h, w, hadj, rfl, (C.mem_supp_congr_adj hadj).mp h, rfl⟩

Premises used: SimpleGraph.ConnectedComponent.mem_supp_congr_adj, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
h : v ∈ C.supp
hadj : G.Adj v w
⊢ ∃ (a : V) (_ : a ∈ (↑C : Set V)) (a_1 : V), G.Adj a a_1 ∧ a = v ∧ ∃ (_ : a_1 ∈ (↑C : Set V)), a_1 = w

Tactic:
exact ⟨v, h, w, hadj, rfl, (C.mem_supp_congr_adj hadj).mp h, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
C : G.ConnectedComponent
u : V
hu hv : u ∈ C
⊢ C.toSimpleGraph.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hv)

Tactic:
exact Walk.nil

Premises used: SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C
hv : v ∈ C
w : V
h : G.Adj u w
p : G.Walk w v
⊢ w ∈ C

Tactic:
have hw : w ∈ C := C.mem_supp_of_adj_mem_supp hu h
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C
hv : v ∈ C
w : V
h : G.Adj u w
p : G.Walk w v
hw : w ∈ C
⊢ C.toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) w hw)

Tactic:
have h' : C.toSimpleGraph.Adj ⟨u, hu⟩ ⟨w, hw⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C
hv : v ∈ C
w : V
h : G.Adj u w
p : G.Walk w v
hw : w ∈ C
h' : C.toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) w hw)
⊢ C.toSimpleGraph.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) v hv)

Tactic:
exact Walk.cons h' (C.walk_toSimpleGraph hw hv p)

Premises used: SimpleGraph.Walk.cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C
hv : v ∈ C
p : G.Walk u v
nil :
  (hv : u ∈ C) →
    C.toSimpleGraph.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hv)
cons :
  {w : V} →
    (h : G.Adj u w) →
      (p : G.Walk w v) →
        C.toSimpleGraph.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) v hv)
⊢ C.toSimpleGraph.Walk (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) v hv)

Tactic:
cases p with
  | nil => exact Walk.nil
  | @cons v w u h p =>
    have hw : w ∈ C := C.mem_supp_of_adj_mem_supp hu h
    have h' : C.toSimpleGraph.Adj ⟨u, hu⟩ ⟨w, hw⟩ := h
    exact Walk.cons h' (C.walk_toSimpleGraph hw hv p)

Premises used: SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C
hv : v ∈ C
⊢ C.toSimpleGraph.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) v hv)

Tactic:
Walk.reachable (C.walk_toSimpleGraph hu hv (C.reachable_of_mem_supp hu hv).some)

Premises used: _private.0.SimpleGraph.ConnectedComponent.walk_toSimpleGraph, SimpleGraph.Walk.reachable, Nonempty.some, SimpleGraph.ConnectedComponent.reachable_of_mem_supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u : V
hu : u ∈ C
this :
  ∀ (v : V) (hv : v ∈ C),
    C.toSimpleGraph.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) v hv)
⊢ ∀ (v : ↥C), C.toSimpleGraph.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) v

Tactic:
⟨v, hv⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u : V
hu : u ∈ C
v : V
hv : v ∈ C
⊢ C.toSimpleGraph.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) v hv)

Tactic:
C.reachable_toSimpleGraph hu hv

Premises used: SimpleGraph.ConnectedComponent.reachable_toSimpleGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u : V
hu : u ∈ C
v : V
hv : v ∈ C
⊢ C.toSimpleGraph.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) v hv)

Tactic:
exact C.reachable_toSimpleGraph hu hv

Premises used: SimpleGraph.ConnectedComponent.reachable_toSimpleGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ Maximal (fun (x : Set V) ↦ (induce x G).Connected) C.supp

Tactic:
C.ind fun v ↦ ?_

Premises used: SimpleGraph.ConnectedComponent.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
refine : ∀ (v : V), Maximal (fun (x : Set V) ↦ (induce x G).Connected) (G.connectedComponentMk v).supp
⊢ Maximal (fun (x : Set V) ↦ (induce x G).Connected) C.supp

Tactic:
refine C.ind fun v ↦ ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
⊢ Maximal (fun (x : Set V) ↦ (induce x G).Connected) (G.connectedComponentMk v).supp

Tactic:
⟨connected_toSimpleGraph _, fun s hconn hle u hu ↦ ConnectedComponent.sound ?_⟩

Premises used: SimpleGraph.ConnectedComponent.connected_toSimpleGraph, And.intro, Maximal, SimpleGraph.ConnectedComponent.sound
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
refine :
  ∀ (s : Set V) (hconn : (fun (x : Set V) ↦ (induce x G).Connected) s) (hle : (G.connectedComponentMk v).supp ≤ s)
    (u : V) (hu : u ∈ s), G.Reachable u v
⊢ Maximal (fun (x : Set V) ↦ (induce x G).Connected) (G.connectedComponentMk v).supp

Tactic:
refine ⟨connected_toSimpleGraph _, fun s hconn hle u hu ↦ ConnectedComponent.sound ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
s : Set V
hconn : (fun (x : Set V) ↦ (induce x G).Connected) s
hle : (G.connectedComponentMk v).supp ≤ s
u : V
hu : u ∈ s
⊢ G.Reachable u v

Tactic:
hconn.preconnected ⟨u, hu⟩ ⟨v, hle rfl⟩ |>.map <| Embedding.induce s |>.toHom

Premises used: SimpleGraph.Connected.preconnected, Subtype.mk, SimpleGraph.Reachable.map, SimpleGraph.Embedding.toHom, SimpleGraph.Embedding.induce, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
s : Set V
hconn : (fun (x : Set V) ↦ (induce x G).Connected) s
hle : (G.connectedComponentMk v).supp ≤ s
u : V
hu : u ∈ s
⊢ G.Reachable u v

Tactic:
exact hconn.preconnected ⟨u, hu⟩ ⟨v, hle rfl⟩ |>.map <| Embedding.induce s |>.toHom

Premises used: SimpleGraph.Connected.preconnected, Subtype.mk, SimpleGraph.Reachable.map, SimpleGraph.Embedding.toHom, SimpleGraph.Embedding.induce, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
s : Set V
⊢ Maximal (fun (x : Set V) ↦ (induce x G).Connected) s ↔ ∃ (C : G.ConnectedComponent), C.supp = s

Tactic:
⟨fun ⟨hconn, h⟩ ↦ ?_, fun ⟨C, h⟩ ↦ ?_⟩

Premises used: _private.0.SimpleGraph.ConnectedComponent.maximal_connected_induce_iff.match_1, _private.0.SimpleGraph.ConnectedComponent.maximal_connected_induce_iff.match_2, Exists, SimpleGraph.Connected, Iff.intro, Maximal, SimpleGraph.induce, Eq, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
s : Set V
refine_1 :
  Maximal (fun (x : Set V) ↦ (induce x G).Connected) s →
    ∀ (hconn : (induce s G).Connected)
      (h : ∀ ⦃y : Set V⦄, (fun (x : Set V) ↦ (induce x G).Connected) y → s ≤ y → y ≤ s),
      ∃ (C : G.ConnectedComponent), C.supp = s
refine_2 :
  (∃ (C : G.ConnectedComponent), C.supp = s) →
    ∀ (C : G.ConnectedComponent) (h : C.supp = s), Maximal (fun (x : Set V) ↦ (induce x G).Connected) s
⊢ Maximal (fun (x : Set V) ↦ (induce x G).Connected) s ↔ ∃ (C : G.ConnectedComponent), C.supp = s

Tactic:
refine ⟨fun ⟨hconn, h⟩ ↦ ?_, fun ⟨C, h⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h_1 : Maximal (fun (x : Set V) ↦ (induce x G).Connected) s
hconn : (fun (x : Set V) ↦ (induce x G).Connected) s
h : ∀ ⦃y : Set V⦄, (fun (x : Set V) ↦ (induce x G).Connected) y → s ≤ y → y ≤ s
refine_1 : ∀ (v : V) (hv : v ∈ s), ∃ (C : G.ConnectedComponent), C.supp = s
⊢ ∃ (C : G.ConnectedComponent), C.supp = s

Tactic:
have ⟨v, hv⟩ := hconn.nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h_1 : Maximal (fun (x : Set V) ↦ (induce x G).Connected) s
hconn : (fun (x : Set V) ↦ (induce x G).Connected) s
h : ∀ ⦃y : Set V⦄, (fun (x : Set V) ↦ (induce x G).Connected) y → s ≤ y → y ≤ s
v : V
hv : v ∈ s
refine_1 : s ≤ (G.connectedComponentMk v).supp
⊢ ∃ (C : G.ConnectedComponent), C.supp = s

Tactic:
suffices s ≤ (G.connectedComponentMk v).supp from
      ⟨G.connectedComponentMk v, le_antisymm (h (connected_toSimpleGraph _) this) this⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h_1 : Maximal (fun (x : Set V) ↦ (induce x G).Connected) s
hconn : (fun (x : Set V) ↦ (induce x G).Connected) s
h : ∀ ⦃y : Set V⦄, (fun (x : Set V) ↦ (induce x G).Connected) y → s ≤ y → y ≤ s
v : V
hv : v ∈ s
⊢ s ≤ (G.connectedComponentMk v).supp

Tactic:
fun u hu ↦ ConnectedComponent.sound <|
      hconn.preconnected ⟨u, hu⟩ ⟨v, hv⟩ |>.map <| Embedding.induce s |>.toHom

Premises used: SimpleGraph.Connected.preconnected, Set.Mem, setOf, Set.Subset, Subtype.mk, SimpleGraph.Reachable.map, SimpleGraph.ConnectedComponent.sound, SimpleGraph.Embedding.toHom, SimpleGraph.Embedding.induce, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h_1 : Maximal (fun (x : Set V) ↦ (induce x G).Connected) s
hconn : (fun (x : Set V) ↦ (induce x G).Connected) s
h : ∀ ⦃y : Set V⦄, (fun (x : Set V) ↦ (induce x G).Connected) y → s ≤ y → y ≤ s
v : V
hv : v ∈ s
⊢ s ≤ (G.connectedComponentMk v).supp

Tactic:
exact fun u hu ↦ ConnectedComponent.sound <|
      hconn.preconnected ⟨u, hu⟩ ⟨v, hv⟩ |>.map <| Embedding.induce s |>.toHom

Premises used: SimpleGraph.Connected.preconnected, Subtype.mk, SimpleGraph.Reachable.map, SimpleGraph.ConnectedComponent.sound, SimpleGraph.Embedding.toHom, SimpleGraph.Embedding.induce
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h_1 : ∃ (C : G.ConnectedComponent), C.supp = s
C : G.ConnectedComponent
h : C.supp = s
⊢ Maximal (fun (x : Set V) ↦ (induce x G).Connected) s

Tactic:
h ▸ maximal_connected_induce_supp _

Premises used: SimpleGraph.ConnectedComponent.maximal_connected_induce_supp, Eq.rec
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h_1 : ∃ (C : G.ConnectedComponent), C.supp = s
C : G.ConnectedComponent
h : C.supp = s
⊢ Maximal (fun (x : Set V) ↦ (induce x G).Connected) s

Tactic:
exact h ▸ maximal_connected_induce_supp _
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
⊢ (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)

Tactic:
simpa using hab
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
⊢ (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)

Tactic:
have h : (G.connectedComponentMk _).toSimpleGraph.Adj ⟨_, rfl⟩
        ⟨_, ((G.connectedComponentMk _).mem_supp_congr_adj hab).1 rfl⟩ := by simpa using hab
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
⊢ H.Adj
    ((C (G.connectedComponentMk a) : (a : ↥(G.connectedComponentMk a)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯))
    ((C (G.connectedComponentMk a) : (a : ↥(G.connectedComponentMk a)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯))

Tactic:
(C (G.connectedComponentMk _)).map_rel h

Premises used: SimpleGraph.connectedComponentMk, RelHom.map_rel
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
h₁ : ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj)
h₂ : Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk a
h₃ :
  ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj) →
    ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a) →
      (HEq (α := outParam (↥(G.connectedComponentMk b) → Type v)) fun (x : ↥(G.connectedComponentMk b)) ↦ V' (β :=
          outParam (↥(G.connectedComponentMk a) → Type v)) fun (x : ↥(G.connectedComponentMk a)) ↦ V') →
        ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a) →
          (G.connectedComponentMk b).toSimpleGraph.Adj ≍ (G.connectedComponentMk a).toSimpleGraph.Adj
h₄ :
  ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj) →
    G.connectedComponentMk b = G.connectedComponentMk a
h₅ :
  ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a) →
    Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk a
⊢ H.Adj
    ((C (G.connectedComponentMk a) : (a : ↥(G.connectedComponentMk a)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯))
    ((C (G.connectedComponentMk b) : (a : ↥(G.connectedComponentMk b)) → V')
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk b) b ⋯))

Tactic:
convert! (C (G.connectedComponentMk _)).map_rel h using 3

Premises used: SimpleGraph.connectedComponentMk, RelHom.map_rel
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
h₁ h₂ : ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk b).toSimpleGraph.Adj →r H.Adj)
⊢ ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj)

Tactic:
rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]

Premises used: SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
h₁ h₂ :
  Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk b
⊢ Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk a

Tactic:
rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]

Premises used: SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
e_1 : ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj)
e_2 : ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a)
e_3 :
  HEq (α := outParam (↥(G.connectedComponentMk b) → Type v)) fun (x : ↥(G.connectedComponentMk b)) ↦ V' (β :=
    outParam (↥(G.connectedComponentMk a) → Type v)) fun (x : ↥(G.connectedComponentMk a)) ↦ V'
e_1_1 : ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a)
h₁ h₂ : (G.connectedComponentMk b).toSimpleGraph.Adj ≍ (G.connectedComponentMk b).toSimpleGraph.Adj
⊢ (G.connectedComponentMk b).toSimpleGraph.Adj ≍ (G.connectedComponentMk a).toSimpleGraph.Adj

Tactic:
rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]

Premises used: SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
e_1 : ((G.connectedComponentMk b).toSimpleGraph →g H) = ((G.connectedComponentMk a).toSimpleGraph.Adj →r H.Adj)
h₁ h₂ : G.connectedComponentMk b = G.connectedComponentMk b
⊢ G.connectedComponentMk b = G.connectedComponentMk a

Tactic:
rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]

Premises used: SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G_1 : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a b : V
hab : G.Adj a b
h :
  (G.connectedComponentMk a).toSimpleGraph.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) a ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ G.connectedComponentMk a) b ⋯)
e_2 : ↥(G.connectedComponentMk b) = ↥(G.connectedComponentMk a)
h₁ h₂ :
  Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk b
⊢ Eq.{u + 1} (α := V → Prop) (fun (x : V) ↦ x ∈ G.connectedComponentMk b) fun (x : V) ↦ x ∈ G.connectedComponentMk a

Tactic:
rw [ConnectedComponent.connectedComponentMk_eq_of_adj hab]

Premises used: SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
simp_rw : Pairwise fun (c c' : G.ConnectedComponent) ↦ ∀ ⦃a : V⦄, a ∈ c.supp → a ∉ c'.supp
⊢ Pairwise fun (c c' : G.ConnectedComponent) ↦ Disjoint c.supp c'.supp

Tactic:
simp_rw [Set.disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
i : G.ConnectedComponent
_ : ∀ ⦃j : G.ConnectedComponent⦄, i ≠ j → (fun (c c' : G.ConnectedComponent) ↦ ∀ ⦃a : V⦄, a ∈ c.supp → a ∉ c'.supp) i j
⊢ ∀ ⦃j : G.ConnectedComponent⦄, i ≠ j → (fun (c c' : G.ConnectedComponent) ↦ ∀ ⦃a : V⦄, a ∈ c.supp → a ∉ c'.supp) i j

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
i j : G.ConnectedComponent
h : i ≠ j
a : V
hsx : a ∈ i.supp
hsy : a ∈ j.supp
⊢ G.connectedComponentMk a = i

Tactic:
rw [ConnectedComponent.mem_supp_iff] at hsx hsy

Premises used: SimpleGraph.ConnectedComponent.mem_supp_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
i j : G.ConnectedComponent
h : i ≠ j
a : V
hsx : a ∈ i.supp
hsy : a ∈ j.supp
hsx₁ : G.connectedComponentMk a = i
⊢ G.connectedComponentMk a = j

Tactic:
rw [ConnectedComponent.mem_supp_iff] at hsx hsy

Premises used: SimpleGraph.ConnectedComponent.mem_supp_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
i j : G.ConnectedComponent
h : i ≠ j
a : V
hsx : G.connectedComponentMk a = i
hsy : G.connectedComponentMk a = j
⊢ i = j

Tactic:
rw [hsx] at hsy
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
i j : G.ConnectedComponent
h : i ≠ j
a : V
hsx : G.connectedComponentMk a = i
hsy : i = j
⊢ False

Tactic:
h hsy