internlm/Lean-Github huggingface dataset:
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (L, R).1
Tactic:
apply Or.elim ℓ_left
Proof state after:
case a.left
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ vocabOfFormula φ → ℓ ∈ voc (L, R).1

case a.right
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ (∃ a ∈ projection L, ℓ ∈ vocabOfFormula a) → ℓ ∈ voc (L, R).1
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a.left
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ vocabOfFormula φ → ℓ ∈ voc (L, R).1
Tactic:
intro ℓ_in_φ
Proof state after:
case a.left
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ voc (L, R).1
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a.left
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ voc (L, R).1
Tactic:
simp
Proof state after:
case a.left
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a.left
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ∃ a ∈ L, ℓ ∈ vocabOfFormula a
Tactic:
use ~(□φ)
Proof state after:
case h
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ~(□φ) ∈ L ∧ ℓ ∈ vocabOfFormula (~(□φ))
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case h
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ~(□φ) ∈ L ∧ ℓ ∈ vocabOfFormula (~(□φ))
Tactic:
constructor
Proof state after:
case h.left
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ~(□φ) ∈ L

case h.right
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ vocabOfFormula (~(□φ))
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case h.left
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ~(□φ) ∈ L

case h.right
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ vocabOfFormula (~(□φ))
Tactic:
exact valid_proj
Proof state after:
case h.right
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ vocabOfFormula (~(□φ))
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case h.right
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ vocabOfFormula (~(□φ))
Tactic:
aesop
Proof state after:
no goals
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a.right
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ (∃ a ∈ projection L, ℓ ∈ vocabOfFormula a) → ℓ ∈ voc (L, R).1
Tactic:
intro ⟨ψ, ψ_in_proj, ℓ_in_ψ⟩
Proof state after:
case a.right
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection L
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ℓ ∈ voc (L, R).1
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a.right
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection L
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ℓ ∈ voc (L, R).1
Tactic:
apply proj_does_not_increase_vocab
Proof state after:
case a.right.a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection L
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ℓ ∈ voc (projection (L, R).1)
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a.right.a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection L
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ℓ ∈ voc (projection (L, R).1)
Tactic:
simp
Proof state after:
case a.right.a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection L
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a.right.a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_left : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection L
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
Tactic:
use ψ
Proof state after:
no goals
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).2
Tactic:
have ℓ_right := (Finset.mem_inter.mp ℓ_in_proj).right
Proof state after:
case a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_right : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).2
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_right : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).2
Tactic:
simp [diamondProjectTNode ] at ℓ_right
Proof state after:
case a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_right : ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (L, R).2
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_right : ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (L, R).2
Tactic:
apply proj_does_not_increase_vocab
Proof state after:
case a.a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_right : ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (projection (L, R).2)
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a.a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_right : ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (projection (L, R).2)
Tactic:
simp
Proof state after:
case a.a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_right : ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
Theorem: diamondproj_does_not_increase_vocab_L
Proof state before:
case a.a
φ : Formula
L R : Finset Formula
valid_proj : ~(□φ) ∈ L
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inl φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inl φ) (L, R)).2
ℓ_right : ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
Tactic:
exact ℓ_right
Proof state after:
no goals
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
⊢ jvoc (diamondProjectTNode (Sum.inr φ) (L, R)) ⊆ jvoc (L, R)
Tactic:
intro ℓ ℓ_in_proj
Proof state after:
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ jvoc (diamondProjectTNode (Sum.inr φ) (L, R))
⊢ ℓ ∈ jvoc (L, R)
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ jvoc (diamondProjectTNode (Sum.inr φ) (L, R))
⊢ ℓ ∈ jvoc (L, R)
Tactic:
unfold jvoc at *
Proof state after:
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).1 ∩ voc (L, R).2
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).1 ∩ voc (L, R).2
Tactic:
apply Finset.mem_inter_of_mem
Proof state after:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).1

case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).2
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).1
Tactic:
have ℓ_left := (Finset.mem_inter.mp ℓ_in_proj).left
Proof state after:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1
⊢ ℓ ∈ voc (L, R).1
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1
⊢ ℓ ∈ voc (L, R).1
Tactic:
simp [diamondProjectTNode ] at ℓ_left
Proof state after:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (L, R).1
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (L, R).1
Tactic:
apply proj_does_not_increase_vocab
Proof state after:
case a.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (projection (L, R).1)
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (projection (L, R).1)
Tactic:
simp
Proof state after:
case a.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_left : ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
⊢ ∃ a ∈ projection L, ℓ ∈ vocabOfFormula a
Tactic:
exact ℓ_left
Proof state after:
no goals
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).2
Tactic:
have ℓ_right := (Finset.mem_inter.mp ℓ_in_proj).right
Proof state after:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).2
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
⊢ ℓ ∈ voc (L, R).2
Tactic:
simp [diamondProjectTNode ] at ℓ_right
Proof state after:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (L, R).2
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ voc (L, R).2
Tactic:
apply Or.elim ℓ_right
Proof state after:
case a.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ vocabOfFormula φ → ℓ ∈ voc (L, R).2

case a.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ (∃ a ∈ projection R, ℓ ∈ vocabOfFormula a) → ℓ ∈ voc (L, R).2
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ ℓ ∈ vocabOfFormula φ → ℓ ∈ voc (L, R).2
Tactic:
intro ℓ_in_φ
Proof state after:
case a.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ voc (L, R).2
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ voc (L, R).2
Tactic:
simp
Proof state after:
case a.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ∃ a ∈ R, ℓ ∈ vocabOfFormula a
Tactic:
use ~(□φ)
Proof state after:
case h
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ~(□φ) ∈ R ∧ ℓ ∈ vocabOfFormula (~(□φ))
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case h
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ~(□φ) ∈ R ∧ ℓ ∈ vocabOfFormula (~(□φ))
Tactic:
constructor
Proof state after:
case h.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ~(□φ) ∈ R

case h.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ vocabOfFormula (~(□φ))
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case h.left
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ~(□φ) ∈ R

case h.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ vocabOfFormula (~(□φ))
Tactic:
exact valid_proj
Proof state after:
case h.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ vocabOfFormula (~(□φ))
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case h.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ vocabOfFormula (~(□φ))
Tactic:
aesop
Proof state after:
no goals
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
⊢ (∃ a ∈ projection R, ℓ ∈ vocabOfFormula a) → ℓ ∈ voc (L, R).2
Tactic:
intro ⟨ψ, ψ_in_proj, ℓ_in_ψ⟩
Proof state after:
case a.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection R
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ℓ ∈ voc (L, R).2