Theorem: notSimpleThenLocalRule (Bml/Tableau.lean)

State before:
L R : Finset Formula
⊢ ¬Simple (L, R) → ∃ Lcond Rcond ress x, Lcond ⊆ L ∧ Rcond ⊆ R
Tactic:
intro not_simple
State after:
L R : Finset Formula
not_simple : ¬Simple (L, R)
⊢ ∃ Lcond Rcond ress x, Lcond ⊆ L ∧ Rcond ⊆ R

State before:
L R : Finset Formula
not_simple : ¬Simple (L, R)
⊢ ∃ Lcond Rcond ress x, Lcond ⊆ L ∧ Rcond ⊆ R
Tactic:
let ⟨C, ruleA⟩ := notSimpleToRuleApp not_simple
State after:
L R : Finset Formula
not_simple : ¬Simple (L, R)
C : List TNode
ruleA : LocalRuleApp (L, R) C
⊢ ∃ Lcond Rcond ress x, Lcond ⊆ L ∧ Rcond ⊆ R

State before:
L R : Finset Formula
not_simple : ¬Simple (L, R)
C : List TNode
ruleA : LocalRuleApp (L, R) C
⊢ ∃ Lcond Rcond ress x, Lcond ⊆ L ∧ Rcond ⊆ R
Tactic:
match ruleA with
| @LocalRuleApp.mk _ _ _ ress Lcond Rcond rule _ pp => exact ⟨Lcond, Rcond, ress, rule, pp⟩
State after:
no goals

State before:
L R : Finset Formula
not_simple : ¬Simple (L, R)
C : List TNode
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC✝ : C = applyLocalRule rule (L, R)
pp : Lcond ⊆ L ∧ Rcond ⊆ R
⊢ ∃ Lcond Rcond ress x, Lcond ⊆ L ∧ Rcond ⊆ R
Tactic:
exact ⟨Lcond, Rcond, ress, rule, pp⟩
State after:
no goals