Theorem: endNodesOfLEQ (Bml/Tableau.lean)

State before:
LR Z : TNode
ltLR : LocalTableau LR
⊢ Z ∈ endNodesOf ⟨LR, ltLR⟩ → lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
cases ltLR
State after:
case fromRule
LR Z : TNode
C✝ : List TNode
subTabs✝ : (c : TNode) → c ∈ C✝ → LocalTableau c
ruleA✝ : LocalRuleApp LR C✝
⊢ Z ∈ endNodesOf ⟨LR, fromRule ruleA✝ subTabs✝⟩ → lengthOfTNode Z ≤ lengthOfTNode LR

case fromSimple
LR Z : TNode
isSimple✝ : Simple LR
⊢ Z ∈ endNodesOf ⟨LR, fromSimple isSimple✝⟩ → lengthOfTNode Z ≤ lengthOfTNode LR

State before:
LR Z : TNode
LR_simp : Simple LR
⊢ Z ∈ endNodesOf ⟨LR, fromSimple LR_simp⟩ → lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
case fromSimple LR_simp => intro Z_endOf_Y; aesop
State after:
no goals

State before:
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
⊢ Z ∈ endNodesOf ⟨LR, fromRule lrApp subTabs⟩ → lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
intro Z_endOf_LR
State after:
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
Z_endOf_LR : Z ∈ endNodesOf ⟨LR, fromRule lrApp subTabs⟩
⊢ lengthOfTNode Z ≤ lengthOfTNode LR

State before:
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
Z_endOf_LR : Z ∈ endNodesOf ⟨LR, fromRule lrApp subTabs⟩
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
simp at Z_endOf_LR
State after:
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
Z_endOf_LR : ∃ l, (∃ a, ∃ (h : a ∈ altLR), endNodesOf ⟨a, subTabs a ⋯⟩ = l) ∧ Z ∈ l
⊢ lengthOfTNode Z ≤ lengthOfTNode LR

State before:
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
Z_endOf_LR : ∃ l, (∃ a, ∃ (h : a ∈ altLR), endNodesOf ⟨a, subTabs a ⋯⟩ = l) ∧ Z ∈ l
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
rcases Z_endOf_LR with ⟨ZS, ⟨c, c_in_C, endNodes_c_eq_ZS⟩, Z_in_ZS⟩
State after:
case intro.intro.intro.intro
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
ZS : List TNode
Z_in_ZS : Z ∈ ZS
c : TNode
c_in_C : c ∈ altLR
endNodes_c_eq_ZS : endNodesOf ⟨c, subTabs c ⋯⟩ = ZS
⊢ lengthOfTNode Z ≤ lengthOfTNode LR

State before:
case intro.intro.intro.intro
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
ZS : List TNode
Z_in_ZS : Z ∈ ZS
c : TNode
c_in_C : c ∈ altLR
endNodes_c_eq_ZS : endNodesOf ⟨c, subTabs c ⋯⟩ = ZS
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
subst endNodes_c_eq_ZS
State after:
case intro.intro.intro.intro
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
c : TNode
c_in_C : c ∈ altLR
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
⊢ lengthOfTNode Z ≤ lengthOfTNode LR

State before:
case intro.intro.intro.intro
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
c : TNode
c_in_C : c ∈ altLR
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
apply le_of_lt
State after:
case intro.intro.intro.intro.a
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
c : TNode
c_in_C : c ∈ altLR
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
⊢ lengthOfTNode Z < lengthOfTNode LR

State before:
case intro.intro.intro.intro.a
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
c : TNode
c_in_C : c ∈ altLR
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
⊢ lengthOfTNode Z < lengthOfTNode LR
Tactic:
have := localRuleAppDecreasesLength lrApp c c_in_C
State after:
case intro.intro.intro.intro.a
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
c : TNode
c_in_C : c ∈ altLR
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
this : lengthOfTNode c < lengthOfTNode (LR.1, LR.2)
⊢ lengthOfTNode Z < lengthOfTNode LR

State before:
case intro.intro.intro.intro.a
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
c : TNode
c_in_C : c ∈ altLR
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
this : lengthOfTNode c < lengthOfTNode (LR.1, LR.2)
⊢ lengthOfTNode Z < lengthOfTNode LR
Tactic:
calc
  lengthOfTNode Z ≤ lengthOfTNode c := endNodesOfLEQ Z_in_ZS
  _ < lengthOfTNode LR := this
State after:
no goals

State before:
LR Z : TNode
LR_simp : Simple LR
⊢ Z ∈ endNodesOf ⟨LR, fromSimple LR_simp⟩ → lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
intro Z_endOf_Y
State after:
LR Z : TNode
LR_simp : Simple LR
Z_endOf_Y : Z ∈ endNodesOf ⟨LR, fromSimple LR_simp⟩
⊢ lengthOfTNode Z ≤ lengthOfTNode LR

State before:
LR Z : TNode
LR_simp : Simple LR
Z_endOf_Y : Z ∈ endNodesOf ⟨LR, fromSimple LR_simp⟩
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
aesop
State after:
no goals