Theorem: endNodeIsEndNodeOfChild (Pdl/Soundness.lean)

State before:
E X : TNode
a✝ : List TNode
subTabs : (Y : TNode) → Y ∈ a✝ → LocalTableau Y
lrA : LocalRuleApp X a✝
E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
⊢ ∃ Y, ∃ (h : Y ∈ a✝), E ∈ endNodesOf (subTabs Y h)
Tactic:
have := endNode_to_endNodeOfChildNonComp lrA E_in
State after:
E X : TNode
a✝ : List TNode
subTabs : (Y : TNode) → Y ∈ a✝ → LocalTableau Y
lrA : LocalRuleApp X a✝
E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
this : { x // ∃ (h : x ∈ a✝), E ∈ endNodesOf (subTabs x h) }
⊢ ∃ Y, ∃ (h : Y ∈ a✝), E ∈ endNodesOf (subTabs Y h)

State before:
E X : TNode
a✝ : List TNode
subTabs : (Y : TNode) → Y ∈ a✝ → LocalTableau Y
lrA : LocalRuleApp X a✝
E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
this : { x // ∃ (h : x ∈ a✝), E ∈ endNodesOf (subTabs x h) }
⊢ ∃ Y, ∃ (h : Y ∈ a✝), E ∈ endNodesOf (subTabs Y h)
Tactic:
use this
State after:
case h
E X : TNode
a✝ : List TNode
subTabs : (Y : TNode) → Y ∈ a✝ → LocalTableau Y
lrA : LocalRuleApp X a✝
E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
this : { x // ∃ (h : x ∈ a✝), E ∈ endNodesOf (subTabs x h) }
⊢ ∃ (h : ↑this ∈ a✝), E ∈ endNodesOf (subTabs (↑this) h)

State before:
case h
E X : TNode
a✝ : List TNode
subTabs : (Y : TNode) → Y ∈ a✝ → LocalTableau Y
lrA : LocalRuleApp X a✝
E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
this : { x // ∃ (h : x ∈ a✝), E ∈ endNodesOf (subTabs x h) }
⊢ ∃ (h : ↑this ∈ a✝), E ∈ endNodesOf (subTabs (↑this) h)
Tactic:
aesop
State after:
no goals