internlm/Lean-Github huggingface dataset:
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
h : ¬size as = 0
h✝ : 0 < size as
⊢ ∃ a, some as[0] = some a
Tactic:
case inl => exists as[0]
Proof state after:
no goals
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
h : ¬size as = 0
hs : ¬0 < size as
⊢ ∃ a, False
Tactic:
case inr hs => exact absurd (Nat.zero_lt_of_ne_zero h) hs
Proof state after:
no goals
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
h : ¬size as = 0
h✝ : 0 < size as
⊢ ∃ a, some as[0] = some a
Tactic:
exists as[0]
Proof state after:
no goals
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
h : ¬size as = 0
hs : ¬0 < size as
⊢ ∃ a, False
Tactic:
exact absurd (Nat.zero_lt_of_ne_zero h) hs
Proof state after:
no goals
Theorem: Array.isEmpty_iff_data_eq_nil
Proof state before:
α : Type u_1
as : Array α
⊢ isEmpty as = true ↔ as.data = []
Tactic:
simp [isEmpty, size]
Proof state after:
α : Type u_1
as : Array α
⊢ List.length as.data = 0 ↔ as.data = []
Theorem: Array.isEmpty_iff_data_eq_nil
Proof state before:
α : Type u_1
as : Array α
⊢ List.length as.data = 0 ↔ as.data = []
Tactic:
exact List.length_eq_zero
Proof state after:
no goals
Theorem: Array.findP?_property
Proof state before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
⊢ findP?.loop idx as p = some a → p a = true
Tactic:
intro h
Proof state after:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
h : findP?.loop idx as p = some a
⊢ p a = true
Theorem: Array.findP?_property
Proof state before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
h : findP?.loop idx as p = some a
⊢ p a = true
Tactic:
unfold findP?.loop at h
Proof state after:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
h :
  (if h : idx < size as then
      let a := as[idx];
      if p a = true then some a else findP?.loop (idx + 1) as p
    else none) =
    some a
⊢ p a = true
Theorem: Array.findP?_property
Proof state before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
h :
  (if h : idx < size as then
      let a := as[idx];
      if p a = true then some a else findP?.loop (idx + 1) as p
    else none) =
    some a
⊢ p a = true
Tactic:
split at h <;> simp at h
Proof state after:
case inl
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
h✝ : idx < size as
h : (if p as[idx] = true then some as[idx] else findP?.loop (idx + 1) as p) = some a
⊢ p a = true
Theorem: Array.findP?_property
Proof state before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h : (if p as[idx] = true then some as[idx] else findP?.loop (idx + 1) as p) = some a
⊢ p a = true
Tactic:
case inl hi =>
  split at h
  case inl => simp_all
  case inr => exact go h
Proof state after:
no goals
Theorem: Array.findP?_property
Proof state before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h : (if p as[idx] = true then some as[idx] else findP?.loop (idx + 1) as p) = some a
⊢ p a = true
Tactic:
split at h
Proof state after:
case inl
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h✝ : p as[idx] = true
h : some as[idx] = some a
⊢ p a = true

case inr
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h✝ : ¬p as[idx] = true
h : findP?.loop (idx + 1) as p = some a
⊢ p a = true
Theorem: Array.findP?_property
Proof state before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h✝ : p as[idx] = true
h : some as[idx] = some a
⊢ p a = true
Tactic:
case inl => simp_all
Proof state after:
no goals
Theorem: Array.findP?_property
Proof state before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h✝ : ¬p as[idx] = true
h : findP?.loop (idx + 1) as p = some a
⊢ p a = true
Tactic:
case inr => exact go h
Proof state after:
no goals
Theorem: Array.findP?_property
Proof state before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h✝ : p as[idx] = true
h : some as[idx] = some a
⊢ p a = true
Tactic:
simp_all
Proof state after:
no goals
Theorem: Array.findP?_property
Proof state before:
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h✝ : ¬p as[idx] = true
h : findP?.loop (idx + 1) as p = some a
⊢ p a = true
Tactic:
exact go h
Proof state after:
no goals
Theorem: Execution.Executable.nextTime_le_queue_nextTime
Proof state before:
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
⊢ nextTime exec = some t → Queue.nextTime exec.queue = some q → t ≤ q
Tactic:
intro ht hq
Proof state after:
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
ht : nextTime exec = some t
hq : Queue.nextTime exec.queue = some q
⊢ t ≤ q
Theorem: Execution.Executable.nextTime_le_queue_nextTime
Proof state before:
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
ht : nextTime exec = some t
hq : Queue.nextTime exec.queue = some q
⊢ t ≤ q
Tactic:
simp [nextTime] at ht
Proof state after:
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
ht :
  (match exec.state with
    | State.shuttingDown => none
    | State.shutdownPending =>
      some
        { val := time exec,
          property :=
            (_ :
              Nat.Linear.ExprCnstr.denote [(time exec).ns]
                { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) }
    | State.executing => Queue.nextTime exec.queue) =
    some t
hq : Queue.nextTime exec.queue = some q
⊢ t ≤ q
Theorem: Execution.Executable.nextTime_le_queue_nextTime
Proof state before:
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
ht :
  (match exec.state with
    | State.shuttingDown => none
    | State.shutdownPending =>
      some
        { val := time exec,
          property :=
            (_ :
              Nat.Linear.ExprCnstr.denote [(time exec).ns]
                { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) }
    | State.executing => Queue.nextTime exec.queue) =
    some t
hq : Queue.nextTime exec.queue = some q
⊢ t ≤ q
Tactic:
split at ht <;> simp_all
Proof state after:
case h_2
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
x✝ : State
hq : Queue.nextTime exec.queue = some q
heq✝ : exec.state = State.shutdownPending
ht :
  { val := time exec,
      property :=
        (_ :
          Nat.Linear.ExprCnstr.denote [(time exec).ns]
            { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) } =
    t
⊢ t ≤ q
Theorem: Execution.Executable.nextTime_le_queue_nextTime
Proof state before:
case h_2
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
x✝ : State
hq : Queue.nextTime exec.queue = some q
heq✝ : exec.state = State.shutdownPending
ht :
  { val := time exec,
      property :=
        (_ :
          Nat.Linear.ExprCnstr.denote [(time exec).ns]
            { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) } =
    t
⊢ t ≤ q
Tactic:
simp [←ht]
Proof state after:
case h_2
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
x✝ : State
hq : Queue.nextTime exec.queue = some q
heq✝ : exec.state = State.shutdownPending
ht :
  { val := time exec,
      property :=
        (_ :
          Nat.Linear.ExprCnstr.denote [(time exec).ns]
            { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) } =
    t
⊢ { val := time exec,
      property :=
        (_ :
          Nat.Linear.ExprCnstr.denote [(time exec).ns]
            { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) } ≤
    q
Theorem: Execution.Executable.nextTime_le_queue_nextTime
Proof state before:
case h_2
net : Network
exec : Executable net
t : Time.From (time exec)
q : Time.From exec.tag.time
x✝ : State
hq : Queue.nextTime exec.queue = some q
heq✝ : exec.state = State.shutdownPending
ht :
  { val := time exec,
      property :=
        (_ :
          Nat.Linear.ExprCnstr.denote [(time exec).ns]
            { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) } =
    t
⊢ { val := time exec,
      property :=
        (_ :
          Nat.Linear.ExprCnstr.denote [(time exec).ns]
            { eq := false, lhs := Nat.Linear.Expr.var 0, rhs := Nat.Linear.Expr.var 0 }) } ≤
    q
Tactic:
exact q.property
Proof state after:
no goals
Theorem: Execution.Executable.Next.for_tag_strictly_monotonic
Proof state before:
net : Network
next : Next net
exec : Executable net
⊢ Next.for exec = some next → exec.tag < next.tag
Tactic:
intro h
Proof state after:
net : Network
next : Next net
exec : Executable net
h : Next.for exec = some next
⊢ exec.tag < next.tag
Theorem: Network.Graph.Path.prefix?_cons_eq_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child : Class.Child start
subpath subprefix : Path graph (Class.Child.class child)
⊢ prefix? subpath = some subprefix → prefix? (cons child subpath) = some (cons child subprefix)
Tactic:
intro h
Proof state after:
graph : Graph
start : Class graph
child : Class.Child start
subpath subprefix : Path graph (Class.Child.class child)
h : prefix? subpath = some subprefix
⊢ prefix? (cons child subpath) = some (cons child subprefix)
Theorem: Network.Graph.Path.prefix?_cons_eq_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child : Class.Child start
subpath subprefix : Path graph (Class.Child.class child)
h : prefix? subpath = some subprefix
⊢ prefix? (cons child subpath) = some (cons child subprefix)
Tactic:
cases subpath
Proof state after:
case nil
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
h : prefix? nil = some subprefix
⊢ prefix? (cons child nil) = some (cons child subprefix)

case cons
graph : Graph
start : Class graph
child : Class.Child start
subprefix : 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 subprefix
⊢ prefix? (cons child (cons child✝ a✝)) = some (cons child subprefix)
Theorem: Network.Graph.Path.prefix?_cons_eq_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
h : prefix? nil = some subprefix
⊢ prefix? (cons child nil) = some (cons child subprefix)
Tactic:
case nil => simp [prefix?] at h
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_cons_eq_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
h : prefix? (cons child' subpath) = some subprefix
⊢ prefix? (cons child (cons child' subpath)) = some (cons child subprefix)
Tactic:
case cons child' subpath => simp [prefix?, h]; rfl
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_cons_eq_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
h : prefix? nil = some subprefix
⊢ prefix? (cons child nil) = some (cons child subprefix)
Tactic:
simp [prefix?] at h
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_cons_eq_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
h : prefix? (cons child' subpath) = some subprefix
⊢ prefix? (cons child (cons child' subpath)) = some (cons child subprefix)
Tactic:
simp [prefix?, h]
Proof state after:
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
h : prefix? (cons child' subpath) = some subprefix
⊢ (do
      let x ← some subprefix
      some (cons child x)) =
    some (cons child subprefix)
Theorem: Network.Graph.Path.prefix?_cons_eq_cons_prefix?
Proof state before:
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
h : prefix? (cons child' subpath) = some subprefix
⊢ (do
      let x ← some subprefix
      some (cons child x)) =
    some (cons child subprefix)
Tactic:
rfl
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
⊢ Option.isSome (prefix? path) = true ↔ isCons path = true
Tactic:
constructor
Proof state after:
case mp
graph : Graph
start : Class graph
path : Path graph start
⊢ Option.isSome (prefix? path) = true → isCons path = true

case mpr
graph : Graph
start : Class graph
path : Path graph start
⊢ isCons path = true → Option.isSome (prefix? path) = true
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
⊢ Option.isSome (prefix? path) = true → isCons path = true
Tactic:
case mp =>
  intro h
  induction path
  case nil => simp [prefix?] at h
  case cons child₁ subpath₁ hi =>
    cases subpath₁
    case nil => rfl
    case cons child₂ subpath₂ => simp [isCons]
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
⊢ isCons path = true → Option.isSome (prefix? path) = true
Tactic:
case mpr =>
  intro h
  induction path
  case nil =>
    have ⟨_, _, _⟩ := isCons_def.mp h
    contradiction
  case cons child₁ subpath₁ hi =>
    cases subpath₁
    case nil => simp [prefix?, Option.isSome]
    case cons child₂ subpath₂ =>
      specialize hi isCons_of_cons
      have ⟨subpath, hi⟩ := Option.isSome_iff_exists.mp hi
      simp [prefix?, hi, Option.isSome_iff_exists]
      exists .cons child₁ subpath
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
⊢ Option.isSome (prefix? path) = true → isCons path = true
Tactic:
intro h
Proof state after:
graph : Graph
start : Class graph
path : Path graph start
h : Option.isSome (prefix? path) = true
⊢ isCons path = true
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
h : Option.isSome (prefix? path) = true
⊢ isCons path = true
Tactic:
induction path
Proof state after:
case nil
graph : Graph
start x✝ : Class graph
h : Option.isSome (prefix? nil) = true
⊢ isCons nil = true

case cons
graph : Graph
start start✝ : Class graph
child✝ : Class.Child start✝
a✝ : Path graph (Class.Child.class child✝)
a_ih✝ : Option.isSome (prefix? a✝) = true → isCons a✝ = true
h : Option.isSome (prefix? (cons child✝ a✝)) = true
⊢ isCons (cons child✝ a✝) = true
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start x✝ : Class graph
h : Option.isSome (prefix? nil) = true
⊢ isCons nil = true
Tactic:
case nil => simp [prefix?] at h
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
subpath₁ : Path graph (Class.Child.class child₁)
hi : Option.isSome (prefix? subpath₁) = true → isCons subpath₁ = true
h : Option.isSome (prefix? (cons child₁ subpath₁)) = true
⊢ isCons (cons child₁ subpath₁) = true
Tactic:
case cons child₁ subpath₁ hi =>
  cases subpath₁
  case nil => rfl
  case cons child₂ subpath₂ => simp [isCons]
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start x✝ : Class graph
h : Option.isSome (prefix? nil) = true
⊢ isCons nil = true
Tactic:
simp [prefix?] at h
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
subpath₁ : Path graph (Class.Child.class child₁)
hi : Option.isSome (prefix? subpath₁) = true → isCons subpath₁ = true
h : Option.isSome (prefix? (cons child₁ subpath₁)) = true
⊢ isCons (cons child₁ subpath₁) = true
Tactic:
cases subpath₁
Proof state after:
case nil
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
hi : Option.isSome (prefix? nil) = true → isCons nil = true
h : Option.isSome (prefix? (cons child₁ nil)) = true
⊢ isCons (cons child₁ nil) = true

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 : Option.isSome (prefix? (cons child✝ a✝)) = true → isCons (cons child✝ a✝) = true
h : Option.isSome (prefix? (cons child₁ (cons child✝ a✝))) = true
⊢ isCons (cons child₁ (cons child✝ a✝)) = true
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
hi : Option.isSome (prefix? nil) = true → isCons nil = true
h : Option.isSome (prefix? (cons child₁ nil)) = true
⊢ isCons (cons child₁ nil) = true
Tactic:
case nil => rfl
Proof state after:
no goals
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 : Option.isSome (prefix? (cons child₂ subpath₂)) = true → isCons (cons child₂ subpath₂) = true
h : Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
⊢ isCons (cons child₁ (cons child₂ subpath₂)) = true
Tactic:
case cons child₂ subpath₂ => simp [isCons]
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
hi : Option.isSome (prefix? nil) = true → isCons nil = true
h : Option.isSome (prefix? (cons child₁ nil)) = true
⊢ isCons (cons child₁ nil) = true
Tactic:
rfl
Proof state after:
no goals
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 : Option.isSome (prefix? (cons child₂ subpath₂)) = true → isCons (cons child₂ subpath₂) = true
h : Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
⊢ isCons (cons child₁ (cons child₂ subpath₂)) = true
Tactic:
simp [isCons]
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
⊢ isCons path = true → Option.isSome (prefix? path) = true
Tactic:
intro h
Proof state after:
graph : Graph
start : Class graph
path : Path graph start
h : isCons path = true
⊢ Option.isSome (prefix? path) = true
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start : Class graph
path : Path graph start
h : isCons path = true
⊢ Option.isSome (prefix? path) = true
Tactic:
induction path
Proof state after:
case nil
graph : Graph
start x✝ : Class graph
h : isCons nil = true
⊢ Option.isSome (prefix? nil) = true

case cons
graph : Graph
start start✝ : Class graph
child✝ : Class.Child start✝
a✝ : Path graph (Class.Child.class child✝)
a_ih✝ : isCons a✝ = true → Option.isSome (prefix? a✝) = true
h : isCons (cons child✝ a✝) = true
⊢ Option.isSome (prefix? (cons child✝ a✝)) = true
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start x✝ : Class graph
h : isCons nil = true
⊢ Option.isSome (prefix? nil) = true
Tactic:
case nil =>
  have ⟨_, _, _⟩ := isCons_def.mp h
  contradiction
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
subpath₁ : Path graph (Class.Child.class child₁)
hi : isCons subpath₁ = true → Option.isSome (prefix? subpath₁) = true
h : isCons (cons child₁ subpath₁) = true
⊢ Option.isSome (prefix? (cons child₁ subpath₁)) = true
Tactic:
case cons child₁ subpath₁ hi =>
  cases subpath₁
  case nil => simp [prefix?, Option.isSome]
  case cons child₂ subpath₂ =>
    specialize hi isCons_of_cons
    have ⟨subpath, hi⟩ := Option.isSome_iff_exists.mp hi
    simp [prefix?, hi, Option.isSome_iff_exists]
    exists .cons child₁ subpath
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start x✝ : Class graph
h : isCons nil = true
⊢ Option.isSome (prefix? nil) = true
Tactic:
have ⟨_, _, _⟩ := isCons_def.mp h
Proof state after:
graph : Graph
start x✝ : Class graph
h : isCons nil = true
w✝¹ : Class.Child x✝
w✝ : Path graph (Class.Child.class w✝¹)
h✝ : nil = cons w✝¹ w✝
⊢ Option.isSome (prefix? nil) = true
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start x✝ : Class graph
h : isCons nil = true
w✝¹ : Class.Child x✝
w✝ : Path graph (Class.Child.class w✝¹)
h✝ : nil = cons w✝¹ w✝
⊢ Option.isSome (prefix? nil) = true
Tactic:
contradiction
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
subpath₁ : Path graph (Class.Child.class child₁)
hi : isCons subpath₁ = true → Option.isSome (prefix? subpath₁) = true
h : isCons (cons child₁ subpath₁) = true
⊢ Option.isSome (prefix? (cons child₁ subpath₁)) = true
Tactic:
cases subpath₁
Proof state after:
case nil
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
hi : isCons nil = true → Option.isSome (prefix? nil) = true
h : isCons (cons child₁ nil) = true
⊢ Option.isSome (prefix? (cons child₁ nil)) = true

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 : isCons (cons child✝ a✝) = true → Option.isSome (prefix? (cons child✝ a✝)) = true
h : isCons (cons child₁ (cons child✝ a✝)) = true
⊢ Option.isSome (prefix? (cons child₁ (cons child✝ a✝))) = true
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
hi : isCons nil = true → Option.isSome (prefix? nil) = true
h : isCons (cons child₁ nil) = true
⊢ Option.isSome (prefix? (cons child₁ nil)) = true
Tactic:
case nil => simp [prefix?, Option.isSome]
Proof state after:
no goals
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:
case cons child₂ subpath₂ =>
  specialize hi isCons_of_cons
  have ⟨subpath, hi⟩ := Option.isSome_iff_exists.mp hi
  simp [prefix?, hi, Option.isSome_iff_exists]
  exists .cons child₁ subpath
Proof state after:
no goals
Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons
Proof state before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
hi : isCons nil = true → Option.isSome (prefix? nil) = true
h : isCons (cons child₁ nil) = true
⊢ Option.isSome (prefix? (cons child₁ nil)) = true
Tactic:
simp [prefix?, Option.isSome]
Proof state after:
no goals