internlm/Lean-Github huggingface dataset:
Theorem: Reactor.Equivalent.trans
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₂ → ∀ {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 _
Proof 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₂✝
Theorem: Reactor.Equivalent.trans
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₂ → ∀ {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⟩
Proof 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₂✝
Theorem: Reactor.Equivalent.trans
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₂ → ∀ {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 ‹_›)
Proof state after:
no goals
Theorem: Reactor.Equivalent.trans
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₂ → ∀ {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 _
Proof 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₂✝
Theorem: Reactor.Equivalent.trans
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₂ → ∀ {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⟩
Proof 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₂✝
Theorem: Reactor.Equivalent.trans
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₂ → ∀ {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 ‹_›)
Proof state after:
no goals
Theorem: Reactor.Equivalent.get?_rcn_some_eq
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
i : ID
r₁ r₂ : Component.type α Component.rcn
⊢ rtr₁{Component.rcn}{i} = some r₁ → rtr₁{Component.rcn}{i} = some r₂ → r₁ = r₂
Tactic:
simp_all
Proof state after:
no goals
Theorem: Reactor.Equivalent.get?_rtr_some_equiv
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
i : ID
n₁ n₂ : Component.type α Component.rtr
⊢ rtr₁{Component.rtr}{i} = some n₁ → rtr₁{Component.rtr}{i} = some n₂ → n₁ ≈ n₂
Tactic:
intros
Proof state after:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
i : ID
n₁ n₂ : Component.type α Component.rtr
a✝¹ : rtr₁{Component.rtr}{i} = some n₁
a✝ : rtr₁{Component.rtr}{i} = some n₂
⊢ n₁ ≈ n₂
Theorem: Reactor.Equivalent.get?_rtr_some_equiv
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
i : ID
n₁ n₂ : Component.type α Component.rtr
a✝¹ : rtr₁{Component.rtr}{i} = some n₁
a✝ : rtr₁{Component.rtr}{i} = some n₂
⊢ n₁ ≈ n₂
Tactic:
simp_all
Proof state after:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
i : ID
n₁ n₂ : Component.type α Component.rtr
a✝¹ : n₂ = n₁
a✝ : rtr₁{Component.rtr}{i} = some n₁
⊢ n₁ ≈ n₁
Theorem: Reactor.Equivalent.get?_rtr_some_equiv
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
i : ID
n₁ n₂ : Component.type α Component.rtr
a✝¹ : n₂ = n₁
a✝ : rtr₁{Component.rtr}{i} = some n₁
⊢ n₁ ≈ n₁
Tactic:
exact .refl _
Proof state after:
no goals
Theorem: Reactor.Equivalent.get?_some_iff
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
cpt : Component
i : ID
e : rtr₁ ≈ rtr₂
⊢ (∃ o, rtr₁{cpt}{i} = some o) ↔ ∃ o, rtr₂{cpt}{i} = some o
Tactic:
simp [←Partial.mem_iff, mem_get?_iff e]
Proof state after:
no goals
Theorem: Reactor.Equivalent.get?_none_iff
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
cpt : Component
i : ID
e : rtr₁ ≈ rtr₂
⊢ rtr₁{cpt}{i} = none ↔ rtr₂{cpt}{i} = none
Tactic:
simp only [Option.eq_none_iff_forall_not_mem, ←not_exists]
Proof state after:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
cpt : Component
i : ID
e : rtr₁ ≈ rtr₂
⊢ (¬∃ x, x ∈ rtr₁{cpt}{i}) ↔ ¬∃ x, x ∈ rtr₂{cpt}{i}
Theorem: Reactor.Equivalent.get?_none_iff
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
cpt : Component
i : ID
e : rtr₁ ≈ rtr₂
⊢ (¬∃ x, x ∈ rtr₁{cpt}{i}) ↔ ¬∃ x, x ∈ rtr₂{cpt}{i}
Tactic:
simp [get?_some_iff e]
Proof state after:
no goals
Theorem: Reactor.Equivalent.get?_rcn_eq
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
⊢ rtr₂{Component.rcn} = rtr₁{Component.rcn}
Tactic:
funext i
Proof state after:
case h
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}
Theorem: Reactor.Equivalent.get?_rcn_eq
Proof 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
Proof 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}
Theorem: Reactor.Equivalent.get?_rcn_eq
Proof 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₂
Proof state after:
no goals
Theorem: Reactor.Equivalent.get?_rcn_eq
Proof 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₂]
Proof state after:
no goals
Theorem: Reactor.Equivalent.get?_rcn_eq
Proof 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₁
Proof 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}
Theorem: Reactor.Equivalent.get?_rcn_eq
Proof 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₁
Proof 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}
Theorem: Reactor.Equivalent.get?_rcn_eq
Proof 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₂
Proof state after:
no goals
Theorem: Reactor.Equivalent.get?_rcn_eq
Proof 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₁
Proof 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}
Theorem: Reactor.Equivalent.get?_rcn_eq
Proof 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₂
Proof 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}
Theorem: Reactor.Equivalent.get?_rcn_eq
Proof 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₂]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ rtr₁ ≈ rtr₂
Tactic:
induction u <;> constructor
Proof state after:
case final.mem_get?_iff
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}

case final.get?_rcn_some_eq
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂

case final.get?_rtr_some_equiv
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝² : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂

case nested.mem_get?_iff
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}

case nested.get?_rcn_some_eq
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : 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 nested.get?_rtr_some_equiv
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : 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₂
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
Tactic:
case final.mem_get?_iff e h₁ h₂ =>
  intro c j
  by_cases hc : c = cpt <;> try subst hc
  case neg => exact e.mem_iff (.inl hc)
  case pos =>
    by_cases hj : j = i <;> try subst hj
    case neg => exact e.mem_iff (.inr hj)
    case pos => simp [Partial.mem_iff, h₁, h₂]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.equiv
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
Tactic:
case final.get?_rcn_some_eq e _ _ =>
  intro j _ _ h₁ h₂
  have h := e (c := .rcn) (j := j) (.inl $ by simp)
  simp_all
Proof state after:
no goals