internlm/Lean-Github huggingface dataset:
Theorem: Execution.Step.Time.RTC.tag_le
Proof state before:
case trans
α : Type
inst✝ : Proper α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a : s₁✝ ↓ₜ s₂✝
a✝ : RTC s₂✝ s₃✝
hi : s₂✝.tag ≤ s₃✝.tag
⊢ s₁✝.tag ≤ s₃✝.tag
Tactic:
exact le_trans (le_of_lt a.tag_lt) hi
Proof state after:
no goals
Theorem: Execution.Step.Time.RTC.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
ht : s₁.tag = s₂.tag
e₁ : RTC s s₁
e₂ : RTC s s₂
⊢ s₁ = s₂
Tactic:
induction e₁ generalizing s₂ <;> cases e₂
Proof state after:
case refl.refl
α : Type
inst✝ : Proper α
s s₁ s✝ : State α
ht : s✝.tag = s✝.tag
⊢ s✝ = s✝

case refl.trans
α : Type
inst✝ : Proper α
s s₁ s✝ s₂ : State α
ht : s✝.tag = s₂.tag
s₂✝ : State α
a✝¹ : s✝ ↓ₜ s₂✝
a✝ : RTC s₂✝ s₂
⊢ s✝ = s₂

case trans.refl
α : Type
inst✝ : Proper α
s s₁ s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ₜ s₂✝
a✝ : RTC s₂✝ s₃✝
a_ih✝ : ∀ {s₂ : State α}, s₃✝.tag = s₂.tag → RTC s₂✝ s₂ → s₃✝ = s₂
ht : s₃✝.tag = s₁✝.tag
⊢ s₃✝ = s₁✝

case trans.trans
α : Type
inst✝ : Proper α
s s₁ s₁✝ s₂✝¹ s₃✝ : State α
a✝³ : s₁✝ ↓ₜ s₂✝¹
a✝² : RTC s₂✝¹ s₃✝
a_ih✝ : ∀ {s₂ : State α}, s₃✝.tag = s₂.tag → RTC s₂✝¹ s₂ → s₃✝ = s₂
s₂ : State α
ht : s₃✝.tag = s₂.tag
s₂✝ : State α
a✝¹ : s₁✝ ↓ₜ s₂✝
a✝ : RTC s₂✝ s₂
⊢ s₃✝ = s₂
Theorem: Execution.Step.Time.RTC.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s✝ : State α
ht : s✝.tag = s✝.tag
⊢ s✝ = s✝
Tactic:
case refl.refl         => rfl
Proof state after:
no goals
Theorem: Execution.Step.Time.RTC.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s✝ s₂ : State α
ht : s✝.tag = s₂.tag
s₂✝ : State α
e : s✝ ↓ₜ s₂✝
e' : RTC s₂✝ s₂
⊢ s✝ = s₂
Tactic:
case refl.trans e e'   => exact absurd ht      (ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le)
Proof state after:
no goals
Theorem: Execution.Step.Time.RTC.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ₜ s₂✝
e' : RTC s₂✝ s₃✝
a_ih✝ : ∀ {s₂ : State α}, s₃✝.tag = s₂.tag → RTC s₂✝ s₂ → s₃✝ = s₂
ht : s₃✝.tag = s₁✝.tag
⊢ s₃✝ = s₁✝
Tactic:
case trans.refl e e' _ => exact absurd ht.symm (ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le)
Proof state after:
no goals
Theorem: Execution.Step.Time.RTC.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₁✝ s₂✝¹ s₃✝ : State α
e₁ : s₁✝ ↓ₜ s₂✝¹
e₁' : RTC s₂✝¹ s₃✝
hi : ∀ {s₂ : State α}, s₃✝.tag = s₂.tag → RTC s₂✝¹ s₂ → s₃✝ = s₂
s₂ : State α
ht : s₃✝.tag = s₂.tag
s₂✝ : State α
e₂ : s₁✝ ↓ₜ s₂✝
e₂' : RTC s₂✝ s₂
⊢ s₃✝ = s₂
Tactic:
case trans.trans e₁ e₁' hi _ e₂ e₂' => exact hi ht (e₂.deterministic e₁ ▸ e₂')
Proof state after:
no goals
Theorem: Execution.Step.Time.RTC.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s✝ : State α
ht : s✝.tag = s✝.tag
⊢ s✝ = s✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Step.Time.RTC.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s✝ s₂ : State α
ht : s✝.tag = s₂.tag
s₂✝ : State α
e : s✝ ↓ₜ s₂✝
e' : RTC s₂✝ s₂
⊢ s✝ = s₂
Tactic:
exact absurd ht      (ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le)
Proof state after:
no goals
Theorem: Execution.Step.Time.RTC.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₁✝ s₂✝ s₃✝ : State α
e : s₁✝ ↓ₜ s₂✝
e' : RTC s₂✝ s₃✝
a_ih✝ : ∀ {s₂ : State α}, s₃✝.tag = s₂.tag → RTC s₂✝ s₂ → s₃✝ = s₂
ht : s₃✝.tag = s₁✝.tag
⊢ s₃✝ = s₁✝
Tactic:
exact absurd ht.symm (ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le)
Proof state after:
no goals
Theorem: Execution.Step.Time.RTC.deterministic
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₁✝ s₂✝¹ s₃✝ : State α
e₁ : s₁✝ ↓ₜ s₂✝¹
e₁' : RTC s₂✝¹ s₃✝
hi : ∀ {s₂ : State α}, s₃✝.tag = s₂.tag → RTC s₂✝¹ s₂ → s₃✝ = s₂
s₂ : State α
ht : s₃✝.tag = s₂.tag
s₂✝ : State α
e₂ : s₁✝ ↓ₜ s₂✝
e₂' : RTC s₂✝ s₂
⊢ s₃✝ = s₂
Tactic:
exact hi ht (e₂.deterministic e₁ ▸ e₂')
Proof state after:
no goals
Theorem: Execution.to_timeStepRTC
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
triv : State.Trivial s₁
e : s₁ ⇓ s₂
⊢ Step.Time.RTC s₁ s₂
Tactic:
induction e <;> try cases ‹_ ↓ _›
Proof state after:
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
triv : State.Trivial s✝
⊢ Step.Time.RTC s✝ s✝

case trans.skip
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
s✝ : s₁✝ ↓ₛ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝

case trans.exec
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e✝ : s₁✝ ↓ₑ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝

case trans.time
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
t✝ : s₁✝ ↓ₜ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝
Theorem: Execution.to_timeStepRTC
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
triv : State.Trivial s✝
⊢ Step.Time.RTC s✝ s✝
Tactic:
case refl            => exact .refl
Proof state after:
no goals
Theorem: Execution.to_timeStepRTC
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e : s₁✝ ↓ₛ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝
Tactic:
case trans.skip e    => exact absurd triv e.not_trivial
Proof state after:
no goals
Theorem: Execution.to_timeStepRTC
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e : s₁✝ ↓ₑ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝
Tactic:
case trans.exec e    => exact absurd triv e.not_trivial
Proof state after:
no goals
Theorem: Execution.to_timeStepRTC
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
hi : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e : s₁✝ ↓ₜ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝
Tactic:
case trans.time hi e => exact .trans e (hi $ e.preserves_trivial triv)
Proof state after:
no goals
Theorem: Execution.to_timeStepRTC
Proof state before:
case trans
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ s₂✝
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
⊢ Step.Time.RTC s₁✝ s₃✝
Tactic:
cases ‹_ ↓ _›
Proof state after:
case trans.skip
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
s✝ : s₁✝ ↓ₛ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝

case trans.exec
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e✝ : s₁✝ ↓ₑ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝

case trans.time
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
t✝ : s₁✝ ↓ₜ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝
Theorem: Execution.to_timeStepRTC
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
triv : State.Trivial s✝
⊢ Step.Time.RTC s✝ s✝
Tactic:
exact .refl
Proof state after:
no goals
Theorem: Execution.to_timeStepRTC
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e : s₁✝ ↓ₛ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝
Tactic:
exact absurd triv e.not_trivial
Proof state after:
no goals
Theorem: Execution.to_timeStepRTC
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
a_ih✝ : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e : s₁✝ ↓ₑ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝
Tactic:
exact absurd triv e.not_trivial
Proof state after:
no goals
Theorem: Execution.to_timeStepRTC
Proof state before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
hi : State.Trivial s₂✝ → Step.Time.RTC s₂✝ s₃✝
triv : State.Trivial s₁✝
e : s₁✝ ↓ₜ s₂✝
⊢ Step.Time.RTC s₁✝ s₃✝
Tactic:
exact .trans e (hi $ e.preserves_trivial triv)
Proof state after:
no goals
Theorem: Reactor.RootEqualUpTo.mem_iff
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
c : Component
j : ID
e : rtr₁ ≃[cpt][i] rtr₂
h : c ≠ cpt ∨ j ≠ i
⊢ j ∈ rtr₁{c} ↔ j ∈ rtr₂{c}
Tactic:
simp [Partial.mem_iff]
Proof state after:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component
i : ID
rtr₂ : α
c : Component
j : ID
e : rtr₁ ≃[cpt][i] rtr₂
h : c ≠ cpt ∨ j ≠ i
⊢ (∃ b, rtr₁{c}{j} = some b) ↔ ∃ b, rtr₂{c}{j} = some b
Theorem: Reactor.RootEqualUpTo.valued
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ : α
i : ID
rtr₂ : α
j : ID
c cpt : Component.Valued
e : rtr₁ ≃[Component.val cpt][i] rtr₂
h : c ≠ cpt ∨ j ≠ i
⊢ c ≠ cpt → Component.val c ≠ Component.val cpt ∨ j ≠ i
Tactic:
simp [*]
Proof state after:
no goals
Theorem: Reactor.Equivalent.symm
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
⊢ rtr₂ ≈ rtr₁
Tactic:
induction e
Proof state after:
case refl
α : Type
inst✝ : Reactor α
rtr₁ 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₂ → n₂ ≈ n₁
⊢ rtr₂✝ ≈ rtr₁✝
Theorem: Reactor.Equivalent.symm
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr✝ : α
⊢ rtr✝ ≈ rtr✝
Tactic:
case refl => exact .refl _
Proof state after:
no goals
Theorem: Reactor.Equivalent.symm
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr✝ : α
⊢ rtr✝ ≈ rtr✝
Tactic:
exact .refl _
Proof state after:
no goals
Theorem: Reactor.Equivalent.symm
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₂ → n₂ ≈ n₁
⊢ rtr₂✝ ≈ rtr₁✝
Tactic:
constructor <;> intros
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₂ → 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₂ → n₂ ≈ n₁
i✝ : ID
r₁✝ r₂✝ : Component.type α Component.rcn
a✝¹ : rtr₂✝{Component.rcn}{i✝} = some r₁✝
a✝ : 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₂ → n₂ ≈ n₁
i✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
a✝¹ : rtr₂✝{Component.rtr}{i✝} = some n₁✝
a✝ : rtr₁✝{Component.rtr}{i✝} = some n₂✝
⊢ Equivalent n₁✝ n₂✝
Theorem: Reactor.Equivalent.symm
Proof 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₂ → n₂ ≈ n₁
cpt✝ : Component
i✝ : ID
⊢ i✝ ∈ rtr₂✝{cpt✝} ↔ i✝ ∈ rtr₁✝{cpt✝}
Tactic:
exact h₁ ‹_› ‹_› |>.symm
Proof state after:
no goals
Theorem: Reactor.Equivalent.symm
Proof 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₂ → n₂ ≈ n₁
i✝ : ID
r₁✝ r₂✝ : Component.type α Component.rcn
a✝¹ : rtr₂✝{Component.rcn}{i✝} = some r₁✝
a✝ : rtr₁✝{Component.rcn}{i✝} = some r₂✝
⊢ r₁✝ = r₂✝
Tactic:
exact h₂ ‹_› ‹_› |>.symm
Proof state after:
no goals
Theorem: Reactor.Equivalent.symm
Proof 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₂ → n₂ ≈ n₁
i✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
a✝¹ : rtr₂✝{Component.rtr}{i✝} = some n₁✝
a✝ : rtr₁✝{Component.rtr}{i✝} = some n₂✝
⊢ Equivalent n₁✝ n₂✝
Tactic:
exact hi ‹_› ‹_›
Proof state after:
no goals
Theorem: Reactor.Equivalent.trans
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr₃ : α
e₁ : rtr₁ ≈ rtr₂
e₂ : rtr₂ ≈ rtr₃
⊢ rtr₁ ≈ rtr₃
Tactic:
induction e₁ generalizing rtr₃
Proof 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₃
Theorem: Reactor.Equivalent.trans
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr✝ rtr₃ : α
e₂ : rtr✝ ≈ rtr₃
⊢ rtr✝ ≈ rtr₃
Tactic:
case refl => exact e₂
Proof state after:
no goals
Theorem: Reactor.Equivalent.trans
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ rtr✝ rtr₃ : α
e₂ : rtr✝ ≈ rtr₃
⊢ rtr✝ ≈ rtr₃
Tactic:
exact e₂
Proof state after:
no goals
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₃ : α
e₂ : rtr₂✝ ≈ rtr₃
⊢ rtr₁✝ ≈ rtr₃
Tactic:
cases e₂
Proof 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₃
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₁✝ ≈ rtr₂✝
Tactic:
case refl => exact .struct ‹_› ‹_› ‹_›
Proof state after:
no goals
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₁✝ ≈ rtr₂✝
Tactic:
exact .struct ‹_› ‹_› ‹_›
Proof state after:
no goals
Theorem: Reactor.Equivalent.trans
Proof 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
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✝}
Theorem: Reactor.Equivalent.trans
Proof 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₁' ‹_› ‹_›)
Proof state after:
no goals