Theorem: localRuleApp_does_not_increase_vocab (Bml/Tableau.lean)

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
⊢ ∀ cLR ∈ C, jvoc cLR ⊆ jvoc (L, R)
Tactic:
intro c cinC ℓ ℓ_in_c
State after:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : ℓ ∈ jvoc c
⊢ ℓ ∈ jvoc (L, R)

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : ℓ ∈ jvoc c
⊢ ℓ ∈ jvoc (L, R)
Tactic:
simp at ℓ_in_c
State after:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ jvoc (L, R)

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ jvoc (L, R)
Tactic:
simp
State after:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
⊢ (∃ a ∈ L, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ R, ℓ ∈ vocabOfFormula a

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
⊢ (∃ a ∈ L, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ R, ℓ ∈ vocabOfFormula a
Tactic:
constructor
State after:
case left
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a

case right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a

State before:
case left
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a
Tactic:
have ⟨Lφ,Lφ_in_cL, ℓ_in_Lφ⟩ := ℓ_in_c.left
State after:
case left
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a

State before:
case left
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a
Tactic:
apply Or.elim (em (Lφ ∈ L))
State after:
case left.left
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
⊢ Lφ ∈ L → ∃ a ∈ L, ℓ ∈ vocabOfFormula a

case left.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
⊢ Lφ ∉ L → ∃ a ∈ L, ℓ ∈ vocabOfFormula a

State before:
case left.left
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
⊢ Lφ ∈ L → ∃ a ∈ L, ℓ ∈ vocabOfFormula a
Tactic:
intro Lφ_in_L
State after:
case left.left
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
Lφ_in_L : Lφ ∈ L
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a

State before:
case left.left
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
Lφ_in_L : Lφ ∈ L
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a
Tactic:
use Lφ
State after:
no goals

State before:
case left.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
⊢ Lφ ∉ L → ∃ a ∈ L, ℓ ∈ vocabOfFormula a
Tactic:
intro not_Lφ_in_L
State after:
case left.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a

State before:
case left.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a
Tactic:
have Lφ_in_res : ∃res ∈ ress, Lφ ∈ res.1 := by aesop
State after:
case left.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a

State before:
case left.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a
Tactic:
let ⟨res, res_in_ress, Lφ_in_res_L⟩ := Lφ_in_res
State after:
case left.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a

State before:
case left.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a
Tactic:
have ℓ_in_ψ_in_Lcond : ∃ψ ∈ Lcond, ℓ ∈ voc ψ := by
  let voc_res_ss_Lcond := localRule_does_not_increase_vocab_L rule res res_in_ress
  simp at voc_res_ss_Lcond
  let ℓ_in_voc_Lcond := voc_res_ss_Lcond Lφ Lφ_in_res_L ℓ_in_Lφ
  simp at ℓ_in_voc_Lcond
  exact ℓ_in_voc_Lcond
State after:
case left.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
ℓ_in_ψ_in_Lcond : ∃ ψ ∈ Lcond, ℓ ∈ voc ψ
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a

State before:
case left.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
ℓ_in_ψ_in_Lcond : ∃ ψ ∈ Lcond, ℓ ∈ voc ψ
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a
Tactic:
let ⟨ψ, ψ_in_Lcond, ℓ_in_ψ⟩ := ℓ_in_ψ_in_Lcond
State after:
case left.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
ℓ_in_ψ_in_Lcond : ∃ ψ ∈ Lcond, ℓ ∈ voc ψ
ψ : Formula
ψ_in_Lcond : ψ ∈ Lcond
ℓ_in_ψ : ℓ ∈ voc ψ
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a

State before:
case left.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
ℓ_in_ψ_in_Lcond : ∃ ψ ∈ Lcond, ℓ ∈ voc ψ
ψ : Formula
ψ_in_Lcond : ψ ∈ Lcond
ℓ_in_ψ : ℓ ∈ voc ψ
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a
Tactic:
use ψ, (by aesop), ℓ_in_ψ
State after:
no goals

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
⊢ ∃ res ∈ ress, Lφ ∈ res.1
Tactic:
aesop
State after:
no goals

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
⊢ ∃ ψ ∈ Lcond, ℓ ∈ voc ψ
Tactic:
let voc_res_ss_Lcond := localRule_does_not_increase_vocab_L rule res res_in_ress
State after:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
voc_res_ss_Lcond : voc res.1 ⊆ voc Lcond := localRule_does_not_increase_vocab_L rule res res_in_ress
⊢ ∃ ψ ∈ Lcond, ℓ ∈ voc ψ

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
voc_res_ss_Lcond : voc res.1 ⊆ voc Lcond := localRule_does_not_increase_vocab_L rule res res_in_ress
⊢ ∃ ψ ∈ Lcond, ℓ ∈ voc ψ
Tactic:
simp at voc_res_ss_Lcond
State after:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
voc_res_ss_Lcond : ∀ x ∈ res.1, vocabOfFormula x ⊆ Lcond.biUnion vocabOfFormula
⊢ ∃ ψ ∈ Lcond, ℓ ∈ voc ψ

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
voc_res_ss_Lcond : ∀ x ∈ res.1, vocabOfFormula x ⊆ Lcond.biUnion vocabOfFormula
⊢ ∃ ψ ∈ Lcond, ℓ ∈ voc ψ
Tactic:
let ℓ_in_voc_Lcond := voc_res_ss_Lcond Lφ Lφ_in_res_L ℓ_in_Lφ
State after:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
voc_res_ss_Lcond : ∀ x ∈ res.1, vocabOfFormula x ⊆ Lcond.biUnion vocabOfFormula
ℓ_in_voc_Lcond : ℓ ∈ Lcond.biUnion vocabOfFormula := voc_res_ss_Lcond Lφ Lφ_in_res_L ℓ_in_Lφ
⊢ ∃ ψ ∈ Lcond, ℓ ∈ voc ψ

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
voc_res_ss_Lcond : ∀ x ∈ res.1, vocabOfFormula x ⊆ Lcond.biUnion vocabOfFormula
ℓ_in_voc_Lcond : ℓ ∈ Lcond.biUnion vocabOfFormula := voc_res_ss_Lcond Lφ Lφ_in_res_L ℓ_in_Lφ
⊢ ∃ ψ ∈ Lcond, ℓ ∈ voc ψ
Tactic:
simp at ℓ_in_voc_Lcond
State after:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
voc_res_ss_Lcond : ∀ x ∈ res.1, vocabOfFormula x ⊆ Lcond.biUnion vocabOfFormula
ℓ_in_voc_Lcond : ∃ a ∈ Lcond, ℓ ∈ vocabOfFormula a
⊢ ∃ ψ ∈ Lcond, ℓ ∈ voc ψ

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
voc_res_ss_Lcond : ∀ x ∈ res.1, vocabOfFormula x ⊆ Lcond.biUnion vocabOfFormula
ℓ_in_voc_Lcond : ∃ a ∈ Lcond, ℓ ∈ vocabOfFormula a
⊢ ∃ ψ ∈ Lcond, ℓ ∈ voc ψ
Tactic:
exact ℓ_in_voc_Lcond
State after:
no goals

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Lφ : Formula
Lφ_in_cL : Lφ ∈ c.1
ℓ_in_Lφ : ℓ ∈ vocabOfFormula Lφ
not_Lφ_in_L : Lφ ∉ L
Lφ_in_res : ∃ res ∈ ress, Lφ ∈ res.1
res : SubPair
res_in_ress : res ∈ ress
Lφ_in_res_L : Lφ ∈ res.1
ℓ_in_ψ_in_Lcond : ∃ ψ ∈ Lcond, ℓ ∈ voc ψ
ψ : Formula
ψ_in_Lcond : ψ ∈ Lcond
ℓ_in_ψ : ℓ ∈ voc ψ
⊢ ψ ∈ L
Tactic:
aesop
State after:
no goals

State before:
case right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a
Tactic:
have ⟨Rφ,Rφ_in_cR, ℓ_in_Rφ⟩ := ℓ_in_c.right
State after:
case right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a

State before:
case right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a
Tactic:
apply Or.elim (em (Rφ ∈ R))
State after:
case right.left
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
⊢ Rφ ∈ R → ∃ a ∈ R, ℓ ∈ vocabOfFormula a

case right.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
⊢ Rφ ∉ R → ∃ a ∈ R, ℓ ∈ vocabOfFormula a

State before:
case right.left
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
⊢ Rφ ∈ R → ∃ a ∈ R, ℓ ∈ vocabOfFormula a
Tactic:
intro Rφ_in_R
State after:
case right.left
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
Rφ_in_R : Rφ ∈ R
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a

State before:
case right.left
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
Rφ_in_R : Rφ ∈ R
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a
Tactic:
use Rφ
State after:
no goals

State before:
case right.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
⊢ Rφ ∉ R → ∃ a ∈ R, ℓ ∈ vocabOfFormula a
Tactic:
intro not_Rφ_in_R
State after:
case right.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a

State before:
case right.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a
Tactic:
have Rφ_in_res : ∃res ∈ ress, Rφ ∈ res.2 := by aesop
State after:
case right.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a

State before:
case right.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a
Tactic:
let ⟨res, res_in_ress, Rφ_in_res_R⟩ := Rφ_in_res
State after:
case right.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a

State before:
case right.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a
Tactic:
have ℓ_in_ψ_in_Rcond : ∃ψ ∈ Rcond, ℓ ∈ voc ψ := by
  let voc_res_ss_Rcond := localRule_does_not_increase_vocab_R rule res res_in_ress
  simp at voc_res_ss_Rcond
  let ℓ_in_voc_Rcond := voc_res_ss_Rcond Rφ Rφ_in_res_R ℓ_in_Rφ
  simp at ℓ_in_voc_Rcond
  exact ℓ_in_voc_Rcond
State after:
case right.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
ℓ_in_ψ_in_Rcond : ∃ ψ ∈ Rcond, ℓ ∈ voc ψ
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a

State before:
case right.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
ℓ_in_ψ_in_Rcond : ∃ ψ ∈ Rcond, ℓ ∈ voc ψ
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a
Tactic:
let ⟨ψ, ψ_in_Rcond, ℓ_in_ψ⟩ := ℓ_in_ψ_in_Rcond
State after:
case right.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
ℓ_in_ψ_in_Rcond : ∃ ψ ∈ Rcond, ℓ ∈ voc ψ
ψ : Formula
ψ_in_Rcond : ψ ∈ Rcond
ℓ_in_ψ : ℓ ∈ voc ψ
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a

State before:
case right.right
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
ℓ_in_ψ_in_Rcond : ∃ ψ ∈ Rcond, ℓ ∈ voc ψ
ψ : Formula
ψ_in_Rcond : ψ ∈ Rcond
ℓ_in_ψ : ℓ ∈ voc ψ
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a
Tactic:
use ψ, (by aesop), ℓ_in_ψ
State after:
no goals

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
⊢ ∃ res ∈ ress, Rφ ∈ res.2
Tactic:
aesop
State after:
no goals

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
⊢ ∃ ψ ∈ Rcond, ℓ ∈ voc ψ
Tactic:
let voc_res_ss_Rcond := localRule_does_not_increase_vocab_R rule res res_in_ress
State after:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
voc_res_ss_Rcond : voc res.2 ⊆ voc Rcond := localRule_does_not_increase_vocab_R rule res res_in_ress
⊢ ∃ ψ ∈ Rcond, ℓ ∈ voc ψ

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
voc_res_ss_Rcond : voc res.2 ⊆ voc Rcond := localRule_does_not_increase_vocab_R rule res res_in_ress
⊢ ∃ ψ ∈ Rcond, ℓ ∈ voc ψ
Tactic:
simp at voc_res_ss_Rcond
State after:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
voc_res_ss_Rcond : ∀ x ∈ res.2, vocabOfFormula x ⊆ Rcond.biUnion vocabOfFormula
⊢ ∃ ψ ∈ Rcond, ℓ ∈ voc ψ

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
voc_res_ss_Rcond : ∀ x ∈ res.2, vocabOfFormula x ⊆ Rcond.biUnion vocabOfFormula
⊢ ∃ ψ ∈ Rcond, ℓ ∈ voc ψ
Tactic:
let ℓ_in_voc_Rcond := voc_res_ss_Rcond Rφ Rφ_in_res_R ℓ_in_Rφ
State after:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
voc_res_ss_Rcond : ∀ x ∈ res.2, vocabOfFormula x ⊆ Rcond.biUnion vocabOfFormula
ℓ_in_voc_Rcond : ℓ ∈ Rcond.biUnion vocabOfFormula := voc_res_ss_Rcond Rφ Rφ_in_res_R ℓ_in_Rφ
⊢ ∃ ψ ∈ Rcond, ℓ ∈ voc ψ

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
voc_res_ss_Rcond : ∀ x ∈ res.2, vocabOfFormula x ⊆ Rcond.biUnion vocabOfFormula
ℓ_in_voc_Rcond : ℓ ∈ Rcond.biUnion vocabOfFormula := voc_res_ss_Rcond Rφ Rφ_in_res_R ℓ_in_Rφ
⊢ ∃ ψ ∈ Rcond, ℓ ∈ voc ψ
Tactic:
simp at ℓ_in_voc_Rcond
State after:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
voc_res_ss_Rcond : ∀ x ∈ res.2, vocabOfFormula x ⊆ Rcond.biUnion vocabOfFormula
ℓ_in_voc_Rcond : ∃ a ∈ Rcond, ℓ ∈ vocabOfFormula a
⊢ ∃ ψ ∈ Rcond, ℓ ∈ voc ψ

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
voc_res_ss_Rcond : ∀ x ∈ res.2, vocabOfFormula x ⊆ Rcond.biUnion vocabOfFormula
ℓ_in_voc_Rcond : ∃ a ∈ Rcond, ℓ ∈ vocabOfFormula a
⊢ ∃ ψ ∈ Rcond, ℓ ∈ voc ψ
Tactic:
exact ℓ_in_voc_Rcond
State after:
no goals

State before:
C : List TNode
L R : Finset Formula
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC : C = applyLocalRule rule (L, R)
preproof : Lcond ⊆ L ∧ Rcond ⊆ R
c : TNode
cinC : c ∈ C
ℓ : Char
ℓ_in_c : (∃ a ∈ c.1, ℓ ∈ vocabOfFormula a) ∧ ∃ a ∈ c.2, ℓ ∈ vocabOfFormula a
Rφ : Formula
Rφ_in_cR : Rφ ∈ c.2
ℓ_in_Rφ : ℓ ∈ vocabOfFormula Rφ
not_Rφ_in_R : Rφ ∉ R
Rφ_in_res : ∃ res ∈ ress, Rφ ∈ res.2
res : SubPair
res_in_ress : res ∈ ress
Rφ_in_res_R : Rφ ∈ res.2
ℓ_in_ψ_in_Rcond : ∃ ψ ∈ Rcond, ℓ ∈ voc ψ
ψ : Formula
ψ_in_Rcond : ψ ∈ Rcond
ℓ_in_ψ : ℓ ∈ voc ψ
⊢ ψ ∈ R
Tactic:
aesop
State after:
no goals