Theorem: Reactor.LawfulUpdate.ne_comm (ReactorModel/Objects/Reactor/Theorems/Proper.lean)

State before:
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
⊢ rtr₂ = rtr₂'
Tactic:
have e₁ := Equivalent.trans u₁.equiv u₂.equiv
State after:
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
⊢ rtr₂ = rtr₂'

State before:
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
⊢ rtr₂ = rtr₂'
Tactic:
have e₂ := Equivalent.trans u₁'.equiv u₂'.equiv
State after:
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
⊢ rtr₂ = rtr₂'

State before:
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
⊢ rtr₂ = rtr₂'
Tactic:
have e := Equivalent.trans (Equivalent.symm e₁) e₂
State after:
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
⊢ rtr₂ = rtr₂'

State before:
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
⊢ rtr₂ = rtr₂'
Tactic:
apply ext_obj? e
State after:
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
⊢ ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₂[Component.val c][i] = some o₁ → rtr₂'[Component.val c][i] = some o₂ → o₁ = o₂

State before:
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
⊢ ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₂[Component.val c][i] = some o₁ → rtr₂'[Component.val c][i] = some o₂ → o₁ = o₂
Tactic:
intro cpt i _ _ ho₁ ho₂
State after:
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
⊢ o₁✝ = o₂✝

State before:
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
by_cases hc₁ : cpt = cpt₁ <;> by_cases hc₂ : cpt = cpt₂ <;> ((try subst hc₁); try subst hc₂)
State after:
case pos
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i₂
⊢ o₁✝ = o₂✝

case neg
α : Type
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i₁ ≠ i₂
⊢ o₁✝ = o₂✝

case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
⊢ o₁✝ = o₂✝

case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
hc₂ : ¬cpt = cpt₂
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : cpt = cpt₁
hc₂ : ¬cpt = cpt₂
⊢ o₁✝ = o₂✝
Tactic:
(try subst hc₁)
State after:
case neg
α : Type
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i₁ ≠ i₂
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
hc₂ : cpt = cpt₂
⊢ o₁✝ = o₂✝
Tactic:
try subst hc₂
State after:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : cpt = cpt₁
hc₂ : ¬cpt = cpt₂
⊢ o₁✝ = o₂✝
Tactic:
try subst hc₁
State after:
case neg
α : Type
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i₁ ≠ i₂
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : cpt = cpt₁
hc₂ : ¬cpt = cpt₂
⊢ o₁✝ = o₂✝
Tactic:
subst hc₁
State after:
case neg
α : Type
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i₁ ≠ i₂
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
hc₂ : cpt = cpt₂
⊢ o₁✝ = o₂✝
Tactic:
subst hc₂
State after:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i₂
⊢ o₁✝ = o₂✝
Tactic:
by_cases hi₁ : i = i₁ <;> by_cases hi₂ : i = i₂ <;> ((try subst hi₁); try subst hi₂)
State after:
case pos
α : Type
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i ≠ i
⊢ o₁✝ = o₂✝

case neg
α : Type
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
hi₂ : ¬i = i₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt ∨ i ≠ i₂
⊢ o₁✝ = o₂✝

case pos
α : Type
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
hi₁ : ¬i = i₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i
⊢ o₁✝ = o₂✝

case neg
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i₂
hi₁ : ¬i = i₁
hi₂ : ¬i = i₂
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i₂
hi₁ : i = i₁
hi₂ : ¬i = i₂
⊢ o₁✝ = o₂✝
Tactic:
(try subst hi₁)
State after:
case neg
α : Type
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
hi₂ : ¬i = i₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt ∨ i ≠ i₂
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i₂
hi₁ : ¬i = i₁
hi₂ : i = i₂
⊢ o₁✝ = o₂✝
Tactic:
try subst hi₂
State after:
case pos
α : Type
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
hi₁ : ¬i = i₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i₂
hi₁ : i = i₁
hi₂ : ¬i = i₂
⊢ o₁✝ = o₂✝
Tactic:
try subst hi₁
State after:
case neg
α : Type
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
hi₂ : ¬i = i₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt ∨ i ≠ i₂
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i₂
hi₁ : i = i₁
hi₂ : ¬i = i₂
⊢ o₁✝ = o₂✝
Tactic:
subst hi₁
State after:
case neg
α : Type
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
hi₂ : ¬i = i₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt ∨ i ≠ i₂
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i₂
hi₁ : ¬i = i₁
hi₂ : i = i₂
⊢ o₁✝ = o₂✝
Tactic:
subst hi₂
State after:
case pos
α : Type
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
hi₁ : ¬i = i₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i ≠ i
⊢ o₁✝ = o₂✝
Tactic:
simp at h
State after:
no goals

State before:
case neg
α : Type
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
hi₂ : ¬i = i₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt ∨ i ≠ i₂
⊢ o₁✝ = o₂✝
Tactic:
have h₁ := u₁.obj?_updated ▸ u₂.obj?_preserved (.inr hi₂)
State after:
case neg
α : Type
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
hi₂ : ¬i = i₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt ∨ i ≠ i₂
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₁) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
hi₂ : ¬i = i₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt ∨ i ≠ i₂
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₁) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
have h₂ := u₁'.obj?_preserved (.inr hi₂) ▸ u₂'.obj?_updated
State after:
case neg
α : Type
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
hi₂ : ¬i = i₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt ∨ i ≠ i₂
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₁) <$> rtr[Component.val cpt][i]
h₂ : rtr₂'[Component.val cpt][i] = (fun x => v₁) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
hi₂ : ¬i = i₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt ∨ i ≠ i₂
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₁) <$> rtr[Component.val cpt][i]
h₂ : rtr₂'[Component.val cpt][i] = (fun x => v₁) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
injection ho₁ ▸ h₂.trans h₁.symm ▸ ho₂
State after:
no goals

State before:
case pos
α : Type
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
hi₁ : ¬i = i₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i
⊢ o₁✝ = o₂✝
Tactic:
have h₁ := u₁.obj?_preserved (.inr hi₁) ▸ u₂.obj?_updated
State after:
case pos
α : Type
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
hi₁ : ¬i = i₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
hi₁ : ¬i = i₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
have h₂ := u₁'.obj?_updated ▸ u₂'.obj?_preserved (.inr hi₁)
State after:
case pos
α : Type
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
hi₁ : ¬i = i₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
h₂ : rtr₂'[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
hi₁ : ¬i = i₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
h₂ : rtr₂'[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
injection ho₁ ▸ h₂.trans h₁.symm ▸ ho₂
State after:
no goals

State before:
case neg
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i₂
hi₁ : ¬i = i₁
hi₂ : ¬i = i₂
⊢ o₁✝ = o₂✝
Tactic:
have := u₁.obj?_preserved  (.inr hi₁) ▸ u₂.obj?_preserved  (.inr hi₂)
State after:
case neg
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i₂
hi₁ : ¬i = i₁
hi₂ : ¬i = i₂
this : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i₂
hi₁ : ¬i = i₁
hi₂ : ¬i = i₂
this : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
have := u₁'.obj?_preserved (.inr hi₂) ▸ u₂'.obj?_preserved (.inr hi₁)
State after:
case neg
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i₂
hi₁ : ¬i = i₁
hi₂ : ¬i = i₂
this✝ : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
this : rtr₂'[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt ≠ cpt ∨ i₁ ≠ i₂
hi₁ : ¬i = i₁
hi₂ : ¬i = i₂
this✝ : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
this : rtr₂'[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
simp_all
State after:
no goals

State before:
case neg
α : Type
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i₁ ≠ i₂
⊢ o₁✝ = o₂✝
Tactic:
by_cases hi₁ : i = i₁ <;> try subst hi₁
State after:
case pos
α : Type
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i ≠ i₂
⊢ o₁✝ = o₂✝

case neg
α : Type
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i₁ ≠ i₂
hi₁ : ¬i = i₁
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i₁ ≠ i₂
hi₁ : i = i₁
⊢ o₁✝ = o₂✝
Tactic:
subst hi₁
State after:
case pos
α : Type
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i ≠ i₂
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i ≠ i₂
⊢ o₁✝ = o₂✝
Tactic:
have h₁ := u₁.obj?_updated ▸ u₂.obj?_preserved (.inl hc₂)
State after:
case pos
α : Type
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i ≠ i₂
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₁) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i ≠ i₂
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₁) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
have h₂ := u₁'.obj?_preserved (.inl hc₂) ▸ u₂'.obj?_updated
State after:
case pos
α : Type
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i ≠ i₂
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₁) <$> rtr[Component.val cpt][i]
h₂ : rtr₂'[Component.val cpt][i] = (fun x => v₁) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i ≠ i₂
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₁) <$> rtr[Component.val cpt][i]
h₂ : rtr₂'[Component.val cpt][i] = (fun x => v₁) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
injection ho₁ ▸ h₂.trans h₁.symm ▸ ho₂
State after:
no goals

State before:
case neg
α : Type
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i₁ ≠ i₂
hi₁ : ¬i = i₁
⊢ o₁✝ = o₂✝
Tactic:
have := u₁.obj?_preserved  (.inr hi₁) ▸ u₂.obj?_preserved (.inl hc₂)
State after:
case neg
α : Type
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i₁ ≠ i₂
hi₁ : ¬i = i₁
this : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i₁ ≠ i₂
hi₁ : ¬i = i₁
this : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
have := u₁'.obj?_preserved (.inl hc₂) ▸ u₂'.obj?_preserved (.inr hi₁)
State after:
case neg
α : Type
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i₁ ≠ i₂
hi₁ : ¬i = i₁
this✝ : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
this : rtr₂'[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₂ : ¬cpt = cpt₂
u₁ : LawfulUpdate cpt i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt i₁ v₁ rtr₁' rtr₂'
h : cpt ≠ cpt₂ ∨ i₁ ≠ i₂
hi₁ : ¬i = i₁
this✝ : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
this : rtr₂'[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
simp_all
State after:
no goals

State before:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
⊢ o₁✝ = o₂✝
Tactic:
by_cases hi₂ : i = i₂ <;> try subst hi₂
State after:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i
⊢ o₁✝ = o₂✝

case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
hi₂ : ¬i = i₂
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
hi₂ : i = i₂
⊢ o₁✝ = o₂✝
Tactic:
subst hi₂
State after:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i
⊢ o₁✝ = o₂✝
Tactic:
have h₁ := u₁.obj?_preserved (.inl hc₁) ▸ u₂.obj?_updated
State after:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
have h₂ := u₁'.obj?_updated ▸ u₂'.obj?_preserved (.inl hc₁)
State after:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
h₂ : rtr₂'[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case pos
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i
h₁ : rtr₂[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
h₂ : rtr₂'[Component.val cpt][i] = (fun x => v₂) <$> rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
injection ho₁ ▸ h₂.trans h₁.symm ▸ ho₂
State after:
no goals

State before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
hi₂ : ¬i = i₂
⊢ o₁✝ = o₂✝
Tactic:
have := u₁.obj?_preserved  (.inl hc₁) ▸ u₂.obj?_preserved (.inr hi₂)
State after:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
hi₂ : ¬i = i₂
this : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
hi₂ : ¬i = i₂
this : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
have := u₁'.obj?_preserved (.inr hi₂) ▸ u₂'.obj?_preserved (.inl hc₁)
State after:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
hi₂ : ¬i = i₂
this✝ : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
this : rtr₂'[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
u₂ : LawfulUpdate cpt i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt i₂ v₂ rtr rtr₁'
h : cpt₁ ≠ cpt ∨ i₁ ≠ i₂
hi₂ : ¬i = i₂
this✝ : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
this : rtr₂'[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
simp_all
State after:
no goals

State before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
hc₂ : ¬cpt = cpt₂
⊢ o₁✝ = o₂✝
Tactic:
have := u₁.obj?_preserved  (j := i) (.inl hc₁) ▸ u₂.obj?_preserved  (.inl hc₂)
State after:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
hc₂ : ¬cpt = cpt₂
this : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
hc₂ : ¬cpt = cpt₂
this : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
have := u₁'.obj?_preserved (j := i) (.inl hc₂) ▸ u₂'.obj?_preserved (.inl hc₁)
State after:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
hc₂ : ¬cpt = cpt₂
this✝ : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
this : rtr₂'[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝

State before:
case neg
α : Type
cpt₁ : Component.Valued
i₁ : ID
v₁ : Value
cpt₂ : Component.Valued
i₂ : ID
v₂ : Value
inst✝ : Proper α
rtr rtr₁ rtr₁' rtr₂ rtr₂' : α
u₁ : LawfulUpdate cpt₁ i₁ v₁ rtr rtr₁
u₂ : LawfulUpdate cpt₂ i₂ v₂ rtr₁ rtr₂
u₁' : LawfulUpdate cpt₂ i₂ v₂ rtr rtr₁'
u₂' : LawfulUpdate cpt₁ i₁ v₁ rtr₁' rtr₂'
h : cpt₁ ≠ cpt₂ ∨ i₁ ≠ i₂
e₁ : rtr ≈ rtr₂
e₂ : rtr ≈ rtr₂'
e : rtr₂ ≈ rtr₂'
cpt : Component.Valued
i : Component.idType (Component.val cpt)
o₁✝ o₂✝ : Component.type α (Component.val cpt)
ho₁ : rtr₂[Component.val cpt][i] = some o₁✝
ho₂ : rtr₂'[Component.val cpt][i] = some o₂✝
hc₁ : ¬cpt = cpt₁
hc₂ : ¬cpt = cpt₂
this✝ : rtr₂[Component.val cpt][i] = rtr[Component.val cpt][i]
this : rtr₂'[Component.val cpt][i] = rtr[Component.val cpt][i]
⊢ o₁✝ = o₂✝
Tactic:
simp_all
State after:
no goals