internlm/Lean-Github huggingface dataset:
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Interface.Subscheme.coe p') =
    true
Tactic:
cases hp : reaction.subPS.coe p'
Proof state after:
case inl
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
val✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl val✝
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inl val✝) =
    true

case inr
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
val✝ : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr val✝
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inr val✝) =
    true
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inl loc) =
    true
Tactic:
case inl loc =>
  simp
  cases he
  case input hi =>
    simp [hi] at hp
    cases h
    case port h =>
      simp [portIsPresent, hp] at h
      exact h
  case output ho =>
    rw [ho] at hp
    contradiction
Proof state after:
no goals
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr sub
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inr sub) =
    true
Tactic:
case inr sub =>
  have ⟨c, output⟩ := sub
  simp at output ⊢
  cases he
  case input hi =>
    rw [hi] at hp
    contradiction
  case output c' output' ho =>
    simp [ho] at hp
    injection hp with hc ho
    subst hc
    subst ho
    cases h
    case port h =>
      simp [portIsPresent] at h
      have ⟨v, hv⟩ := h
      exists cast sorry v
      simp [hv]
      sorry
Proof state after:
no goals
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inl loc) =
    true
Tactic:
simp
Proof state after:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
cases he
Proof state after:
case input
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
a✝ : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v

case output
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
c✝ : Child (Path.class reactor)
output✝ : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c✝, port := cast _ output✝ })
a✝ : Interface.Subscheme.coe p' = Sum.inr { fst := c✝, snd := output✝ }
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
case input hi =>
  simp [hi] at hp
  cases h
  case port h =>
    simp [portIsPresent, hp] at h
    exact h
Proof state after:
no goals
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
c✝ : Child (Path.class reactor)
output✝ : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c✝, port := cast _ output✝ })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c✝, snd := output✝ }
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
case output ho =>
  rw [ho] at hp
  contradiction
Proof state after:
no goals
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
simp [hi] at hp
Proof state after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
hp : input✝ = loc
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
hp : input✝ = loc
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
cases h
Proof state after:
case port
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hi : Interface.Subscheme.coe p' = Sum.inl input✝
hp : input✝ = loc
a✝ : portIsPresent exec { reactor := reactor, port := input✝ } = true
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hi : Interface.Subscheme.coe p' = Sum.inl input✝
hp : input✝ = loc
h : portIsPresent exec { reactor := reactor, port := input✝ } = true
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
case port h =>
  simp [portIsPresent, hp] at h
  exact h
Proof state after:
no goals
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hi : Interface.Subscheme.coe p' = Sum.inl input✝
hp : input✝ = loc
h : portIsPresent exec { reactor := reactor, port := input✝ } = true
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
simp [portIsPresent, hp] at h
Proof state after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hi : Interface.Subscheme.coe p' = Sum.inl input✝
hp : input✝ = loc
h : ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hi : Interface.Subscheme.coe p' = Sum.inl input✝
hp : input✝ = loc
h : ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
exact h
Proof state after:
no goals
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Interface.Subscheme.coe p' = Sum.inl loc
c✝ : Child (Path.class reactor)
output✝ : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c✝, port := cast _ output✝ })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c✝, snd := output✝ }
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
rw [ho] at hp
Proof state after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
c✝ : Child (Path.class reactor)
output✝ : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
hp : Sum.inr { fst := c✝, snd := output✝ } = Sum.inl loc
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c✝, port := cast _ output✝ })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c✝, snd := output✝ }
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
loc : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
c✝ : Child (Path.class reactor)
output✝ : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
hp : Sum.inr { fst := c✝, snd := output✝ } = Sum.inl loc
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c✝, port := cast _ output✝ })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c✝, snd := output✝ }
⊢ ∃ v, interface exec reactor Reactor.InterfaceKind.inputs loc = some v
Tactic:
contradiction
Proof state after:
no goals
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr sub
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inr sub) =
    true
Tactic:
have ⟨c, output⟩ := sub
Proof state after:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inr { fst := c, snd := output }) =
    true
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
⊢ Interface?.isPresent
      (fun x =>
        match x with
        | Sum.inl input => interface exec reactor Reactor.InterfaceKind.inputs input
        | Sum.inr { fst := child, snd := output } =>
          cast _ (interface exec (Path.extend reactor child) Reactor.InterfaceKind.outputs (cast _ output)))
      (Sum.inr { fst := c, snd := output }) =
    true
Tactic:
simp at output ⊢
Proof state after:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Activates exec (Reaction.Trigger.port p)
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
cases he
Proof state after:
case input
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
a✝ : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v

case output
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
c✝ : Child (Path.class reactor)
output✝ : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c✝).vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c✝, port := cast _ output✝ })
a✝ : Interface.Subscheme.coe p' = Sum.inr { fst := c✝, snd := output✝ }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
case input hi =>
  rw [hi] at hp
  contradiction
Proof state after:
no goals
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
case output c' output' ho =>
  simp [ho] at hp
  injection hp with hc ho
  subst hc
  subst ho
  cases h
  case port h =>
    simp [portIsPresent] at h
    have ⟨v, hv⟩ := h
    exists cast sorry v
    simp [hv]
    sorry
Proof state after:
no goals