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

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
⊢ rtr₂{Component.rcn} = rtr₁{Component.rcn}
Tactic:
funext i
State after:
case h
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}

State before:
case h
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}
Tactic:
by_cases h₁ : ∃ o, rtr₁{.rcn}{i} = some o
State after:
case pos
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ∃ o, rtr₁{Component.rcn}{i} = some o
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}

case neg
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ¬∃ o, rtr₁{Component.rcn}{i} = some o
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ∃ o, rtr₁{Component.rcn}{i} = some o
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}
Tactic:
case pos =>
  have ⟨_, h₂⟩ := get?_some_iff e |>.mp h₁
  have ⟨_, h₁⟩ := h₁
  exact get?_rcn_some_eq e h₁ h₂ ▸ h₁ |>.symm ▸ h₂
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ¬∃ o, rtr₁{Component.rcn}{i} = some o
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}
Tactic:
case neg =>
  have h₂ := get?_some_iff e |>.not.mp h₁
  push_neg at h₁ h₂
  simp [Option.eq_none_iff_forall_not_mem.mpr h₁, Option.eq_none_iff_forall_not_mem.mpr h₂]
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ∃ o, rtr₁{Component.rcn}{i} = some o
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}
Tactic:
have ⟨_, h₂⟩ := get?_some_iff e |>.mp h₁
State after:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ∃ o, rtr₁{Component.rcn}{i} = some o
w✝ : Component.type α Component.rcn
h₂ : rtr₂{Component.rcn}{i} = some w✝
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ∃ o, rtr₁{Component.rcn}{i} = some o
w✝ : Component.type α Component.rcn
h₂ : rtr₂{Component.rcn}{i} = some w✝
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}
Tactic:
have ⟨_, h₁⟩ := h₁
State after:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁✝ : ∃ o, rtr₁{Component.rcn}{i} = some o
w✝¹ : Component.type α Component.rcn
h₂ : rtr₂{Component.rcn}{i} = some w✝¹
w✝ : Component.type α Component.rcn
h₁ : rtr₁{Component.rcn}{i} = some w✝
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁✝ : ∃ o, rtr₁{Component.rcn}{i} = some o
w✝¹ : Component.type α Component.rcn
h₂ : rtr₂{Component.rcn}{i} = some w✝¹
w✝ : Component.type α Component.rcn
h₁ : rtr₁{Component.rcn}{i} = some w✝
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}
Tactic:
exact get?_rcn_some_eq e h₁ h₂ ▸ h₁ |>.symm ▸ h₂
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ¬∃ o, rtr₁{Component.rcn}{i} = some o
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}
Tactic:
have h₂ := get?_some_iff e |>.not.mp h₁
State after:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ¬∃ o, rtr₁{Component.rcn}{i} = some o
h₂ : ¬∃ o, rtr₂{Component.rcn}{i} = some o
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ¬∃ o, rtr₁{Component.rcn}{i} = some o
h₂ : ¬∃ o, rtr₂{Component.rcn}{i} = some o
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}
Tactic:
push_neg at h₁ h₂
State after:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ∀ (o : Component.type α Component.rcn), rtr₁{Component.rcn}{i} ≠ some o
h₂ : ∀ (o : Component.type α Component.rcn), rtr₂{Component.rcn}{i} ≠ some o
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ∀ (o : Component.type α Component.rcn), rtr₁{Component.rcn}{i} ≠ some o
h₂ : ∀ (o : Component.type α Component.rcn), rtr₂{Component.rcn}{i} ≠ some o
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}
Tactic:
simp [Option.eq_none_iff_forall_not_mem.mpr h₁, Option.eq_none_iff_forall_not_mem.mpr h₂]
State after:
no goals