Theorem: zlengthOfSet.pos (Bml/Tableau.lean)

State before:
X : Finset Formula
⊢ zlengthOfSet X ≥ 0
Tactic:
apply Finset.sum_induction zlengthOf
State after:
case hom
X : Finset Formula
⊢ ∀ (a b : ℤ), 0 ≤ a → 0 ≤ b → 0 ≤ a + b

case unit
X : Finset Formula
⊢ 0 ≤ 0

case base
X : Finset Formula
⊢ ∀ x ∈ X, 0 ≤ zlengthOf x

State before:
case hom
X : Finset Formula
⊢ ∀ (a b : ℤ), 0 ≤ a → 0 ≤ b → 0 ≤ a + b
Tactic:
intro a b a_ge b_ge
State after:
case hom
X : Finset Formula
a b : ℤ
a_ge : 0 ≤ a
b_ge : 0 ≤ b
⊢ 0 ≤ a + b

State before:
case hom
X : Finset Formula
a b : ℤ
a_ge : 0 ≤ a
b_ge : 0 ≤ b
⊢ 0 ≤ a + b
Tactic:
linarith
State after:
no goals

State before:
case unit
X : Finset Formula
⊢ 0 ≤ 0
Tactic:
simp
State after:
no goals

State before:
case base
X : Finset Formula
⊢ ∀ x ∈ X, 0 ≤ zlengthOf x
Tactic:
intro f _
State after:
case base
X : Finset Formula
f : Formula
a✝ : f ∈ X
⊢ 0 ≤ zlengthOf f

State before:
case base
X : Finset Formula
f : Formula
a✝ : f ∈ X
⊢ 0 ≤ zlengthOf f
Tactic:
exact zlengthOf.pos
State after:
no goals