awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact hnp.eq ▸ hv'
-- 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:
aux (H.edge_vert (h _ hv' _ (Walk.adj_snd hnp)).symm) p.tail

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Subgraph.Adj.symm, SimpleGraph.Walk.tail, SimpleGraph.Walk.adj_snd
-- 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:
exact aux (H.edge_vert (h _ hv' _ (Walk.adj_snd hnp)).symm) p.tail

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Subgraph.Adj.symm, SimpleGraph.Walk.tail, SimpleGraph.Walk.adj_snd
-- 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 ∈ H.verts

Tactic:
aux hu hr.some

Premises used: Nonempty.some
-- 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 ∈ H.verts

Tactic:
exact aux hu hr.some

Premises used: Nonempty.some
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v
h_1 :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
          PSigma.casesOn (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) (motive :=
            fun (_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) x
            fun (v' : V) (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
            PSigma.casesOn (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) (motive :=
              fun (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) hv' fun (hv' : v' ∈ H.verts) (p : G.Walk v' v) ↦
              p.length)
        y _x →
      v ∈ H.verts
v' : V
hv'_1 : (_ : v' ∈ H.verts) ×' G.Walk v' v
h_2 :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
          PSigma.casesOn (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) (motive :=
            fun (_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) x
            fun (v' : V) (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
            PSigma.casesOn (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) (motive :=
              fun (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) hv' fun (hv' : v' ∈ H.verts) (p : G.Walk v' v) ↦
              p.length)
        y (PSigma.mk (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) v' hv'_1) →
      v ∈ H.verts
hv' : v' ∈ H.verts
p : G.Walk v' v
h_3 :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
          PSigma.casesOn (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) (motive :=
            fun (_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) x
            fun (v' : V) (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
            PSigma.casesOn (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) (motive :=
              fun (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) hv' fun (hv' : v' ∈ H.verts) (p : G.Walk v' v) ↦
              p.length)
        y
        (PSigma.mk (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) v'
          (PSigma.mk (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) hv' p)) →
      v ∈ H.verts
hnp : ¬p.Nil
rw : p.tail.length < p.tail.length + 1
⊢ p.tail.length < p.length

Tactic:
rw [← Walk.length_tail_add_one hnp]

Premises used: SimpleGraph.Walk.length_tail_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v
h_1 :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
          PSigma.casesOn (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) (motive :=
            fun (_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) x
            fun (v' : V) (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
            PSigma.casesOn (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) (motive :=
              fun (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) hv' fun (hv' : v' ∈ H.verts) (p : G.Walk v' v) ↦
              p.length)
        y _x →
      v ∈ H.verts
v' : V
hv'_1 : (_ : v' ∈ H.verts) ×' G.Walk v' v
h_2 :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
          PSigma.casesOn (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) (motive :=
            fun (_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) x
            fun (v' : V) (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
            PSigma.casesOn (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) (motive :=
              fun (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) hv' fun (hv' : v' ∈ H.verts) (p : G.Walk v' v) ↦
              p.length)
        y (PSigma.mk (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) v' hv'_1) →
      v ∈ H.verts
hv' : v' ∈ H.verts
p : G.Walk v' v
h_3 :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
          PSigma.casesOn (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) (motive :=
            fun (_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) x
            fun (v' : V) (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
            PSigma.casesOn (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) (motive :=
              fun (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) hv' fun (hv' : v' ∈ H.verts) (p : G.Walk v' v) ↦
              p.length)
        y
        (PSigma.mk (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) v'
          (PSigma.mk (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) hv' p)) →
      v ∈ H.verts
hnp : ¬p.Nil
⊢ p.tail.length < p.tail.length + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v
h_1 :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
          PSigma.casesOn (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) (motive :=
            fun (_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) x
            fun (v' : V) (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
            PSigma.casesOn (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) (motive :=
              fun (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) hv' fun (hv' : v' ∈ H.verts) (p : G.Walk v' v) ↦
              p.length)
        y _x →
      v ∈ H.verts
v' : V
hv'_1 : (_ : v' ∈ H.verts) ×' G.Walk v' v
h_2 :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
          PSigma.casesOn (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) (motive :=
            fun (_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) x
            fun (v' : V) (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
            PSigma.casesOn (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) (motive :=
              fun (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) hv' fun (hv' : v' ∈ H.verts) (p : G.Walk v' v) ↦
              p.length)
        y (PSigma.mk (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) v' hv'_1) →
      v ∈ H.verts
hv' : v' ∈ H.verts
p : G.Walk v' v
h_3 :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
          PSigma.casesOn (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) (motive :=
            fun (_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) x
            fun (v' : V) (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
            PSigma.casesOn (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) (motive :=
              fun (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) hv' fun (hv' : v' ∈ H.verts) (p : G.Walk v' v) ↦
              p.length)
        y
        (PSigma.mk (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) v'
          (PSigma.mk (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) hv' p)) →
      v ∈ H.verts
hnp : ¬p.Nil
rw rw₁ rw₂ : p.tail.length < p.tail.length + 1
⊢ p.tail.length < p.length

Tactic:
{
    rw [← Walk.length_tail_add_one hnp]
    lia
  }

Premises used: SimpleGraph.Walk.length_tail_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v
h_1 :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
          PSigma.casesOn (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) (motive :=
            fun (_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) x
            fun (v' : V) (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
            PSigma.casesOn (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) (motive :=
              fun (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) hv' fun (hv' : v' ∈ H.verts) (p : G.Walk v' v) ↦
              p.length)
        y _x →
      v ∈ H.verts
v' : V
hv'_1 : (_ : v' ∈ H.verts) ×' G.Walk v' v
h_2 :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
          PSigma.casesOn (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) (motive :=
            fun (_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) x
            fun (v' : V) (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
            PSigma.casesOn (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) (motive :=
              fun (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) hv' fun (hv' : v' ∈ H.verts) (p : G.Walk v' v) ↦
              p.length)
        y (PSigma.mk (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) v' hv'_1) →
      v ∈ H.verts
hv' : v' ∈ H.verts
p : G.Walk v' v
h_3 :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
          PSigma.casesOn (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) (motive :=
            fun (_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) x
            fun (v' : V) (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦
            PSigma.casesOn (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) (motive :=
              fun (hv' : (_ : v' ∈ H.verts) ×' G.Walk v' v) ↦ ℕ) hv' fun (hv' : v' ∈ H.verts) (p : G.Walk v' v) ↦
              p.length)
        y
        (PSigma.mk (β := fun {v' : V} ↦ (_ : v' ∈ H.verts) ×' G.Walk v' v) v'
          (PSigma.mk (β := fun (hv' : v' ∈ H.verts) ↦ G.Walk v' v) hv' p)) →
      v ∈ H.verts
hnp : ¬p.Nil
decreasing_by decreasing_by₁ decreasing_by₂ : p.tail.length < p.tail.length + 1
⊢ p.tail.length < p.length

Tactic:
decreasing_by {
    rw [← Walk.length_tail_add_one hnp]
    lia
  }

Premises used: SimpleGraph.Walk.length_tail_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
⊢ Equivalence G.Reachable

Tactic:
Equivalence.mk (@Reachable.refl _ G) (@Reachable.symm _ G) (@Reachable.trans _ G)

Premises used: SimpleGraph.Reachable.symm, SimpleGraph.Reachable.trans, Equivalence.mk, SimpleGraph.Reachable.refl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
u v : V
⊢ Reachable ⊥ u v ↔ u = v

Tactic:
⟨fun h ↦ h.elim fun p ↦ match p with | .nil => rfl, fun h ↦ h ▸ .rfl⟩

Premises used: SimpleGraph.Reachable.elim, _private.0.SimpleGraph.reachable_bot.match_1, Eq.rec, SimpleGraph.Reachable.rfl, Iff.intro, Eq, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
u v : V
inl : (completeGraph V).Reachable u u
inr : ∀ (huv : u ≠ v), (completeGraph V).Reachable u v
⊢ (completeGraph V).Reachable u v

Tactic:
obtain rfl | huv := eq_or_ne u v

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
u : V
⊢ (completeGraph V).Reachable u u

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
u v : V
huv : u ≠ v
⊢ (completeGraph V).Reachable u v

Tactic:
⟨.cons huv .nil⟩

Premises used: Nonempty.intro, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, SimpleGraph.Reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
u v : V
huv : u ≠ v
⊢ (completeGraph V).Reachable u v

Tactic:
exact ⟨.cons huv .nil⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : Subsingleton V
u v : V
rw rw₁ : G.Reachable v v
⊢ G.Reachable u v

Tactic:
rw [Subsingleton.allEq u v]

Premises used: Subsingleton.allEq
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
hreach : G.Reachable u v
nil : ∀ (huv : u ≠ u), (G.neighborSet u).Nonempty
cons : ∀ {x : V} (hadj : G.Adj u x) (w' : G.Walk x v), (G.neighborSet u).Nonempty
⊢ (G.neighborSet u).Nonempty

Tactic:
obtain ⟨_ | @⟨u, x, v, hadj, w'⟩⟩ := hreach
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u : V
huv : u ≠ u
⊢ (G.neighborSet u).Nonempty

Tactic:
contradiction
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
x : V
hadj : G.Adj u x
w' : G.Walk x v
⊢ (G.neighborSet u).Nonempty

Tactic:
⟨x, hadj⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
x : V
hadj : G.Adj u x
w' : G.Walk x v
⊢ (G.neighborSet u).Nonempty

Tactic:
exact ⟨x, hadj⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
hreach : G.Reachable u v
⊢ (G.neighborSet v).Nonempty

Tactic:
hreach.symm.nonempty_neighborSet_left huv.symm

Premises used: SimpleGraph.Reachable.symm, Ne.symm, SimpleGraph.Reachable.nonempty_neighborSet_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : Fintype (↑(G.neighborSet u) : Type u)
huv : u ≠ v
hreach : G.Reachable u v
⊢ 0 < G.degree u

Tactic:
degree_pos_iff_nonempty.mpr (hreach.nonempty_neighborSet_left huv)

Premises used: Iff.mpr, SimpleGraph.degree_pos_iff_nonempty, SimpleGraph.Reachable.nonempty_neighborSet_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : Fintype (↑(G.neighborSet v) : Type u)
huv : u ≠ v
hreach : G.Reachable u v
⊢ 0 < G.degree v

Tactic:
hreach.symm.degree_pos_left huv.symm

Premises used: SimpleGraph.Reachable.symm, Ne.symm, SimpleGraph.Reachable.degree_pos_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
hu : G.neighborSet u = ∅
⊢ ¬G.Reachable u v

Tactic:
(Reachable.nonempty_neighborSet_left huv).mt (Set.not_nonempty_iff_eq_empty.mpr hu)

Premises used: Iff.mpr, Function.mt, Set.not_nonempty_iff_eq_empty, SimpleGraph.Reachable.nonempty_neighborSet_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
hv : G.neighborSet v = ∅
⊢ ¬G.Reachable u v

Tactic:
fun r ↦ not_reachable_of_neighborSet_left_eq_empty huv.symm hv r.symm

Premises used: SimpleGraph.Reachable.symm, Ne.symm, SimpleGraph.not_reachable_of_neighborSet_left_eq_empty, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : Fintype (↑(G.neighborSet u) : Type u)
huv : u ≠ v
hu : G.degree u = 0
⊢ ¬0 < G.degree u

Tactic:
simp [hu]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : Fintype (↑(G.neighborSet v) : Type u)
huv : u ≠ v
hu : G.degree v = 0
rw : ¬G.Reachable v u
⊢ ¬G.Reachable u v

Tactic:
rw [reachable_comm]

Premises used: SimpleGraph.reachable_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : Fintype (↑(G.neighborSet v) : Type u)
huv : u ≠ v
hu : G.degree v = 0
⊢ ¬G.Reachable v u

Tactic:
not_reachable_of_left_degree_zero huv.symm hu

Premises used: Ne.symm, SimpleGraph.not_reachable_of_left_degree_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
u v : V
inst : Fintype (↑(G.neighborSet v) : Type u)
huv : u ≠ v
hu : G.degree v = 0
⊢ ¬G.Reachable v u

Tactic:
exact not_reachable_of_left_degree_zero huv.symm hu

Premises used: Ne.symm, SimpleGraph.not_reachable_of_left_degree_zero
-- 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.Preconnected
⊢ H.Preconnected

Tactic:
hf.forall₂.2 fun _ _ => Nonempty.map (Walk.map _) <| hG _ _

Premises used: SimpleGraph.Walk.map, Iff.mpr, SimpleGraph.Preconnected, Nonempty.map, Function.Surjective.forall₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
hG : G.Preconnected
⊢ G'.Preconnected

Tactic:
fun u v => (hG u v).mono h

Premises used: SimpleGraph.Preconnected, SimpleGraph.Reachable.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
⊢ G.Preconnected ↔ G.Reachable = ⊤

Tactic:
aesop (add simp Preconnected)

Premises used: SimpleGraph.Preconnected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
h : Subsingleton V
⊢ Preconnected.{u} (V := V) ⊥

Tactic:
simp [Preconnected]

Premises used: SimpleGraph.Preconnected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
refine : ∀ (h : Preconnected.{u} (V := V) ⊥), Subsingleton V
⊢ Preconnected.{u} (V := V) ⊥ ↔ Subsingleton V

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [Preconnected]⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
h : Preconnected.{u} (V := V) ⊥
contrapose! : ∀ (h : Nontrivial V), ¬Preconnected.{u} (V := V) ⊥
⊢ Subsingleton V

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
h : Nontrivial V
⊢ ¬Preconnected.{u} (V := V) ⊥

Tactic:
simp [nontrivial_iff.mp h, Preconnected, reachable_bot]

Premises used: SimpleGraph.Preconnected, nontrivial_iff, SimpleGraph.reachable_bot, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Subsingleton V
⊢ Preconnected.{u} (V := V) ⊥

Tactic:
preconnected_bot_iff_subsingleton.mpr ‹_›

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

Tactic:
preconnected_bot_iff_subsingleton.not.mpr <| not_subsingleton_iff_nontrivial.mpr ‹_›

Premises used: Iff.mpr, Iff.not, SimpleGraph.preconnected_bot_iff_subsingleton, not_subsingleton_iff_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
x y : V
h : x = y
rw rw₁ : Reachable ⊤ y y
⊢ Reachable ⊤ x y

Tactic:
rw [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
x y : V
h : ¬x = y
⊢ Reachable ⊤ x y

Tactic:
Adj.reachable h

Premises used: SimpleGraph.Adj.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
x y : V
h : ¬x = y
⊢ Reachable ⊤ x y

Tactic:
exact Adj.reachable h

Premises used: SimpleGraph.Adj.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
x y : V
if : ∀ (h : x = y), Reachable ⊤ x y
if₁ : ∀ (h : ¬x = y), Reachable ⊤ x y
if₂ : ∀ (h : x = y), Reachable ⊤ x y
if₃ if₄ : ∀ (h : ¬x = y), Reachable ⊤ x y
⊢ Reachable ⊤ x y

Tactic:
if h : x = y then rw [h] else exact Adj.reachable h
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
G : SimpleGraph V
inst : Subsingleton V
⊢ G.Preconnected

Tactic:
fun _ _ ↦ .of_subsingleton

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

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

Premises used: SimpleGraph.Preconnected.map, SimpleGraph.Iso.toHom, Iff.intro, SimpleGraph.Iso.symm, Equiv.surjective, RelIso.toEquiv
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
simp : ∀ (x : V), x ∈ G.support
⊢ G.support = Set.univ

Tactic:
simp only [Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v : V
obtain : ∀ (w : V) (hw : w ≠ v), v ∈ G.support
⊢ v ∈ G.support

Tactic:
obtain ⟨w, hw⟩ := exists_ne v

Premises used: exists_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v w : V
hw : w ≠ v
obtain : ∀ (p : G.Walk v w), v ∈ G.support
⊢ v ∈ G.support

Tactic:
obtain ⟨p⟩ := h v w
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v : V
hw : v ≠ v
⊢ v ∈ G.support

Tactic:
contradiction
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v w_1 : V
hw : w_1 ≠ v
w : V
h_1 : G.Adj v w
p : G.Walk w w_1
⊢ v ∈ G.support

Tactic:
⟨w, ‹_›⟩

Premises used: Set.Mem, setOf, SetRel.dom, SimpleGraph.support, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v w_1 : V
hw : w_1 ≠ v
w : V
h_1 : G.Adj v w
p : G.Walk w w_1
⊢ v ∈ G.support

Tactic:
exact ⟨w, ‹_›⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v w : V
hw : w ≠ v
p : G.Walk v w
nil : ∀ (hw : v ≠ v), v ∈ G.support
cons : ∀ {w_1 : V}, G.Adj v w_1 → ∀ (p : G.Walk w_1 w), v ∈ G.support
⊢ v ∈ G.support

Tactic:
cases p with
  | nil => contradiction
  | @cons _ w => exact ⟨w, ‹_›⟩