internlm/Lean-Github huggingface dataset:
Theorem: Reactor.StrictMember.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
s₁ : StrictMember cpt i rtr₂✝
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
o✝ : Component.type α cpt
h₂ : rtr₂{cpt}{i} = some o✝
⊢ nested h₁ s₁ ∼ final h₂
Tactic:
case nested.final h₁ s₁ _ _ h₂ =>
  injection (nested h₁ s₁).unique (final h₂ |>.fromEquiv $ Reactor.Equivalent.symm e)
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝¹ : Component.type α cpt
a✝¹ : rtr✝{cpt}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α cpt
a✝ : rtr₂{cpt}{i} = some o✝
⊢ final a✝¹ ∼ final a✝
Tactic:
constructor
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ nested h₁ s₁ ∼ nested h₂ s₂
Tactic:
suffices hj : j₁ = j₂ by 
  subst hj
  exact Equivalent.nested h₁ h₂ $ hi (Equivalent.get?_rtr_some_equiv e h₁ h₂) s₂
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ j₁ = j₂
Theorem: Reactor.StrictMember.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ j₁ = j₂
Tactic:
have hs := (nested h₁ s₁ |>.fromEquiv e).unique (nested h₂ s₂)
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : fromEquiv e (nested h₁ s₁) = nested h₂ s₂
⊢ j₁ = j₂
Theorem: Reactor.StrictMember.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : fromEquiv e (nested h₁ s₁) = nested h₂ s₂
⊢ j₁ = j₂
Tactic:
simp [fromEquiv] at hs
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : j₁ = j₂ ∧ Exists.choose ⋯ = rtr₂✝ ∧ HEq (fromEquiv ⋯ s₁) s₂
⊢ j₁ = j₂
Theorem: Reactor.StrictMember.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : j₁ = j₂ ∧ Exists.choose ⋯ = rtr₂✝ ∧ HEq (fromEquiv ⋯ s₁) s₂
⊢ j₁ = j₂
Tactic:
exact hs.left
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hj : j₁ = j₂
⊢ nested h₁ s₁ ∼ nested h₂ s₂
Tactic:
subst hj
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
⊢ nested h₁ s₁ ∼ nested h₂ s₂
Theorem: Reactor.StrictMember.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
⊢ nested h₁ s₁ ∼ nested h₂ s₂
Tactic:
exact Equivalent.nested h₁ h₂ $ hi (Equivalent.get?_rtr_some_equiv e h₁ h₂) s₂
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝ : Component.type α cpt
h₁ : rtr✝{cpt}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ final h₁ ∼ nested h₂ s₂
Tactic:
injection (final h₁ |>.fromEquiv e).unique (nested h₂ s₂)
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
s₁ : StrictMember cpt i rtr₂✝
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
o✝ : Component.type α cpt
h₂ : rtr₂{cpt}{i} = some o✝
⊢ nested h₁ s₁ ∼ final h₂
Tactic:
injection (nested h₁ s₁).unique (final h₂ |>.fromEquiv $ Reactor.Equivalent.symm e)
Proof state after:
no goals
Theorem: Reactor.StrictMember.rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
i : ID
e : rtr₁ ≈ rtr₂
s₁ : StrictMember Component.rtr i rtr₁
s₂ : StrictMember Component.rtr i rtr₂
⊢ object s₁ ≈ object s₂
Tactic:
induction s₁ generalizing rtr₂ <;> cases s₂
Proof state after:
case final.final
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr✝ : α
o✝¹ : Component.type α Component.rtr
a✝¹ : rtr✝{Component.rtr}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α Component.rtr
a✝ : rtr₂{Component.rtr}{i} = some o✝
⊢ object (final a✝¹) ≈ object (final a✝)

case final.nested
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr✝ : α
o✝ : Component.type α Component.rtr
a✝² : rtr✝{Component.rtr}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i rtr₂✝
a✝ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ object (final a✝²) ≈ object (nested a✝ a✝¹)

case nested.final
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝¹ : StrictMember Component.rtr i rtr₂✝
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object a✝¹ ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
o✝ : Component.type α Component.rtr
a✝ : rtr₂{Component.rtr}{i} = some o✝
⊢ object (nested a✝² a✝¹) ≈ object (final a✝)

case nested.nested
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i rtr₂✝¹
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object a✝² ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i rtr₂✝
a✝ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ object (nested a✝³ a✝²) ≈ object (nested a✝ a✝¹)
Theorem: Reactor.StrictMember.rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr✝ : α
o✝¹ : Component.type α Component.rtr
h₁ : rtr✝{Component.rtr}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α Component.rtr
h₂ : rtr₂{Component.rtr}{i} = some o✝
⊢ object (final h₁) ≈ object (final h₂)
Tactic:
case final.final h₁ _ h₂ => exact Equivalent.get?_rtr_some_equiv e h₁ h₂
Proof state after:
no goals
Theorem: Reactor.StrictMember.rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rtr i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object s₁ ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rtr i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ object (nested h₁ s₁) ≈ object (nested h₂ s₂)
Tactic:
case nested.nested j₁ _ h₁ s₁ hi j₂ _ s₂ h₂ =>
  suffices hj : j₁ = j₂ by subst hj; exact hi (Equivalent.get?_rtr_some_equiv e h₁ h₂) _
  have hs := (nested h₁ s₁ |>.fromEquiv e).unique (nested h₂ s₂)
  simp [fromEquiv] at hs
  exact hs.left
Proof state after:
no goals
Theorem: Reactor.StrictMember.rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr✝ : α
o✝ : Component.type α Component.rtr
h₁ : rtr✝{Component.rtr}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rtr i rtr₂✝
h₂ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ object (final h₁) ≈ object (nested h₂ s₂)
Tactic:
case final.nested h₁ _ _ s₂ h₂ => 
  injection (final h₁ |>.fromEquiv e).unique (nested h₂ s₂)
Proof state after:
no goals
Theorem: Reactor.StrictMember.rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
s₁ : StrictMember Component.rtr i rtr₂✝
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object s₁ ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
o✝ : Component.type α Component.rtr
h₂ : rtr₂{Component.rtr}{i} = some o✝
⊢ object (nested h₁ s₁) ≈ object (final h₂)
Tactic:
case nested.final h₁ s₁ _ _ h₂ =>
  injection (nested h₁ s₁).unique (final h₂ |>.fromEquiv $ Reactor.Equivalent.symm e)
Proof state after:
no goals
Theorem: Reactor.StrictMember.rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr✝ : α
o✝¹ : Component.type α Component.rtr
h₁ : rtr✝{Component.rtr}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α Component.rtr
h₂ : rtr₂{Component.rtr}{i} = some o✝
⊢ object (final h₁) ≈ object (final h₂)
Tactic:
exact Equivalent.get?_rtr_some_equiv e h₁ h₂
Proof state after:
no goals
Theorem: Reactor.StrictMember.rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rtr i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object s₁ ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rtr i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ object (nested h₁ s₁) ≈ object (nested h₂ s₂)
Tactic:
suffices hj : j₁ = j₂ by subst hj; exact hi (Equivalent.get?_rtr_some_equiv e h₁ h₂) _
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rtr i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object s₁ ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rtr i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ j₁ = j₂
Theorem: Reactor.StrictMember.rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rtr i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object s₁ ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rtr i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ j₁ = j₂
Tactic:
have hs := (nested h₁ s₁ |>.fromEquiv e).unique (nested h₂ s₂)
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rtr i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object s₁ ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rtr i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : fromEquiv e (nested h₁ s₁) = nested h₂ s₂
⊢ j₁ = j₂
Theorem: Reactor.StrictMember.rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rtr i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object s₁ ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rtr i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : fromEquiv e (nested h₁ s₁) = nested h₂ s₂
⊢ j₁ = j₂
Tactic:
simp [fromEquiv] at hs
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rtr i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object s₁ ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rtr i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : j₁ = j₂ ∧ Exists.choose ⋯ = rtr₂✝ ∧ HEq (fromEquiv ⋯ s₁) s₂
⊢ j₁ = j₂
Theorem: Reactor.StrictMember.rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rtr i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object s₁ ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rtr i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : j₁ = j₂ ∧ Exists.choose ⋯ = rtr₂✝ ∧ HEq (fromEquiv ⋯ s₁) s₂
⊢ j₁ = j₂
Tactic:
exact hs.left
Proof state after:
no goals
Theorem: Reactor.StrictMember.rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rtr i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object s₁ ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rtr i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hj : j₁ = j₂
⊢ object (nested h₁ s₁) ≈ object (nested h₂ s₂)
Tactic:
subst hj
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rtr i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object s₁ ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rtr i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
⊢ object (nested h₁ s₁) ≈ object (nested h₂ s₂)
Theorem: Reactor.StrictMember.rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rtr i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object s₁ ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rtr i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
⊢ object (nested h₁ s₁) ≈ object (nested h₂ s₂)
Tactic:
exact hi (Equivalent.get?_rtr_some_equiv e h₁ h₂) _
Proof state after:
no goals
Theorem: Reactor.StrictMember.rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr✝ : α
o✝ : Component.type α Component.rtr
h₁ : rtr✝{Component.rtr}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rtr i rtr₂✝
h₂ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ object (final h₁) ≈ object (nested h₂ s₂)
Tactic:
injection (final h₁ |>.fromEquiv e).unique (nested h₂ s₂)
Proof state after:
no goals
Theorem: Reactor.StrictMember.rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
s₁ : StrictMember Component.rtr i rtr₂✝
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rtr i rtr₂), object s₁ ≈ object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
o✝ : Component.type α Component.rtr
h₂ : rtr₂{Component.rtr}{i} = some o✝
⊢ object (nested h₁ s₁) ≈ object (final h₂)
Tactic:
injection (nested h₁ s₁).unique (final h₂ |>.fromEquiv $ Reactor.Equivalent.symm e)
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
i : ID
e : rtr₁ ≈ rtr₂
s₁ : StrictMember Component.rcn i rtr₁
s₂ : StrictMember Component.rcn i rtr₂
⊢ object s₁ = object s₂
Tactic:
induction s₁ generalizing rtr₂ <;> cases s₂
Proof state after:
case final.final
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr✝ : α
o✝¹ : Component.type α Component.rcn
a✝¹ : rtr✝{Component.rcn}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α Component.rcn
a✝ : rtr₂{Component.rcn}{i} = some o✝
⊢ object (final a✝¹) = object (final a✝)

case final.nested
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr✝ : α
o✝ : Component.type α Component.rcn
a✝² : rtr✝{Component.rcn}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rcn i rtr₂✝
a✝ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ object (final a✝²) = object (nested a✝ a✝¹)

case nested.final
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝¹ : StrictMember Component.rcn i rtr₂✝
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object a✝¹ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
o✝ : Component.type α Component.rcn
a✝ : rtr₂{Component.rcn}{i} = some o✝
⊢ object (nested a✝² a✝¹) = object (final a✝)

case nested.nested
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rcn i rtr₂✝¹
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object a✝² = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rcn i rtr₂✝
a✝ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ object (nested a✝³ a✝²) = object (nested a✝ a✝¹)
Theorem: Reactor.StrictMember.equiv_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr✝ : α
o✝¹ : Component.type α Component.rcn
h₁ : rtr✝{Component.rcn}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α Component.rcn
h₂ : rtr₂{Component.rcn}{i} = some o✝
⊢ object (final h₁) = object (final h₂)
Tactic:
case final.final h₁ _ h₂ => exact Equivalent.get?_rcn_some_eq e h₁ h₂
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ object (nested h₁ s₁) = object (nested h₂ s₂)
Tactic:
case nested.nested j₁ _ h₁ s₁ hi j₂ _ s₂ h₂ => 
  suffices hj : j₁ = j₂ by subst hj; exact hi (Equivalent.get?_rtr_some_equiv e h₁ h₂) _ 
  have hs := (nested h₁ s₁ |>.fromEquiv e).unique (nested h₂ s₂)
  simp [fromEquiv] at hs
  exact hs.left
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr✝ : α
o✝ : Component.type α Component.rcn
h₁ : rtr✝{Component.rcn}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ object (final h₁) = object (nested h₂ s₂)
Tactic:
case final.nested h₁ _ _ s₂ h₂ =>
  injection (final h₁ |>.fromEquiv e).unique (nested h₂ s₂)
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
s₁ : StrictMember Component.rcn i rtr₂✝
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
o✝ : Component.type α Component.rcn
h₂ : rtr₂{Component.rcn}{i} = some o✝
⊢ object (nested h₁ s₁) = object (final h₂)
Tactic:
case nested.final h₁ s₁ _ _ h₂ =>
  injection (nested h₁ s₁).unique (final h₂ |>.fromEquiv $ Reactor.Equivalent.symm e)
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr✝ : α
o✝¹ : Component.type α Component.rcn
h₁ : rtr✝{Component.rcn}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α Component.rcn
h₂ : rtr₂{Component.rcn}{i} = some o✝
⊢ object (final h₁) = object (final h₂)
Tactic:
exact Equivalent.get?_rcn_some_eq e h₁ h₂
Proof state after:
no goals