Theorem: Reactor.Equivalent.get?_rtr_some_equiv (ReactorModel/Objects/Reactor/Theorems/Basic.lean)

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
i : ID
n₁ n₂ : Component.type α Component.rtr
⊢ rtr₁{Component.rtr}{i} = some n₁ → rtr₁{Component.rtr}{i} = some n₂ → n₁ ≈ n₂
Tactic:
intros
State after:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
i : ID
n₁ n₂ : Component.type α Component.rtr
a✝¹ : rtr₁{Component.rtr}{i} = some n₁
a✝ : rtr₁{Component.rtr}{i} = some n₂
⊢ n₁ ≈ n₂

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
i : ID
n₁ n₂ : Component.type α Component.rtr
a✝¹ : rtr₁{Component.rtr}{i} = some n₁
a✝ : rtr₁{Component.rtr}{i} = some n₂
⊢ n₁ ≈ n₂
Tactic:
simp_all
State after:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
i : ID
n₁ n₂ : Component.type α Component.rtr
a✝¹ : n₂ = n₁
a✝ : rtr₁{Component.rtr}{i} = some n₁
⊢ n₁ ≈ n₁

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
i : ID
n₁ n₂ : Component.type α Component.rtr
a✝¹ : n₂ = n₁
a✝ : rtr₁{Component.rtr}{i} = some n₁
⊢ n₁ ≈ n₁
Tactic:
exact .refl _
State after:
no goals