Theorem: Reactor.LawfulMemUpdate.unique (ReactorModel/Objects/Reactor/Theorems/Readable.lean)

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u₁ : LawfulMemUpdate cpt i v rtr rtr₁
u₂ : LawfulMemUpdate cpt i v rtr rtr₂
⊢ rtr₁ = rtr₂
Tactic:
induction u₁ generalizing rtr₂ <;> cases u₂
State after:
case final.final
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝¹ : Component.type α (Component.val cpt)
a✝⁵ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝⁴ : rtr₁✝{Component.val cpt}{i} = some o✝¹
a✝³ : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂{Component.val cpt}{i} = some v
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂

case final.nested
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝⁶ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝⁵ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝⁴ : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝² : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂{Component.rtr}{j✝} = some n₂✝
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂
⊢ rtr₂✝ = rtr₂

case nested.final
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝⁶ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
a✝⁵ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝⁴ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝³ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝ = rtr₂
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂{Component.val cpt}{i} = some v
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂

case nested.nested
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j✝¹ : ID
rtr₁✝ rtr₂✝ : α
n₁✝¹ n₂✝¹ : Component.type α Component.rtr
a✝⁷ : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝
a✝⁶ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝¹
a✝⁵ : rtr₂✝{Component.rtr}{j✝¹} = some n₂✝¹
a✝⁴ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
a_ih✝ : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝² : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂{Component.rtr}{j✝} = some n₂✝
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂
⊢ rtr₂✝ = rtr₂

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝¹ : Component.type α (Component.val cpt)
e₁ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝¹
h₁' : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
a✝ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂' : rtr₂{Component.val cpt}{i} = some v
e₂ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
case final.final e₁ _ h₁' _ _ h₂' e₂ =>
  exact RootEqualUpTo.ext (RootEqualUpTo.trans e₁.symm e₂) (h₂' ▸ h₁')
State after:
no goals

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j₁ : ID
rtr₁✝ rtr₂✝ : α
n₁✝¹ n₂✝¹ : Component.type α Component.rtr
e₁ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j₁} = some n₁✝¹
h₁' : rtr₂✝{Component.rtr}{j₁} = some n₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
j₂ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₂} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₂} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₂] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
case nested.nested j₁ _ _ _ _ e₁ h₁ h₁' u₁ hi j₂ _ _ u₂ h₂ h₂' e₂ =>
  have h : j₁ = j₂ := by injection (u₁.member₁.nested h₁).unique (u₂.member₁.nested h₂)
  subst h; cases h₁ ▸ h₂; cases hi u₂
  exact RootEqualUpTo.ext (RootEqualUpTo.trans e₁.symm e₂) $ h₁' ▸ h₂'.symm
State after:
no goals

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝³ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝² : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂{Component.rtr}{j✝} = some n₂✝
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
case final.nested h₁ _ _ _ _ u h₂ _ _ =>
  injection (StrictMember.final h₁).unique (u.member₁.nested h₂)
State after:
no goals

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝² : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝ = rtr₂
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
h₂ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂{Component.val cpt}{i} = some v
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
case nested.final h₁ _ u _ _ h₂ _ _ =>
  injection (StrictMember.final h₂).unique (u.member₁.nested h₁)
State after:
no goals

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝¹ : Component.type α (Component.val cpt)
e₁ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝¹
h₁' : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
a✝ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂' : rtr₂{Component.val cpt}{i} = some v
e₂ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
exact RootEqualUpTo.ext (RootEqualUpTo.trans e₁.symm e₂) (h₂' ▸ h₁')
State after:
no goals

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j₁ : ID
rtr₁✝ rtr₂✝ : α
n₁✝¹ n₂✝¹ : Component.type α Component.rtr
e₁ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j₁} = some n₁✝¹
h₁' : rtr₂✝{Component.rtr}{j₁} = some n₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
j₂ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₂} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₂} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₂] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
have h : j₁ = j₂ := by injection (u₁.member₁.nested h₁).unique (u₂.member₁.nested h₂)
State after:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j₁ : ID
rtr₁✝ rtr₂✝ : α
n₁✝¹ n₂✝¹ : Component.type α Component.rtr
e₁ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j₁} = some n₁✝¹
h₁' : rtr₂✝{Component.rtr}{j₁} = some n₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
j₂ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₂} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₂} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₂] rtr₂
h : j₁ = j₂
⊢ rtr₂✝ = rtr₂

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j₁ : ID
rtr₁✝ rtr₂✝ : α
n₁✝¹ n₂✝¹ : Component.type α Component.rtr
e₁ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j₁} = some n₁✝¹
h₁' : rtr₂✝{Component.rtr}{j₁} = some n₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
j₂ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₂} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₂} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₂] rtr₂
h : j₁ = j₂
⊢ rtr₂✝ = rtr₂
Tactic:
subst h
State after:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j₁ : ID
rtr₁✝ rtr₂✝ : α
n₁✝¹ n₂✝¹ : Component.type α Component.rtr
e₁ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j₁} = some n₁✝¹
h₁' : rtr₂✝{Component.rtr}{j₁} = some n₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₁} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂
⊢ rtr₂✝ = rtr₂

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j₁ : ID
rtr₁✝ rtr₂✝ : α
n₁✝¹ n₂✝¹ : Component.type α Component.rtr
e₁ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j₁} = some n₁✝¹
h₁' : rtr₂✝{Component.rtr}{j₁} = some n₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₁} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
cases h₁ ▸ h₂
State after:
case refl
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j₁ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝¹ : Component.type α Component.rtr
e₁ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
h₁' : rtr₂✝{Component.rtr}{j₁} = some n₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
n₂✝ : Component.type α Component.rtr
h₂' : rtr₂{Component.rtr}{j₁} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
⊢ rtr₂✝ = rtr₂

State before:
case refl
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j₁ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝¹ : Component.type α Component.rtr
e₁ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
h₁' : rtr₂✝{Component.rtr}{j₁} = some n₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
n₂✝ : Component.type α Component.rtr
h₂' : rtr₂{Component.rtr}{j₁} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
⊢ rtr₂✝ = rtr₂
Tactic:
cases hi u₂
State after:
case refl.refl
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j₁ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e₁ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
h₁' : rtr₂✝{Component.rtr}{j₁} = some n₂✝
u₁ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝ = rtr₂
rtr₂ : α
e₂ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂
h₂ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₁} = some n₂✝
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
⊢ rtr₂✝ = rtr₂

State before:
case refl.refl
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j₁ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e₁ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
h₁' : rtr₂✝{Component.rtr}{j₁} = some n₂✝
u₁ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝ = rtr₂
rtr₂ : α
e₂ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂
h₂ : rtr₁✝{Component.rtr}{j₁} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₁} = some n₂✝
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
⊢ rtr₂✝ = rtr₂
Tactic:
exact RootEqualUpTo.ext (RootEqualUpTo.trans e₁.symm e₂) $ h₁' ▸ h₂'.symm
State after:
no goals

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j₁ : ID
rtr₁✝ rtr₂✝ : α
n₁✝¹ n₂✝¹ : Component.type α Component.rtr
e₁ : rtr₁✝ ≃[Component.rtr][j₁] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j₁} = some n₁✝¹
h₁' : rtr₂✝{Component.rtr}{j₁} = some n₂✝¹
u₁ : LawfulMemUpdate cpt i v n₁✝¹ n₂✝¹
hi : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝¹ rtr₂ → n₂✝¹ = rtr₂
rtr₂ : α
j₂ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u₂ : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j₂} = some n₁✝
h₂' : rtr₂{Component.rtr}{j₂} = some n₂✝
e₂ : rtr₁✝ ≃[Component.rtr][j₂] rtr₂
⊢ j₁ = j₂
Tactic:
injection (u₁.member₁.nested h₁).unique (u₂.member₁.nested h₂)
State after:
no goals

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝³ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝² : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂{Component.rtr}{j✝} = some n₂✝
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
injection (StrictMember.final h₁).unique (u.member₁.nested h₂)
State after:
no goals

State before:
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝² : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ {rtr₂ : α}, LawfulMemUpdate cpt i v n₁✝ rtr₂ → n₂✝ = rtr₂
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
h₂ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂{Component.val cpt}{i} = some v
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂
Tactic:
injection (StrictMember.final h₂).unique (u.member₁.nested h₁)
State after:
no goals