internlm/Lean-Github huggingface dataset:
Theorem: Digraph.strong_induction
Proof state before:
V : Type u_1
inst✝ : Finite V
motive : Digraph V → Prop
hind : ∀ (G : Digraph V), (∀ (G' : Digraph V), G' < G → motive G') → motive G
this : Fintype V
G : Digraph V
ih : ∀ (t : Finset (V × V)), t ⊂ Set.toFinset (edgeSet G) → ∀ (G : Digraph V), Set.toFinset (edgeSet G) = t → motive G
G' : Digraph V
hG : G' < G
⊢ Set.toFinset (edgeSet G') ⊂ Set.toFinset (edgeSet G)
Tactic:
simpa using hG
Proof state after:
no goals
Theorem: Digraph.Walk.copy_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u' v' u'' v'' : V
p : Walk G u v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
⊢ Walk.copy (Walk.copy p hu hv) hu' hv' = Walk.copy p (_ : u = u'') (_ : v = v'')
Tactic:
subst_vars
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u'' v'' : V
p : Walk G u'' v''
⊢ Walk.copy (Walk.copy p (_ : u'' = u'') (_ : v'' = v'')) (_ : u'' = u'') (_ : v'' = v'') =
    Walk.copy p (_ : u'' = u'') (_ : v'' = v'')
Theorem: Digraph.Walk.copy_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u'' v'' : V
p : Walk G u'' v''
⊢ Walk.copy (Walk.copy p (_ : u'' = u'') (_ : v'' = v'')) (_ : u'' = u'') (_ : v'' = v'') =
    Walk.copy p (_ : u'' = u'') (_ : v'' = v'')
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.copy_nil
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u u' : V
hu : u = u'
⊢ Walk.copy nil hu hu = nil
Tactic:
subst_vars
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' : V
⊢ Walk.copy nil (_ : u' = u') (_ : u' = u') = nil
Theorem: Digraph.Walk.copy_nil
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' : V
⊢ Walk.copy nil (_ : u' = u') (_ : u' = u') = nil
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.copy_cons
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w u' w' : V
h : G.Adj u v
p : Walk G v w
hu : u = u'
hw : w = w'
⊢ Walk.copy (cons h p) hu hw = cons (_ : G.Adj u' v) (Walk.copy p (_ : v = v) hw)
Tactic:
subst_vars
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v u' w' : V
h : G.Adj u' v
p : Walk G v w'
⊢ Walk.copy (cons h p) (_ : u' = u') (_ : w' = w') = cons (_ : G.Adj u' v) (Walk.copy p (_ : v = v) (_ : w' = w'))
Theorem: Digraph.Walk.copy_cons
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v u' w' : V
h : G.Adj u' v
p : Walk G v w'
⊢ Walk.copy (cons h p) (_ : u' = u') (_ : w' = w') = cons (_ : G.Adj u' v) (Walk.copy p (_ : v = v) (_ : w' = w'))
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.cons_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w v' w' : V
h : G.Adj u v
p : Walk G v' w'
hv : v' = v
hw : w' = w
⊢ cons h (Walk.copy p hv hw) = Walk.copy (cons (_ : G.Adj u v') p) (_ : u = u) hw
Tactic:
subst_vars
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v' w' : V
p : Walk G v' w'
h : G.Adj u v'
⊢ cons h (Walk.copy p (_ : v' = v') (_ : w' = w')) = Walk.copy (cons (_ : G.Adj u v') p) (_ : u = u) (_ : w' = w')
Theorem: Digraph.Walk.cons_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v' w' : V
p : Walk G v' w'
h : G.Adj u v'
⊢ cons h (Walk.copy p (_ : v' = v') (_ : w' = w')) = Walk.copy (cons (_ : G.Adj u v') p) (_ : u = u) (_ : w' = w')
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.getVert_zero
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
w : Walk G u v
⊢ getVert w 0 = u
Tactic:
cases w <;> rfl
Proof state after:
no goals
Theorem: Digraph.Walk.getVert_of_length_le
Proof state before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ : V
i : ℕ
hi : length nil ≤ i
⊢ getVert nil i = u✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.getVert_of_length_le
Proof state before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, length p✝ ≤ i → getVert p✝ i = w✝
i : ℕ
hi : length (cons h✝ p✝) ≤ i
⊢ getVert (cons h✝ p✝) i = w✝
Tactic:
cases i
Proof state after:
case cons.zero
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, length p✝ ≤ i → getVert p✝ i = w✝
hi : length (cons h✝ p✝) ≤ Nat.zero
⊢ getVert (cons h✝ p✝) Nat.zero = w✝

case cons.succ
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, length p✝ ≤ i → getVert p✝ i = w✝
n✝ : ℕ
hi : length (cons h✝ p✝) ≤ Nat.succ n✝
⊢ getVert (cons h✝ p✝) (Nat.succ n✝) = w✝
Theorem: Digraph.Walk.getVert_of_length_le
Proof state before:
case cons.zero
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, length p✝ ≤ i → getVert p✝ i = w✝
hi : length (cons h✝ p✝) ≤ Nat.zero
⊢ getVert (cons h✝ p✝) Nat.zero = w✝
Tactic:
cases hi
Proof state after:
no goals
Theorem: Digraph.Walk.getVert_of_length_le
Proof state before:
case cons.succ
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, length p✝ ≤ i → getVert p✝ i = w✝
n✝ : ℕ
hi : length (cons h✝ p✝) ≤ Nat.succ n✝
⊢ getVert (cons h✝ p✝) (Nat.succ n✝) = w✝
Tactic:
exact ih (Nat.succ_le_succ_iff.1 hi)
Proof state after:
no goals
Theorem: Digraph.Walk.adj_getVert_succ
Proof state before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ : V
i : ℕ
hi : i < length nil
⊢ G.Adj (getVert nil i) (getVert nil (i + 1))
Tactic:
cases hi
Proof state after:
no goals
Theorem: Digraph.Walk.adj_getVert_succ
Proof state before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, i < length p✝ → G.Adj (getVert p✝ i) (getVert p✝ (i + 1))
i : ℕ
hi : i < length (cons hxy p✝)
⊢ G.Adj (getVert (cons hxy p✝) i) (getVert (cons hxy p✝) (i + 1))
Tactic:
cases i
Proof state after:
case cons.zero
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, i < length p✝ → G.Adj (getVert p✝ i) (getVert p✝ (i + 1))
hi : Nat.zero < length (cons hxy p✝)
⊢ G.Adj (getVert (cons hxy p✝) Nat.zero) (getVert (cons hxy p✝) (Nat.zero + 1))

case cons.succ
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, i < length p✝ → G.Adj (getVert p✝ i) (getVert p✝ (i + 1))
n✝ : ℕ
hi : Nat.succ n✝ < length (cons hxy p✝)
⊢ G.Adj (getVert (cons hxy p✝) (Nat.succ n✝)) (getVert (cons hxy p✝) (Nat.succ n✝ + 1))
Theorem: Digraph.Walk.adj_getVert_succ
Proof state before:
case cons.zero
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, i < length p✝ → G.Adj (getVert p✝ i) (getVert p✝ (i + 1))
hi : Nat.zero < length (cons hxy p✝)
⊢ G.Adj (getVert (cons hxy p✝) Nat.zero) (getVert (cons hxy p✝) (Nat.zero + 1))
Tactic:
simp [getVert, hxy]
Proof state after:
no goals
Theorem: Digraph.Walk.adj_getVert_succ
Proof state before:
case cons.succ
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, i < length p✝ → G.Adj (getVert p✝ i) (getVert p✝ (i + 1))
n✝ : ℕ
hi : Nat.succ n✝ < length (cons hxy p✝)
⊢ G.Adj (getVert (cons hxy p✝) (Nat.succ n✝)) (getVert (cons hxy p✝) (Nat.succ n✝ + 1))
Tactic:
exact ih (Nat.succ_lt_succ_iff.1 hi)
Proof state after:
no goals
Theorem: Digraph.Walk.append_nil
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
⊢ append p nil = p
Tactic:
induction p with
| nil => rfl
| cons _ _ ih => rw [cons_append, ih]
Proof state after:
no goals
Theorem: Digraph.Walk.append_nil
Proof state before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ : V
⊢ append nil nil = nil
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.append_nil
Proof state before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : append p✝ nil = p✝
⊢ append (cons h✝ p✝) nil = cons h✝ p✝
Tactic:
rw [cons_append, ih]
Proof state after:
no goals
Theorem: Digraph.Walk.append_assoc
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w x : V
p : Walk G u v
q : Walk G v w
r : Walk G w x
⊢ append p (append q r) = append (append p q) r
Tactic:
induction p with
| nil => rfl
| cons h p' ih =>
  dsimp only [append]
  rw [ih]
Proof state after:
no goals
Theorem: Digraph.Walk.append_assoc
Proof state before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w x : V
r : Walk G w x
u✝ : V
q : Walk G u✝ w
⊢ append nil (append q r) = append (append nil q) r
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.append_assoc
Proof state before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w x : V
r : Walk G w x
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : ∀ (q : Walk G w✝ w), append p' (append q r) = append (append p' q) r
q : Walk G w✝ w
⊢ append (cons h p') (append q r) = append (append (cons h p') q) r
Tactic:
dsimp only [append]
Proof state after:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w x : V
r : Walk G w x
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : ∀ (q : Walk G w✝ w), append p' (append q r) = append (append p' q) r
q : Walk G w✝ w
⊢ cons h (append p' (append q r)) = cons h (append (append p' q) r)
Theorem: Digraph.Walk.append_assoc
Proof state before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w x : V
r : Walk G w x
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : ∀ (q : Walk G w✝ w), append p' (append q r) = append (append p' q) r
q : Walk G w✝ w
⊢ cons h (append p' (append q r)) = cons h (append (append p' q) r)
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: Digraph.Walk.append_copy_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w u' v' w' : V
p : Walk G u v
q : Walk G v w
hu : u = u'
hv : v = v'
hw : w = w'
⊢ append (Walk.copy p hu hv) (Walk.copy q hv hw) = Walk.copy (append p q) hu hw
Tactic:
subst_vars
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' v' w' : V
p : Walk G u' v'
q : Walk G v' w'
⊢ append (Walk.copy p (_ : u' = u') (_ : v' = v')) (Walk.copy q (_ : v' = v') (_ : w' = w')) =
    Walk.copy (append p q) (_ : u' = u') (_ : w' = w')
Theorem: Digraph.Walk.append_copy_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' v' w' : V
p : Walk G u' v'
q : Walk G v' w'
⊢ append (Walk.copy p (_ : u' = u') (_ : v' = v')) (Walk.copy q (_ : v' = v') (_ : w' = w')) =
    Walk.copy (append p q) (_ : u' = u') (_ : w' = w')
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.concat_append
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w x : V
p : Walk G u v
h : G.Adj v w
q : Walk G w x
⊢ append (concat p h) q = append p (cons h q)
Tactic:
rw [concat_eq_append, ← append_assoc, cons_nil_append]
Proof state after:
no goals
Theorem: Digraph.Walk.exists_cons_eq_concat
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
h : G.Adj u v
p : Walk G v w
⊢ ∃ x q h', cons h p = concat q h'
Tactic:
induction p generalizing u with
| nil => exact ⟨_, nil, h, rfl⟩
| cons h' p ih =>
  obtain ⟨y, q, h'', hc⟩ := ih h'
  refine' ⟨y, cons h q, h'', _⟩
  rw [concat_cons, hc]
Proof state after:
no goals
Theorem: Digraph.Walk.exists_cons_eq_concat
Proof state before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w u✝ u : V
h : G.Adj u u✝
⊢ ∃ x q h', cons h nil = concat q h'
Tactic:
exact ⟨_, nil, h, rfl⟩
Proof state after:
no goals
Theorem: Digraph.Walk.exists_cons_eq_concat
Proof state before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : G.Adj u u✝
⊢ ∃ x q h'_1, cons h (cons h' p) = concat q h'_1
Tactic:
obtain ⟨y, q, h'', hc⟩ := ih h'
Proof state after:
case cons.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : G.Adj u u✝
y : V
q : Walk G u✝ y
h'' : G.Adj y w✝
hc : cons h' p = concat q h''
⊢ ∃ x q h'_1, cons h (cons h' p) = concat q h'_1
Theorem: Digraph.Walk.exists_cons_eq_concat
Proof state before:
case cons.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : G.Adj u u✝
y : V
q : Walk G u✝ y
h'' : G.Adj y w✝
hc : cons h' p = concat q h''
⊢ ∃ x q h'_1, cons h (cons h' p) = concat q h'_1
Tactic:
refine' ⟨y, cons h q, h'', _⟩
Proof state after:
case cons.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : G.Adj u u✝
y : V
q : Walk G u✝ y
h'' : G.Adj y w✝
hc : cons h' p = concat q h''
⊢ cons h (cons h' p) = concat (cons h q) h''
Theorem: Digraph.Walk.exists_cons_eq_concat
Proof state before:
case cons.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : G.Adj u u✝
y : V
q : Walk G u✝ y
h'' : G.Adj y w✝
hc : cons h' p = concat q h''
⊢ cons h (cons h' p) = concat (cons h q) h''
Tactic:
rw [concat_cons, hc]
Proof state after:
no goals
Theorem: Digraph.Walk.length_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u' v' : V
p : Walk G u v
hu : u = u'
hv : v = v'
⊢ length (Walk.copy p hu hv) = length p
Tactic:
subst_vars
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' v' : V
p : Walk G u' v'
⊢ length (Walk.copy p (_ : u' = u') (_ : v' = v')) = length p
Theorem: Digraph.Walk.length_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' v' : V
p : Walk G u' v'
⊢ length (Walk.copy p (_ : u' = u') (_ : v' = v')) = length p
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Walk.length_append
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
p : Walk G u v
q : Walk G v w
⊢ length (append p q) = length p + length q
Tactic:
induction p with
| nil => simp
| cons _ _ ih => simp [ih, add_comm, add_left_comm, add_assoc]
Proof state after:
no goals
Theorem: Digraph.Walk.length_append
Proof state before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w u✝ : V
q : Walk G u✝ w
⊢ length (append nil q) = length nil + length q
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.Walk.length_append
Proof state before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ (q : Walk G w✝ w), length (append p✝ q) = length p✝ + length q
q : Walk G w✝ w
⊢ length (append (cons h✝ p✝) q) = length (cons h✝ p✝) + length q
Tactic:
simp [ih, add_comm, add_left_comm, add_assoc]
Proof state after:
no goals
Theorem: Digraph.Walk.exists_length_eq_zero_iff
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ (∃ p, length p = 0) ↔ u = v
Tactic:
constructor
Proof state after:
case mp
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ (∃ p, length p = 0) → u = v

case mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ u = v → ∃ p, length p = 0
Theorem: Digraph.Walk.exists_length_eq_zero_iff
Proof state before:
case mp
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ (∃ p, length p = 0) → u = v
Tactic:
rintro ⟨p, hp⟩
Proof state after:
case mp.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
hp : length p = 0
⊢ u = v
Theorem: Digraph.Walk.exists_length_eq_zero_iff
Proof state before:
case mp.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
hp : length p = 0
⊢ u = v
Tactic:
exact eq_of_length_eq_zero hp
Proof state after:
no goals
Theorem: Digraph.Walk.exists_length_eq_zero_iff
Proof state before:
case mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ u = v → ∃ p, length p = 0
Tactic:
rintro rfl
Proof state after:
case mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
⊢ ∃ p, length p = 0
Theorem: Digraph.Walk.exists_length_eq_zero_iff
Proof state before:
case mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
⊢ ∃ p, length p = 0
Tactic:
exact ⟨nil, rfl⟩
Proof state after:
no goals
Theorem: Digraph.Walk.length_eq_zero_iff
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
p : Walk G u u
⊢ length p = 0 ↔ p = nil
Tactic:
cases p <;> simp
Proof state after:
no goals
Theorem: Digraph.Walk.concat_ne_nil
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
h : G.Adj v u
⊢ concat p h ≠ nil
Tactic:
cases p <;> simp [concat]
Proof state after:
no goals
Theorem: Digraph.Walk.concat_inj
Proof state before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
p' : Walk G u✝ v'
he : concat nil h = concat p' h'
⊢ ∃ hv, Walk.copy nil (_ : u✝ = u✝) hv = p'
Tactic:
cases p'
Proof state after:
case nil.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' h : G.Adj v' w
he : concat nil h = concat nil h'
⊢ ∃ hv, Walk.copy nil (_ : v' = v') hv = nil

case nil.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ v'
he : concat nil h = concat (cons h✝ p✝) h'
⊢ ∃ hv, Walk.copy nil (_ : u✝ = u✝) hv = cons h✝ p✝
Theorem: Digraph.Walk.concat_inj
Proof state before:
case nil.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' h : G.Adj v' w
he : concat nil h = concat nil h'
⊢ ∃ hv, Walk.copy nil (_ : v' = v') hv = nil
Tactic:
exact ⟨rfl, rfl⟩
Proof state after:
no goals
Theorem: Digraph.Walk.concat_inj
Proof state before:
case nil.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ v'
he : concat nil h = concat (cons h✝ p✝) h'
⊢ ∃ hv, Walk.copy nil (_ : u✝ = u✝) hv = cons h✝ p✝
Tactic:
exfalso
Proof state after:
case nil.cons.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ v'
he : concat nil h = concat (cons h✝ p✝) h'
⊢ False
Theorem: Digraph.Walk.concat_inj
Proof state before:
case nil.cons.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ v'
he : concat nil h = concat (cons h✝ p✝) h'
⊢ False
Tactic:
simp only [concat_nil, concat_cons, cons.injEq] at he
Proof state after:
case nil.cons.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ v'
he : w = v✝ ∧ HEq nil (concat p✝ h')
⊢ False
Theorem: Digraph.Walk.concat_inj
Proof state before:
case nil.cons.h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ : V
h : G.Adj u✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ v'
he : w = v✝ ∧ HEq nil (concat p✝ h')
⊢ False
Tactic:
obtain ⟨rfl, he⟩ := he
Proof state after:
case nil.cons.h.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ : V
h h✝ : G.Adj u✝ w
p✝ : Walk G w v'
he : HEq nil (concat p✝ h')
⊢ False
Theorem: Digraph.Walk.concat_inj
Proof state before:
case nil.cons.h.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ : V
h h✝ : G.Adj u✝ w
p✝ : Walk G w v'
he : HEq nil (concat p✝ h')
⊢ False
Tactic:
simp only [heq_iff_eq] at he
Proof state after:
case nil.cons.h.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ : V
h h✝ : G.Adj u✝ w
p✝ : Walk G w v'
he : nil = concat p✝ h'
⊢ False
Theorem: Digraph.Walk.concat_inj
Proof state before:
case nil.cons.h.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ : V
h h✝ : G.Adj u✝ w
p✝ : Walk G w v'
he : nil = concat p✝ h'
⊢ False
Tactic:
exact concat_ne_nil _ _ he.symm
Proof state after:
no goals
Theorem: Digraph.Walk.concat_inj
Proof state before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ v'}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ w
p' : Walk G u✝ v'
he : concat (cons h✝ p✝) h = concat p' h'
⊢ ∃ hv, Walk.copy (cons h✝ p✝) (_ : u✝ = u✝) hv = p'
Tactic:
rw [concat_cons] at he
Proof state after:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v' w : V
h' : G.Adj v' w
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : Walk G v✝ v'}, concat p✝ h = concat p' h' → ∃ hv, Walk.copy p✝ (_ : v✝ = v✝) hv = p'
h : G.Adj w✝ w
p' : Walk G u✝ v'
he : cons h✝ (concat p✝ h) = concat p' h'
⊢ ∃ hv, Walk.copy (cons h✝ p✝) (_ : u✝ = u✝) hv = p'