internlm/Lean-Github huggingface dataset:
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ prefix? path₁ = prefix? path₂ → path₁ ≂ path₂
Tactic:
case mpr =>
  intro h
  by_cases path₁.prefix?.isSome
  case inr hp =>
    have hc₁ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp; simp at hc₁
    rw [h] at hp
    have hc₂ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp; simp at hc₂
    simp [hc₁, hc₂, Sibling.nil]
  case inl hp =>
    have ⟨_, hp₁⟩ := Option.isSome_iff_exists.mp hp
    rw [h] at hp
    have ⟨_, hp₂⟩ := Option.isSome_iff_exists.mp hp
    simp_all
    exact Sibling.cons hp₁ hp₂
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ path₁ ≂ path₂ → prefix? path₁ = prefix? path₂
Tactic:
cases path₁ <;> cases path₂
Proof state after:
case nil.nil
graph✝ : Graph
a✝ : Class graph✝
⊢ Path.nil ≂ Path.nil → prefix? Path.nil = prefix? Path.nil

case nil.cons
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.nil ≂ Path.cons child✝ a✝ → prefix? Path.nil = prefix? (Path.cons child✝ a✝)

case cons.nil
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.cons child✝ a✝ ≂ Path.nil → prefix? (Path.cons child✝ a✝) = prefix? Path.nil

case cons.cons
graph✝ : Graph
a✝² : Class graph✝
child✝¹ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝²
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.cons child✝¹ a✝¹ ≂ Path.cons child✝ a✝ → prefix? (Path.cons child✝¹ a✝¹) = prefix? (Path.cons child✝ a✝)
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
⊢ Path.nil ≂ Path.nil → prefix? Path.nil = prefix? Path.nil
Tactic:
case nil.nil => simp
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝² : Class graph✝
child✝¹ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝²
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.cons child✝¹ a✝¹ ≂ Path.cons child✝ a✝ → prefix? (Path.cons child✝¹ a✝¹) = prefix? (Path.cons child✝ a✝)
Tactic:
case cons.cons => intro h; cases h; simp_all [Succ]
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.nil ≂ Path.cons child✝ a✝ → prefix? Path.nil = prefix? (Path.cons child✝ a✝)
Tactic:
case nil.cons => intro h; cases h; case _ h _ => have := h.isCons; contradiction
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.cons child✝ a✝ ≂ Path.nil → prefix? (Path.cons child✝ a✝) = prefix? Path.nil
Tactic:
case cons.nil => intro h; cases h; case _ h   => have := h.isCons; contradiction
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
⊢ Path.nil ≂ Path.nil → prefix? Path.nil = prefix? Path.nil
Tactic:
simp
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝² : Class graph✝
child✝¹ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝²
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.cons child✝¹ a✝¹ ≂ Path.cons child✝ a✝ → prefix? (Path.cons child✝¹ a✝¹) = prefix? (Path.cons child✝ a✝)
Tactic:
intro h
Proof state after:
graph✝ : Graph
a✝² : Class graph✝
child✝¹ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝²
a✝ : Path graph✝ (Class.Child.class child✝)
h : Path.cons child✝¹ a✝¹ ≂ Path.cons child✝ a✝
⊢ prefix? (Path.cons child✝¹ a✝¹) = prefix? (Path.cons child✝ a✝)
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝² : Class graph✝
child✝¹ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝²
a✝ : Path graph✝ (Class.Child.class child✝)
h : Path.cons child✝¹ a✝¹ ≂ Path.cons child✝ a✝
⊢ prefix? (Path.cons child✝¹ a✝¹) = prefix? (Path.cons child✝ a✝)
Tactic:
cases h
Proof state after:
case cons
graph✝ : Graph
a✝⁴ : Class graph✝
child✝¹ : Class.Child a✝⁴
a✝³ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝⁴
a✝² : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝⁴
a✝¹ : Path.cons child✝¹ a✝³ ≻ parent✝
a✝ : Path.cons child✝ a✝² ≻ parent✝
⊢ prefix? (Path.cons child✝¹ a✝³) = prefix? (Path.cons child✝ a✝²)
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
case cons
graph✝ : Graph
a✝⁴ : Class graph✝
child✝¹ : Class.Child a✝⁴
a✝³ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝⁴
a✝² : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝⁴
a✝¹ : Path.cons child✝¹ a✝³ ≻ parent✝
a✝ : Path.cons child✝ a✝² ≻ parent✝
⊢ prefix? (Path.cons child✝¹ a✝³) = prefix? (Path.cons child✝ a✝²)
Tactic:
simp_all [Succ]
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.nil ≂ Path.cons child✝ a✝ → prefix? Path.nil = prefix? (Path.cons child✝ a✝)
Tactic:
intro h
Proof state after:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
h : Path.nil ≂ Path.cons child✝ a✝
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝)
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
h : Path.nil ≂ Path.cons child✝ a✝
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝)
Tactic:
cases h
Proof state after:
case cons
graph✝ : Graph
a✝³ : Class graph✝
child✝ : Class.Child a✝³
a✝² : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝³
a✝¹ : Path.nil ≻ parent✝
a✝ : Path.cons child✝ a✝² ≻ parent✝
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝²)
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
h : Path.nil ≻ parent✝
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝¹)
Tactic:
case _ h _ => have := h.isCons; contradiction
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
h : Path.nil ≻ parent✝
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝¹)
Tactic:
have := h.isCons
Proof state after:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
h : Path.nil ≻ parent✝
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
this : isCons Path.nil = true
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝¹)
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
h : Path.nil ≻ parent✝
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
this : isCons Path.nil = true
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝¹)
Tactic:
contradiction
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.cons child✝ a✝ ≂ Path.nil → prefix? (Path.cons child✝ a✝) = prefix? Path.nil
Tactic:
intro h
Proof state after:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
h : Path.cons child✝ a✝ ≂ Path.nil
⊢ prefix? (Path.cons child✝ a✝) = prefix? Path.nil
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
h : Path.cons child✝ a✝ ≂ Path.nil
⊢ prefix? (Path.cons child✝ a✝) = prefix? Path.nil
Tactic:
cases h
Proof state after:
case cons
graph✝ : Graph
a✝³ : Class graph✝
child✝ : Class.Child a✝³
a✝² : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝³
a✝¹ : Path.cons child✝ a✝² ≻ parent✝
a✝ : Path.nil ≻ parent✝
⊢ prefix? (Path.cons child✝ a✝²) = prefix? Path.nil
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
h : Path.nil ≻ parent✝
⊢ prefix? (Path.cons child✝ a✝¹) = prefix? Path.nil
Tactic:
case _ h   => have := h.isCons; contradiction
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
h : Path.nil ≻ parent✝
⊢ prefix? (Path.cons child✝ a✝¹) = prefix? Path.nil
Tactic:
have := h.isCons
Proof state after:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
h : Path.nil ≻ parent✝
this : isCons Path.nil = true
⊢ prefix? (Path.cons child✝ a✝¹) = prefix? Path.nil
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
h : Path.nil ≻ parent✝
this : isCons Path.nil = true
⊢ prefix? (Path.cons child✝ a✝¹) = prefix? Path.nil
Tactic:
contradiction
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ prefix? path₁ = prefix? path₂ → path₁ ≂ path₂
Tactic:
intro h
Proof state after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
⊢ path₁ ≂ path₂
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
⊢ path₁ ≂ path₂
Tactic:
by_cases path₁.prefix?.isSome
Proof state after:
case inl
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
h✝ : Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂

case inr
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
h✝ : ¬Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂
Tactic:
case inr hp =>
  have hc₁ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp; simp at hc₁
  rw [h] at hp
  have hc₂ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp; simp at hc₂
  simp [hc₁, hc₂, Sibling.nil]
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂
Tactic:
case inl hp =>
  have ⟨_, hp₁⟩ := Option.isSome_iff_exists.mp hp
  rw [h] at hp
  have ⟨_, hp₂⟩ := Option.isSome_iff_exists.mp hp
  simp_all
  exact Sibling.cons hp₁ hp₂
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂
Tactic:
have hc₁ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp
Proof state after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₁) = true
hc₁ : isNil path₁ = true
⊢ path₁ ≂ path₂
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₁) = true
hc₁ : isNil path₁ = true
⊢ path₁ ≂ path₂
Tactic:
simp at hc₁
Proof state after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₁) = true
hc₁ : path₁ = Path.nil
⊢ path₁ ≂ path₂
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₁) = true
hc₁ : path₁ = Path.nil
⊢ path₁ ≂ path₂
Tactic:
rw [h] at hp
Proof state after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₂) = true
hc₁ : path₁ = Path.nil
⊢ path₁ ≂ path₂
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₂) = true
hc₁ : path₁ = Path.nil
⊢ path₁ ≂ path₂
Tactic:
have hc₂ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp
Proof state after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₂) = true
hc₁ : path₁ = Path.nil
hc₂ : isNil path₂ = true
⊢ path₁ ≂ path₂
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₂) = true
hc₁ : path₁ = Path.nil
hc₂ : isNil path₂ = true
⊢ path₁ ≂ path₂
Tactic:
simp at hc₂
Proof state after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₂) = true
hc₁ : path₁ = Path.nil
hc₂ : path₂ = Path.nil
⊢ path₁ ≂ path₂
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₂) = true
hc₁ : path₁ = Path.nil
hc₂ : path₂ = Path.nil
⊢ path₁ ≂ path₂
Tactic:
simp [hc₁, hc₂, Sibling.nil]
Proof state after:
no goals
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂
Tactic:
have ⟨_, hp₁⟩ := Option.isSome_iff_exists.mp hp
Proof state after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₁) = true
w✝ : Path graph✝ a✝
hp₁ : prefix? path₁ = some w✝
⊢ path₁ ≂ path₂
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₁) = true
w✝ : Path graph✝ a✝
hp₁ : prefix? path₁ = some w✝
⊢ path₁ ≂ path₂
Tactic:
rw [h] at hp
Proof state after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₂) = true
w✝ : Path graph✝ a✝
hp₁ : prefix? path₁ = some w✝
⊢ path₁ ≂ path₂
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₂) = true
w✝ : Path graph✝ a✝
hp₁ : prefix? path₁ = some w✝
⊢ path₁ ≂ path₂
Tactic:
have ⟨_, hp₂⟩ := Option.isSome_iff_exists.mp hp
Proof state after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₂) = true
w✝¹ : Path graph✝ a✝
hp₁ : prefix? path₁ = some w✝¹
w✝ : Path graph✝ a✝
hp₂ : prefix? path₂ = some w✝
⊢ path₁ ≂ path₂
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₂) = true
w✝¹ : Path graph✝ a✝
hp₁ : prefix? path₁ = some w✝¹
w✝ : Path graph✝ a✝
hp₂ : prefix? path₂ = some w✝
⊢ path₁ ≂ path₂
Tactic:
simp_all
Proof state after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ w✝¹ w✝ : Path graph✝ a✝
h : w✝¹ = w✝
hp₁ : prefix? path₁ = some w✝
hp₂ : prefix? path₂ = some w✝
⊢ path₁ ≂ path₂
Theorem: Network.Graph.Path.Sibling.iff_eq_prefix
Proof state before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ w✝¹ w✝ : Path graph✝ a✝
h : w✝¹ = w✝
hp₁ : prefix? path₁ = some w✝
hp₂ : prefix? path₂ = some w✝
⊢ path₁ ≂ path₂
Tactic:
exact Sibling.cons hp₁ hp₂
Proof state after:
no goals
Theorem: Nat.div_eq_sub_div
Proof state before:
b a : Nat
h₁ : 0 < b
h₂ : b ≤ a
⊢ a / b = (a - b) / b + 1
Tactic:
rw [div_eq a, if_pos]
Proof state after:
case hc
b a : Nat
h₁ : 0 < b
h₂ : b ≤ a
⊢ 0 < b ∧ b ≤ a
Theorem: Nat.div_eq_sub_div
Proof state before:
case hc
b a : Nat
h₁ : 0 < b
h₂ : b ≤ a
⊢ 0 < b ∧ b ≤ a
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: Nat.add_div_right
Proof state before:
x z : Nat
H : 0 < z
⊢ (x + z) / z = succ (x / z)
Tactic:
rw [div_eq_sub_div H (Nat.le_add_left _ _), Nat.add_sub_cancel]
Proof state after:
no goals
Theorem: Nat.add_mul_div_left
Proof state before:
x z y : Nat
H : 0 < y
⊢ (x + y * z) / y = x / y + z
Tactic:
induction z with
| zero => rw [Nat.mul_zero, Nat.add_zero, Nat.add_zero]
| succ z ih => rw [mul_succ, ← Nat.add_assoc, add_div_right _ H, ih]; rfl
Proof state after:
no goals
Theorem: Nat.add_mul_div_left
Proof state before:
case zero
x y : Nat
H : 0 < y
⊢ (x + y * zero) / y = x / y + zero
Tactic:
rw [Nat.mul_zero, Nat.add_zero, Nat.add_zero]
Proof state after:
no goals
Theorem: Nat.add_mul_div_left
Proof state before:
case succ
x y : Nat
H : 0 < y
z : Nat
ih : (x + y * z) / y = x / y + z
⊢ (x + y * succ z) / y = x / y + succ z
Tactic:
rw [mul_succ, ← Nat.add_assoc, add_div_right _ H, ih]
Proof state after:
case succ
x y : Nat
H : 0 < y
z : Nat
ih : (x + y * z) / y = x / y + z
⊢ succ (x / y + z) = x / y + succ z
Theorem: Nat.add_mul_div_left
Proof state before:
case succ
x y : Nat
H : 0 < y
z : Nat
ih : (x + y * z) / y = x / y + z
⊢ succ (x / y + z) = x / y + succ z
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.add_mul_div_right
Proof state before:
x y z : Nat
H : 0 < z
⊢ (x + y * z) / z = x / z + y
Tactic:
rw [Nat.mul_comm, add_mul_div_left _ _ H]
Proof state after:
no goals
Theorem: Nat.mul_div_cancel
Proof state before:
m n : Nat
H : 0 < n
⊢ m * n / n = m
Tactic:
let t := add_mul_div_right 0 m H
Proof state after:
m n : Nat
H : 0 < n
t : (0 + m * n) / n = 0 / n + m := add_mul_div_right 0 m H
⊢ m * n / n = m
Theorem: Nat.mul_div_cancel
Proof state before:
m n : Nat
H : 0 < n
t : (0 + m * n) / n = 0 / n + m := add_mul_div_right 0 m H
⊢ m * n / n = m
Tactic:
rwa [Nat.zero_add, Nat.zero_div, Nat.zero_add] at t
Proof state after:
no goals
Theorem: Option.isSome_iff_exists
Proof state before:
α : Sort ?u.13403
p q : α → Prop
α✝ : Type u_1
x : Option α✝
⊢ isSome x = true ↔ ∃ a, x = some a
Tactic:
cases x <;> simp [isSome]
Proof state after:
case some
α : Sort ?u.13403
p q : α → Prop
α✝ : Type u_1
val✝ : α✝
⊢ ∃ a, val✝ = a
Theorem: Option.isSome_iff_exists
Proof state before:
case some
α : Sort ?u.13403
p q : α → Prop
α✝ : Type u_1
val✝ : α✝
⊢ ∃ a, val✝ = a
Tactic:
exists ‹_›
Proof state after:
no goals
Theorem: Array.getElem?_nil
Proof state before:
α : Type u_1
i : Nat
⊢ #[][i]? = none
Tactic:
simp [getElem?]
Proof state after:
α : Type u_1
i : Nat
⊢ (if h : i < size #[] then some #[][i] else none) = none
Theorem: Array.getElem?_nil
Proof state before:
α : Type u_1
i : Nat
⊢ (if h : i < size #[] then some #[][i] else none) = none
Tactic:
split <;> simp
Proof state after:
case inl
α : Type u_1
i : Nat
h✝ : i < size #[]
⊢ False
Theorem: Array.getElem?_nil
Proof state before:
case inl
α : Type u_1
i : Nat
h✝ : i < size #[]
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
⊢ Option.isSome as[0]? = true ↔ ¬isEmpty as = true
Tactic:
simp [Array.isEmpty, Option.isSome_iff_exists, getElem?]
Proof state after:
α : Type u_1
as : Array α
⊢ (∃ a, (if h : 0 < size as then some as[0] else none) = some a) ↔ ¬size as = 0
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
⊢ (∃ a, (if h : 0 < size as then some as[0] else none) = some a) ↔ ¬size as = 0
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
as : Array α
⊢ (∃ a, (if h : 0 < size as then some as[0] else none) = some a) → ¬size as = 0

case mpr
α : Type u_1
as : Array α
⊢ ¬size as = 0 → ∃ a, (if h : 0 < size as then some as[0] else none) = some a
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
⊢ (∃ a, (if h : 0 < size as then some as[0] else none) = some a) → ¬size as = 0
Tactic:
case mp =>
  intro ⟨_, h⟩
  split at h
  case inl hs => exact Nat.not_eq_zero_of_lt hs
  case inr => contradiction
Proof state after:
no goals
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
⊢ ¬size as = 0 → ∃ a, (if h : 0 < size as then some as[0] else none) = some a
Tactic:
case mpr =>
  intro h
  split
  case inl => exists as[0]
  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 α
⊢ (∃ a, (if h : 0 < size as then some as[0] else none) = some a) → ¬size as = 0
Tactic:
intro ⟨_, h⟩
Proof state after:
α : Type u_1
as : Array α
w✝ : α
h : (if h : 0 < size as then some as[0] else none) = some w✝
⊢ ¬size as = 0
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
w✝ : α
h : (if h : 0 < size as then some as[0] else none) = some w✝
⊢ ¬size as = 0
Tactic:
split at h
Proof state after:
case inl
α : Type u_1
as : Array α
w✝ : α
h✝ : 0 < size as
h : some as[0] = some w✝
⊢ ¬size as = 0

case inr
α : Type u_1
as : Array α
w✝ : α
h✝ : ¬0 < size as
h : False
⊢ ¬size as = 0
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
w✝ : α
hs : 0 < size as
h : some as[0] = some w✝
⊢ ¬size as = 0
Tactic:
case inl hs => exact Nat.not_eq_zero_of_lt hs
Proof state after:
no goals
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
w✝ : α
h✝ : ¬0 < size as
h : False
⊢ ¬size as = 0
Tactic:
case inr => contradiction
Proof state after:
no goals
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
w✝ : α
hs : 0 < size as
h : some as[0] = some w✝
⊢ ¬size as = 0
Tactic:
exact Nat.not_eq_zero_of_lt hs
Proof state after:
no goals
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
w✝ : α
h✝ : ¬0 < size as
h : False
⊢ ¬size as = 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
⊢ ¬size as = 0 → ∃ a, (if h : 0 < size as then some as[0] else none) = some a
Tactic:
intro h
Proof state after:
α : Type u_1
as : Array α
h : ¬size as = 0
⊢ ∃ a, (if h : 0 < size as then some as[0] else none) = some a
Theorem: Array.getElem?_zero_isSome_iff_not_isEmpty
Proof state before:
α : Type u_1
as : Array α
h : ¬size as = 0
⊢ ∃ a, (if h : 0 < size as then some as[0] else none) = some a
Tactic:
split
Proof state after:
case inl
α : Type u_1
as : Array α
h : ¬size as = 0
h✝ : 0 < size as
⊢ ∃ a, some as[0] = some a

case inr
α : Type u_1
as : Array α
h : ¬size as = 0
h✝ : ¬0 < size as
⊢ ∃ a, False