awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
v' : V'
C : G.ConnectedComponent
u : V
⊢ G.connectedComponentMk ((φ.symm : (a : V') → V) v') = G.connectedComponentMk u ↔
    G'.connectedComponentMk v' =
      map ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) φ).toRelHom (r := G.Adj) (s := G'.Adj))
        (G.connectedComponentMk u)

Tactic:
simp only [Iso.symm_apply_reachable, ConnectedComponent.eq, ConnectedComponent.map_mk,
    RelEmbedding.coe_toRelHom, RelIso.coe_toRelEmbedding]

Premises used: SimpleGraph.Iso.symm_apply_reachable, RelEmbedding.coe_toRelHom, SimpleGraph.ConnectedComponent.map_mk, SimpleGraph.ConnectedComponent.eq, RelIso.coe_toRelEmbedding
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
H :
  ∀ (x : G.ConnectedComponent) (v : V),
    Eq (α := G.ConnectedComponent)
      ((connectedComponentEquiv refl : (a : G.ConnectedComponent) → G.ConnectedComponent) (Quot.mk G.Reachable v) :
        G.ConnectedComponent)
      ((Equiv.refl G.ConnectedComponent : (a : G.ConnectedComponent) → G.ConnectedComponent) (Quot.mk G.Reachable v) :
        G.ConnectedComponent)
⊢ Eq.{u + 1} (α := G.ConnectedComponent ≃ G.ConnectedComponent) (connectedComponentEquiv refl)
    (Equiv.refl G.ConnectedComponent)

Tactic:
ext ⟨v⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
x : G.ConnectedComponent
v : V
⊢ Eq (α := G.ConnectedComponent)
    ((connectedComponentEquiv refl : (a : G.ConnectedComponent) → G.ConnectedComponent) (Quot.mk G.Reachable v) :
      G.ConnectedComponent)
    ((Equiv.refl G.ConnectedComponent : (a : G.ConnectedComponent) → G.ConnectedComponent) (Quot.mk G.Reachable v) :
      G.ConnectedComponent)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
H :
  ∀ (x : G'.ConnectedComponent) (a : V'),
    Eq.{u + 1} (α := G.ConnectedComponent)
      ((φ.symm.connectedComponentEquiv : (a : G'.ConnectedComponent) → G.ConnectedComponent) (Quot.mk G'.Reachable a) :
        G.ConnectedComponent)
      ((φ.connectedComponentEquiv.symm : (a : G'.ConnectedComponent) → G.ConnectedComponent) (Quot.mk G'.Reachable a) :
        G.ConnectedComponent)
⊢ φ.symm.connectedComponentEquiv = φ.connectedComponentEquiv.symm

Tactic:
ext ⟨_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
x : G'.ConnectedComponent
a : V'
⊢ Eq.{u + 1} (α := G.ConnectedComponent)
    ((φ.symm.connectedComponentEquiv : (a : G'.ConnectedComponent) → G.ConnectedComponent) (Quot.mk G'.Reachable a) :
      G.ConnectedComponent)
    ((φ.connectedComponentEquiv.symm : (a : G'.ConnectedComponent) → G.ConnectedComponent) (Quot.mk G'.Reachable a) :
      G.ConnectedComponent)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
φ : G ≃g G'
φ' : G' ≃g G''
H :
  ∀ (x : G.ConnectedComponent) (a : V),
    Eq.{w + 1} (α := G''.ConnectedComponent)
      ((connectedComponentEquiv (RelIso.trans (r := G.Adj) (s := G'.Adj) (t := G''.Adj) φ φ') :
            (a : G.ConnectedComponent) → G''.ConnectedComponent)
          (Quot.mk G.Reachable a) :
        G''.ConnectedComponent)
      ((φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv :
            (a : G.ConnectedComponent) → G''.ConnectedComponent)
          (Quot.mk G.Reachable a) :
        G''.ConnectedComponent)
⊢ connectedComponentEquiv (RelIso.trans (r := G.Adj) (s := G'.Adj) (t := G''.Adj) φ φ') =
    φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv

Tactic:
ext ⟨_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
φ : G ≃g G'
φ' : G' ≃g G''
x : G.ConnectedComponent
a : V
⊢ Eq.{w + 1} (α := G''.ConnectedComponent)
    ((connectedComponentEquiv (RelIso.trans (r := G.Adj) (s := G'.Adj) (t := G''.Adj) φ φ') :
          (a : G.ConnectedComponent) → G''.ConnectedComponent)
        (Quot.mk G.Reachable a) :
      G''.ConnectedComponent)
    ((φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv : (a : G.ConnectedComponent) → G''.ConnectedComponent)
        (Quot.mk G.Reachable a) :
      G''.ConnectedComponent)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
⊢ Injective.{u + 1, u + 1} (α := G.ConnectedComponent) supp

Tactic:
ConnectedComponent.ind₂ ?_

Premises used: SimpleGraph.ConnectedComponent.ind₂, Function.Injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
refine :
  ∀ (v w : V),
    (G.connectedComponentMk v).supp = (G.connectedComponentMk w).supp →
      G.connectedComponentMk v = G.connectedComponentMk w
⊢ Injective.{u + 1, u + 1} (α := G.ConnectedComponent) supp

Tactic:
refine ConnectedComponent.ind₂ ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
simp : ∀ (v w : V), (∀ (x : V), G.Reachable x v ↔ G.Reachable x w) → G.Reachable v w
⊢ ∀ (v w : V),
    (G.connectedComponentMk v).supp = (G.connectedComponentMk w).supp →
      G.connectedComponentMk v = G.connectedComponentMk w

Tactic:
simp only [ConnectedComponent.supp, Set.ext_iff, ConnectedComponent.eq, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, SimpleGraph.ConnectedComponent.eq, Set.ext_iff, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ (x : V), G.Reachable x v ↔ G.Reachable x w
rw : G.Reachable w v
rw₁ rw₂ : G.Reachable w w
⊢ G.Reachable v w

Tactic:
rw [reachable_comm, h]

Premises used: SimpleGraph.reachable_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C D : G.ConnectedComponent
⊢ C.supp = D.supp ↔ C = D

Tactic:
ConnectedComponent.supp_injective.eq_iff

Premises used: SimpleGraph.ConnectedComponent.supp_injective, Function.Injective.eq_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
v : V
⊢ v ∈ C.supp ↔ G.connectedComponentMk v = C

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
mp : G.connectedComponentMk v = c → G.connectedComponentMk w = c
mpr : G.connectedComponentMk w = c → G.connectedComponentMk v = c
⊢ G.connectedComponentMk v = c ↔ G.connectedComponentMk w = c

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
mp : G.connectedComponentMk w = G.connectedComponentMk v
⊢ G.connectedComponentMk w = c

Tactic:
simp only [← h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
mpr : G.connectedComponentMk v = G.connectedComponentMk w
⊢ G.connectedComponentMk v = c

Tactic:
simp only [← h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
mp : G.Adj w v
⊢ G.connectedComponentMk w = G.connectedComponentMk v

Tactic:
apply connectedComponentMk_eq_of_adj

Premises used: SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
mpr : G.Adj v w
⊢ G.connectedComponentMk v = G.connectedComponentMk w

Tactic:
apply connectedComponentMk_eq_of_adj

Premises used: SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
⊢ G.Adj w v

Tactic:
hadj.symm

Premises used: SimpleGraph.Adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk v = c
⊢ G.Adj w v

Tactic:
exact hadj.symm

Premises used: SimpleGraph.Adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
⊢ G.Adj v w

Tactic:
hadj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
h : G.connectedComponentMk w = c
⊢ G.Adj v w

Tactic:
exact hadj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ v ∈ G.connectedComponentMk v

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ C.supp.Nonempty

Tactic:
C.exists_rep

Premises used: SimpleGraph.connectedComponentMk, Set.Mem, setOf, Quot.exists_rep, SimpleGraph.ConnectedComponent, Set.Nonempty, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hv : v ∈ Subtype.val (p := fun (x : V) ↦ x ∈ H.verts) '' (↑c : Set (↑H.verts : Type u))
hw : w ∈ H.verts
hadj : H.Adj v w
obtain :
  ∀ (w_1 : (↑H.verts : Type u)) (h : w_1 ∈ (↑c : Set (↑H.verts : Type u)) ∧ (↑w_1 : V) = v),
    w ∈ Subtype.val (p := fun (x : V) ↦ x ∈ H.verts) '' (↑c : Set (↑H.verts : Type u))
⊢ w ∈ Subtype.val (p := fun (x : V) ↦ x ∈ H.verts) '' (↑c : Set (↑H.verts : Type u))

Tactic:
obtain ⟨_, h⟩ := hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w_1 : (↑H.verts : Type u)
h : w_1 ∈ (↑c : Set (↑H.verts : Type u)) ∧ (↑w_1 : V) = v
h₁ :
  Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw ∈ (↑c : Set (↑H.verts : Type u)) ∧
    (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw) : V) = w
⊢ w ∈ Subtype.val (p := fun (x : V) ↦ x ∈ H.verts) '' (↑c : Set (↑H.verts : Type u))

Tactic:
use ⟨w, hw⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w_1 : (↑H.verts : Type u)
h : w_1 ∈ (↑c : Set (↑H.verts : Type u)) ∧ (↑w_1 : V) = v
h₁ :
  Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw ∈ (↑(H.coe.connectedComponentMk w_1) : Set (↑H.verts : Type u)) ∧
    (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw) : V) = w
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw ∈ (↑c : Set (↑H.verts : Type u)) ∧
    (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw) : V) = w

Tactic:
rw [← (mem_supp_iff _ _).mp h.1]

Premises used: SimpleGraph.ConnectedComponent.mem_supp_iff, And.left, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w_1 : (↑H.verts : Type u)
h : w_1 ∈ (↑c : Set (↑H.verts : Type u)) ∧ (↑w_1 : V) = v
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw ∈ (↑(H.coe.connectedComponentMk w_1) : Set (↑H.verts : Type u)) ∧
    (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw) : V) = w

Tactic:
⟨connectedComponentMk_eq_of_adj <| Subgraph.Adj.coe <| h.2 ▸ hadj.symm, rfl⟩

Premises used: And.intro, SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj, SimpleGraph.Subgraph.Adj.coe, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w_1 : (↑H.verts : Type u)
h : w_1 ∈ (↑c : Set (↑H.verts : Type u)) ∧ (↑w_1 : V) = v
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw ∈ (↑(H.coe.connectedComponentMk w_1) : Set (↑H.verts : Type u)) ∧
    (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) w hw) : V) = w

Tactic:
exact ⟨connectedComponentMk_eq_of_adj <| Subgraph.Adj.coe <| h.2 ▸ hadj.symm, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v : V
c c' : G.ConnectedComponent
hc : v ∈ c.supp
hc' : v ∈ c'.supp
⊢ G.connectedComponentMk v = c

Tactic:
simp only [mem_supp_iff] at *

Premises used: SimpleGraph.ConnectedComponent.mem_supp_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v : V
c c' : G.ConnectedComponent
hc : v ∈ c.supp
hc' : v ∈ c'.supp
hc₁ : G.connectedComponentMk v = c
⊢ G.connectedComponentMk v = c'

Tactic:
simp only [mem_supp_iff] at *

Premises used: SimpleGraph.ConnectedComponent.mem_supp_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v : V
c c' : G.ConnectedComponent
hc : G.connectedComponentMk v = c
hc' rw : G.connectedComponentMk v = c'
rw₁ rw₂ : G.connectedComponentMk v = G.connectedComponentMk v
⊢ c = c'

Tactic:
rw [← hc, ← hc']
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : v' ∈ (G.connectedComponentMk v).supp
⊢ G.Reachable v' v

Tactic:
simp only [mem_supp_iff, ConnectedComponent.eq] at hv' ⊢

Premises used: SimpleGraph.ConnectedComponent.mem_supp_iff, SimpleGraph.ConnectedComponent.eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : G.Reachable v' v
rw : G'.connectedComponentMk v = c'
⊢ G'.connectedComponentMk v' = c'

Tactic:
rw [ConnectedComponent.sound (hv'.mono h)]

Premises used: SimpleGraph.Reachable.mono, SimpleGraph.ConnectedComponent.sound
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : G.Reachable v' v
⊢ G'.connectedComponentMk v = c'

Tactic:
hc'

Premises used: Set.Mem, setOf, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : G.Reachable v' v
⊢ G'.connectedComponentMk v = c'

Tactic:
exact hc'
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
h₁ :
  ∀ (v : V),
    Membership.mem (γ := Set V) (⋃ (c : G.ConnectedComponent), ⋃ (_ : c.supp ⊆ c'.supp), c.supp) v ↔ v ∈ c'.supp
⊢ ⋃ (c : G.ConnectedComponent), ⋃ (_ : c.supp ⊆ c'.supp), c.supp = c'.supp

Tactic:
ext v
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
h₁ : (∃ (i : G.ConnectedComponent) (_ : i.supp ⊆ c'.supp), v ∈ i.supp) ↔ v ∈ c'.supp
⊢ Membership.mem (γ := Set V) (⋃ (c : G.ConnectedComponent), ⋃ (_ : c.supp ⊆ c'.supp), c.supp) v ↔ v ∈ c'.supp

Tactic:
simp_rw [Set.mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ (∃ (i : G.ConnectedComponent) (_ : i.supp ⊆ c'.supp), v ∈ i.supp) ↔ v ∈ c'.supp

Tactic:
⟨fun ⟨_, ⟨hi, hi'⟩⟩ ↦ hi hi', ?_⟩

Premises used: Membership.mem, _private.0.SimpleGraph.ConnectedComponent.biUnion_supp_eq_supp.match_1, Iff.intro, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
h₁ : v ∈ c'.supp → ∃ (i : G.ConnectedComponent) (_ : i.supp ⊆ c'.supp), v ∈ i.supp
⊢ (∃ (i : G.ConnectedComponent) (_ : i.supp ⊆ c'.supp), v ∈ i.supp) ↔ v ∈ c'.supp

Tactic:
refine ⟨fun ⟨_, ⟨hi, hi'⟩⟩ ↦ hi hi', ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
hv : v ∈ c'.supp
h₁ : ∃ (_ : (G.connectedComponentMk v).supp ⊆ c'.supp), v ∈ (G.connectedComponentMk v).supp
⊢ ∃ (i : G.ConnectedComponent) (_ : i.supp ⊆ c'.supp), v ∈ i.supp

Tactic:
use G.connectedComponentMk v

Premises used: SimpleGraph.connectedComponentMk
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
hv : v ∈ c'.supp
h₁ : v ∈ (G.connectedComponentMk v).supp
⊢ ∃ (_ : (G.connectedComponentMk v).supp ⊆ c'.supp), v ∈ (G.connectedComponentMk v).supp

Tactic:
use c'.connectedComponentMk_supp_subset_supp h hv

Premises used: SimpleGraph.ConnectedComponent.connectedComponentMk_supp_subset_supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
hv : v ∈ c'.supp
⊢ v ∈ (G.connectedComponentMk v).supp

Tactic:
simp only [mem_supp_iff]

Premises used: SimpleGraph.ConnectedComponent.mem_supp_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
c : ConnectedComponent (V := V) ⊤
obtain : ∀ (w : V), supp (G := ⊤) (Quot.mk (Reachable ⊤) w) = Set.univ
⊢ c.supp = Set.univ

Tactic:
obtain ⟨w, rfl⟩ := c.exists_rep

Premises used: Quot.exists_rep, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
w : V
h : ∀ (v : V), v ∈ supp (G := ⊤) (Quot.mk (Reachable ⊤) w) ↔ Membership.mem (γ := Set V) Set.univ v
⊢ supp (G := ⊤) (Quot.mk (Reachable ⊤) w) = Set.univ

Tactic:
ext v
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
w v : V
⊢ v ∈ supp (G := ⊤) (Quot.mk (Reachable ⊤) w) ↔ Membership.mem (γ := Set V) Set.univ v

Tactic:
simpa [-ConnectedComponent.eq] using ConnectedComponent.sound (G := ⊤)

Premises used: SimpleGraph.ConnectedComponent.eq, SimpleGraph.ConnectedComponent.sound
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C.supp
hv : v ∈ C.supp
⊢ G.connectedComponentMk u = C

Tactic:
rw [mem_supp_iff] at hu hv

Premises used: SimpleGraph.ConnectedComponent.mem_supp_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C.supp
hv : v ∈ C.supp
hu₁ : G.connectedComponentMk u = C
⊢ G.connectedComponentMk v = C

Tactic:
rw [mem_supp_iff] at hu hv

Premises used: SimpleGraph.ConnectedComponent.mem_supp_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : G.connectedComponentMk u = C
hv : G.connectedComponentMk v = C
⊢ G.Reachable u v

Tactic:
ConnectedComponent.exact (hv ▸ hu)

Premises used: Eq.rec, Eq.symm, SimpleGraph.ConnectedComponent.exact
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : G.connectedComponentMk u = C
hv : G.connectedComponentMk v = C
⊢ G.Reachable u v

Tactic:
exact ConnectedComponent.exact (hv ▸ hu)

Premises used: SimpleGraph.ConnectedComponent.exact
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : u ∈ C.supp
hadj : G.Adj u v
⊢ v ∈ C.supp

Tactic:
(mem_supp_congr_adj C hadj).mp hu

Premises used: SimpleGraph.ConnectedComponent.mem_supp_congr_adj, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u : ↥C
⊢ (C.toSimpleGraph_hom : (a : ↥C) → V) u = (↑u : V)

Tactic:
rfl

Premises used: rfl
-- 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.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ C) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ C) v hv) ↔
    G.Adj u v

Tactic:
simp [toSimpleGraph]

Premises used: SimpleGraph.ConnectedComponent.toSimpleGraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
mp : C.toSimpleGraph.spanningCoe (s := (↑C : Set V)).Adj v w → v ∈ C.supp ∧ G.Adj v w
mpr : v ∈ C.supp ∧ G.Adj v w → C.toSimpleGraph.spanningCoe (s := (↑C : Set V)).Adj v w
⊢ C.toSimpleGraph.spanningCoe (s := (↑C : Set V)).Adj v w ↔ v ∈ C.supp ∧ G.Adj v w

Tactic:
apply Iff.intro

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
h : C.toSimpleGraph.spanningCoe (s := (↑C : Set V)).Adj v w
⊢ ∃ (a : V) (b : a ∈ C) (a_1 : V) (b_1 : a_1 ∈ C),
    C.toSimpleGraph.Adj (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a b) (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a_1 b_1) ∧
      (Embedding.subtype fun (x : V) ↦ x ∈ (↑C : Set V) : (a : ↥C) → V) (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a b) =
          v ∧
        (Embedding.subtype fun (x : V) ↦ x ∈ (↑C : Set V) : (a : ↥C) → V)
            (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a_1 b_1) =
          w

Tactic:
simp_all only [map_adj, SetLike.coe_sort_coe, Subtype.exists, mem_supp_iff]

Premises used: SetLike.coe_sort_coe, Subtype.exists, SimpleGraph.map_adj, SimpleGraph.ConnectedComponent.mem_supp_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
h :
  ∃ (a : V) (b : a ∈ C) (a_1 : V) (b_1 : a_1 ∈ C),
    C.toSimpleGraph.Adj (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a b) (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a_1 b_1) ∧
      (Embedding.subtype fun (x : V) ↦ x ∈ (↑C : Set V) : (a : ↥C) → V) (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a b) =
          v ∧
        (Embedding.subtype fun (x : V) ↦ x ∈ (↑C : Set V) : (a : ↥C) → V)
            (Subtype.mk (p := fun (a : V) ↦ a ∈ C) a_1 b_1) =
          w
mp :
  ∀ (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))
⊢ G.connectedComponentMk v = C ∧ G.Adj v w

Tactic:
obtain ⟨_, a, _, _, h₁, rfl, rfl⟩ := h

Premises used: rfl
-- 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:
⟨a, h₁⟩

Premises used: And.intro