Theorem: lengthSetRemove (Bml/Setsimp.lean)

State before:
X Y : Finset Formula
h : Y ⊆ X
⊢ lengthOfSet (X \ Y) + lengthOfSet Y = lengthOfSet X
Tactic:
induction Y using Finset.induction_on
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

State before:
X : Finset Formula
h : ∅ ⊆ X
⊢ lengthOfSet (X \ ∅) + lengthOfSet ∅ = lengthOfSet X
Tactic:
case empty => simp
State after:
no goals

State before:
X : Finset Formula
h : ∅ ⊆ X
⊢ lengthOfSet (X \ ∅) + lengthOfSet ∅ = lengthOfSet X
Tactic:
simp
State after:
no goals

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
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

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
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

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]
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

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) ϕ))]
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

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]
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

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
State after:
no goals

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]
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

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
State after:
no goals

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
State after:
no goals

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]
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

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
State after:
no goals

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals