Theorem: Change.Targets.norm_not (ReactorModel/Objects/Change.lean)

State before:
c : Component.Valued
j : ID
v : Component.Valued.changeType c
cpt : Component.Valued
i : ID
h : ¬Targets (norm { cpt := c, id := j, value := v }) cpt i
⊢ cpt ≠ c ∨ i ≠ j
Tactic:
by_contra hc
State after:
c : Component.Valued
j : ID
v : Component.Valued.changeType c
cpt : Component.Valued
i : ID
h : ¬Targets (norm { cpt := c, id := j, value := v }) cpt i
hc : ¬(cpt ≠ c ∨ i ≠ j)
⊢ False

State before:
c : Component.Valued
j : ID
v : Component.Valued.changeType c
cpt : Component.Valued
i : ID
h : ¬Targets (norm { cpt := c, id := j, value := v }) cpt i
hc : ¬(cpt ≠ c ∨ i ≠ j)
⊢ False
Tactic:
simp [not_or] at hc
State after:
c : Component.Valued
j : ID
v : Component.Valued.changeType c
cpt : Component.Valued
i : ID
h : ¬Targets (norm { cpt := c, id := j, value := v }) cpt i
hc : cpt = c ∧ i = j
⊢ False

State before:
c : Component.Valued
j : ID
v : Component.Valued.changeType c
cpt : Component.Valued
i : ID
h : ¬Targets (norm { cpt := c, id := j, value := v }) cpt i
hc : cpt = c ∧ i = j
⊢ False
Tactic:
exact hc.left ▸ hc.right ▸ h $ .intro
State after:
no goals