Theorem: Reaction.Output.target_mem_targets (ReactorModel/Objects/Reaction.lean)

State before:
c : Change
out : Output
t : Component.Valued × ID
hc : c ∈ out
ht : Change.target c = some t
⊢ t ∈ targets out
Tactic:
exists c, hc
State after:
c : Change
out : Output
t : Component.Valued × ID
hc : c ∈ out
ht : Change.target c = some t
⊢ Change.Targets c t.1 t.2

State before:
c : Change
out : Output
t : Component.Valued × ID
hc : c ∈ out
ht : Change.target c = some t
⊢ Change.Targets c t.1 t.2
Tactic:
cases c <;> simp [Change.target] at *
State after:
case norm
out : Output
t : Component.Valued × ID
a✝ : Change.Normal
hc : Change.norm a✝ ∈ out
ht : (a✝.cpt, a✝.id) = t
⊢ Change.Targets (Change.norm a✝) t.1 t.2

State before:
case norm
out : Output
t : Component.Valued × ID
a✝ : Change.Normal
hc : Change.norm a✝ ∈ out
ht : (a✝.cpt, a✝.id) = t
⊢ Change.Targets (Change.norm a✝) t.1 t.2
Tactic:
subst ht
State after:
case norm
out : Output
a✝ : Change.Normal
hc : Change.norm a✝ ∈ out
⊢ Change.Targets (Change.norm a✝) (a✝.cpt, a✝.id).1 (a✝.cpt, a✝.id).2

State before:
case norm
out : Output
a✝ : Change.Normal
hc : Change.norm a✝ ∈ out
⊢ Change.Targets (Change.norm a✝) (a✝.cpt, a✝.id).1 (a✝.cpt, a✝.id).2
Tactic:
constructor
State after:
no goals