Theorem: BunchImpl.Subbunch.size_lt (BunchImpl/Subbunch.lean)

State before:
P : Sort u_1
b1 B1 : Bunch P
⊢ Subbunch B1 b1 → sizeOf B1 ≥ sizeOf b1
Tactic:
intro h1
State after:
P : Sort u_1
b1 B1 : Bunch P
h1 : Subbunch B1 b1
⊢ sizeOf B1 ≥ sizeOf b1

State before:
P : Sort u_1
b1 B1 : Bunch P
h1 : Subbunch B1 b1
⊢ sizeOf B1 ≥ sizeOf b1
Tactic:
induction h1 <;> simp <;> linarith
State after:
no goals