Theorem: Reactor.Equivalent.obj?_none_iff (ReactorModel/Objects/Reactor/Theorems/Hierarchical.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ rtr₁[cpt][i] = none ↔ rtr₂[cpt][i] = none
Tactic:
simp [←Object.not_iff_obj?_none]
State after:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o) ↔ ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o) ↔ ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o
Tactic:
constructor
State after:
case mp
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o) → ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o

case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o) → ∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o

State before:
case mp
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o) → ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o

case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o) → ∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o
Tactic:
all_goals
  intro h o ⟨m⟩
  refine h _ ⟨m.fromEquiv ?_⟩
State after:
case mp
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₂
⊢ rtr₂ ≈ rtr₁

case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₁
⊢ rtr₁ ≈ rtr₂

State before:
case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o) → ∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o
Tactic:
intro h o ⟨m⟩
State after:
case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₁
⊢ False

State before:
case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₁
⊢ False
Tactic:
refine h _ ⟨m.fromEquiv ?_⟩
State after:
case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₁
⊢ rtr₁ ≈ rtr₂

State before:
case mp
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₂
⊢ rtr₂ ≈ rtr₁
Tactic:
exact Equivalent.symm e
State after:
no goals

State before:
case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₁
⊢ rtr₁ ≈ rtr₂
Tactic:
exact e
State after:
no goals