awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
hs_mem : s ∈ K.parts
rw : 0 < t
⊢ s.Nonempty

Tactic:
rw [← Finset.card_pos, hs]

Premises used: Finset.card_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
hs_mem : s ∈ K.parts
⊢ 0 < t

Tactic:
Nat.pos_of_ne_zero ht

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
hs_mem : s ∈ K.parts
⊢ 0 < t

Tactic:
exact Nat.pos_of_ne_zero ht

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
hs_mem : s ∈ K.parts
neg : ∀ (v : V) (hv : v ∈ s), False
⊢ False

Tactic:
obtain ⟨v, hv⟩ : s.Nonempty := by
          rw [← Finset.card_pos, hs]
          exact Nat.pos_of_ne_zero ht

Premises used: Finset.Nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
hs_mem : s ∈ K.parts
v : V
hv : v ∈ s
⊢ ¬?_mvar.101240

Tactic:
hadj s hs_mem hv hv
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
hs_mem : s ∈ K.parts
v : V
hv : v ∈ s
neg : ¬G.Adj v v
⊢ False

Tactic:
absurd hadj s hs_mem hv hv
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
hs_mem : s ∈ K.parts
v : V
hv : v ∈ s
⊢ ¬G.Adj v v

Tactic:
G.loopless.irrefl v

Premises used: Std.Irrefl.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
hs_mem : s ∈ K.parts
v : V
hv : v ∈ s
⊢ ¬G.Adj v v

Tactic:
exact G.loopless.irrefl v

Premises used: Std.Irrefl.irrefl
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
neg : r + 1 = r + 1 ∨ t = 0
⊢ #(cons s K.parts ⋯) = r + 1 ∨ t = 0

Tactic:
rw [Finset.card_cons, K.card_parts.resolve_right ht]

Premises used: SimpleGraph.CompleteEquipartiteSubgraph.card_parts, Finset.card_cons, Or.resolve_right
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
⊢ r + 1 = r + 1 ∨ t = 0

Tactic:
.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
⊢ r + 1 = r + 1 ∨ t = 0

Tactic:
exact .inl rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
neg : #s = t ∧ ∀ a ∈ K.parts, #a = t
⊢ ∀ {p : Finset V}, p ∈ cons s K.parts ⋯ → #p = t

Tactic:
simp_rw [mem_cons, forall_eq_or_imp]

Premises used: forall_eq_or_imp, Finset.mem_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
⊢ #s = t ∧ ∀ a ∈ K.parts, #a = t

Tactic:
⟨hs, fun p ↦ K.card_mem_parts⟩

Premises used: And.intro, SimpleGraph.CompleteEquipartiteSubgraph.card_mem_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
⊢ #s = t ∧ ∀ a ∈ K.parts, #a = t

Tactic:
exact ⟨hs, fun p ↦ K.card_mem_parts⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
neg :
  (insert s (↑K.parts : Set (Finset V))).Pairwise fun (x1 x2 : Finset V) ↦
    G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)
⊢ (↑(cons s K.parts ⋯) : Set (Finset V)).Pairwise fun (x1 x2 : Finset V) ↦
    G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)

Tactic:
rw [coe_cons]

Premises used: Finset.coe_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
⊢ (insert s (↑K.parts : Set (Finset V))).Pairwise fun (x1 x2 : Finset V) ↦
    G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)

Tactic:
K.isCompleteBetween.insert_of_symmetric ?_ (fun p hp _ ↦ (hadj p hp).symm)

Premises used: SimpleGraph.CompleteEquipartiteSubgraph.isCompleteBetween, SimpleGraph.IsCompleteBetween.symm, Set.Pairwise.insert_of_symmetric
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
neg : Symmetric fun (x1 x2 : Finset V) ↦ G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)
⊢ (insert s (↑K.parts : Set (Finset V))).Pairwise fun (x1 x2 : Finset V) ↦
    G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)

Tactic:
refine K.isCompleteBetween.insert_of_symmetric ?_ (fun p hp _ ↦ (hadj p hp).symm)

Premises used: SimpleGraph.CompleteEquipartiteSubgraph.isCompleteBetween, SimpleGraph.IsCompleteBetween.symm, Set.Pairwise.insert_of_symmetric
-- Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
Goal:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
h :
  ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V),
    #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween (↑p : Set V) (↑s : Set V)
neg : ∀ ⦃x y : Finset V⦄, G.IsCompleteBetween (↑x : Set V) (↑y : Set V) → G.IsCompleteBetween (↑y : Set V) (↑x : Set V)
neg₁ : ∀ ⦃x y : Finset V⦄, G.IsCompleteBetween (↑x : Set V) (↑y : Set V) → G.IsCompleteBetween (↑x : Set V) (↑y : Set V)
neg₂ : ∀ ⦃x y : Finset V⦄, True
⊢ Symmetric fun (x1 x2 : Finset V) ↦ G.IsCompleteBetween (↑x1 : Set V) (↑x2 : Set V)

Tactic:
simp_rw [Symmetric, isCompleteBetween_comm, imp_self, implies_true]

Premises used: Symmetric, imp_self, SimpleGraph.isCompleteBetween_comm, implies_true
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u v ↔ Set.Nonempty.{u} (α := G.Walk u v) Set.univ

Tactic:
Set.nonempty_iff_univ_nonempty

Premises used: Set.nonempty_iff_univ_nonempty, SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ ¬G.Reachable u v ↔ IsEmpty.{u + 1} (G.Walk u v)

Tactic:
not_nonempty_iff

Premises used: not_nonempty_iff, SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
p : Prop
u v : V
h : G.Reachable u v
hp : ∀ (a : G.Walk u v), p
⊢ p

Tactic:
Nonempty.elim h hp

Premises used: Nonempty.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
p : Prop
u v : V
h : G.Reachable u v
hp : ∀ (a : G.Path u v), p
⊢ p

Tactic:
h.elim fun q => hp q.toPath

Premises used: SimpleGraph.Reachable.elim, SimpleGraph.Walk.toPath
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
p : Prop
u v : V
h : G.Reachable u v
hp : ∀ (a : G.Path u v), p
⊢ p

Tactic:
exact h.elim fun q => hp q.toPath

Premises used: SimpleGraph.Reachable.elim, SimpleGraph.Walk.toPath
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
p : Prop
u v : V
h : G.Reachable u v
hp : ∀ (a : G.Path u v), p
⊢ p

Tactic:
classical exact h.elim fun q => hp q.toPath
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ G.Reachable u v

Tactic:
⟨p⟩

Premises used: Nonempty.intro, SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ G.Reachable u v

Tactic:
h.toWalk.reachable

Premises used: SimpleGraph.Adj.toWalk, SimpleGraph.Walk.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
⊢ G.Adj ≤ G.Reachable

Tactic:
fun _ _ ↦ Adj.reachable

Premises used: SimpleGraph.Adj.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ G.Reachable u u

Tactic:
⟨Walk.nil⟩

Premises used: Nonempty.intro, SimpleGraph.Walk.nil, SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ G.Reachable u u

Tactic:
Reachable.refl _

Premises used: SimpleGraph.Reachable.refl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Reachable u v
⊢ G.Reachable v u

Tactic:
huv.elim fun p => ⟨p.reverse⟩

Premises used: SimpleGraph.Reachable.elim, Nonempty.intro, SimpleGraph.Walk.reverse
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u v ↔ G.Reachable v u

Tactic:
⟨Reachable.symm, Reachable.symm⟩

Premises used: SimpleGraph.Reachable.symm, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v w : V
huv : G.Reachable u v
hvw : G.Reachable v w
⊢ G.Reachable u w

Tactic:
huv.elim fun puv => hvw.elim fun pvw => ⟨puv.append pvw⟩

Premises used: SimpleGraph.Reachable.elim, Nonempty.intro, SimpleGraph.Walk.append
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
mp : G.Reachable u v → Relation.ReflTransGen G.Adj u v
mpr : Relation.ReflTransGen G.Adj u v → G.Reachable u v
⊢ G.Reachable u v ↔ Relation.ReflTransGen G.Adj u v

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Relation.ReflTransGen G.Adj u_1 u_1

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h' : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : Relation.ReflTransGen G.Adj v_1 w
⊢ Relation.ReflTransGen G.Adj u_1 w

Tactic:
(Relation.ReflTransGen.single h').trans ih

Premises used: Relation.ReflTransGen.trans, Relation.ReflTransGen.single
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h' : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : Relation.ReflTransGen G.Adj v_1 w
⊢ Relation.ReflTransGen G.Adj u_1 w

Tactic:
exact (Relation.ReflTransGen.single h').trans ih

Premises used: Relation.ReflTransGen.trans, Relation.ReflTransGen.single
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Walk u v
mp : ∀ {u : V}, Relation.ReflTransGen G.Adj u u
mp₁ :
  ∀ {u v w : V} (h' : G.Adj u v) (p : G.Walk v w) (ih : Relation.ReflTransGen G.Adj v w),
    Relation.ReflTransGen G.Adj u w
⊢ Relation.ReflTransGen G.Adj u v

Tactic:
induction h with
    | nil => rfl
    | cons h' _ ih => exact (Relation.ReflTransGen.single h').trans ih
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u u

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v b c : V
h : Relation.ReflTransGen G.Adj u b
ha : G.Adj b c
hr : G.Reachable u b
⊢ G.Reachable u c

Tactic:
Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩

Premises used: SimpleGraph.Reachable.trans, Nonempty.intro, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v b c : V
h : Relation.ReflTransGen G.Adj u b
ha : G.Adj b c
hr : G.Reachable u b
⊢ G.Reachable u c

Tactic:
exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩

Premises used: SimpleGraph.Reachable.trans, Nonempty.intro, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : Relation.ReflTransGen G.Adj u v
mpr : G.Reachable u u
mpr₁ : ∀ {b c : V}, Relation.ReflTransGen G.Adj u b → ∀ (ha : G.Adj b c) (hr : G.Reachable u b), G.Reachable u c
⊢ G.Reachable u v

Tactic:
induction h with
    | refl => rfl
    | tail _ ha hr => exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩

Premises used: refl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
h : ∀ (x x_1 : V), G.Reachable x x_1 ↔ Relation.ReflTransGen G.Adj x x_1
⊢ G.Reachable = Relation.ReflTransGen G.Adj

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
x x_1 : V
⊢ G.Reachable x x_1 ↔ Relation.ReflTransGen G.Adj x x_1

Tactic:
reachable_iff_reflTransGen ..

Premises used: SimpleGraph.reachable_iff_reflTransGen
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
x x_1 : V
⊢ G.Reachable x x_1 ↔ Relation.ReflTransGen G.Adj x x_1

Tactic:
exact reachable_iff_reflTransGen ..

Premises used: SimpleGraph.reachable_iff_reflTransGen
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
s : Set (Sym2 V)
rw : Relation.TransGen (Relation.ReflGen (fromEdgeSet s).Adj) = Relation.TransGen (Relation.ReflGen (Sym2.ToRel s))
⊢ (fromEdgeSet s).Reachable = Relation.ReflTransGen (Sym2.ToRel s)

Tactic:
rw [reachable_eq_reflTransGen, ← Relation.transGen_reflGen, ← Relation.transGen_reflGen]

Premises used: Relation.transGen_reflGen, SimpleGraph.reachable_eq_reflTransGen
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
s : Set (Sym2 V)
e_r : Relation.ReflGen (fromEdgeSet s).Adj = Relation.ReflGen (Sym2.ToRel s)
⊢ Relation.TransGen (Relation.ReflGen (fromEdgeSet s).Adj) = Relation.TransGen (Relation.ReflGen (Sym2.ToRel s))

Tactic:
congr 1
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
s : Set (Sym2 V)
e_r : ∀ (x x_1 : V), Relation.ReflGen (fromEdgeSet s).Adj x x_1 ↔ Relation.ReflGen (Sym2.ToRel s) x x_1
⊢ Relation.ReflGen (fromEdgeSet s).Adj = Relation.ReflGen (Sym2.ToRel s)

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
s : Set (Sym2 V)
x x_1 : V
mp : x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 → x_1 = x ∨ s(x, x_1) ∈ s
mpr : x_1 = x ∨ s(x, x_1) ∈ s → x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1
mp₁ : x_1 = x → x_1 = x ∨ s(x, x_1) ∈ s
mp₂ : s(x, x_1) ∈ s → ¬x = x_1 → x_1 = x ∨ s(x, x_1) ∈ s
mp₃ : x_1 = x → x_1 = x ∨ s(x, x_1) ∈ s
mp₄ : s(x, x_1) ∈ s → ¬x = x_1 → x_1 = x ∨ s(x, x_1) ∈ s
mp₅ : x_1 = x → ¬x_1 = x → s(x, x_1) ∈ s
mp₆ : s(x, x_1) ∈ s → ¬x = x_1 → ¬x_1 = x → s(x, x_1) ∈ s
mpr₁ : x_1 = x → x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1
mpr₂ : s(x, x_1) ∈ s → x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1
mpr₃ : x_1 = x → x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1
mpr₄ : s(x, x_1) ∈ s → x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1
mpr₅ : x_1 = x → ¬x_1 = x → s(x, x_1) ∈ s
mpr₆ : x_1 = x → ¬x_1 = x → ¬x = x_1
mpr₇ : s(x, x_1) ∈ s → ¬x_1 = x → s(x, x_1) ∈ s
mpr₈ : s(x, x_1) ∈ s → ¬x_1 = x → ¬x = x_1
mp₇ mpr₉ : x_1 = x → ¬x_1 = x → s(x, x_1) ∈ s
mpr₁₀ : x_1 = x → ¬x_1 = x → x = x_1 → False
mpr₁₁ mpr₁₂ mpr₁₃ mpr₁₄ mpr₁₅ mpr₁₆ mpr₁₇ mpr₁₈ : s(x, x_1) ∈ s → ¬x_1 = x → x = x_1 → False
⊢ x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 ↔ x_1 = x ∨ s(x, x_1) ∈ s

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
s : Set (Sym2 V)
x x_1 : V
simpa : x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 ↔ x_1 = x ∨ s(x, x_1) ∈ s
⊢ Relation.ReflGen (fromEdgeSet s).Adj x x_1 ↔ Relation.ReflGen (Sym2.ToRel s) x x_1

Tactic:
simpa [Relation.reflGen_iff] using by tauto

Premises used: Relation.reflGen_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
r : V → V → Prop
sym : Symmetric r
⊢ (fromEdgeSet (Sym2.fromRel (r := r) sym)).Reachable = Relation.ReflTransGen r

Tactic:
reachable_fromEdgeSet_eq_reflTransGen_toRel

Premises used: Set.Mem, setOf, SimpleGraph.reachable_fromEdgeSet_eq_reflTransGen_toRel, Sym2.fromRel, Sym2.ToRel
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
u v : V
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
h : G.Reachable u v
⊢ G'.Reachable ((f : (a : V) → V') u) ((f : (a : V) → V') v)

Tactic:
h.elim fun p => ⟨p.map f⟩

Premises used: SimpleGraph.Walk.map, SimpleGraph.Reachable.elim, Nonempty.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
u v : V
G G' : SimpleGraph V
h : G ≤ G'
Guv : G.Reachable u v
⊢ G'.Reachable u v

Tactic:
Guv.map (.ofLE h)

Premises used: SimpleGraph.Reachable.map, SimpleGraph.Hom.ofLE
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
⊢ G.Reachable ≤ G'.Reachable

Tactic:
fun _ _ ↦ Reachable.mono h

Premises used: SimpleGraph.Reachable.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
hr : G.Reachable u v
obtain : ∀ (W : G.Walk u v), ∃ (p : G.Walk u v), p.IsPath
⊢ ∃ (p : G.Walk u v), p.IsPath

Tactic:
obtain ⟨W⟩ := hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
W : G.Walk u v
⊢ ∃ (p : G.Walk u v), p.IsPath

Tactic:
⟨_, Path.isPath W.toPath⟩

Premises used: SimpleGraph.Walk.toPath, SimpleGraph.Path.isPath, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
W : G.Walk u v
⊢ ∃ (p : G.Walk u v), p.IsPath

Tactic:
exact ⟨_, Path.isPath W.toPath⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
hr : G.Reachable u v
obtain : ∀ (W : G.Walk u v), ∃ (p : G.Walk u v), p.IsPath
⊢ ∃ (p : G.Walk u v), p.IsPath

Tactic:
classical
  obtain ⟨W⟩ := hr
  exact ⟨_, Path.isPath W.toPath⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u v : V
⊢ G'.Reachable ((φ : (a : V) → V') u) ((φ : (a : V) → V') v) ↔ G.Reachable u v

Tactic:
⟨fun r => φ.left_inv u ▸ φ.left_inv v ▸ r.map φ.symm.toHom, Reachable.map φ.toHom⟩

Premises used: Eq.rec, SimpleGraph.Iso.toHom, SimpleGraph.Reachable.map, Iff.intro, SimpleGraph.Iso.symm, RelIso.toEquiv, Equiv.left_inv
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u : V
v : V'
rw :
  G'.Reachable ((φ : (a : V) → V') ((φ.symm : (a : V') → V) v : V)) ((φ : (a : V) → V') u) ↔
    G'.Reachable v ((φ : (a : V) → V') u)
rw₁ : Type v
rw₂ : SimpleGraph V'
rw₃ : G ≃g G'
rw₄ rw₅ : G'.Reachable v ((φ : (a : V) → V') u) ↔ G'.Reachable v ((φ : (a : V) → V') u)
⊢ G.Reachable ((φ.symm : (a : V') → V) v) u ↔ G'.Reachable v ((φ : (a : V) → V') u)

Tactic:
rw [← Iso.reachable_iff, RelIso.apply_symm_apply]

Premises used: SimpleGraph.Iso.reachable_iff, RelIso.apply_symm_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
v' : V
hv' : v' ∈ H.verts
p : G.Walk v' v
pos : ∀ (hnp : p.Nil), v ∈ H.verts
neg : ∀ (hnp : ¬p.Nil), v ∈ H.verts
⊢ v ∈ H.verts

Tactic:
by_cases hnp : p.Nil

Premises used: SimpleGraph.Walk.Nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
v' : V
hv' : v' ∈ H.verts
p : G.Walk v' v
hnp : p.Nil
⊢ v ∈ H.verts

Tactic:
hnp.eq ▸ hv'

Premises used: Eq.rec, SimpleGraph.Walk.Nil.eq