internlm/Lean-Github huggingface dataset:
Theorem: truthLemma
Proof state before:
case h.left
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
notBoxP_in_X : ~(□P) ∈ ↑X
Y : { x // x ∈ Worlds }
X_rel_Y : M.Rel X Y
notP_in_Y : ~P ∈ ↑Y
⊢ M.Rel X Y

case h.right
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
notBoxP_in_X : ~(□P) ∈ ↑X
Y : { x // x ∈ Worlds }
X_rel_Y : M.Rel X Y
notP_in_Y : ~P ∈ ↑Y
⊢ ¬Evaluate (M, Y) P
Tactic:
exact X_rel_Y
Proof state after:
case h.right
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
notBoxP_in_X : ~(□P) ∈ ↑X
Y : { x // x ∈ Worlds }
X_rel_Y : M.Rel X Y
notP_in_Y : ~P ∈ ↑Y
⊢ ¬Evaluate (M, Y) P
Theorem: truthLemma
Proof state before:
case h.right
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
notBoxP_in_X : ~(□P) ∈ ↑X
Y : { x // x ∈ Worlds }
X_rel_Y : M.Rel X Y
notP_in_Y : ~P ∈ ↑Y
⊢ ¬Evaluate (M, Y) P
Tactic:
rcases IH Y with ⟨_, minus_IH_Y, _⟩
Proof state after:
case h.right.intro.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
notBoxP_in_X : ~(□P) ∈ ↑X
Y : { x // x ∈ Worlds }
X_rel_Y : M.Rel X Y
notP_in_Y : ~P ∈ ↑Y
left✝ : plus P Y
minus_IH_Y : minus P Y
right✝ : oh P Y
⊢ ¬Evaluate (M, Y) P
Theorem: truthLemma
Proof state before:
case h.right.intro.intro
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
notBoxP_in_X : ~(□P) ∈ ↑X
Y : { x // x ∈ Worlds }
X_rel_Y : M.Rel X Y
notP_in_Y : ~P ∈ ↑Y
left✝ : plus P Y
minus_IH_Y : minus P Y
right✝ : oh P Y
⊢ ¬Evaluate (M, Y) P
Tactic:
exact minus_IH_Y notP_in_Y
Proof state after:
no goals
Theorem: truthLemma
Proof state before:
case right.right
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
⊢ oh (□P) X
Tactic:
intro boxBoxP_in_X Y X_rel_Y
Proof state after:
case right.right
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
boxBoxP_in_X : □□P ∈ ↑X
Y : { x // x ∈ Worlds }
X_rel_Y : M.Rel X Y
⊢ □P ∈ ↑Y
Theorem: truthLemma
Proof state before:
case right.right
Worlds : Set (Finset Formula)
X✝ : ↑Worlds
P✝ : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
oh : Formula → ↑Worlds → Prop := fun P X => □P ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), M.Rel X Y → P ∈ ↑Y
P : Formula
IH : ∀ (X : ↑Worlds), plus P X ∧ minus P X ∧ oh P X
X : ↑Worlds
boxBoxP_in_X : □□P ∈ ↑X
Y : { x // x ∈ Worlds }
X_rel_Y : M.Rel X Y
⊢ □P ∈ ↑Y
Tactic:
exact iii X Y (□P) X_rel_Y boxBoxP_in_X
Proof state after:
no goals
Theorem: lengthAdd
Proof state before:
X : Finset Formula
ϕ : Formula
⊢ ϕ ∉ X → lengthOf (insert ϕ X) = lengthOf X + lengthOfFormula ϕ
Tactic:
intro notin
Proof state after:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOf (insert ϕ X) = lengthOf X + lengthOfFormula ϕ
Theorem: lengthAdd
Proof state before:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOf (insert ϕ X) = lengthOf X + lengthOfFormula ϕ
Tactic:
unfold lengthOf
Proof state after:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ setFormulaHasLength.1 (insert ϕ X) = setFormulaHasLength.1 X + lengthOfFormula ϕ
Theorem: lengthAdd
Proof state before:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ setFormulaHasLength.1 (insert ϕ X) = setFormulaHasLength.1 X + lengthOfFormula ϕ
Tactic:
simp
Proof state after:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ (insert ϕ X).sum lengthOfFormula = X.sum lengthOfFormula + lengthOfFormula ϕ
Theorem: lengthAdd
Proof state before:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ (insert ϕ X).sum lengthOfFormula = X.sum lengthOfFormula + lengthOfFormula ϕ
Tactic:
rw [Finset.sum_insert notin]
Proof state after:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOfFormula ϕ + ∑ x ∈ X, lengthOfFormula x = X.sum lengthOfFormula + lengthOfFormula ϕ
Theorem: lengthAdd
Proof state before:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOfFormula ϕ + ∑ x ∈ X, lengthOfFormula x = X.sum lengthOfFormula + lengthOfFormula ϕ
Tactic:
apply Nat.add_comm
Proof state after:
no goals
Theorem: lengthOf_insert_leq_plus
Proof state before:
X : Finset Formula
ϕ : Formula
⊢ lengthOf (insert ϕ X) ≤ lengthOf X + lengthOfFormula ϕ
Tactic:
cases' em (ϕ ∈ X) with in_x not_in_x
Proof state after:
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOf (insert ϕ X) ≤ lengthOf X + lengthOfFormula ϕ

case inr
X : Finset Formula
ϕ : Formula
not_in_x : ϕ ∉ X
⊢ lengthOf (insert ϕ X) ≤ lengthOf X + lengthOfFormula ϕ
Theorem: lengthOf_insert_leq_plus
Proof state before:
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOf (insert ϕ X) ≤ lengthOf X + lengthOfFormula ϕ
Tactic:
rw [Finset.insert_eq_of_mem in_x]
Proof state after:
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOf X ≤ lengthOf X + lengthOfFormula ϕ
Theorem: lengthOf_insert_leq_plus
Proof state before:
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOf X ≤ lengthOf X + lengthOfFormula ϕ
Tactic:
simp
Proof state after:
no goals
Theorem: lengthOf_insert_leq_plus
Proof state before:
case inr
X : Finset Formula
ϕ : Formula
not_in_x : ϕ ∉ X
⊢ lengthOf (insert ϕ X) ≤ lengthOf X + lengthOfFormula ϕ
Tactic:
rw [lengthAdd not_in_x]
Proof state after:
no goals
Theorem: lengthRemove
Proof state before:
X : Finset Formula
⊢ ∀ ϕ ∈ X, lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X
Tactic:
intro ϕ in_X
Proof state after:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X
Theorem: lengthRemove
Proof state before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X
Tactic:
have claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ :=
  by
  apply lengthAdd
  simp
Proof state after:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
⊢ lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X
Theorem: lengthRemove
Proof state before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
⊢ lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X
Tactic:
have anotherClaim : insert ϕ (X \ {ϕ}) = X := by
  ext1
  simp only [Finset.mem_sdiff, Finset.mem_insert, Finset.mem_singleton]
  constructor
  aesop
  tauto
Proof state after:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
anotherClaim : insert ϕ (X \ {ϕ}) = X
⊢ lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X
Theorem: lengthRemove
Proof state before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
anotherClaim : insert ϕ (X \ {ϕ}) = X
⊢ lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X
Tactic:
rw [anotherClaim] at claim
Proof state after:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf X = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
anotherClaim : insert ϕ (X \ {ϕ}) = X
⊢ lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X
Theorem: lengthRemove
Proof state before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf X = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
anotherClaim : insert ϕ (X \ {ϕ}) = X
⊢ lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X
Tactic:
rw [sdiff_singleton_is_erase] at claim
Proof state after:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf X = lengthOf (X.erase ϕ) + lengthOfFormula ϕ
anotherClaim : insert ϕ (X \ {ϕ}) = X
⊢ lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X
Theorem: lengthRemove
Proof state before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf X = lengthOf (X.erase ϕ) + lengthOfFormula ϕ
anotherClaim : insert ϕ (X \ {ϕ}) = X
⊢ lengthOf (X.erase ϕ) + lengthOfFormula ϕ = lengthOf X
Tactic:
aesop
Proof state after:
no goals
Theorem: lengthRemove
Proof state before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
Tactic:
apply lengthAdd
Proof state after:
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ ϕ ∉ X \ {ϕ}
Theorem: lengthRemove
Proof state before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
⊢ insert ϕ (X \ {ϕ}) = X
Tactic:
ext1
Proof state after:
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ ∈ insert ϕ (X \ {ϕ}) ↔ a✝ ∈ X
Theorem: lengthRemove
Proof state before:
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ ∈ insert ϕ (X \ {ϕ}) ↔ a✝ ∈ X
Tactic:
simp only [Finset.mem_sdiff, Finset.mem_insert, Finset.mem_singleton]
Proof state after:
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ ↔ a✝ ∈ X
Theorem: lengthRemove
Proof state before:
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ ↔ a✝ ∈ X
Tactic:
constructor
Proof state after:
case a.mp
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ → a✝ ∈ X

case a.mpr
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ ∈ X → a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ
Theorem: lengthRemove
Proof state before:
case a.mp
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ → a✝ ∈ X

case a.mpr
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ ∈ X → a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ
Tactic:
aesop
Proof state after:
case a.mpr
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ ∈ X → a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ
Theorem: lengthRemove
Proof state before:
case a.mpr
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOf (insert ϕ (X \ {ϕ})) = lengthOf (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ ∈ X → a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ
Tactic:
tauto
Proof state after:
no goals
Theorem: freshVarForm_is_larger
Proof state before:
φ : Formula
⊢ ∀ n ∈ voc φ, n < freshVarForm φ
Tactic:
cases φ
Proof state after:
case bottom

⊢ ∀ n ∈ voc Formula.bottom, n < freshVarForm Formula.bottom

case atom_prop
a✝ : ℕ
⊢ ∀ n ∈ voc (·a✝), n < freshVarForm (·a✝)

case neg
a✝ : Formula
⊢ ∀ n ∈ voc (~a✝), n < freshVarForm (~a✝)

case and
a✝¹ a✝ : Formula
⊢ ∀ n ∈ voc (a✝¹⋀a✝), n < freshVarForm (a✝¹⋀a✝)

case box
a✝¹ : Program
a✝ : Formula
⊢ ∀ n ∈ voc (⌈a✝¹⌉a✝), n < freshVarForm (⌈a✝¹⌉a✝)
Theorem: freshVarForm_is_larger
Proof state before:
case bottom

⊢ ∀ n ∈ voc Formula.bottom, n < freshVarForm Formula.bottom

case atom_prop
a✝ : ℕ
⊢ ∀ n ∈ voc (·a✝), n < freshVarForm (·a✝)

case neg
a✝ : Formula
⊢ ∀ n ∈ voc (~a✝), n < freshVarForm (~a✝)

case and
a✝¹ a✝ : Formula
⊢ ∀ n ∈ voc (a✝¹⋀a✝), n < freshVarForm (a✝¹⋀a✝)

case box
a✝¹ : Program
a✝ : Formula
⊢ ∀ n ∈ voc (⌈a✝¹⌉a✝), n < freshVarForm (⌈a✝¹⌉a✝)
Tactic:
all_goals simp [freshVarForm, voc, vocabOfFormula, not_or]
Proof state after:
case neg
a✝ : Formula
⊢ ∀ n ∈ vocabOfFormula a✝, n < freshVarForm a✝

case and
a✝¹ a✝ : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula a✝¹ ∨ n ∈ vocabOfFormula a✝ → n < freshVarForm a✝¹ ∨ n < freshVarForm a✝

case box
a✝¹ : Program
a✝ : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram a✝¹ ∨ n ∈ vocabOfFormula a✝ → n < freshVarProg a✝¹ ∨ n < freshVarForm a✝
Theorem: freshVarForm_is_larger
Proof state before:
φ : Formula
⊢ ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
Tactic:
case neg φ =>
  apply freshVarForm_is_larger
Proof state after:
no goals
Theorem: freshVarForm_is_larger
Proof state before:
φ1 φ2 : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2
Tactic:
case and φ1 φ2 =>
  have IH1 := freshVarForm_is_larger φ1
  have IH2 := freshVarForm_is_larger φ2
  aesop
Proof state after:
no goals
Theorem: freshVarForm_is_larger
Proof state before:
α : Program
φ : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfFormula φ → n < freshVarProg α ∨ n < freshVarForm φ
Tactic:
case box α φ =>
  have IHφ := freshVarForm_is_larger φ
  have IHα := freshVarProg_is_larger α
  aesop
Proof state after:
no goals
Theorem: freshVarForm_is_larger
Proof state before:
case box
a✝¹ : Program
a✝ : Formula
⊢ ∀ n ∈ voc (⌈a✝¹⌉a✝), n < freshVarForm (⌈a✝¹⌉a✝)
Tactic:
simp [freshVarForm, voc, vocabOfFormula, not_or]
Proof state after:
case box
a✝¹ : Program
a✝ : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram a✝¹ ∨ n ∈ vocabOfFormula a✝ → n < freshVarProg a✝¹ ∨ n < freshVarForm a✝
Theorem: freshVarForm_is_larger
Proof state before:
φ : Formula
⊢ ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
Tactic:
apply freshVarForm_is_larger
Proof state after:
no goals
Theorem: freshVarForm_is_larger
Proof state before:
φ1 φ2 : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2
Tactic:
have IH1 := freshVarForm_is_larger φ1
Proof state after:
φ1 φ2 : Formula
IH1 : ∀ n ∈ voc φ1, n < freshVarForm φ1
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2
Theorem: freshVarForm_is_larger
Proof state before:
φ1 φ2 : Formula
IH1 : ∀ n ∈ voc φ1, n < freshVarForm φ1
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2
Tactic:
have IH2 := freshVarForm_is_larger φ2
Proof state after:
φ1 φ2 : Formula
IH1 : ∀ n ∈ voc φ1, n < freshVarForm φ1
IH2 : ∀ n ∈ voc φ2, n < freshVarForm φ2
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2
Theorem: freshVarForm_is_larger
Proof state before:
φ1 φ2 : Formula
IH1 : ∀ n ∈ voc φ1, n < freshVarForm φ1
IH2 : ∀ n ∈ voc φ2, n < freshVarForm φ2
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2
Tactic:
aesop
Proof state after:
no goals
Theorem: freshVarForm_is_larger
Proof state before:
α : Program
φ : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfFormula φ → n < freshVarProg α ∨ n < freshVarForm φ
Tactic:
have IHφ := freshVarForm_is_larger φ
Proof state after:
α : Program
φ : Formula
IHφ : ∀ n ∈ voc φ, n < freshVarForm φ
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfFormula φ → n < freshVarProg α ∨ n < freshVarForm φ
Theorem: freshVarForm_is_larger
Proof state before:
α : Program
φ : Formula
IHφ : ∀ n ∈ voc φ, n < freshVarForm φ
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfFormula φ → n < freshVarProg α ∨ n < freshVarForm φ
Tactic:
have IHα := freshVarProg_is_larger α
Proof state after:
α : Program
φ : Formula
IHφ : ∀ n ∈ voc φ, n < freshVarForm φ
IHα : ∀ n ∈ voc α, n < freshVarProg α
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfFormula φ → n < freshVarProg α ∨ n < freshVarForm φ
Theorem: freshVarForm_is_larger
Proof state before:
α : Program
φ : Formula
IHφ : ∀ n ∈ voc φ, n < freshVarForm φ
IHα : ∀ n ∈ voc α, n < freshVarProg α
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfFormula φ → n < freshVarProg α ∨ n < freshVarForm φ
Tactic:
aesop
Proof state after:
no goals
Theorem: freshVarProg_is_larger
Proof state before:
α : Program
⊢ ∀ n ∈ voc α, n < freshVarProg α
Tactic:
cases α
Proof state after:
case atom_prog
a✝ : ℕ
⊢ ∀ n ∈ voc (·a✝), n < freshVarProg (·a✝)

case sequence
a✝¹ a✝ : Program
⊢ ∀ n ∈ voc (a✝¹;'a✝), n < freshVarProg (a✝¹;'a✝)

case union
a✝¹ a✝ : Program
⊢ ∀ n ∈ voc (a✝¹⋓a✝), n < freshVarProg (a✝¹⋓a✝)

case star
a✝ : Program
⊢ ∀ n ∈ voc (∗a✝), n < freshVarProg (∗a✝)

case test
a✝ : Formula
⊢ ∀ n ∈ voc (?'a✝), n < freshVarProg (?'a✝)
Theorem: freshVarProg_is_larger
Proof state before:
case atom_prog
a✝ : ℕ
⊢ ∀ n ∈ voc (·a✝), n < freshVarProg (·a✝)

case sequence
a✝¹ a✝ : Program
⊢ ∀ n ∈ voc (a✝¹;'a✝), n < freshVarProg (a✝¹;'a✝)

case union
a✝¹ a✝ : Program
⊢ ∀ n ∈ voc (a✝¹⋓a✝), n < freshVarProg (a✝¹⋓a✝)

case star
a✝ : Program
⊢ ∀ n ∈ voc (∗a✝), n < freshVarProg (∗a✝)

case test
a✝ : Formula
⊢ ∀ n ∈ voc (?'a✝), n < freshVarProg (?'a✝)
Tactic:
all_goals simp [freshVarProg, voc, vocabOfProgram]
Proof state after:
case sequence
a✝¹ a✝ : Program
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram a✝¹ ∨ n ∈ vocabOfProgram a✝ → n < freshVarProg a✝¹ ∨ n < freshVarProg a✝

case union
a✝¹ a✝ : Program
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram a✝¹ ∨ n ∈ vocabOfProgram a✝ → n < freshVarProg a✝¹ ∨ n < freshVarProg a✝

case star
a✝ : Program
⊢ ∀ n ∈ vocabOfProgram a✝, n < freshVarProg a✝

case test
a✝ : Formula
⊢ ∀ n ∈ vocabOfFormula a✝, n < freshVarForm a✝
Theorem: freshVarProg_is_larger
Proof state before:
α β : Program
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β
Tactic:
case union α β =>
  have IHα := freshVarProg_is_larger α
  have IHβ := freshVarProg_is_larger β
  aesop
Proof state after:
no goals
Theorem: freshVarProg_is_larger
Proof state before:
α β : Program
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β
Tactic:
case sequence α β =>
  have IHα := freshVarProg_is_larger α
  have IHβ := freshVarProg_is_larger β
  aesop
Proof state after:
no goals
Theorem: freshVarProg_is_larger
Proof state before:
α : Program
⊢ ∀ n ∈ vocabOfProgram α, n < freshVarProg α
Tactic:
case star α =>
  have IHα := freshVarProg_is_larger α
  aesop
Proof state after:
no goals
Theorem: freshVarProg_is_larger
Proof state before:
φ : Formula
⊢ ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
Tactic:
case test φ =>
  have IHφ := freshVarForm_is_larger φ
  aesop
Proof state after:
no goals
Theorem: freshVarProg_is_larger
Proof state before:
case test
a✝ : Formula
⊢ ∀ n ∈ voc (?'a✝), n < freshVarProg (?'a✝)
Tactic:
simp [freshVarProg, voc, vocabOfProgram]
Proof state after:
case test
a✝ : Formula
⊢ ∀ n ∈ vocabOfFormula a✝, n < freshVarForm a✝
Theorem: freshVarProg_is_larger
Proof state before:
α β : Program
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β
Tactic:
have IHα := freshVarProg_is_larger α
Proof state after:
α β : Program
IHα : ∀ n ∈ voc α, n < freshVarProg α
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β