internlm/Lean-Github huggingface dataset:
Theorem: freshVarProg_is_larger
Proof state before:
α β : Program
IHα : ∀ n ∈ voc α, n < freshVarProg α
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β
Tactic:
have IHβ := freshVarProg_is_larger β
Proof state after:
α β : Program
IHα : ∀ n ∈ voc α, n < freshVarProg α
IHβ : ∀ n ∈ voc β, n < freshVarProg β
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β
Theorem: freshVarProg_is_larger
Proof state before:
α β : Program
IHα : ∀ n ∈ voc α, n < freshVarProg α
IHβ : ∀ n ∈ voc β, n < freshVarProg β
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β
Tactic:
aesop
Proof state after:
no goals
Theorem: freshVarProg_is_larger
Proof state before:
α : Program
⊢ ∀ n ∈ vocabOfProgram α, n < freshVarProg α
Tactic:
have IHα := freshVarProg_is_larger α
Proof state after:
α : Program
IHα : ∀ n ∈ voc α, n < freshVarProg α
⊢ ∀ n ∈ vocabOfProgram α, n < freshVarProg α
Theorem: freshVarProg_is_larger
Proof state before:
α : Program
IHα : ∀ n ∈ voc α, n < freshVarProg α
⊢ ∀ n ∈ vocabOfProgram α, n < freshVarProg α
Tactic:
aesop
Proof state after:
no goals
Theorem: freshVarProg_is_larger
Proof state before:
φ : Formula
⊢ ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
Tactic:
have IHφ := freshVarForm_is_larger φ
Proof state after:
φ : Formula
IHφ : ∀ n ∈ voc φ, n < freshVarForm φ
⊢ ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
Theorem: freshVarProg_is_larger
Proof state before:
φ : Formula
IHφ : ∀ n ∈ voc φ, n < freshVarForm φ
⊢ ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
Tactic:
aesop
Proof state after:
no goals
Theorem: freshVarForm_is_fresh
Proof state before:
φ : Formula
⊢ freshVarForm φ ∉ voc φ
Tactic:
have := freshVarForm_is_larger φ
Proof state after:
φ : Formula
this : ∀ n ∈ voc φ, n < freshVarForm φ
⊢ freshVarForm φ ∉ voc φ
Theorem: freshVarForm_is_fresh
Proof state before:
φ : Formula
this : ∀ n ∈ voc φ, n < freshVarForm φ
⊢ freshVarForm φ ∉ voc φ
Tactic:
simp [freshVarForm, voc, vocabOfFormula] at *
Proof state after:
φ : Formula
this : ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
⊢ freshVarForm φ ∉ vocabOfFormula φ
Theorem: freshVarForm_is_fresh
Proof state before:
φ : Formula
this : ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
⊢ freshVarForm φ ∉ vocabOfFormula φ
Tactic:
by_contra hyp
Proof state after:
φ : Formula
this : ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
hyp : freshVarForm φ ∈ vocabOfFormula φ
⊢ False
Theorem: freshVarForm_is_fresh
Proof state before:
φ : Formula
this : ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
hyp : freshVarForm φ ∈ vocabOfFormula φ
⊢ False
Tactic:
specialize this (freshVarForm φ)
Proof state after:
φ : Formula
hyp : freshVarForm φ ∈ vocabOfFormula φ
this : freshVarForm φ ∈ vocabOfFormula φ → freshVarForm φ < freshVarForm φ
⊢ False
Theorem: freshVarForm_is_fresh
Proof state before:
φ : Formula
hyp : freshVarForm φ ∈ vocabOfFormula φ
this : freshVarForm φ ∈ vocabOfFormula φ → freshVarForm φ < freshVarForm φ
⊢ False
Tactic:
have := Nat.lt_irrefl (freshVarForm φ)
Proof state after:
φ : Formula
hyp : freshVarForm φ ∈ vocabOfFormula φ
this✝ : freshVarForm φ ∈ vocabOfFormula φ → freshVarForm φ < freshVarForm φ
this : ¬freshVarForm φ < freshVarForm φ
⊢ False
Theorem: freshVarForm_is_fresh
Proof state before:
φ : Formula
hyp : freshVarForm φ ∈ vocabOfFormula φ
this✝ : freshVarForm φ ∈ vocabOfFormula φ → freshVarForm φ < freshVarForm φ
this : ¬freshVarForm φ < freshVarForm φ
⊢ False
Tactic:
tauto
Proof state after:
no goals
Theorem: freshVarProg_is_fresh
Proof state before:
α : Program
⊢ freshVarProg α ∉ voc α
Tactic:
have := freshVarProg_is_larger α
Proof state after:
α : Program
this : ∀ n ∈ voc α, n < freshVarProg α
⊢ freshVarProg α ∉ voc α
Theorem: freshVarProg_is_fresh
Proof state before:
α : Program
this : ∀ n ∈ voc α, n < freshVarProg α
⊢ freshVarProg α ∉ voc α
Tactic:
simp [freshVarProg, voc, vocabOfFormula] at *
Proof state after:
α : Program
this : ∀ n ∈ vocabOfProgram α, n < freshVarProg α
⊢ freshVarProg α ∉ vocabOfProgram α
Theorem: freshVarProg_is_fresh
Proof state before:
α : Program
this : ∀ n ∈ vocabOfProgram α, n < freshVarProg α
⊢ freshVarProg α ∉ vocabOfProgram α
Tactic:
by_contra hyp
Proof state after:
α : Program
this : ∀ n ∈ vocabOfProgram α, n < freshVarProg α
hyp : freshVarProg α ∈ vocabOfProgram α
⊢ False
Theorem: freshVarProg_is_fresh
Proof state before:
α : Program
this : ∀ n ∈ vocabOfProgram α, n < freshVarProg α
hyp : freshVarProg α ∈ vocabOfProgram α
⊢ False
Tactic:
specialize this (freshVarProg α)
Proof state after:
α : Program
hyp : freshVarProg α ∈ vocabOfProgram α
this : freshVarProg α ∈ vocabOfProgram α → freshVarProg α < freshVarProg α
⊢ False
Theorem: freshVarProg_is_fresh
Proof state before:
α : Program
hyp : freshVarProg α ∈ vocabOfProgram α
this : freshVarProg α ∈ vocabOfProgram α → freshVarProg α < freshVarProg α
⊢ False
Tactic:
have := Nat.lt_irrefl (freshVarProg α)
Proof state after:
α : Program
hyp : freshVarProg α ∈ vocabOfProgram α
this✝ : freshVarProg α ∈ vocabOfProgram α → freshVarProg α < freshVarProg α
this : ¬freshVarProg α < freshVarProg α
⊢ False
Theorem: freshVarProg_is_fresh
Proof state before:
α : Program
hyp : freshVarProg α ∈ vocabOfProgram α
this✝ : freshVarProg α ∈ vocabOfProgram α → freshVarProg α < freshVarProg α
this : ¬freshVarProg α < freshVarProg α
⊢ False
Tactic:
tauto
Proof state after:
no goals
Theorem: projectionUnion
Proof state before:
X Y : Finset Formula
⊢ projection (X ∪ Y) = projection X ∪ projection Y
Tactic:
unfold projection
Proof state after:
X Y : Finset Formula
⊢ (let X := X ∪ Y;
    X.biUnion fun x => (formProjection x).toFinset) =
    (let X := X;
      X.biUnion fun x => (formProjection x).toFinset) ∪
      let X := Y;
      X.biUnion fun x => (formProjection x).toFinset
Theorem: projectionUnion
Proof state before:
X Y : Finset Formula
⊢ (let X := X ∪ Y;
    X.biUnion fun x => (formProjection x).toFinset) =
    (let X := X;
      X.biUnion fun x => (formProjection x).toFinset) ∪
      let X := Y;
      X.biUnion fun x => (formProjection x).toFinset
Tactic:
aesop
Proof state after:
no goals
Theorem: proj
Proof state before:
g : Formula
X : Finset Formula
⊢ g ∈ projection X ↔ □g ∈ X
Tactic:
rw [projection]
Proof state after:
g : Formula
X : Finset Formula
⊢ (g ∈
      let X := X;
      X.biUnion fun x => (formProjection x).toFinset) ↔
    □g ∈ X
Theorem: proj
Proof state before:
g : Formula
X : Finset Formula
⊢ (g ∈
      let X := X;
      X.biUnion fun x => (formProjection x).toFinset) ↔
    □g ∈ X
Tactic:
simp
Proof state after:
g : Formula
X : Finset Formula
⊢ (∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g) ↔
    □g ∈ X
Theorem: proj
Proof state before:
g : Formula
X : Finset Formula
⊢ (∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g) ↔
    □g ∈ X
Tactic:
constructor
Proof state after:
case mp
g : Formula
X : Finset Formula
⊢ (∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g) →
    □g ∈ X

case mpr
g : Formula
X : Finset Formula
⊢ □g ∈ X →
    ∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g
Theorem: proj
Proof state before:
case mp
g : Formula
X : Finset Formula
⊢ (∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g) →
    □g ∈ X
Tactic:
intro lhs
Proof state after:
case mp
g : Formula
X : Finset Formula
lhs :
  ∃ a ∈ X,
    (match a with
      | □f => some f
      | x => none) =
      some g
⊢ □g ∈ X
Theorem: proj
Proof state before:
case mp
g : Formula
X : Finset Formula
lhs :
  ∃ a ∈ X,
    (match a with
      | □f => some f
      | x => none) =
      some g
⊢ □g ∈ X
Tactic:
rcases lhs with ⟨boxg, boxg_in_X, projboxg_is_g⟩
Proof state after:
case mp.intro.intro
g : Formula
X : Finset Formula
boxg : Formula
boxg_in_X : boxg ∈ X
projboxg_is_g :
  (match boxg with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X
Theorem: proj
Proof state before:
case mp.intro.intro
g : Formula
X : Finset Formula
boxg : Formula
boxg_in_X : boxg ∈ X
projboxg_is_g :
  (match boxg with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X
Tactic:
cases boxg
Proof state after:
case mp.intro.intro.bottom
g : Formula
X : Finset Formula
boxg_in_X : bottom ∈ X
projboxg_is_g :
  (match bottom with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.atom_prop
g : Formula
X : Finset Formula
a✝ : Char
boxg_in_X : (·a✝) ∈ X
projboxg_is_g :
  (match ·a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.neg
g : Formula
X : Finset Formula
a✝ : Formula
boxg_in_X : ~a✝ ∈ X
projboxg_is_g :
  (match ~a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.And
g : Formula
X : Finset Formula
a✝¹ a✝ : Formula
boxg_in_X : a✝¹⋀a✝ ∈ X
projboxg_is_g :
  (match a✝¹⋀a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.box
g : Formula
X : Finset Formula
a✝ : Formula
boxg_in_X : □a✝ ∈ X
projboxg_is_g :
  (match □a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X
Theorem: proj
Proof state before:
case mp.intro.intro.bottom
g : Formula
X : Finset Formula
boxg_in_X : bottom ∈ X
projboxg_is_g :
  (match bottom with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.atom_prop
g : Formula
X : Finset Formula
a✝ : Char
boxg_in_X : (·a✝) ∈ X
projboxg_is_g :
  (match ·a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.neg
g : Formula
X : Finset Formula
a✝ : Formula
boxg_in_X : ~a✝ ∈ X
projboxg_is_g :
  (match ~a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.And
g : Formula
X : Finset Formula
a✝¹ a✝ : Formula
boxg_in_X : a✝¹⋀a✝ ∈ X
projboxg_is_g :
  (match a✝¹⋀a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X

case mp.intro.intro.box
g : Formula
X : Finset Formula
a✝ : Formula
boxg_in_X : □a✝ ∈ X
projboxg_is_g :
  (match □a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X
Tactic:
repeat' aesop
Proof state after:
no goals
Theorem: proj
Proof state before:
case mp.intro.intro.box
g : Formula
X : Finset Formula
a✝ : Formula
boxg_in_X : □a✝ ∈ X
projboxg_is_g :
  (match □a✝ with
    | □f => some f
    | x => none) =
    some g
⊢ □g ∈ X
Tactic:
aesop
Proof state after:
no goals
Theorem: proj
Proof state before:
case mpr
g : Formula
X : Finset Formula
⊢ □g ∈ X →
    ∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g
Tactic:
intro rhs
Proof state after:
case mpr
g : Formula
X : Finset Formula
rhs : □g ∈ X
⊢ ∃ a ∈ X,
    (match a with
      | □f => some f
      | x => none) =
      some g
Theorem: proj
Proof state before:
case mpr
g : Formula
X : Finset Formula
rhs : □g ∈ X
⊢ ∃ a ∈ X,
    (match a with
      | □f => some f
      | x => none) =
      some g
Tactic:
use □g
Proof state after:
no goals
Theorem: projSet
Proof state before:
X : Finset Formula
⊢ ↑(projection X) = {ϕ | □ϕ ∈ X}
Tactic:
ext1
Proof state after:
case h
X : Finset Formula
x✝ : Formula
⊢ x✝ ∈ ↑(projection X) ↔ x✝ ∈ {ϕ | □ϕ ∈ X}
Theorem: projSet
Proof state before:
case h
X : Finset Formula
x✝ : Formula
⊢ x✝ ∈ ↑(projection X) ↔ x✝ ∈ {ϕ | □ϕ ∈ X}
Tactic:
simp
Proof state after:
case h
X : Finset Formula
x✝ : Formula
⊢ x✝ ∈ projection X ↔ □x✝ ∈ X
Theorem: projSet
Proof state before:
case h
X : Finset Formula
x✝ : Formula
⊢ x✝ ∈ projection X ↔ □x✝ ∈ X
Tactic:
exact proj
Proof state after:
no goals
Theorem: projection_length_leq
Proof state before:
⊢ ∀ (f : Formula), (projection {f}).sum lengthOfFormula ≤ lengthOfFormula f
Tactic:
intro f
Proof state after:
f : Formula
⊢ (projection {f}).sum lengthOfFormula ≤ lengthOfFormula f
Theorem: projection_length_leq
Proof state before:
f : Formula
⊢ (projection {f}).sum lengthOfFormula ≤ lengthOfFormula f
Tactic:
cases f
Proof state after:
case bottom

⊢ (projection {bottom}).sum lengthOfFormula ≤ lengthOfFormula bottom

case atom_prop
a✝ : Char
⊢ (projection {·a✝}).sum lengthOfFormula ≤ lengthOfFormula (·a✝)

case neg
a✝ : Formula
⊢ (projection {~a✝}).sum lengthOfFormula ≤ lengthOfFormula (~a✝)

case And
a✝¹ a✝ : Formula
⊢ (projection {a✝¹⋀a✝}).sum lengthOfFormula ≤ lengthOfFormula (a✝¹⋀a✝)

case box
a✝ : Formula
⊢ (projection {□a✝}).sum lengthOfFormula ≤ lengthOfFormula (□a✝)
Theorem: projection_length_leq
Proof state before:
f : Formula
⊢ (projection {□f}).sum lengthOfFormula ≤ lengthOfFormula (□f)
Tactic:
case box f =>
  have subsubClaim : projection {□f} = {f} := by ext1; rw [proj]; simp
  rw [subsubClaim]
  simp
Proof state after:
no goals
Theorem: projection_length_leq
Proof state before:
case bottom

⊢ (projection {bottom}).sum lengthOfFormula ≤ lengthOfFormula bottom
Tactic:
unfold projection
Proof state after:
case bottom

⊢ (let X := {bottom};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula bottom
Theorem: projection_length_leq
Proof state before:
case bottom

⊢ (let X := {bottom};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula bottom
Tactic:
simp
Proof state after:
no goals
Theorem: projection_length_leq
Proof state before:
case atom_prop
a✝ : Char
⊢ (projection {·a✝}).sum lengthOfFormula ≤ lengthOfFormula (·a✝)
Tactic:
unfold projection
Proof state after:
case atom_prop
a✝ : Char
⊢ (let X := {·a✝};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula (·a✝)
Theorem: projection_length_leq
Proof state before:
case atom_prop
a✝ : Char
⊢ (let X := {·a✝};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula (·a✝)
Tactic:
simp
Proof state after:
no goals
Theorem: projection_length_leq
Proof state before:
case neg
a✝ : Formula
⊢ (projection {~a✝}).sum lengthOfFormula ≤ lengthOfFormula (~a✝)
Tactic:
unfold projection
Proof state after:
case neg
a✝ : Formula
⊢ (let X := {~a✝};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula (~a✝)
Theorem: projection_length_leq
Proof state before:
case neg
a✝ : Formula
⊢ (let X := {~a✝};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula (~a✝)
Tactic:
simp
Proof state after:
no goals
Theorem: projection_length_leq
Proof state before:
case And
a✝¹ a✝ : Formula
⊢ (projection {a✝¹⋀a✝}).sum lengthOfFormula ≤ lengthOfFormula (a✝¹⋀a✝)
Tactic:
unfold projection
Proof state after:
case And
a✝¹ a✝ : Formula
⊢ (let X := {a✝¹⋀a✝};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula (a✝¹⋀a✝)
Theorem: projection_length_leq
Proof state before:
case And
a✝¹ a✝ : Formula
⊢ (let X := {a✝¹⋀a✝};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula (a✝¹⋀a✝)
Tactic:
simp
Proof state after:
no goals
Theorem: projection_length_leq
Proof state before:
f : Formula
⊢ (projection {□f}).sum lengthOfFormula ≤ lengthOfFormula (□f)
Tactic:
have subsubClaim : projection {□f} = {f} := by ext1; rw [proj]; simp
Proof state after:
f : Formula
subsubClaim : projection {□f} = {f}
⊢ (projection {□f}).sum lengthOfFormula ≤ lengthOfFormula (□f)
Theorem: projection_length_leq
Proof state before:
f : Formula
subsubClaim : projection {□f} = {f}
⊢ (projection {□f}).sum lengthOfFormula ≤ lengthOfFormula (□f)
Tactic:
rw [subsubClaim]
Proof state after:
f : Formula
subsubClaim : projection {□f} = {f}
⊢ {f}.sum lengthOfFormula ≤ lengthOfFormula (□f)
Theorem: projection_length_leq
Proof state before:
f : Formula
subsubClaim : projection {□f} = {f}
⊢ {f}.sum lengthOfFormula ≤ lengthOfFormula (□f)
Tactic:
simp
Proof state after:
no goals
Theorem: projection_length_leq
Proof state before:
f : Formula
⊢ projection {□f} = {f}
Tactic:
ext1
Proof state after:
case a
f a✝ : Formula
⊢ a✝ ∈ projection {□f} ↔ a✝ ∈ {f}
Theorem: projection_length_leq
Proof state before:
case a
f a✝ : Formula
⊢ a✝ ∈ projection {□f} ↔ a✝ ∈ {f}
Tactic:
rw [proj]
Proof state after:
case a
f a✝ : Formula
⊢ □a✝ ∈ {□f} ↔ a✝ ∈ {f}
Theorem: projection_length_leq
Proof state before:
case a
f a✝ : Formula
⊢ □a✝ ∈ {□f} ↔ a✝ ∈ {f}
Tactic:
simp
Proof state after:
no goals
Theorem: projection_set_length_leq
Proof state before:
⊢ ∀ (X : Finset Formula), lengthOfSet (projection X) ≤ lengthOfSet X
Tactic:
intro X
Proof state after:
X : Finset Formula
⊢ lengthOfSet (projection X) ≤ lengthOfSet X
Theorem: projection_set_length_leq
Proof state before:
X : Finset Formula
⊢ lengthOfSet (projection X) ≤ lengthOfSet X
Tactic:
induction X using Finset.induction_on
Proof state after:
case empty

⊢ lengthOfSet (projection ∅) ≤ lengthOfSet ∅

case insert
a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : lengthOfSet (projection s✝) ≤ lengthOfSet s✝
⊢ lengthOfSet (projection (insert a✝² s✝)) ≤ lengthOfSet (insert a✝² s✝)
Theorem: projection_set_length_leq
Proof state before:
case empty

⊢ lengthOfSet (projection ∅) ≤ lengthOfSet ∅
Tactic:
simp [projection]
Proof state after:
no goals
Theorem: projection_set_length_leq
Proof state before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ lengthOfSet (projection (insert f S)) ≤ lengthOfSet (insert f S)
Tactic:
unfold lengthOfSet
Proof state after:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    let X := insert f S;
    X.sum lengthOfFormula
Theorem: projection_set_length_leq
Proof state before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    let X := insert f S;
    X.sum lengthOfFormula
Tactic:
rw [Finset.sum_insert f_not_in_S]
Proof state after:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    lengthOfFormula f + ∑ x ∈ S, lengthOfFormula x
Theorem: projection_set_length_leq
Proof state before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    lengthOfFormula f + ∑ x ∈ S, lengthOfFormula x
Tactic:
have insert_comm_proj : ∀ X f, projection (insert f X) = projection {f} ∪ projection X :=
  by
  intro X f
  unfold projection
  simp
Proof state after:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    lengthOfFormula f + ∑ x ∈ S, lengthOfFormula x
Theorem: projection_set_length_leq
Proof state before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
Tactic:
intro X f
Proof state after:
f✝ : Formula
S : Finset Formula
f_not_in_S : f✝ ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
X : Finset Formula
f : Formula
⊢ projection (insert f X) = projection {f} ∪ projection X
Theorem: projection_set_length_leq
Proof state before:
f✝ : Formula
S : Finset Formula
f_not_in_S : f✝ ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
X : Finset Formula
f : Formula
⊢ projection (insert f X) = projection {f} ∪ projection X
Tactic:
unfold projection
Proof state after:
f✝ : Formula
S : Finset Formula
f_not_in_S : f✝ ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
X : Finset Formula
f : Formula
⊢ (let X := insert f X;
    X.biUnion fun x => (formProjection x).toFinset) =
    (let X := {f};
      X.biUnion fun x => (formProjection x).toFinset) ∪
      let X := X;
      X.biUnion fun x => (formProjection x).toFinset
Theorem: projection_set_length_leq
Proof state before:
f✝ : Formula
S : Finset Formula
f_not_in_S : f✝ ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
X : Finset Formula
f : Formula
⊢ (let X := insert f X;
    X.biUnion fun x => (formProjection x).toFinset) =
    (let X := {f};
      X.biUnion fun x => (formProjection x).toFinset) ∪
      let X := X;
      X.biUnion fun x => (formProjection x).toFinset
Tactic:
simp
Proof state after:
no goals
Theorem: projection_set_length_leq
Proof state before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    lengthOfFormula f + ∑ x ∈ S, lengthOfFormula x
Tactic:
calc
  (projection (insert f S)).sum lengthOfFormula
    = (projection {f} ∪ projection S).sum lengthOfFormula := by rw [insert_comm_proj S f]
  _ ≤ (projection {f}).sum lengthOfFormula + (projection S).sum lengthOfFormula := by
    apply sum_union_le
  _ ≤ lengthOfFormula f + (projection S).sum lengthOfFormula := by
    simp only [add_le_add_iff_right, projection_length_leq]
  _ ≤ lengthOfFormula f + S.sum lengthOfFormula := by simp; apply IH
Proof state after:
no goals
Theorem: projection_set_length_leq
Proof state before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (projection (insert f S)).sum lengthOfFormula = (projection {f} ∪ projection S).sum lengthOfFormula
Tactic:
rw [insert_comm_proj S f]
Proof state after:
no goals
Theorem: projection_set_length_leq
Proof state before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (projection {f} ∪ projection S).sum lengthOfFormula ≤
    (projection {f}).sum lengthOfFormula + (projection S).sum lengthOfFormula
Tactic:
apply sum_union_le
Proof state after:
no goals
Theorem: projection_set_length_leq
Proof state before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (projection {f}).sum lengthOfFormula + (projection S).sum lengthOfFormula ≤
    lengthOfFormula f + (projection S).sum lengthOfFormula
Tactic:
simp only [add_le_add_iff_right, projection_length_leq]
Proof state after:
no goals
Theorem: projection_set_length_leq
Proof state before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ lengthOfFormula f + (projection S).sum lengthOfFormula ≤ lengthOfFormula f + S.sum lengthOfFormula
Tactic:
simp
Proof state after:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (projection S).sum lengthOfFormula ≤ S.sum lengthOfFormula
Theorem: projection_set_length_leq
Proof state before:
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
insert_comm_proj : ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
⊢ (projection S).sum lengthOfFormula ≤ S.sum lengthOfFormula
Tactic:
apply IH
Proof state after:
no goals
Theorem: oneSidedRule_preserves_other_side_L
Proof state before:
L R : Finset Formula
C : List TNode
fst✝ : Finset Formula
a✝ : List (Finset Formula)
rule : LocalRule (fst✝, ∅) (List.map (fun res => (res, ∅)) a✝)
hC : C = applyLocalRule rule (L, R)
preproof : fst✝ ⊆ L ∧ ∅ ⊆ R
orule : OneSidedLocalRule fst✝ a✝
ruleApp : LocalRuleApp (L, R) C
hmyrule : ruleApp = LocalRuleApp.mk (List.map (fun res => (res, ∅)) a✝) fst✝ ∅ rule preproof
rule_is_left : rule = LocalRule.oneSidedL orule
⊢ ∀ c ∈ C, c.2 = R
Tactic:
aesop
Proof state after:
no goals