awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 ↔ x_1 = x ∨ s(x, x_1) ∈ s
have mp₁ : x_1 = x → x_1 = x ∨ s(x, x_1) ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 ↔ x_1 = x ∨ s(x, x_1) ∈ s
have mp₂ : s(x, x_1) ∈ s → ¬x = x_1 → x_1 = x ∨ s(x, x_1) ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 ↔ x_1 = x ∨ s(x, x_1) ∈ s
have mp₅ : x_1 = x → ¬x_1 = x → s(x, x_1) ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 ↔ x_1 = x ∨ s(x, x_1) ∈ s
have mp₆ : s(x, x_1) ∈ s → ¬x = x_1 → ¬x_1 = x → s(x, x_1) ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 ↔ x_1 = x ∨ s(x, x_1) ∈ s
have mpr₁ : x_1 = x → x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 ↔ x_1 = x ∨ s(x, x_1) ∈ s
have mpr₂ : s(x, x_1) ∈ s → x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 ↔ x_1 = x ∨ s(x, x_1) ∈ s
have mpr₆ : x_1 = x → ¬x_1 = x → ¬x = x_1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 ↔ x_1 = x ∨ s(x, x_1) ∈ s
have mpr₇ : s(x, x_1) ∈ s → ¬x_1 = x → s(x, x_1) ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 ↔ x_1 = x ∨ s(x, x_1) ∈ s
have mpr₈ : s(x, x_1) ∈ s → ¬x_1 = x → ¬x = x_1
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
s : Set (Sym2 V)
x x_1 : V
⊢ Relation.ReflGen (fromEdgeSet s).Adj x x_1 ↔ Relation.ReflGen (Sym2.ToRel s) x x_1
have simpa : x_1 = x ∨ s(x, x_1) ∈ s ∧ ¬x = x_1 ↔ x_1 = x ∨ s(x, x_1) ∈ s
Tactic: simpa [Relation.reflGen_iff] using by tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
hr : G.Reachable u v
⊢ ∃ (p : G.Walk u v), p.IsPath
have obtain : ∀ (W : G.Walk u v), ∃ (p : G.Walk u v), p.IsPath
Tactic: obtain ⟨W⟩ := hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
hr : G.Reachable u v
⊢ ∃ (p : G.Walk u v), p.IsPath
have obtain : ∀ (W : G.Walk u v), ∃ (p : G.Walk u v), p.IsPath
Tactic: classical
  obtain ⟨W⟩ := hr
  exact ⟨_, Path.isPath W.toPath⟩
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u : V
v : V'
⊢ G.Reachable ((φ.symm : (a : V') → V) v) u ↔ G'.Reachable v ((φ : (a : V) → V') u)
have rw : G'.Reachable ((φ : (a : V) → V') ((φ.symm : (a : V') → V) v : V)) ((φ : (a : V) → V') u) ↔
  G'.Reachable v ((φ : (a : V) → V') u)
Tactic: rw [← Iso.reachable_iff, RelIso.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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'
⊢ G.Reachable ((φ.symm : (a : V') → V) v) u ↔ G'.Reachable v ((φ : (a : V) → V') u)
have rw₄ : G'.Reachable v ((φ : (a : V) → V') u) ↔ G'.Reachable v ((φ : (a : V) → V') u)
Tactic: rw [← Iso.reachable_iff, RelIso.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ v ∈ H.verts
have pos : ∀ (hnp : p.Nil), v ∈ H.verts
Tactic: by_cases hnp : p.Nil
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ v ∈ H.verts
have neg : ∀ (hnp : ¬p.Nil), v ∈ H.verts
Tactic: by_cases hnp : p.Nil
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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.length
have rw : p.tail.length < p.tail.length + 1
Tactic: rw [← Walk.length_tail_add_one hnp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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.length
have rw : p.tail.length < p.tail.length + 1
Tactic: {
    rw [← Walk.length_tail_add_one hnp]
    lia
  }
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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.length
have decreasing_by : p.tail.length < p.tail.length + 1
Tactic: decreasing_by {
    rw [← Walk.length_tail_add_one hnp]
    lia
  }
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
u v : V
⊢ (completeGraph V).Reachable u v
have inl : (completeGraph V).Reachable u u
Tactic: obtain rfl | huv := eq_or_ne u v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
u v : V
inl : (completeGraph V).Reachable u u
⊢ (completeGraph V).Reachable u v
have inr : ∀ (huv : u ≠ v), (completeGraph V).Reachable u v
Tactic: obtain rfl | huv := eq_or_ne u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Subsingleton V
u v : V
⊢ G.Reachable u v
have rw : G.Reachable v v
Tactic: rw [Subsingleton.allEq u v]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
hreach : G.Reachable u v
⊢ (G.neighborSet u).Nonempty
have nil : ∀ (huv : u ≠ u), (G.neighborSet u).Nonempty
Tactic: obtain ⟨_ | @⟨u, x, v, hadj, w'⟩⟩ := hreach
Cleared hypotheses: v, huv, hreach
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ (G.neighborSet u).Nonempty
have cons : ∀ {x : V} (hadj : G.Adj u x) (w' : G.Walk x v), (G.neighborSet u).Nonempty
Tactic: obtain ⟨_ | @⟨u, x, v, hadj, w'⟩⟩ := hreach
Cleared hypotheses: hreach
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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 u v
have rw : ¬G.Reachable v u
Tactic: rw [reachable_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
⊢ Preconnected.{u} (V := V) ⊥ ↔ Subsingleton V
have refine : ∀ (h : Preconnected.{u} (V := V) ⊥), Subsingleton V
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [Preconnected]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
h : Preconnected.{u} (V := V) ⊥
⊢ Subsingleton V
have contrapose! : ∀ (h : Nontrivial V), ¬Preconnected.{u} (V := V) ⊥
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
x y : V
h : x = y
⊢ Reachable ⊤ x y
have rw : Reachable ⊤ y y
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
x y : V
⊢ Reachable ⊤ x y
have if : ∀ (h : x = y), Reachable ⊤ x y
Tactic: if h : x = y then rw [h] else exact Adj.reachable h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
x y : V
if : ∀ (h : x = y), Reachable ⊤ x y
⊢ Reachable ⊤ x y
have if₁ : ∀ (h : ¬x = y), Reachable ⊤ x y
Tactic: if h : x = y then rw [h] else exact Adj.reachable h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
⊢ G.support = Set.univ
have simp : ∀ (x : V), x ∈ G.support
Tactic: simp only [Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v : V
⊢ v ∈ G.support
have obtain : ∀ (w : V) (hw : w ≠ v), v ∈ G.support
Tactic: obtain ⟨w, hw⟩ := exists_ne v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v w : V
hw : w ≠ v
⊢ v ∈ G.support
have obtain : ∀ (p : G.Walk v w), v ∈ G.support
Tactic: obtain ⟨p⟩ := h v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
inst : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v w : V
hw : w ≠ v
p : G.Walk v w
⊢ v ∈ G.support
have nil : ∀ (hw : v ≠ v), v ∈ G.support
Tactic: cases p with
  | nil => contradiction
  | @cons _ w => exact ⟨w, ‹_›⟩
Cleared hypotheses: w, hw, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ v ∈ G.support
have cons : ∀ {w_1 : V}, G.Adj v w_1 → ∀ (p : G.Walk w_1 w), v ∈ G.support
Tactic: cases p with
  | nil => contradiction
  | @cons _ w => exact ⟨w, ‹_›⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
inst : Nontrivial V
inst_1 : Fintype V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
h : G.Preconnected
⊢ 0 < G.minDegree
have obtain : ∀ (v : V) (hv : G.minDegree = G.degree v), 0 < G.minDegree
Tactic: obtain ⟨v, hv⟩ := G.exists_minimal_degree_vertex
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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.minDegree
have rw : 0 < G.degree v
Tactic: rw [hv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
x : V
hx : x ∈ p.support
⊢ ∃ y ∈ p.support, G.Adj x y
have 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
Tactic: induction p with grind [Walk.nil_iff_support_eq, Walk.cons_tail_support, adj_comm]
Cleared hypotheses: p, hp, hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
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
⊢ ∃ y ∈ p.support, G.Adj x y
have 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
Tactic: induction p with grind [Walk.nil_iff_support_eq, Walk.cons_tail_support, adj_comm]
Cleared hypotheses: p, hp, hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
w : V
hw : w ∈ p.support
⊢ w ∈ G.support
have obtain : ∀ (y : V) (hy : y ∈ p.support ∧ G.Adj w y), w ∈ G.support
Tactic: obtain ⟨y, hy⟩ := adj_of_mem_walk_support p hp hw