awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
hG : G.Preconnected
v : V
⊢ ¬G.IsIsolated v

Tactic:
simp [← mem_support_iff_not_isIsolated, hG]

Premises used: SimpleGraph.mem_support_iff_not_isIsolated
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v : V
inst_1 : Fintype (↑(G.neighborSet v) : Type u)
⊢ 0 < G.degree v

Tactic:
simp [degree_pos_iff_mem_support, h.support_eq_univ]

Premises used: SimpleGraph.Preconnected.support_eq_univ, SimpleGraph.degree_pos_iff_mem_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
h : G.Preconnected
obtain : ∀ (v : V) (hv : G.minDegree = G.degree v), 0 < G.minDegree
⊢ 0 < G.minDegree

Tactic:
obtain ⟨v, hv⟩ := G.exists_minimal_degree_vertex

Premises used: SimpleGraph.exists_minimal_degree_vertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
h : G.Preconnected
v : V
hv : G.minDegree = G.degree v
rw : 0 < G.degree v
⊢ 0 < G.minDegree

Tactic:
rw [hv]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
h : G.Preconnected
v : V
hv : G.minDegree = G.degree v
⊢ 0 < G.degree v

Tactic:
h.degree_pos_of_nontrivial v

Premises used: SimpleGraph.Preconnected.degree_pos_of_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
h : G.Preconnected
v : V
hv : G.minDegree = G.degree v
⊢ 0 < G.degree v

Tactic:
exact h.degree_pos_of_nontrivial v

Premises used: SimpleGraph.Preconnected.degree_pos_of_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v x u_1 : V
hp : ¬Walk.Nil.{u} (V := V) (G := G) (v := u_1) Walk.nil
hx : Membership.mem (γ := List V) (Walk.support (G := G) (u := u_1) Walk.nil) x
⊢ ∃ (y : V), Membership.mem (γ := List V) (Walk.support (G := G) (u := u_1) Walk.nil) y ∧ G.Adj x y

Tactic:
grind [Walk.nil_iff_support_eq, Walk.cons_tail_support, adj_comm]

Premises used: SimpleGraph.Walk.nil_iff_support_eq, SimpleGraph.Walk.cons_tail_support, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v x u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (hp : ¬p.Nil) (hx : x ∈ p.support), ∃ y ∈ p.support, G.Adj x y
hp : ¬(Walk.cons h p).Nil
hx : x ∈ (Walk.cons h p).support
⊢ ∃ y ∈ (Walk.cons h p).support, G.Adj x y

Tactic:
grind [Walk.nil_iff_support_eq, Walk.cons_tail_support, adj_comm]

Premises used: SimpleGraph.Walk.nil_iff_support_eq, SimpleGraph.Walk.cons_tail_support, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
x : V
hx : x ∈ p.support
nil :
  ∀ {u : V} (hp : ¬Walk.Nil.{u} (V := V) (G := G) (v := u) Walk.nil)
    (hx : Membership.mem (γ := List V) (Walk.support (G := G) (u := u) Walk.nil) x),
    ∃ (y : V), Membership.mem (γ := List V) (Walk.support (G := G) (u := u) Walk.nil) y ∧ G.Adj x y
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (hp : ¬p.Nil) (hx : x ∈ p.support), ∃ y ∈ p.support, G.Adj x y) →
      ∀ (hp : ¬(Walk.cons h p).Nil) (hx : x ∈ (Walk.cons h p).support), ∃ y ∈ (Walk.cons h p).support, G.Adj x y
⊢ ∃ y ∈ p.support, G.Adj x y

Tactic:
induction p with grind [Walk.nil_iff_support_eq, Walk.cons_tail_support, adj_comm]

Premises used: SimpleGraph.Walk.nil_iff_support_eq, SimpleGraph.Walk.cons_tail_support, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
w : V
hw : w ∈ p.support
obtain : ∀ (y : V) (hy : y ∈ p.support ∧ G.Adj w y), w ∈ G.support
⊢ w ∈ G.support

Tactic:
obtain ⟨y, hy⟩ := adj_of_mem_walk_support p hp hw

Premises used: SimpleGraph.adj_of_mem_walk_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
w : V
hw : w ∈ p.support
y : V
hy : y ∈ p.support ∧ G.Adj w y
⊢ w ∈ G.support

Tactic:
(mem_support G).mpr ⟨y, hy.right⟩

Premises used: Iff.mpr, SimpleGraph.mem_support, And.right, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
w : V
hw : w ∈ p.support
y : V
hy : y ∈ p.support ∧ G.Adj w y
⊢ w ∈ G.support

Tactic:
exact (mem_support G).mpr ⟨y, hy.right⟩

Premises used: Iff.mpr, SimpleGraph.mem_support, And.right, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
h : G.Reachable u v
p : G.Walk u v := Classical.choice h
⊢ ¬p.Nil

Tactic:
have hp : ¬p.Nil := Walk.not_nil_of_ne huv
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
h : G.Reachable u v
p : G.Walk u v := Classical.choice h
hp : ¬p.Nil
⊢ u ∈ G.support

Tactic:
mem_support_of_mem_walk_support p hp p.start_mem_support

Premises used: SimpleGraph.Walk.start_mem_support, SimpleGraph.mem_support_of_mem_walk_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
h : G.Reachable u v
p : G.Walk u v := Classical.choice h
hp : ¬p.Nil
⊢ u ∈ G.support

Tactic:
exact mem_support_of_mem_walk_support p hp p.start_mem_support

Premises used: SimpleGraph.Walk.start_mem_support, SimpleGraph.mem_support_of_mem_walk_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
h : G.Preconnected
u v : V
⊢ ∃ (p : G.Walk u v), p.IsPath

Tactic:
(h u v).exists_isPath

Premises used: SimpleGraph.Reachable.exists_isPath
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
rw : G.Preconnected ∧ Nonempty V ↔ ∃ (v : V), ∀ (w : V), G.Reachable v w
⊢ G.Connected ↔ ∃ (v : V), ∀ (w : V), G.Reachable v w

Tactic:
rw [connected_iff]

Premises used: SimpleGraph.connected_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
mp : G.Preconnected ∧ Nonempty V → ∃ (v : V), ∀ (w : V), G.Reachable v w
mpr : (∃ (v : V), ∀ (w : V), G.Reachable v w) → G.Preconnected ∧ Nonempty V
⊢ G.Preconnected ∧ Nonempty V ↔ ∃ (v : V), ∀ (w : V), G.Reachable v w

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hp : G.Preconnected
v : V
⊢ ∃ (v : V), ∀ (w : V), G.Reachable v w

Tactic:
⟨v, fun w => hp v w⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
hp : G.Preconnected
v : V
⊢ ∃ (v : V), ∀ (w : V), G.Reachable v w

Tactic:
exact ⟨v, fun w => hp v w⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v : V
h : ∀ (w : V), G.Reachable v w
⊢ G.Preconnected ∧ Nonempty V

Tactic:
⟨fun u w => (h u).symm.trans (h w), ⟨v⟩⟩

Premises used: SimpleGraph.Reachable.symm, SimpleGraph.Reachable.trans, Nonempty.intro, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v : V
h : ∀ (w : V), G.Reachable v w
⊢ G.Preconnected ∧ Nonempty V

Tactic:
exact ⟨fun u w => (h u).symm.trans (h w), ⟨v⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
H : SimpleGraph V'
f : G →g H
hf : Surjective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
hG : G.Connected
⊢ H.Connected

Tactic:
haveI := hG.nonempty.map f
  ⟨hG.preconnected.map f hf⟩

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.Connected.mk, SimpleGraph.Preconnected.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
h : G.Connected
u v : V
⊢ ∃ (p : G.Walk u v), p.IsPath

Tactic:
(h u v).exists_isPath

Premises used: SimpleGraph.Reachable.exists_isPath, SimpleGraph.Connected.preconnected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
⊢ Connected.{u} (V := V) ⊥ ↔ Subsingleton V ∧ Nonempty V

Tactic:
simp [preconnected_bot_iff_subsingleton, connected_iff]

Premises used: SimpleGraph.preconnected_bot_iff_subsingleton, SimpleGraph.connected_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
⊢ ¬Connected.{u} (V := V) ⊥

Tactic:
simp [not_preconnected_bot, connected_iff]

Premises used: SimpleGraph.connected_iff, SimpleGraph.not_preconnected_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
⊢ (completeGraph V).Connected ↔ Nonempty V

Tactic:
simp [connected_iff]

Premises used: SimpleGraph.connected_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst rwa rwa₁ rwa₂ rwa₃ : Nonempty V
⊢ (completeGraph V).Connected

Tactic:
rwa [connected_top_iff]

Premises used: SimpleGraph.connected_top_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : Nonempty V
inst_1 : Subsingleton V
⊢ G.Connected

Tactic:
⟨.of_subsingleton⟩

Premises used: SimpleGraph.Connected.mk, SimpleGraph.Preconnected.of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
H : SimpleGraph V'
e : G ≃g H
⊢ G.Connected ↔ H.Connected

Tactic:
⟨Connected.map e.toHom e.toEquiv.surjective, Connected.map e.symm.toHom e.symm.toEquiv.surjective⟩

Premises used: SimpleGraph.Connected.map, SimpleGraph.Iso.toHom, Iff.intro, SimpleGraph.Iso.symm, Equiv.surjective, RelIso.toEquiv
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u v ∨ Gᶜ.Adj u v

Tactic:
or_iff_not_imp_left.mpr fun huv ↦ ⟨fun heq ↦ huv <| heq ▸ Reachable.rfl, mt Adj.reachable huv⟩

Premises used: Iff.mpr, SimpleGraph.Adj.reachable, mt, Eq.rec, SimpleGraph.Reachable.rfl, Classical.or_iff_not_imp_left, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v w : V
⊢ G.Reachable u v ∨ Gᶜ.Reachable u w

Tactic:
or_iff_not_imp_left.mpr fun huv ↦ ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v w : V
refine : ∀ (huv : ¬G.Reachable u v), Gᶜ.Reachable u w
⊢ G.Reachable u v ∨ Gᶜ.Reachable u w

Tactic:
refine or_iff_not_imp_left.mpr fun huv ↦ ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
pos : ∀ (huw : G.Reachable u w), Gᶜ.Reachable u w
neg : ∀ (huw : ¬G.Reachable u w), Gᶜ.Reachable u w
⊢ Gᶜ.Reachable u w

Tactic:
by_cases huw : G.Reachable u w

Premises used: SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
huw : G.Reachable u w
⊢ Gᶜ.Adj u v

Tactic:
have huv' := G.reachable_or_compl_adj .. |>.resolve_left huv
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
huw : G.Reachable u w
huv' : Gᶜ.Adj u v
⊢ Gᶜ.Adj v w

Tactic:
have hvw' := G.reachable_or_compl_adj .. |>.resolve_left fun hvw ↦ huv <| huw.trans hvw.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
huw : G.Reachable u w
huv' : Gᶜ.Adj u v
hvw' : Gᶜ.Adj v w
⊢ Gᶜ.Reachable u w

Tactic:
huv'.reachable.trans hvw'.reachable

Premises used: SimpleGraph.Adj.reachable, SimpleGraph.Reachable.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
huw : G.Reachable u w
huv' : Gᶜ.Adj u v
hvw' : Gᶜ.Adj v w
⊢ Gᶜ.Reachable u w

Tactic:
exact huv'.reachable.trans hvw'.reachable

Premises used: SimpleGraph.Adj.reachable, SimpleGraph.Reachable.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
huw : ¬G.Reachable u w
⊢ Gᶜ.Reachable u w

Tactic:
G.reachable_or_compl_adj .. |>.resolve_left huw |>.reachable

Premises used: SimpleGraph.Adj.reachable, Or.resolve_left, SimpleGraph.reachable_or_compl_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
huw : ¬G.Reachable u w
⊢ Gᶜ.Reachable u w

Tactic:
exact G.reachable_or_compl_adj .. |>.resolve_left huw |>.reachable

Premises used: SimpleGraph.Adj.reachable, Or.resolve_left, SimpleGraph.reachable_or_compl_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
rw : (¬∃ (v : V), ∀ (w : V), G.Reachable v w) → Gᶜ.Preconnected
⊢ G.Connected ∨ Gᶜ.Preconnected

Tactic:
rw [or_iff_not_imp_left, G.connected_iff_exists_forall_reachable]

Premises used: Classical.or_iff_not_imp_left, SimpleGraph.connected_iff_exists_forall_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
h : ¬∃ (v : V), ∀ (w : V), G.Reachable v w
u v : V
⊢ ∀ (v : V), ∃ (w : V), ¬G.Reachable v w

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : ∀ (v : V), ∃ (w : V), ¬G.Reachable v w
have : ∀ (w : V) (huw : ¬G.Reachable u w), Gᶜ.Reachable u v
⊢ Gᶜ.Reachable u v

Tactic:
have ⟨w, huw⟩ := h u
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : ∀ (v : V), ∃ (w : V), ¬G.Reachable v w
w : V
huw : ¬G.Reachable u w
⊢ Gᶜ.Reachable u v

Tactic:
reachable_or_reachable_compl .. |>.resolve_left huw

Premises used: SimpleGraph.reachable_or_reachable_compl, Or.resolve_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : ∀ (v : V), ∃ (w : V), ¬G.Reachable v w
w : V
huw : ¬G.Reachable u w
⊢ Gᶜ.Reachable u v

Tactic:
exact reachable_or_reachable_compl .. |>.resolve_left huw

Premises used: SimpleGraph.reachable_or_reachable_compl, Or.resolve_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : Nonempty V
⊢ G.Connected ∨ Gᶜ.Connected

Tactic:
G.connected_or_preconnected_compl.elim .inl (.inr ⟨·⟩)

Premises used: SimpleGraph.Connected.mk, Or.inl, SimpleGraph.connected_or_preconnected_compl, Or.elim, Or.inr
-- 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''
inst : IsEmpty V
⊢ IsEmpty.{u + 1} G.ConnectedComponent

Tactic:
Quot.instIsEmpty

Premises used: Quot.instIsEmpty, SimpleGraph.ConnectedComponent
-- 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''
inst : Subsingleton V
⊢ Subsingleton.{u + 1} G.ConnectedComponent

Tactic:
Quot.Subsingleton

Premises used: SimpleGraph.ConnectedComponent, Quot.Subsingleton
-- 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''
inst : Nonempty V
⊢ Nonempty.{u + 1} G.ConnectedComponent

Tactic:
Nonempty.map G.connectedComponentMk ‹_›

Premises used: SimpleGraph.connectedComponentMk, Nonempty.map
-- 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''
inst : Finite V
⊢ Finite.{u + 1} G.ConnectedComponent

Tactic:
Quot.finite _

Premises used: Quot.finite, SimpleGraph.ConnectedComponent
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
β : G.ConnectedComponent → Prop
h : ∀ (v : V), β (G.connectedComponentMk v)
c : G.ConnectedComponent
⊢ β c

Tactic:
Quot.ind h c

Premises used: Quot.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
β : G.ConnectedComponent → G.ConnectedComponent → Prop
h : ∀ (v w : V), β (G.connectedComponentMk v) (G.connectedComponentMk w)
c d : G.ConnectedComponent
⊢ β c d

Tactic:
Quot.induction_on₂ c d h

Premises used: Quot.induction_on₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.Reachable v w → G.connectedComponentMk v = G.connectedComponentMk w

Tactic:
Quot.sound

Premises used: SimpleGraph.connectedComponentMk, Quot.sound, SimpleGraph.ConnectedComponent
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.connectedComponentMk v = G.connectedComponentMk w → G.Reachable v w

Tactic:
@Quotient.exact _ G.reachableSetoid _ _

Premises used: SimpleGraph.connectedComponentMk, SimpleGraph.ConnectedComponent, Quotient, Quotient.exact
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.connectedComponentMk v = G.connectedComponentMk w ↔ G.Reachable v w

Tactic:
@Quotient.eq' _ G.reachableSetoid _ _

Premises used: SimpleGraph.connectedComponentMk, SimpleGraph.ConnectedComponent, Quotient.eq', Quotient
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v w : V
a : G.Adj v w
⊢ G.connectedComponentMk v = G.connectedComponentMk w

Tactic:
ConnectedComponent.sound a.reachable

Premises used: SimpleGraph.Adj.reachable, SimpleGraph.ConnectedComponent.sound
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
β : Sort u_1
f : V → β
h : ∀ (v w : V) (p : G.Walk v w), p.IsPath → f v = f w
v : V
⊢ ConnectedComponent.lift f h (G.connectedComponentMk v) = f v

Tactic:
rfl

Premises used: SimpleGraph.ConnectedComponent.lift, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
p : G.ConnectedComponent → Prop
⊢ (∃ (c : G.ConnectedComponent), p c) ↔ ∃ (v : V), p (G.connectedComponentMk v)

Tactic:
Quot.mk_surjective.exists

Premises used: SimpleGraph.connectedComponentMk, Function.Surjective.exists, SimpleGraph.ConnectedComponent, Quot.mk_surjective
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
p : G.ConnectedComponent → Prop
⊢ (∀ (c : G.ConnectedComponent), p c) ↔ ∀ (v : V), p (G.connectedComponentMk v)

Tactic:
Quot.mk_surjective.forall

Premises used: Function.Surjective.forall, SimpleGraph.connectedComponentMk, SimpleGraph.ConnectedComponent, Quot.mk_surjective
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
h : G.Preconnected
⊢ Subsingleton.{u + 1} G.ConnectedComponent

Tactic:
⟨ConnectedComponent.ind₂ fun v w => ConnectedComponent.sound (h v w)⟩

Premises used: Subsingleton.intro, SimpleGraph.ConnectedComponent.ind₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G →g G'
v : V
⊢ map φ (G.connectedComponentMk v) = G'.connectedComponentMk ((φ : (a : V) → V') v)

Tactic:
rfl

Premises used: SimpleGraph.connectedComponentMk, SimpleGraph.ConnectedComponent.map, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ map Hom.id C = C

Tactic:
C.ind (fun _ => rfl)

Premises used: SimpleGraph.ConnectedComponent.ind
-- 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''
C : G.ConnectedComponent
φ : G →g G'
ψ : G' →g G''
⊢ map ψ (map φ C) = map (ψ.comp φ) C

Tactic:
C.ind (fun _ => rfl)

Premises used: SimpleGraph.ConnectedComponent.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
⊢ Surjective (map (Hom.ofLE h))

Tactic:
Quot.ind fun v ↦ ⟨G.connectedComponentMk v, rfl⟩

Premises used: SimpleGraph.connectedComponentMk, Quot.ind, SimpleGraph.ConnectedComponent, Exists.intro, Function.Surjective, rfl
-- 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
⊢ G'.connectedComponentMk ((φ : (a : V) → V') v) =
      map ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) φ).toRelHom (r := G.Adj) (s := G'.Adj)) C ↔
    G.connectedComponentMk v = C

Tactic:
C.ind fun u => ?_

Premises used: SimpleGraph.ConnectedComponent.ind
-- 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
refine :
  ∀ (u : V),
    G'.connectedComponentMk ((φ : (a : V) → V') v) =
        map ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) φ).toRelHom (r := G.Adj) (s := G'.Adj))
          (G.connectedComponentMk u) ↔
      G.connectedComponentMk v = G.connectedComponentMk u
⊢ G'.connectedComponentMk ((φ : (a : V) → V') v) =
      map ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) φ).toRelHom (r := G.Adj) (s := G'.Adj)) C ↔
    G.connectedComponentMk v = C

Tactic:
refine C.ind fun u => ?_
-- 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 ((φ : (a : V) → V') v) =
      map ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) φ).toRelHom (r := G.Adj) (s := G'.Adj))
        (G.connectedComponentMk u) ↔
    G.connectedComponentMk v = G.connectedComponentMk u

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

Premises used: SimpleGraph.Iso.reachable_iff, RelEmbedding.coe_toRelHom, SimpleGraph.ConnectedComponent.map_mk, SimpleGraph.ConnectedComponent.eq, RelIso.coe_toRelEmbedding
-- 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
⊢ G.connectedComponentMk ((φ.symm : (a : V') → V) v') = C ↔
    G'.connectedComponentMk v' =
      map ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) φ).toRelHom (r := G.Adj) (s := G'.Adj)) C

Tactic:
C.ind fun u => ?_

Premises used: SimpleGraph.ConnectedComponent.ind
-- 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
refine :
  ∀ (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)
⊢ G.connectedComponentMk ((φ.symm : (a : V') → V) v') = C ↔
    G'.connectedComponentMk v' =
      map ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) φ).toRelHom (r := G.Adj) (s := G'.Adj)) C

Tactic:
refine C.ind fun u => ?_