internlm/Lean-Github huggingface dataset:
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
child₂ : Class.Child (Class.Child.class child₁)
subpath₂ : Path graph (Class.Child.class child₂)
hi : isCons (cons child₂ subpath₂) = true → Option.isSome (prefix? (cons child₂ subpath₂)) = true
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
⊢ Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
Tactic:
specialize hi isCons_of_cons
Proof state after:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
child₂ : Class.Child (Class.Child.class child₁)
subpath₂ : Path graph (Class.Child.class child₂)
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
hi : Option.isSome (prefix? (cons child₂ subpath₂)) = true
⊢ Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
child₂ : Class.Child (Class.Child.class child₁)
subpath₂ : Path graph (Class.Child.class child₂)
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
hi : Option.isSome (prefix? (cons child₂ subpath₂)) = true
⊢ Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
Tactic:
have ⟨subpath, hi⟩ := Option.isSome_iff_exists.mp hi
Proof state after:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
child₂ : Class.Child (Class.Child.class child₁)
subpath₂ : Path graph (Class.Child.class child₂)
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
hi✝ : Option.isSome (prefix? (cons child₂ subpath₂)) = true
subpath : Path graph (Class.Child.class child₁)
hi : prefix? (cons child₂ subpath₂) = some subpath
⊢ Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
child₂ : Class.Child (Class.Child.class child₁)
subpath₂ : Path graph (Class.Child.class child₂)
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
hi✝ : Option.isSome (prefix? (cons child₂ subpath₂)) = true
subpath : Path graph (Class.Child.class child₁)
hi : prefix? (cons child₂ subpath₂) = some subpath
⊢ Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
Tactic:
simp [prefix?, hi, Option.isSome_iff_exists]
Proof state after:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
child₂ : Class.Child (Class.Child.class child₁)
subpath₂ : Path graph (Class.Child.class child₂)
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
hi✝ : Option.isSome (prefix? (cons child₂ subpath₂)) = true
subpath : Path graph (Class.Child.class child₁)
hi : prefix? (cons child₂ subpath₂) = some subpath
⊢ ∃ a,
    (do
        let x ← some subpath
        some (cons child₁ x)) =
      some a
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
child₂ : Class.Child (Class.Child.class child₁)
subpath₂ : Path graph (Class.Child.class child₂)
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
hi✝ : Option.isSome (prefix? (cons child₂ subpath₂)) = true
subpath : Path graph (Class.Child.class child₁)
hi : prefix? (cons child₂ subpath₂) = some subpath
⊢ ∃ a,
    (do
        let x ← some subpath
        some (cons child₁ x)) =
      some a
Tactic:
exists .cons child₁ subpath
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? path₁ = some path₂ ↔ prefix? (cons child path₁) = some (cons child path₂)
Tactic:
constructor
Proof state after:
case mp
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? path₁ = some path₂ → prefix? (cons child path₁) = some (cons child path₂)

case mpr
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? (cons child path₁) = some (cons child path₂) → prefix? path₁ = some path₂
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
case mp
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? path₁ = some path₂ → prefix? (cons child path₁) = some (cons child path₂)

case mpr
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? (cons child path₁) = some (cons child path₂) → prefix? path₁ = some path₂
Tactic:
all_goals
  intro h
  cases path₁
  case nil => simp [prefix?] at h
Proof state after:
case mp.cons
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child✝ a✝) = some path₂
⊢ prefix? (cons child (cons child✝ a✝)) = some (cons child path₂)

case mpr.cons
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child (cons child✝ a✝)) = some (cons child path₂)
⊢ prefix? (cons child✝ a✝) = some path₂
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child✝ a✝) = some path₂
⊢ prefix? (cons child (cons child✝ a✝)) = some (cons child path₂)
Tactic:
case mp.cons => simp [prefix?, h]; rfl
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
h : prefix? (cons child✝ (cons child subpath)) = some (cons child✝ path₂)
⊢ prefix? (cons child subpath) = some path₂
Tactic:
case mpr.cons child subpath =>
  have hs := prefix?_isSome_iff_isCons.mpr (@isCons_of_cons _ _ child subpath)
  have ⟨_, hs⟩ := Option.isSome_iff_exists.mp hs
  simp [hs, prefix?] at h ⊢
  injection h with h
  injection h
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
case mpr
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? (cons child path₁) = some (cons child path₂) → prefix? path₁ = some path₂
Tactic:
intro h
Proof state after:
case mpr
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
h : prefix? (cons child path₁) = some (cons child path₂)
⊢ prefix? path₁ = some path₂
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
case mpr
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
h : prefix? (cons child path₁) = some (cons child path₂)
⊢ prefix? path₁ = some path₂
Tactic:
cases path₁
Proof state after:
case mpr.nil
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
h : prefix? (cons child nil) = some (cons child path₂)
⊢ prefix? nil = some path₂

case mpr.cons
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child (cons child✝ a✝)) = some (cons child path₂)
⊢ prefix? (cons child✝ a✝) = some path₂
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
h : prefix? (cons child nil) = some (cons child path₂)
⊢ prefix? nil = some path₂
Tactic:
case nil => simp [prefix?] at h
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
h : prefix? (cons child nil) = some (cons child path₂)
⊢ prefix? nil = some path₂
Tactic:
simp [prefix?] at h
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child✝ a✝) = some path₂
⊢ prefix? (cons child (cons child✝ a✝)) = some (cons child path₂)
Tactic:
simp [prefix?, h]
Proof state after:
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child✝ a✝) = some path₂
⊢ (do
      let x ← some path₂
      some (cons child x)) =
    some (cons child path₂)
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child✝ a✝) = some path₂
⊢ (do
      let x ← some path₂
      some (cons child x)) =
    some (cons child path₂)
Tactic:
rfl
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
h : prefix? (cons child✝ (cons child subpath)) = some (cons child✝ path₂)
⊢ prefix? (cons child subpath) = some path₂
Tactic:
have hs := prefix?_isSome_iff_isCons.mpr (@isCons_of_cons _ _ child subpath)
Proof state after:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
h : prefix? (cons child✝ (cons child subpath)) = some (cons child✝ path₂)
hs : Option.isSome (prefix? (cons child subpath)) = true
⊢ prefix? (cons child subpath) = some path₂
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
h : prefix? (cons child✝ (cons child subpath)) = some (cons child✝ path₂)
hs : Option.isSome (prefix? (cons child subpath)) = true
⊢ prefix? (cons child subpath) = some path₂
Tactic:
have ⟨_, hs⟩ := Option.isSome_iff_exists.mp hs
Proof state after:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
h : prefix? (cons child✝ (cons child subpath)) = some (cons child✝ path₂)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
⊢ prefix? (cons child subpath) = some path₂
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
h : prefix? (cons child✝ (cons child subpath)) = some (cons child✝ path₂)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
⊢ prefix? (cons child subpath) = some path₂
Tactic:
simp [hs, prefix?] at h ⊢
Proof state after:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
h :
  (do
      let x ← some w✝
      some (cons child✝ x)) =
    some (cons child✝ path₂)
⊢ w✝ = path₂
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
h :
  (do
      let x ← some w✝
      some (cons child✝ x)) =
    some (cons child✝ path₂)
⊢ w✝ = path₂
Tactic:
injection h with h
Proof state after:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
h : cons child✝ w✝ = cons child✝ path₂
⊢ w✝ = path₂
Theorem: Network.Graph.Path.prefix?_iff_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
h : cons child✝ w✝ = cons child✝ path₂
⊢ w✝ = path₂
Tactic:
injection h
Proof state after:
no goals
Theorem: Network.Graph.Path.suffix_class
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
h : isCons path = true
⊢ class (suffix path h) = class path
Tactic:
rw [suffix]
Proof state after:
graph : Graph
start : Class graph
path : Path graph start
h : isCons path = true
⊢ class
      (match path, h with
      | nil, h => Bool.noConfusion h
      | cons child subpath, h => subpath) =
    class path
Theorem: Network.Graph.Path.suffix_class
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
h : isCons path = true
⊢ class
      (match path, h with
      | nil, h => Bool.noConfusion h
      | cons child subpath, h => subpath) =
    class path
Tactic:
split
Proof state after:
case h_1
graph : Graph
start : Class graph
path✝ : Path graph start
x✝¹ : isCons path✝ = true
x✝ : isCons nil = true
⊢ class (Bool.noConfusion x✝) = class nil

case h_2
graph : Graph
start : Class graph
path✝ : Path graph start
x✝¹ : isCons path✝ = true
child✝ : Class.Child start
a✝ : Path graph (Class.Child.class child✝)
x✝ : isCons (cons child✝ a✝) = true
⊢ class a✝ = class (cons child✝ a✝)
Theorem: Network.Graph.Path.suffix_class
Proof state before:
graph : Graph
start : Class graph
path✝ : Path graph start
x✝ : isCons path✝ = true
h : isCons nil = true
⊢ class (Bool.noConfusion h) = class nil
Tactic:
case _ h => simp [isCons] at h
Proof state after:
no goals
Theorem: Network.Graph.Path.suffix_class
Proof state before:
graph : Graph
start : Class graph
path✝ : Path graph start
x✝ : isCons path✝ = true
h : isCons nil = true
⊢ class (Bool.noConfusion h) = class nil
Tactic:
simp [isCons] at h
Proof state after:
no goals
Theorem: Network.Graph.Path.split_class
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
h : isCons path = true
⊢ Class.Child.class (split path h).snd = class path
Tactic:
induction path
Proof state after:
case nil
graph : Graph
start x✝ : Class graph
h : isCons nil = true
⊢ Class.Child.class (split nil h).snd = class nil

case cons
graph : Graph
start start✝ : Class graph
child✝ : Class.Child start✝
a✝ : Path graph (Class.Child.class child✝)
a_ih✝ : ∀ (h : isCons a✝ = true), Class.Child.class (split a✝ h).snd = class a✝
h : isCons (cons child✝ a✝) = true
⊢ Class.Child.class (split (cons child✝ a✝) h).snd = class (cons child✝ a✝)
Theorem: Network.Graph.Path.split_class
Proof state before:
graph : Graph
start x✝ : Class graph
h : isCons nil = true
⊢ Class.Child.class (split nil h).snd = class nil
Tactic:
case nil => contradiction
Proof state after:
no goals
Theorem: Network.Graph.Path.split_class
Proof state before:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
subpath : Path graph (Class.Child.class child)
hi : ∀ (h : isCons subpath = true), Class.Child.class (split subpath h).snd = class subpath
h : isCons (cons child subpath) = true
⊢ Class.Child.class (split (cons child subpath) h).snd = class (cons child subpath)
Tactic:
case cons child subpath hi =>
  cases subpath
  case nil => rfl
  case cons child' subpath => rw [split]; exact hi h
Proof state after:
no goals
Theorem: Network.Graph.Path.split_class
Proof state before:
graph : Graph
start x✝ : Class graph
h : isCons nil = true
⊢ Class.Child.class (split nil h).snd = class nil
Tactic:
contradiction
Proof state after:
no goals
Theorem: Network.Graph.Path.split_class
Proof state before:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
subpath : Path graph (Class.Child.class child)
hi : ∀ (h : isCons subpath = true), Class.Child.class (split subpath h).snd = class subpath
h : isCons (cons child subpath) = true
⊢ Class.Child.class (split (cons child subpath) h).snd = class (cons child subpath)
Tactic:
cases subpath
Proof state after:
case nil
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
hi : ∀ (h : isCons nil = true), Class.Child.class (split nil h).snd = class nil
h : isCons (cons child nil) = true
⊢ Class.Child.class (split (cons child nil) h).snd = class (cons child nil)

case cons
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
hi : ∀ (h : isCons (cons child✝ a✝) = true), Class.Child.class (split (cons child✝ a✝) h).snd = class (cons child✝ a✝)
h : isCons (cons child (cons child✝ a✝)) = true
⊢ Class.Child.class (split (cons child (cons child✝ a✝)) h).snd = class (cons child (cons child✝ a✝))
Theorem: Network.Graph.Path.split_class
Proof state before:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
hi : ∀ (h : isCons nil = true), Class.Child.class (split nil h).snd = class nil
h : isCons (cons child nil) = true
⊢ Class.Child.class (split (cons child nil) h).snd = class (cons child nil)
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: Network.Graph.Path.split_class
Proof state before:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
hi :
  ∀ (h : isCons (cons child' subpath) = true),
    Class.Child.class (split (cons child' subpath) h).snd = class (cons child' subpath)
h : isCons (cons child (cons child' subpath)) = true
⊢ Class.Child.class (split (cons child (cons child' subpath)) h).snd = class (cons child (cons child' subpath))
Tactic:
case cons child' subpath => rw [split]; exact hi h
Proof state after:
no goals
Theorem: Network.Graph.Path.split_class
Proof state before:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
hi : ∀ (h : isCons nil = true), Class.Child.class (split nil h).snd = class nil
h : isCons (cons child nil) = true
⊢ Class.Child.class (split (cons child nil) h).snd = class (cons child nil)
Tactic:
rfl
Proof state after:
no goals
Theorem: Network.Graph.Path.split_class
Proof state before:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
hi :
  ∀ (h : isCons (cons child' subpath) = true),
    Class.Child.class (split (cons child' subpath) h).snd = class (cons child' subpath)
h : isCons (cons child (cons child' subpath)) = true
⊢ Class.Child.class (split (cons child (cons child' subpath)) h).snd = class (cons child (cons child' subpath))
Tactic:
rw [split]
Proof state after:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
hi :
  ∀ (h : isCons (cons child' subpath) = true),
    Class.Child.class (split (cons child' subpath) h).snd = class (cons child' subpath)
h : isCons (cons child (cons child' subpath)) = true
⊢ Class.Child.class
      (match split (cons child' subpath) (_ : isCons (cons child' subpath) = true) with
        | { fst := sub, snd := cls } => { fst := cons child sub, snd := cls }).snd =
    class (cons child (cons child' subpath))
Theorem: Network.Graph.Path.split_class
Proof state before:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
hi :
  ∀ (h : isCons (cons child' subpath) = true),
    Class.Child.class (split (cons child' subpath) h).snd = class (cons child' subpath)
h : isCons (cons child (cons child' subpath)) = true
⊢ Class.Child.class
      (match split (cons child' subpath) (_ : isCons (cons child' subpath) = true) with
        | { fst := sub, snd := cls } => { fst := cons child sub, snd := cls }).snd =
    class (cons child (cons child' subpath))
Tactic:
exact hi h
Proof state after:
no goals
Theorem: Network.Graph.Path.Succ.isCons'
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
⊢ cons c₁ (cons c₂ path₁) ≻ path₂ → Path.isCons path₂ = true
Tactic:
intro h
Proof state after:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
h : cons c₁ (cons c₂ path₁) ≻ path₂
⊢ Path.isCons path₂ = true
Theorem: Network.Graph.Path.Succ.isCons'
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
h : cons c₁ (cons c₂ path₁) ≻ path₂
⊢ Path.isCons path₂ = true
Tactic:
have ⟨subpath, hp⟩ := prefix?_isSome_iff_isCons.mpr (@isCons_of_cons _ _ c₂ path₁) |> Option.isSome_iff_exists.mp
Proof state after:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
h : cons c₁ (cons c₂ path₁) ≻ path₂
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
⊢ Path.isCons path₂ = true
Theorem: Network.Graph.Path.Succ.isCons'
Proof state before:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
h : cons c₁ (cons c₂ path₁) ≻ path₂
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
⊢ Path.isCons path₂ = true
Tactic:
simp [Succ, prefix?, hp] at h
Proof state after:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h :
  (do
      let x ← some subpath
      some (cons c₁ x)) =
    some path₂
⊢ Path.isCons path₂ = true