internlm/Lean-Github huggingface dataset:
Theorem: existsBoxFP
Proof state before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ (δ != []) = true
Tactic:
aesop
Proof state after:
no goals
Theorem: existsBoxFP
Proof state before:
case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ relateSeq M (δ ++ [∗β]) v w
Tactic:
simp [relateSeq_append]
Proof state after:
case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ ∃ u, relateSeq M δ v u ∧ Relation.ReflTransGen (relate M β) u w
Theorem: existsBoxFP
Proof state before:
case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
u : W✝
δ : List Program
v_neq_w : ¬v = w
v_neq_u : ¬v = u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ : evaluate M v (Con (F β fun x => ℓ ⟨↑x, ⋯⟩))
δ_in : δ ∈ P β fun x => ℓ ⟨↑x, ⋯⟩
v_δ_w : relateSeq M δ v u
claim : ¬δ = []
⊢ ∃ u, relateSeq M δ v u ∧ Relation.ReflTransGen (relate M β) u w
Tactic:
use u
Proof state after:
no goals
Theorem: union_singleton_is_insert
Proof state before:
X : Finset Formula
ϕ : Formula
⊢ X ∪ {ϕ} = insert ϕ X
Tactic:
have fo := Finset.insert_eq ϕ X
Proof state after:
X : Finset Formula
ϕ : Formula
fo : insert ϕ X = {ϕ} ∪ X
⊢ X ∪ {ϕ} = insert ϕ X
Theorem: union_singleton_is_insert
Proof state before:
X : Finset Formula
ϕ : Formula
fo : insert ϕ X = {ϕ} ∪ X
⊢ X ∪ {ϕ} = insert ϕ X
Tactic:
aesop
Proof state after:
no goals
Theorem: sdiff_singleton_is_erase
Proof state before:
X : Finset Formula
ϕ : Formula
⊢ X \ {ϕ} = X.erase ϕ
Tactic:
induction X using Finset.induction_on
Proof state after:
case empty
ϕ : Formula
⊢ ∅ \ {ϕ} = ∅.erase ϕ

case insert
ϕ a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : s✝ \ {ϕ} = s✝.erase ϕ
⊢ insert a✝² s✝ \ {ϕ} = (insert a✝² s✝).erase ϕ
Theorem: sdiff_singleton_is_erase
Proof state before:
case empty
ϕ : Formula
⊢ ∅ \ {ϕ} = ∅.erase ϕ

case insert
ϕ a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : s✝ \ {ϕ} = s✝.erase ϕ
⊢ insert a✝² s✝ \ {ϕ} = (insert a✝² s✝).erase ϕ
Tactic:
simp
Proof state after:
case insert
ϕ a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : s✝ \ {ϕ} = s✝.erase ϕ
⊢ insert a✝² s✝ \ {ϕ} = (insert a✝² s✝).erase ϕ
Theorem: sdiff_singleton_is_erase
Proof state before:
case insert
ϕ a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : s✝ \ {ϕ} = s✝.erase ϕ
⊢ insert a✝² s✝ \ {ϕ} = (insert a✝² s✝).erase ϕ
Tactic:
ext1
Proof state after:
case insert.a
ϕ a✝³ : Formula
s✝ : Finset Formula
a✝² : a✝³ ∉ s✝
a✝¹ : s✝ \ {ϕ} = s✝.erase ϕ
a✝ : Formula
⊢ a✝ ∈ insert a✝³ s✝ \ {ϕ} ↔ a✝ ∈ (insert a✝³ s✝).erase ϕ
Theorem: sdiff_singleton_is_erase
Proof state before:
case insert.a
ϕ a✝³ : Formula
s✝ : Finset Formula
a✝² : a✝³ ∉ s✝
a✝¹ : s✝ \ {ϕ} = s✝.erase ϕ
a✝ : Formula
⊢ a✝ ∈ insert a✝³ s✝ \ {ϕ} ↔ a✝ ∈ (insert a✝³ s✝).erase ϕ
Tactic:
aesop
Proof state after:
no goals
Theorem: lengthAdd
Proof state before:
X : Finset Formula
ϕ : Formula
⊢ ϕ ∉ X → lengthOfSet (insert ϕ X) = lengthOfSet X + lengthOfFormula ϕ
Tactic:
intro notin
Proof state after:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOfSet (insert ϕ X) = lengthOfSet X + lengthOfFormula ϕ
Theorem: lengthAdd
Proof state before:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOfSet (insert ϕ X) = lengthOfSet X + lengthOfFormula ϕ
Tactic:
unfold lengthOfSet
Proof state after:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ (let X := insert ϕ X;
    X.sum lengthOfFormula) =
    (let X := X;
      X.sum lengthOfFormula) +
      lengthOfFormula ϕ
Theorem: lengthAdd
Proof state before:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ (let X := insert ϕ X;
    X.sum lengthOfFormula) =
    (let X := X;
      X.sum lengthOfFormula) +
      lengthOfFormula ϕ
Tactic:
rw [Finset.sum_insert notin]
Proof state after:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOfFormula ϕ + ∑ x ∈ X, lengthOfFormula x =
    (let X := X;
      X.sum lengthOfFormula) +
      lengthOfFormula ϕ
Theorem: lengthAdd
Proof state before:
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOfFormula ϕ + ∑ x ∈ X, lengthOfFormula x =
    (let X := 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
⊢ lengthOfSet (insert ϕ X) ≤ lengthOfSet X + lengthOfFormula ϕ
Tactic:
cases' em (ϕ ∈ X) with in_x not_in_x
Proof state after:
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOfSet (insert ϕ X) ≤ lengthOfSet X + lengthOfFormula ϕ

case inr
X : Finset Formula
ϕ : Formula
not_in_x : ϕ ∉ X
⊢ lengthOfSet (insert ϕ X) ≤ lengthOfSet X + lengthOfFormula ϕ
Theorem: lengthOf_insert_leq_plus
Proof state before:
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOfSet (insert ϕ X) ≤ lengthOfSet X + lengthOfFormula ϕ
Tactic:
rw [Finset.insert_eq_of_mem in_x]
Proof state after:
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOfSet X ≤ lengthOfSet X + lengthOfFormula ϕ
Theorem: lengthOf_insert_leq_plus
Proof state before:
case inl
X : Finset Formula
ϕ : Formula
in_x : ϕ ∈ X
⊢ lengthOfSet X ≤ lengthOfSet 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
⊢ lengthOfSet (insert ϕ X) ≤ lengthOfSet X + lengthOfFormula ϕ
Tactic:
rw [lengthAdd not_in_x]
Proof state after:
no goals
Theorem: lengthRemove
Proof state before:
X : Finset Formula
⊢ ∀ ϕ ∈ X, lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X
Tactic:
intro ϕ in_X
Proof state after:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X
Theorem: lengthRemove
Proof state before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X
Tactic:
have claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ :=
  by
  apply lengthAdd
  simp
Proof state after:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
⊢ lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X
Theorem: lengthRemove
Proof state before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
⊢ lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet 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 : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
anotherClaim : insert ϕ (X \ {ϕ}) = X
⊢ lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X
Theorem: lengthRemove
Proof state before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
anotherClaim : insert ϕ (X \ {ϕ}) = X
⊢ lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X
Tactic:
rw [anotherClaim] at claim
Proof state after:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet X = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
anotherClaim : insert ϕ (X \ {ϕ}) = X
⊢ lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X
Theorem: lengthRemove
Proof state before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet X = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
anotherClaim : insert ϕ (X \ {ϕ}) = X
⊢ lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X
Tactic:
aesop
Proof state after:
no goals
Theorem: lengthRemove
Proof state before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
Tactic:
apply lengthAdd
Proof state after:
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ ϕ ∉ X \ {ϕ}
Theorem: lengthRemove
Proof state before:
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ ϕ ∉ X \ {ϕ}
Tactic:
simp
Proof state after:
no goals
Theorem: lengthRemove
Proof state before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
⊢ insert ϕ (X \ {ϕ}) = X
Tactic:
ext1
Proof state after:
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ ∈ insert ϕ (X \ {ϕ}) ↔ a✝ ∈ X
Theorem: lengthRemove
Proof state before:
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (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 : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (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 : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (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 : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ → a✝ ∈ X

case a.mpr
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (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 : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ → a✝ ∈ X

case a.mpr
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (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 : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (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 : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
a✝ : Formula
⊢ a✝ ∈ X → a✝ = ϕ ∨ a✝ ∈ X ∧ ¬a✝ = ϕ
Tactic:
tauto
Proof state after:
no goals
Theorem: lengthSetRemove
Proof state before:
X Y : Finset Formula
h : Y ⊆ X
⊢ lengthOfSet (X \ Y) + lengthOfSet Y = lengthOfSet X
Tactic:
induction Y using Finset.induction_on
Proof state after:
case empty
X : Finset Formula
h : ∅ ⊆ X
⊢ lengthOfSet (X \ ∅) + lengthOfSet ∅ = lengthOfSet X

case insert
X : Finset Formula
a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : s✝ ⊆ X → lengthOfSet (X \ s✝) + lengthOfSet s✝ = lengthOfSet X
h : insert a✝² s✝ ⊆ X
⊢ lengthOfSet (X \ insert a✝² s✝) + lengthOfSet (insert a✝² s✝) = lengthOfSet X
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
h : ∅ ⊆ X
⊢ lengthOfSet (X \ ∅) + lengthOfSet ∅ = lengthOfSet X
Tactic:
case empty => simp
Proof state after:
no goals
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
h : ∅ ⊆ X
⊢ lengthOfSet (X \ ∅) + lengthOfSet ∅ = lengthOfSet X
Tactic:
simp
Proof state after:
no goals
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
⊢ lengthOfSet (X \ insert ϕ S) + lengthOfSet (insert ϕ S) = lengthOfSet X
Tactic:
have subs_X : S ⊆ X := subset_trans (by aesop) h
Proof state after:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
⊢ lengthOfSet (X \ insert ϕ S) + lengthOfSet (insert ϕ S) = lengthOfSet X
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
⊢ lengthOfSet (X \ insert ϕ S) + lengthOfSet (insert ϕ S) = lengthOfSet X
Tactic:
have phi_in_X : ϕ ∈ X :=
  by
    rw [←Finset.singleton_subset_iff]
    exact subset_trans (by aesop) h
Proof state after:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ lengthOfSet (X \ insert ϕ S) + lengthOfSet (insert ϕ S) = lengthOfSet X
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ lengthOfSet (X \ insert ϕ S) + lengthOfSet (insert ϕ S) = lengthOfSet X
Tactic:
rw [Finset.sdiff_insert X S ϕ, ←lengthRemove X ϕ, lengthAdd]
Proof state after:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ lengthOfSet ((X \ S).erase ϕ) + (lengthOfSet S + lengthOfFormula ϕ) = lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∉ S

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ lengthOfSet ((X \ S).erase ϕ) + (lengthOfSet S + lengthOfFormula ϕ) = lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∉ S

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X
Tactic:
rw [Nat.add_comm, Nat.add_assoc, Nat.add_comm (lengthOfFormula ϕ) (lengthOfSet (Finset.erase (X \ S) ϕ))]
Proof state after:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ lengthOfSet S + (lengthOfSet ((X \ S).erase ϕ) + lengthOfFormula ϕ) = lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∉ S

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ lengthOfSet S + (lengthOfSet ((X \ S).erase ϕ) + lengthOfFormula ϕ) = lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∉ S

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X
Tactic:
rw [lengthRemove (X \ S) ϕ, Nat.add_comm, ih subs_X]
Proof state after:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ lengthOfSet X = lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X \ S

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∉ S

X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
⊢ S ⊆ insert ϕ S
Tactic:
aesop
Proof state after:
no goals
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
⊢ ϕ ∈ X
Tactic:
rw [←Finset.singleton_subset_iff]
Proof state after:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
⊢ {ϕ} ⊆ X
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
⊢ {ϕ} ⊆ X
Tactic:
exact subset_trans (by aesop) h
Proof state after:
no goals
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
⊢ {ϕ} ⊆ insert ϕ S
Tactic:
aesop
Proof state after:
no goals
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ lengthOfSet X = lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ
Tactic:
rw [lengthRemove X]
Proof state after:
case a
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X
Theorem: lengthSetRemove
Proof state before:
case a
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X
Tactic:
assumption
Proof state after:
no goals
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X \ S
Tactic:
simp
Proof state after:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X ∧ ϕ ∉ S
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X ∧ ϕ ∉ S
Tactic:
exact And.intro phi_in_X not_in_S
Proof state after:
no goals
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∉ S
Tactic:
exact not_in_S
Proof state after:
no goals
Theorem: lengthSetRemove
Proof state before:
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∈ X
Tactic:
exact phi_in_X
Proof state after:
no goals
Theorem: lengthOfEqualSets
Proof state before:
X Y : Finset Formula
⊢ X = Y → lengthOfSet X = lengthOfSet Y
Tactic:
intro hyp
Proof state after:
X Y : Finset Formula
hyp : X = Y
⊢ lengthOfSet X = lengthOfSet Y
Theorem: lengthOfEqualSets
Proof state before:
X Y : Finset Formula
hyp : X = Y
⊢ lengthOfSet X = lengthOfSet Y
Tactic:
aesop
Proof state after:
no goals
Theorem: sum_union_le
Proof state before:
T : Type u_1
inst✝ : DecidableEq T
⊢ ∀ {X Y : Finset T} {F : T → ℕ}, (X ∪ Y).sum F ≤ X.sum F + Y.sum F
Tactic:
intro X Y F
Proof state after:
T : Type u_1
inst✝ : DecidableEq T
X Y : Finset T
F : T → ℕ
⊢ (X ∪ Y).sum F ≤ X.sum F + Y.sum F
Theorem: sum_union_le
Proof state before:
T : Type u_1
inst✝ : DecidableEq T
X Y : Finset T
F : T → ℕ
⊢ (X ∪ Y).sum F ≤ X.sum F + Y.sum F
Tactic:
calc
  (X ∪ Y).sum F ≤ (X ∪ Y).sum F + (X ∩ Y).sum F := by simp
  _ = X.sum F + Y.sum F := Finset.sum_union_inter
Proof state after:
no goals
Theorem: sum_union_le
Proof state before:
T : Type u_1
inst✝ : DecidableEq T
X Y : Finset T
F : T → ℕ
⊢ (X ∪ Y).sum F ≤ (X ∪ Y).sum F + (X ∩ Y).sum F
Tactic:
simp
Proof state after:
no goals
Theorem: vocOfBigDis
Proof state before:
x : Char
l : List Formula
⊢ x ∈ voc (bigDis l) → ∃ φ ∈ l, x ∈ voc φ
Tactic:
intro hyp
Proof state after:
x : Char
l : List Formula
hyp : x ∈ voc (bigDis l)
⊢ ∃ φ ∈ l, x ∈ voc φ
Theorem: vocOfBigDis
Proof state before:
x : Char
l : List Formula
hyp : x ∈ voc (bigDis l)
⊢ ∃ φ ∈ l, x ∈ voc φ
Tactic:
induction l
Proof state after:
case nil
x : Char
hyp : x ∈ voc (bigDis [])
⊢ ∃ φ ∈ [], x ∈ voc φ

case cons
x : Char
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : x ∈ voc (bigDis tail✝) → ∃ φ ∈ tail✝, x ∈ voc φ
hyp : x ∈ voc (bigDis (head✝ :: tail✝))
⊢ ∃ φ ∈ head✝ :: tail✝, x ∈ voc φ
Theorem: vocOfBigDis
Proof state before:
x : Char
hyp : x ∈ voc (bigDis [])
⊢ ∃ φ ∈ [], x ∈ voc φ
Tactic:
case nil  => aesop
Proof state after:
no goals
Theorem: vocOfBigDis
Proof state before:
x : Char
hyp : x ∈ voc (bigDis [])
⊢ ∃ φ ∈ [], x ∈ voc φ
Tactic:
aesop
Proof state after:
no goals
Theorem: vocOfBigDis
Proof state before:
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigDis (head :: tail))
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
cases em (x ∈ vocabOfFormula head)
Proof state after:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigDis (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ

case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigDis (head :: tail))
h✝ : x ∉ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ