Theorem: Reactor.Equivalent.trans (ReactorModel/Objects/Reactor/Theorems/Basic.lean)

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₃ : α
e₁ : rtr₁ ≈ rtr₂
e₂ : rtr₂ ≈ rtr₃
⊢ rtr₁ ≈ rtr₃
Tactic:
induction e₁ generalizing rtr₃
State after:
case refl
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr✝ rtr₃ : α
e₂ : rtr✝ ≈ rtr₃
⊢ rtr✝ ≈ rtr₃

case struct
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
mem_get?_iff✝ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
get?_rcn_some_eq✝ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
get?_rtr_some_equiv_ih✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
e₂ : rtr₂✝ ≈ rtr₃
⊢ rtr₁✝ ≈ rtr₃

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr✝ rtr₃ : α
e₂ : rtr✝ ≈ rtr₃
⊢ rtr✝ ≈ rtr₃
Tactic:
case refl => exact e₂
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr✝ rtr₃ : α
e₂ : rtr✝ ≈ rtr₃
⊢ rtr✝ ≈ rtr₃
Tactic:
exact e₂
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
e₂ : rtr₂✝ ≈ rtr₃
⊢ rtr₁✝ ≈ rtr₃
Tactic:
cases e₂
State after:
case refl
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
⊢ rtr₁✝ ≈ rtr₂✝

case struct
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝¹ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
mem_get?_iff✝ : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
get?_rcn_some_eq✝ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
⊢ rtr₁✝ ≈ rtr₃

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
⊢ rtr₁✝ ≈ rtr₂✝
Tactic:
case refl => exact .struct ‹_› ‹_› ‹_›
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
⊢ rtr₁✝ ≈ rtr₂✝
Tactic:
exact .struct ‹_› ‹_› ‹_›
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
⊢ rtr₁✝ ≈ rtr₃
Tactic:
apply Equivalent.struct
State after:
case mem_get?_iff
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₃{cpt}

case get?_rcn_some_eq
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂

case get?_rtr_some_equiv
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂

State before:
case mem_get?_iff
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₃{cpt}
Tactic:
intros
State after:
case mem_get?_iff
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
cpt✝ : Component
i✝ : ID
⊢ i✝ ∈ rtr₁✝{cpt✝} ↔ i✝ ∈ rtr₃{cpt✝}

State before:
case mem_get?_iff
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
cpt✝ : Component
i✝ : ID
⊢ i✝ ∈ rtr₁✝{cpt✝} ↔ i✝ ∈ rtr₃{cpt✝}
Tactic:
exact h₁ ‹_› ‹_› |>.trans (h₁' ‹_› ‹_›)
State after:
no goals

State before:
case get?_rcn_some_eq
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
Tactic:
intro _ _ _ h _
State after:
case get?_rcn_some_eq
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
i✝ : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h : rtr₁✝{Component.rcn}{i✝} = some r₁✝
a✝ : rtr₃{Component.rcn}{i✝} = some r₂✝
⊢ r₁✝ = r₂✝

State before:
case get?_rcn_some_eq
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
i✝ : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h : rtr₁✝{Component.rcn}{i✝} = some r₁✝
a✝ : rtr₃{Component.rcn}{i✝} = some r₂✝
⊢ r₁✝ = r₂✝
Tactic:
have ⟨_, h⟩ := Partial.mem_iff.mp <| h₁ .rcn ‹_› |>.mp $ Partial.mem_iff.mpr ⟨_, h⟩
State after:
case get?_rcn_some_eq
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
i✝ : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h✝ : rtr₁✝{Component.rcn}{i✝} = some r₁✝
a✝ : rtr₃{Component.rcn}{i✝} = some r₂✝
w✝ : Component.type α Component.rcn
h : rtr₂✝{Component.rcn}{i✝} = some w✝
⊢ r₁✝ = r₂✝

State before:
case get?_rcn_some_eq
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
i✝ : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h✝ : rtr₁✝{Component.rcn}{i✝} = some r₁✝
a✝ : rtr₃{Component.rcn}{i✝} = some r₂✝
w✝ : Component.type α Component.rcn
h : rtr₂✝{Component.rcn}{i✝} = some w✝
⊢ r₁✝ = r₂✝
Tactic:
exact h₂ ‹_› h |>.trans (h₂' h ‹_›)
State after:
no goals

State before:
case get?_rtr_some_equiv
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
Tactic:
intro _ _ _ h _
State after:
case get?_rtr_some_equiv
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
i✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
h : rtr₁✝{Component.rtr}{i✝} = some n₁✝
a✝ : rtr₃{Component.rtr}{i✝} = some n₂✝
⊢ Equivalent n₁✝ n₂✝

State before:
case get?_rtr_some_equiv
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
i✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
h : rtr₁✝{Component.rtr}{i✝} = some n₁✝
a✝ : rtr₃{Component.rtr}{i✝} = some n₂✝
⊢ Equivalent n₁✝ n₂✝
Tactic:
have ⟨_, h⟩ := Partial.mem_iff.mp <| h₁ .rtr ‹_› |>.mp $ Partial.mem_iff.mpr ⟨_, h⟩
State after:
case get?_rtr_some_equiv
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
i✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
h✝ : rtr₁✝{Component.rtr}{i✝} = some n₁✝
a✝ : rtr₃{Component.rtr}{i✝} = some n₂✝
w✝ : Component.type α Component.rtr
h : rtr₂✝{Component.rtr}{i✝} = some w✝
⊢ Equivalent n₁✝ n₂✝

State before:
case get?_rtr_some_equiv
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₁✝ rtr₂✝ : α
h₁ : ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
h₂ :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
get?_rtr_some_equiv✝ :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
hi :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → ∀ {rtr₃ : α}, n₂ ≈ rtr₃ → n₁ ≈ rtr₃
rtr₃ : α
h₁' : ∀ (cpt : Component) (i : ID), i ∈ rtr₂✝{cpt} ↔ i ∈ rtr₃{cpt}
h₂' :
  ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₂✝{Component.rcn}{i} = some r₁ → rtr₃{Component.rcn}{i} = some r₂ → r₁ = r₂
h₃' :
  ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₂✝{Component.rtr}{i} = some n₁ → rtr₃{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
i✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
h✝ : rtr₁✝{Component.rtr}{i✝} = some n₁✝
a✝ : rtr₃{Component.rtr}{i✝} = some n₂✝
w✝ : Component.type α Component.rtr
h : rtr₂✝{Component.rtr}{i✝} = some w✝
⊢ Equivalent n₁✝ n₂✝
Tactic:
exact hi ‹_› h (h₃' h ‹_›)
State after:
no goals