Theorem: Reactor.RootEqualUpTo.ext (ReactorModel/Objects/Reactor/Theorems/Extensional.lean)

State before:
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
⊢ rtr₁ = rtr₂
Tactic:
ext1
State after:
case a
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
⊢ get? rtr₁ = get? rtr₂

State before:
case a
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
⊢ get? rtr₁ = get? rtr₂
Tactic:
ext1 c
State after:
case a.h
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
⊢ rtr₁{c} = rtr₂{c}

State before:
case a.h
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
⊢ rtr₁{c} = rtr₂{c}
Tactic:
ext1 j
State after:
case a.h.h
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
⊢ rtr₁{c}{j} = rtr₂{c}{j}

State before:
case a.h.h
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
⊢ rtr₁{c}{j} = rtr₂{c}{j}
Tactic:
by_cases hc : c = cpt <;> by_cases hj : j = i
State after:
case pos
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : c = cpt
hj : j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}

case neg
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : c = cpt
hj : ¬j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}

case pos
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : ¬c = cpt
hj : j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}

case neg
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : ¬c = cpt
hj : ¬j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}

State before:
case pos
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : c = cpt
hj : j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}
Tactic:
exact hc ▸ hj ▸ h
State after:
no goals

State before:
case neg
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : c = cpt
hj : ¬j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}
Tactic:
exact hc ▸ e (.inr hj)
State after:
no goals

State before:
case pos
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : ¬c = cpt
hj : j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}
Tactic:
exact e (.inl hc)
State after:
no goals

State before:
case neg
α : Type
inst✝ : Extensional α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
e : rtr₁ ≃[cpt][i] rtr₂
h : rtr₁{cpt}{i} = rtr₂{cpt}{i}
c : Component
j : ID
hc : ¬c = cpt
hj : ¬j = i
⊢ rtr₁{c}{j} = rtr₂{c}{j}
Tactic:
exact e (.inl hc)
State after:
no goals