Theorem: oneSidedRule_preserves_other_side_L (Bml/Tableau.lean)

State before:
L R : Finset Formula
C : List TNode
fst✝ : Finset Formula
a✝ : List (Finset Formula)
rule : LocalRule (fst✝, ∅) (List.map (fun res => (res, ∅)) a✝)
hC : C = applyLocalRule rule (L, R)
preproof : fst✝ ⊆ L ∧ ∅ ⊆ R
orule : OneSidedLocalRule fst✝ a✝
ruleApp : LocalRuleApp (L, R) C
hmyrule : ruleApp = LocalRuleApp.mk (List.map (fun res => (res, ∅)) a✝) fst✝ ∅ rule preproof
rule_is_left : rule = LocalRule.oneSidedL orule
⊢ ∀ c ∈ C, c.2 = R
Tactic:
aesop
State after:
no goals