Theorem: lengthRemove (Bml/Setsimp.lean)

State before:
X : Finset Formula
⊢ ∀ ϕ ∈ X, lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X
Tactic:
intro ϕ in_X
State after:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X

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
State after:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
⊢ lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X

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

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

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

State before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
Tactic:
apply lengthAdd
State after:
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ ϕ ∉ X \ {ϕ}

State before:
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ ϕ ∉ X \ {ϕ}
Tactic:
simp
State after:
no goals

State before:
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
claim : lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
⊢ insert ϕ (X \ {ϕ}) = X
Tactic:
ext1
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

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

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
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✝ = ϕ

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
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✝ = ϕ

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