Theorem: zlen_iff (Bml/Tableau.lean)

State before:
X Y : Finset Formula
⊢ lengthOf X < lengthOf Y ↔ zlengthOfSet X < zlengthOfSet Y
Tactic:
have : ∀ W, zlengthOfSet W = lengthOfSet W := by intro W; simp
State after:
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ lengthOf X < lengthOf Y ↔ zlengthOfSet X < zlengthOfSet Y

State before:
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ lengthOf X < lengthOf Y ↔ zlengthOfSet X < zlengthOfSet Y
Tactic:
rw [this, this]
State after:
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ lengthOf X < lengthOf Y ↔ ↑(lengthOfSet X) < ↑(lengthOfSet Y)

State before:
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ lengthOf X < lengthOf Y ↔ ↑(lengthOfSet X) < ↑(lengthOfSet Y)
Tactic:
zify
State after:
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ ↑(lengthOf X) < ↑(lengthOf Y) ↔ ↑(lengthOfSet X) < ↑(lengthOfSet Y)

State before:
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ ↑(lengthOf X) < ↑(lengthOf Y) ↔ ↑(lengthOfSet X) < ↑(lengthOfSet Y)
Tactic:
simp
State after:
no goals

State before:
X Y : Finset Formula
⊢ ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
Tactic:
intro W
State after:
X Y W : Finset Formula
⊢ zlengthOfSet W = ↑(lengthOfSet W)

State before:
X Y W : Finset Formula
⊢ zlengthOfSet W = ↑(lengthOfSet W)
Tactic:
simp
State after:
no goals