Theorem: lengthRemove (Pdl/Setsimp.lean)

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

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

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

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

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

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

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

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

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

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

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