Theorem: Reactor.ext_obj?
Proof state before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {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₂
cpt : Component
i : ID
n₁ : Component.type α cpt
hc₁ : rtr₁{cpt}{i} = some n₁
n₂ : Component.type α cpt
hc₂ : rtr₂{cpt}{i} = some n₂
⊢ n₁ = n₂
Tactic:
cases cpt
Proof state after:
case val
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {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₂
i : ID
v✝ : Component.Valued
n₁ : Component.type α (Component.val v✝)
hc₁ : rtr₁{Component.val v✝}{i} = some n₁
n₂ : Component.type α (Component.val v✝)
hc₂ : rtr₂{Component.val v✝}{i} = some n₂
⊢ n₁ = n₂

case rtr
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {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₂
i : ID
n₁ : Component.type α Component.rtr
hc₁ : rtr₁{Component.rtr}{i} = some n₁
n₂ : Component.type α Component.rtr
hc₂ : rtr₂{Component.rtr}{i} = some n₂
⊢ n₁ = n₂

case rcn
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {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₂
i : ID
n₁ : Component.type α Component.rcn
hc₁ : rtr₁{Component.rcn}{i} = some n₁
n₂ : Component.type α Component.rcn
hc₂ : rtr₂{Component.rcn}{i} = some n₂
⊢ n₁ = n₂