Theorem: Variable.eq (FormalSystems/Computability/Loop.lean)

State before:
v₁ v₂ : Variable
⊢ v₁ = v₂ ↔ v₁.index = v₂.index
Tactic:
constructor
State after:
case mp
v₁ v₂ : Variable
⊢ v₁ = v₂ → v₁.index = v₂.index

case mpr
v₁ v₂ : Variable
⊢ v₁.index = v₂.index → v₁ = v₂

State before:
case mp
v₁ v₂ : Variable
⊢ v₁ = v₂ → v₁.index = v₂.index

case mpr
v₁ v₂ : Variable
⊢ v₁.index = v₂.index → v₁ = v₂
Tactic:
. intro; congr
State after:
case mpr
v₁ v₂ : Variable
⊢ v₁.index = v₂.index → v₁ = v₂

State before:
case mpr
v₁ v₂ : Variable
⊢ v₁.index = v₂.index → v₁ = v₂
Tactic:
. intro h
  cases v₁; cases v₂
  dsimp at h; rw [h]
State after:
no goals

State before:
case mp
v₁ v₂ : Variable
⊢ v₁ = v₂ → v₁.index = v₂.index
Tactic:
intro
State after:
case mp
v₁ v₂ : Variable
a✝ : v₁ = v₂
⊢ v₁.index = v₂.index

State before:
case mp
v₁ v₂ : Variable
a✝ : v₁ = v₂
⊢ v₁.index = v₂.index
Tactic:
congr
State after:
no goals

State before:
case mpr
v₁ v₂ : Variable
⊢ v₁.index = v₂.index → v₁ = v₂
Tactic:
intro h
State after:
case mpr
v₁ v₂ : Variable
h : v₁.index = v₂.index
⊢ v₁ = v₂

State before:
case mpr
v₁ v₂ : Variable
h : v₁.index = v₂.index
⊢ v₁ = v₂
Tactic:
cases v₁
State after:
case mpr.mk
v₂ : Variable
index✝ : ℕ
h : { index := index✝ }.index = v₂.index
⊢ { index := index✝ } = v₂

State before:
case mpr.mk
v₂ : Variable
index✝ : ℕ
h : { index := index✝ }.index = v₂.index
⊢ { index := index✝ } = v₂
Tactic:
cases v₂
State after:
case mpr.mk.mk
index✝¹ index✝ : ℕ
h : { index := index✝¹ }.index = { index := index✝ }.index
⊢ { index := index✝¹ } = { index := index✝ }

State before:
case mpr.mk.mk
index✝¹ index✝ : ℕ
h : { index := index✝¹ }.index = { index := index✝ }.index
⊢ { index := index✝¹ } = { index := index✝ }
Tactic:
dsimp at h
State after:
case mpr.mk.mk
index✝¹ index✝ : ℕ
h : index✝¹ = index✝
⊢ { index := index✝¹ } = { index := index✝ }

State before:
case mpr.mk.mk
index✝¹ index✝ : ℕ
h : index✝¹ = index✝
⊢ { index := index✝¹ } = { index := index✝ }
Tactic:
rw [h]
State after:
no goals