Theorem: Reactor.Equivalent.trans
Proof 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
Proof 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₂