internlm/Lean-Github huggingface dataset:
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
Tactic:
case final.get?_rtr_some_equiv e _ _ =>
  intro j _ _ h₁ h₂
  have h := e (c := .rtr) (j := j) (.inl $ by simp)
  simp_all
  apply Equivalent.refl
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
Tactic:
case nested.mem_get?_iff j _ _ _ _ e h₁ h₂ _ _ =>
  intro c j'
  by_cases hc : c = .rtr <;> try subst hc
  case neg => exact e.mem_iff (.inl hc)
  case pos => 
    by_cases hj : j' = j <;> try subst hj
    case neg => exact e.mem_iff (.inr hj)
    case pos => simp [Partial.mem_iff, h₁, h₂]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
Tactic:
case nested.get?_rcn_some_eq e h₁ h₂ _ _ =>
  intro j _ _ h₁ h₂
  have h := e (c := .rcn) (j := j) (.inl $ by simp)
  simp_all
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : 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₂✝
hi : n₁✝ ≈ n₂✝
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
Tactic:
case nested.get?_rtr_some_equiv j _ _ _ _ e _ _ _ hi =>
  intro j' n₁' n₂' h₁' h₂'
  by_cases hj : j' = j <;> try subst hj
  case pos => simp_all; assumption
  case neg => 
    have := e (c := .rtr) (j := j') (.inr hj)
    simp_all
    apply Equivalent.refl
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
Tactic:
intro c j
Proof state after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
c : Component
j : ID
⊢ j ∈ rtr₁✝{c} ↔ j ∈ rtr₂✝{c}
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
c : Component
j : ID
⊢ j ∈ rtr₁✝{c} ↔ j ∈ rtr₂✝{c}
Tactic:
by_cases hc : c = cpt <;> try subst hc
Proof state after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}

case neg
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
c : Component
j : ID
hc : ¬c = Component.val cpt
⊢ j ∈ rtr₁✝{c} ↔ j ∈ rtr₂✝{c}
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
c : Component
j : ID
hc : ¬c = Component.val cpt
⊢ j ∈ rtr₁✝{c} ↔ j ∈ rtr₂✝{c}
Tactic:
case neg => exact e.mem_iff (.inl hc)
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Tactic:
case pos =>
  by_cases hj : j = i <;> try subst hj
  case neg => exact e.mem_iff (.inr hj)
  case pos => simp [Partial.mem_iff, h₁, h₂]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
c : Component
j : ID
hc : c = Component.val cpt
⊢ j ∈ rtr₁✝{c} ↔ j ∈ rtr₂✝{c}
Tactic:
subst hc
Proof state after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
c : Component
j : ID
hc : ¬c = Component.val cpt
⊢ j ∈ rtr₁✝{c} ↔ j ∈ rtr₂✝{c}
Tactic:
exact e.mem_iff (.inl hc)
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Tactic:
by_cases hj : j = i <;> try subst hj
Proof state after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
j : ID
e : rtr₁✝ ≃[Component.val cpt][j] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{j} = some o✝
h₂ : rtr₂✝{Component.val cpt}{j} = some v
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}

case neg
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
hj : ¬j = i
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
hj : ¬j = i
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Tactic:
case neg => exact e.mem_iff (.inr hj)
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
j : ID
e : rtr₁✝ ≃[Component.val cpt][j] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{j} = some o✝
h₂ : rtr₂✝{Component.val cpt}{j} = some v
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Tactic:
case pos => simp [Partial.mem_iff, h₁, h₂]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
hj : j = i
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Tactic:
subst hj
Proof state after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
j : ID
e : rtr₁✝ ≃[Component.val cpt][j] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{j} = some o✝
h₂ : rtr₂✝{Component.val cpt}{j} = some v
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
hj : ¬j = i
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Tactic:
exact e.mem_iff (.inr hj)
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
j : ID
e : rtr₁✝ ≃[Component.val cpt][j] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{j} = some o✝
h₂ : rtr₂✝{Component.val cpt}{j} = some v
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Tactic:
simp [Partial.mem_iff, h₁, h₂]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
Tactic:
intro j _ _ h₁ h₂
Proof state after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
⊢ r₁✝ = r₂✝
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
⊢ r₁✝ = r₂✝
Tactic:
have h := e (c := .rcn) (j := j) (.inl $ by simp)
Proof state after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
h : rtr₁✝{Component.rcn}{j} = rtr₂✝{Component.rcn}{j}
⊢ r₁✝ = r₂✝
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
h : rtr₁✝{Component.rcn}{j} = rtr₂✝{Component.rcn}{j}
⊢ r₁✝ = r₂✝
Tactic:
simp_all
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
⊢ Component.rcn ≠ Component.val cpt
Tactic:
simp
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
Tactic:
intro j _ _ h₁ h₂
Proof state after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
n₁✝ n₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₂✝
⊢ Equivalent n₁✝ n₂✝
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
n₁✝ n₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₂✝
⊢ Equivalent n₁✝ n₂✝
Tactic:
have h := e (c := .rtr) (j := j) (.inl $ by simp)
Proof state after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
n₁✝ n₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₂✝
h : rtr₁✝{Component.rtr}{j} = rtr₂✝{Component.rtr}{j}
⊢ Equivalent n₁✝ n₂✝
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
n₁✝ n₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₂✝
h : rtr₁✝{Component.rtr}{j} = rtr₂✝{Component.rtr}{j}
⊢ Equivalent n₁✝ n₂✝
Tactic:
simp_all
Proof state after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
n₁✝ n₂✝ : Component.type α Component.rtr
h₁ : n₂✝ = n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₁✝
h : rtr₁✝{Component.rtr}{j} = some n₁✝
⊢ Equivalent n₁✝ n₁✝
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
n₁✝ n₂✝ : Component.type α Component.rtr
h₁ : n₂✝ = n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₁✝
h : rtr₁✝{Component.rtr}{j} = some n₁✝
⊢ Equivalent n₁✝ n₁✝
Tactic:
apply Equivalent.refl
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
n₁✝ n₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₂✝
⊢ Component.rtr ≠ Component.val cpt
Tactic:
simp
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
Tactic:
intro c j'
Proof state after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
c : Component
j' : ID
⊢ j' ∈ rtr₁✝{c} ↔ j' ∈ rtr₂✝{c}
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
c : Component
j' : ID
⊢ j' ∈ rtr₁✝{c} ↔ j' ∈ rtr₂✝{c}
Tactic:
by_cases hc : c = .rtr <;> try subst hc
Proof state after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}

case neg
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
c : Component
j' : ID
hc : ¬c = Component.rtr
⊢ j' ∈ rtr₁✝{c} ↔ j' ∈ rtr₂✝{c}
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
c : Component
j' : ID
hc : ¬c = Component.rtr
⊢ j' ∈ rtr₁✝{c} ↔ j' ∈ rtr₂✝{c}
Tactic:
case neg => exact e.mem_iff (.inl hc)
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Tactic:
case pos => 
  by_cases hj : j' = j <;> try subst hj
  case neg => exact e.mem_iff (.inr hj)
  case pos => simp [Partial.mem_iff, h₁, h₂]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
c : Component
j' : ID
hc : c = Component.rtr
⊢ j' ∈ rtr₁✝{c} ↔ j' ∈ rtr₂✝{c}
Tactic:
subst hc
Proof state after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
c : Component
j' : ID
hc : ¬c = Component.rtr
⊢ j' ∈ rtr₁✝{c} ↔ j' ∈ rtr₂✝{c}
Tactic:
exact e.mem_iff (.inl hc)
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Tactic:
by_cases hj : j' = j <;> try subst hj
Proof state after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j'} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}

case neg
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
hj : ¬j' = j
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
hj : ¬j' = j
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Tactic:
case neg => exact e.mem_iff (.inr hj)
Proof state after:
no goals