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

State before:
t : Component.Valued × ID
tl : Output
hd : Change
h : t ∈ targets tl
⊢ t ∈ targets (hd :: tl)
Tactic:
have ⟨c, hm, _⟩ := h
State after:
t : Component.Valued × ID
tl : Output
hd : Change
h : t ∈ targets tl
c : Change
hm : c ∈ tl
right✝ : Change.Targets c t.1 t.2
⊢ t ∈ targets (hd :: tl)

State before:
t : Component.Valued × ID
tl : Output
hd : Change
h : t ∈ targets tl
c : Change
hm : c ∈ tl
right✝ : Change.Targets c t.1 t.2
⊢ t ∈ targets (hd :: tl)
Tactic:
exists c, by simp [hm]
State after:
no goals

State before:
t : Component.Valued × ID
tl : Output
hd : Change
h : t ∈ targets tl
c : Change
hm : c ∈ tl
right✝ : Change.Targets c t.1 t.2
⊢ c ∈ hd :: tl
Tactic:
simp [hm]
State after:
no goals